Quanta of 10d representations

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.

## Key definitions

• 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.anomalyCoefficent is the anomaly coefficent associated with a TenQuanta.
• TenQuanta.ofChargesExpand is the TenQuanta with fluxes {(1, 0), (1, 0), (1, 0)} or {(1, 1), (1, -1), (1, 0)} and finite set of charges equal to a given c.

Key theorems

• mem_ofChargesExpand_map_reduce_iff states that a TenQuanta is in the image of ofChargesExpand c under reduce if and only if it is a TenQuanta with charges equal to c and fluxes which have no exotics or zero.

@[reducible, inline]

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

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

Equations

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

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

The underlying FluxesTen from a TenQuanta.

Equations

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

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

The underlying Multiset charges from a TenQuanta.

Equations

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

Reduce

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. represenation) added together.

Equations

• x.reduce = Multiset.map (fun (q10 : 𝓩) => (q10, (Multiset.map (fun (y : 𝓩 × ℤ × ℤ) => y.2) (Multiset.filter (fun (f : 𝓩 × ℤ × ℤ) => f.1 = q10) x)).sum)) x.toCharges.dedup

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

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

theorem FTheory.SU5.TenQuanta.reduce_eq_val {𝓩 : Type} [DecidableEq 𝓩] (x : TenQuanta 𝓩) : x.reduce = (Finset.image (fun (q10 : 𝓩) => (q10, (Multiset.map (fun (y : 𝓩 × ℤ × ℤ) => y.2) (Multiset.filter (fun (f : 𝓩 × ℤ × ℤ) => f.1 = q10) x)).sum)) x.toCharges.toFinset).val

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

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

@[simp]

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

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

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

Anomaly cancellation

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

The anomaly coefficent 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.anomalyCoefficent = ((Multiset.map (fun (x : 𝓩 × ℤ × ℤ) => x.2.2 • x.1) F).sum, 3 * (Multiset.map (fun (x : 𝓩 × ℤ × ℤ) => x.2.2 • (x.1 * x.1)) F).sum)

@[simp]

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

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

toChargesExpand

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

Given a finite set of charges c the TenQuanta with fluxes {(1, 0), (1, 0), (1, 0)} and {(1, 1), (1, -1), (1, 0)} and finite set of charges equal to c.

Equations

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

theorem FTheory.SU5.TenQuanta.toFluxesFive_of_mem_ofChargesExpand {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h : x ∈ ofChargesExpand c) : x.toFluxesTen = {(1, 0), (1, 0), (1, 0)} ∨ x.toFluxesTen = {(1, 1), (1, -1), (1, 0)}

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

theorem FTheory.SU5.TenQuanta.mem_ofChargesExpand_of_toCharges_toFluxesTen {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} (h : x.toCharges.toFinset = c) (h2 : x.toFluxesTen = {(1, 0), (1, 0), (1, 0)} ∨ x.toFluxesTen = {(1, 1), (1, -1), (1, 0)}) : x ∈ ofChargesExpand c

theorem FTheory.SU5.TenQuanta.mem_ofChargesExpand_iff {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) {x : TenQuanta 𝓩} : x ∈ ofChargesExpand c ↔ x.toCharges.toFinset = c ∧ (x.toFluxesTen = {(1, 0), (1, 0), (1, 0)} ∨ x.toFluxesTen = {(1, 1), (1, -1), (1, 0)})

theorem FTheory.SU5.TenQuanta.mem_ofChargesExpand_of_noExotics_hasNoZero {𝓩 : Type} [DecidableEq 𝓩] (F : TenQuanta 𝓩) (c : Finset 𝓩) (hc : F.toCharges.toFinset = c) (h1 : F.toFluxesTen.NoExotics) (h2 : F.toFluxesTen.HasNoZero) : ∃ y ∈ ofChargesExpand c, y.reduce = F.reduce

theorem FTheory.SU5.TenQuanta.reduce_hasNoZeros_of_mem_ofChargesExpand {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (F : TenQuanta 𝓩) (h : F ∈ ofChargesExpand c) : F.reduce.toFluxesTen.HasNoZero

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

theorem FTheory.SU5.TenQuanta.reduce_mem_elemsNoExotics_of_mem_ofChargesExpand {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (F : TenQuanta 𝓩) (h : F ∈ ofChargesExpand c) : F.reduce.toFluxesTen ∈ FluxesTen.elemsNoExotics

theorem FTheory.SU5.TenQuanta.mem_ofChargesExpand_map_reduce_iff {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (S : TenQuanta 𝓩) : S ∈ Multiset.map reduce (ofChargesExpand c) ↔ S.toFluxesTen ∈ FluxesTen.elemsNoExotics ∧ S.toCharges.toFinset = c ∧ S.reduce = S