Quanta of 10d representations

i. Overview

The 10d representations of the SU(5)×U(1) carry the quantum numbers of their U(1) charges and their fluxes.

In this module we define the data structure for these quanta and properties thereof.

ii. Key results

• TenQuanta is the type of quanta of 10d representations.
• TenQuanta.toFluxesTen is the underlying FluxesTen of a TenQuanta.
• TenQuanta.toCharges is the underlying Multiset charges of a TenQuanta.
• TenQuanta.reduce is the reduction of a TenQuanta which adds together all the fluxes corresponding to the same charge (i.e. representation).
• TenQuanta.liftCharges given a charge c the TenQuanta which have charge c and no exotics or zero fluxes.
• TenQuanta.anomalyCoefficient is the anomaly coefficient associated with a TenQuanta.

iii. Table of contents

• A. The definition of TenQuanta
  • A.1. The map to underlying fluxes
  • A.2. The map to underlying charges
  • A.3. The map from charges to fluxes
• B. The reduction of a TenQuanta
  • B.1. The reduced TenQuanta has no duplicate elements
  • B.2. The underlying charges of the reduced TenQuanta are the deduped charges
  • B.3. Membership condition on the reduced TenQuanta
  • B.4. Filter of the reduced TenQuanta by a charge
  • B.5. The reduction is idempotent
  • B.6. Preservation of certain sums under reduction
  • B.7. Reduction does nothing if no duplicate charges
  • B.8. The charge map is preserved by reduction
  • B.9. A fluxes in the reduced TenQuanta is a sum of fluxes in the original TenQuanta
  • B.10. No exotics condition on the reduced TenQuanta
    • B.10.1. Number of chiral U
    • B.10.2. Number of anti-chiral U
    • B.10.3. Number of chiral Q
    • B.10.4. Number of anti-chiral Q
    • B.10.5. Number of chiral E
    • B.10.6. Number of anti-chiral E
    • B.10.7. The NoExotics condition on the reduced TenQuanta
  • B.11. Reduce member of FLuxesTen.elemsNoExotics
• C. Decomposition of a TenQuanta into basic fluxes
  • C.1. Decomposition of fluxes
  • C.2. Decomposition of a TenQuanta (with no exotics)
    • C.2.1. Decomposition distributes over addition
    • C.2.2. Decomposition commutes with filtering charges
    • C.2.3. Decomposition preserves the charge map
    • C.2.4. Decomposition preserves the charges
    • C.2.5. Decomposition preserves the reduction
    • C.2.6. Fluxes of the decomposition of a TenQuanta
• D. Lifting charges to TenQuanta
  • D.1. liftCharge c: multiset of ten-quanta for a finite set of charges c with no exotics
  • D.2. TenQuanta in liftCharge c have a finite set of charges c
  • D.3. TenQuanta in liftCharge c have no duplicate charges
  • D.4. Membership in liftCharge c iff is reduction of TenQuanta with given fluxes
  • D.5. TenQuanta in liftCharge c do not have zero fluxes
  • D.6. TenQuanta in liftCharge c have no exotics
  • D.7. Membership in liftCharge c iff have no exotics, no zero fluxes, and charges c
  • D.8. liftCharge c is preserved under a map if reduced
• E. Anomaly cancellation coefficients
  • E.1. Anomaly coefficients of a TenQuanta
  • E.2. Anomaly coefficients under a map
  • E.3. Anomaly coefficients is preserved under reduce

iv. References

A reference for the anomaly cancellation conditions is arXiv:1401.5084.

A. The definition of TenQuanta

@[reducible, inline]

abbrev FTheory.SU5.TenQuanta (𝓩 : Type := ℤ) : Type

The quanta of w0d representations corresponding to a multiset of (q, M, N) for each particle. (M, N) are defined in the FluxesFive module.

Equations

• FTheory.SU5.TenQuanta 𝓩 = Multiset (𝓩 × FTheory.SU5.Fluxes)

A.1. The map to underlying fluxes

def FTheory.SU5.TenQuanta.toFluxesTen {𝓩 : Type} (x : TenQuanta 𝓩) : FluxesTen

The underlying FluxesTen from a TenQuanta.

Equations

• x.toFluxesTen = Multiset.map Prod.snd x

A.2. The map to underlying charges

def FTheory.SU5.TenQuanta.toCharges {𝓩 : Type} (x : TenQuanta 𝓩) : Multiset 𝓩

The underlying Multiset charges from a TenQuanta.

Equations

• x.toCharges = Multiset.map Prod.fst x

A.3. The map from charges to fluxes

def FTheory.SU5.TenQuanta.toChargeMap {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : 𝓩 → Fluxes

The map which takes a charge to the overall flux it corresponds to in a TenQuanta.

Equations

• x.toChargeMap z = (Multiset.map Prod.snd (Multiset.filter (fun (p : 𝓩 × FTheory.SU5.Fluxes) => p.1 = z) x)).sum

theorem FTheory.SU5.TenQuanta.toChargeMap_of_not_mem {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) {z : 𝓩} (h : z ∉ x.toCharges) : x.toChargeMap z = 0

B. The reduction of a TenQuanta

def FTheory.SU5.TenQuanta.reduce {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : TenQuanta 𝓩

The reduce of TenQuanta is a new TenQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together.

Equations

• One or more equations did not get rendered due to their size.

B.1. The reduced TenQuanta has no duplicate elements

theorem FTheory.SU5.TenQuanta.reduce_nodup {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : Multiset.Nodup x.reduce

@[simp]

theorem FTheory.SU5.TenQuanta.reduce_dedup {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : Multiset.dedup x.reduce = x.reduce

B.2. The underlying charges of the reduced TenQuanta are the deduped charges

theorem FTheory.SU5.TenQuanta.reduce_toCharges {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : x.reduce.toCharges = x.toCharges.dedup

B.3. Membership condition on the reduced TenQuanta

theorem FTheory.SU5.TenQuanta.mem_reduce_iff {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) (p : 𝓩 × Fluxes) : p ∈ x.reduce ↔ p.1 ∈ x.toCharges ∧ p.2 = (Multiset.map (fun (y : 𝓩 × Fluxes) => y.2) (Multiset.filter (fun (f : 𝓩 × Fluxes) => f.1 = p.1) x)).sum

B.4. Filter of the reduced TenQuanta by a charge

theorem FTheory.SU5.TenQuanta.reduce_filter {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) (q : 𝓩) (h : q ∈ x.toCharges) : Multiset.filter (fun (f : 𝓩 × Fluxes) => f.1 = q) x.reduce = {(q, (Multiset.map (fun (y : 𝓩 × Fluxes) => y.2) (Multiset.filter (fun (f : 𝓩 × Fluxes) => f.1 = q) x)).sum)}

B.5. The reduction is idempotent

@[simp]

theorem FTheory.SU5.TenQuanta.reduce_reduce {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : x.reduce.reduce = x.reduce

B.6. Preservation of certain sums under reduction

theorem FTheory.SU5.TenQuanta.reduce_sum_eq_sum_toCharges {𝓩 : Type} [DecidableEq 𝓩] {M : Type u_1} [AddCommMonoid M] (x : TenQuanta 𝓩) (f : 𝓩 → Fluxes →+ M) : (Multiset.map (fun (x : 𝓩 × Fluxes) => match x with | (q, x) => (f q) x) x.reduce).sum = (Multiset.map (fun (x : 𝓩 × Fluxes) => match x with | (q, x) => (f q) x) x).sum

B.7. Reduction does nothing if no duplicate charges

theorem FTheory.SU5.TenQuanta.reduce_eq_self_of_ofCharges_nodup {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) (h : x.toCharges.Nodup) : x.reduce = x

B.8. The charge map is preserved by reduction

theorem FTheory.SU5.TenQuanta.reduce_toChargeMap_eq {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : x.reduce.toChargeMap = x.toChargeMap

B.9. A fluxes in the reduced TenQuanta is a sum of fluxes in the original TenQuanta

theorem FTheory.SU5.TenQuanta.mem_powerset_sum_of_mem_reduce_toFluxesTen {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} {f : Fluxes} (hf : f ∈ F.reduce.toFluxesTen) : f ∈ Multiset.map (fun (s : Multiset Fluxes) => s.sum) (Multiset.powerset F.toFluxesTen)

theorem FTheory.SU5.TenQuanta.mem_powerset_sum_of_mem_reduce_toFluxesTen_filter {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} {f : Fluxes} (hf : f ∈ F.reduce.toFluxesTen) : f ∈ Multiset.map (fun (s : Multiset Fluxes) => s.sum) (Multiset.filter (fun (s : Multiset Fluxes) => s ≠ 0) (Multiset.powerset F.toFluxesTen))

B.10. No exotics condition on the reduced TenQuanta

B.10.1. Number of chiral U

theorem FTheory.SU5.TenQuanta.reduce_numChiralU_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen.numChiralU = 3

B.10.2. Number of anti-chiral U

theorem FTheory.SU5.TenQuanta.reduce_numAntiChiralU_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen.numAntiChiralU = 0

B.10.3. Number of chiral Q

theorem FTheory.SU5.TenQuanta.reduce_numChiralQ_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen.numChiralQ = 3

B.10.4. Number of anti-chiral Q

theorem FTheory.SU5.TenQuanta.reduce_numAntiChiralQ_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen.numAntiChiralQ = 0

B.10.5. Number of chiral E

theorem FTheory.SU5.TenQuanta.reduce_numChiralE_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen.numChiralE = 3

B.10.6. Number of anti-chiral E

theorem FTheory.SU5.TenQuanta.reduce_numAntiChiralE_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen.numAntiChiralE = 0

B.10.7. The NoExotics condition on the reduced TenQuanta

theorem FTheory.SU5.TenQuanta.reduce_noExotics_of_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen.NoExotics

B.11. Reduce member of FLuxesTen.elemsNoExotics

theorem FTheory.SU5.TenQuanta.reduce_mem_elemsNoExotics {𝓩 : Type} [DecidableEq 𝓩] {F : TenQuanta 𝓩} (hx : F.toFluxesTen ∈ FluxesTen.elemsNoExotics) : F.reduce.toFluxesTen ∈ FluxesTen.elemsNoExotics

C. Decomposition of a TenQuanta into basic fluxes

C.1. Decomposition of fluxes

def FTheory.SU5.TenQuanta.decomposeFluxes (f : Fluxes) : Multiset Fluxes

The decomposition of a relevant flux into ⟨1, 0⟩, ⟨1, 1⟩ and ⟨1, -1⟩ .

Equations

• One or more equations did not get rendered due to their size.

theorem FTheory.SU5.TenQuanta.decomposeFluxes_sum_of_noExotics (f : Fluxes) (hf : ∃ F ∈ FluxesTen.elemsNoExotics, f ∈ F) : (decomposeFluxes f).sum = f

C.2. Decomposition of a TenQuanta (with no exotics)

def FTheory.SU5.TenQuanta.decompose {𝓩 : Type} (x : TenQuanta 𝓩) : TenQuanta 𝓩

The decomposition of a TenQuanta into a TenQuanta which has the same reduce by has fluxes {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩} or {⟨1, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩} only.

This only works for fluxes which have no exotics or zeros.

Equations

• x.decompose = Multiset.bind x fun (p : 𝓩 × FTheory.SU5.Fluxes) => Multiset.map (fun (f : FTheory.SU5.Fluxes) => (p.1, f)) (FTheory.SU5.TenQuanta.decomposeFluxes p.2)

C.2.1. Decomposition distributes over addition

theorem FTheory.SU5.TenQuanta.decompose_add {𝓩 : Type} (x y : TenQuanta 𝓩) : (x + y).decompose = x.decompose + y.decompose

C.2.2. Decomposition commutes with filtering charges

theorem FTheory.SU5.TenQuanta.decompose_filter_charge {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) (q : 𝓩) : Multiset.filter (fun (p : 𝓩 × Fluxes) => p.1 = q) x.decompose = decompose (Multiset.filter (fun (p : 𝓩 × Fluxes) => p.1 = q) x)

C.2.3. Decomposition preserves the charge map

theorem FTheory.SU5.TenQuanta.decompose_toChargeMap {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) (hx : x.toFluxesTen ∈ FluxesTen.elemsNoExotics) : x.decompose.toChargeMap = x.toChargeMap

C.2.4. Decomposition preserves the charges

theorem FTheory.SU5.TenQuanta.decompose_toCharges_dedup {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) (hx : x.toFluxesTen ∈ FluxesTen.elemsNoExotics) : x.decompose.toCharges.dedup = x.toCharges.dedup

C.2.5. Decomposition preserves the reduction

theorem FTheory.SU5.TenQuanta.decompose_reduce {𝓩 : Type} (x : TenQuanta 𝓩) [DecidableEq 𝓩] (hx : x.toFluxesTen ∈ FluxesTen.elemsNoExotics) : x.decompose.reduce = x.reduce

C.2.6. Fluxes of the decomposition of a TenQuanta

theorem FTheory.SU5.TenQuanta.decompose_toFluxesTen {𝓩 : Type} (x : TenQuanta 𝓩) (hx : x.toFluxesTen ∈ FluxesTen.elemsNoExotics) : x.decompose.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ x.decompose.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }}

D. Lifting charges to TenQuanta

D.1. liftCharge c: multiset of ten-quanta for a finite set of charges c with no exotics

This is an efficient definition, we will later show that it gives the correct answer

def FTheory.SU5.TenQuanta.liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) : Multiset (TenQuanta 𝓩)

Given a finite set of charges c the TenQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c. This is defined to be as efficient as possible.

Equations

• One or more equations did not get rendered due to their size.

D.2. TenQuanta in liftCharge c have a finite set of charges c

theorem FTheory.SU5.TenQuanta.toCharge_toFinset_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h : x ∈ liftCharge c) : x.toCharges.toFinset = c

D.3. TenQuanta in liftCharge c have no duplicate charges

theorem FTheory.SU5.TenQuanta.toCharges_nodup_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h : x ∈ liftCharge c) : x.toCharges.Nodup

D.4. Membership in liftCharge c iff is reduction of TenQuanta with given fluxes

theorem FTheory.SU5.TenQuanta.exists_toCharges_toFluxesTen_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h : x ∈ liftCharge c) : ∃ (a : TenQuanta 𝓩), a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }})

theorem FTheory.SU5.TenQuanta.mem_liftCharge_of_exists_toCharges_toFluxesTen {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h : ∃ (a : TenQuanta 𝓩), a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }})) : x ∈ liftCharge c

theorem FTheory.SU5.TenQuanta.mem_liftCharge_iff_exists {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} : x ∈ liftCharge c ↔ ∃ (a : TenQuanta 𝓩), a.reduce = x ∧ a.toCharges.toFinset = c ∧ (a.toFluxesTen = {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }} ∨ a.toFluxesTen = {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := 0 }})

D.5. TenQuanta in liftCharge c do not have zero fluxes

theorem FTheory.SU5.TenQuanta.hasNoZero_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h : x ∈ liftCharge c) : x.toFluxesTen.HasNoZero

D.6. TenQuanta in liftCharge c have no exotics

theorem FTheory.SU5.TenQuanta.noExotics_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (F : TenQuanta 𝓩) (h : F ∈ liftCharge c) : F.toFluxesTen.NoExotics

D.7. Membership in liftCharge c iff have no exotics, no zero fluxes, and charges c

theorem FTheory.SU5.TenQuanta.mem_liftCharge_of_mem_noExotics_hasNoZero {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h1 : x.toFluxesTen.NoExotics) (h2 : x.toFluxesTen.HasNoZero) (h3 : x.toCharges.toFinset = c) (h4 : x.toCharges.Nodup) : x ∈ liftCharge c

theorem FTheory.SU5.TenQuanta.mem_liftCharge_iff {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (x : TenQuanta 𝓩) : x ∈ liftCharge c ↔ x.toFluxesTen ∈ FluxesTen.elemsNoExotics ∧ x.toCharges.toFinset = c ∧ x.toCharges.Nodup

D.8. liftCharge c is preserved under a map if reduced

theorem FTheory.SU5.TenQuanta.map_liftCharge {𝓩 𝓩1 : Type} [DecidableEq 𝓩] [DecidableEq 𝓩1] [CommRing 𝓩] [CommRing 𝓩1] (f : 𝓩 →+* 𝓩1) (c : Finset 𝓩) (F : TenQuanta 𝓩) (h : F ∈ liftCharge c) : reduce (Multiset.map (fun (y : 𝓩 × Fluxes) => (f y.1, y.2)) F) ∈ liftCharge (Finset.image (⇑f) c)

E. Anomaly cancellation coefficients

E.1. Anomaly coefficients of a TenQuanta

def FTheory.SU5.TenQuanta.anomalyCoefficient {𝓩 : Type} [CommRing 𝓩] (F : TenQuanta 𝓩) : 𝓩 × 𝓩

The anomaly coefficient of a TenQuanta is given by the pair of integers: (∑ᵢ qᵢ Nᵢ, 3 * ∑ᵢ qᵢ² Nᵢ).

The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084. The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly, see equation (23) of arXiv:1401.5084.

Equations

• F.anomalyCoefficient = ((Multiset.map (fun (x : 𝓩 × FTheory.SU5.Fluxes) => x.2.N • x.1) F).sum, 3 * (Multiset.map (fun (x : 𝓩 × FTheory.SU5.Fluxes) => x.2.N • (x.1 * x.1)) F).sum)

E.2. Anomaly coefficients under a map

@[simp]

theorem FTheory.SU5.TenQuanta.anomalyCoefficient_of_map {𝓩 𝓩1 : Type} [CommRing 𝓩] [CommRing 𝓩1] (f : 𝓩 →+* 𝓩1) (F : TenQuanta 𝓩) : anomalyCoefficient (Multiset.map (fun (y : 𝓩 × Fluxes) => (f y.1, y.2)) F) = (f.prodMap f) F.anomalyCoefficient

E.3. Anomaly coefficients is preserved under reduce

theorem FTheory.SU5.TenQuanta.anomalyCoefficient_of_reduce {𝓩 : Type} [CommRing 𝓩] [DecidableEq 𝓩] (F : TenQuanta 𝓩) : F.reduce.anomalyCoefficient = F.anomalyCoefficient