Quanta of 5-d representations

The 5-bar 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

• FiveQuanta is the type of quanta of 5-bar representations.
• FiveQuanta.toFluxesFive is the underlying FluxesFive of a FiveQuanta.
• FiveQuanta.toCharges is the underlying Multiset charges of a FiveQuanta.
• FiveQuanta.reduce is the reduction of a FiveQuanta which adds together all the fluxes corresponding to the same charge (i.e. representation).
• FiveQuanta.anomalyCoefficent is the anomaly coefficent associated with a FiveQuanta.
• FiveQuanta.ofChargesExpand is the FiveQuanta with fluxes {(1, -1), (1, -1), (1, -1), (0, 1), (0, 1), (0, 1)} and finite set of charges equal to a given c.

Key theorems

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

@[reducible, inline]

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

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

Equations

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

def FTheory.SU5.FiveQuanta.toFluxesFive {𝓩 : Type} (x : FiveQuanta 𝓩) : FluxesFive

The underlying FluxesFive from a FiveQuanta.

Equations

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

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

The underlying Multiset charges from a FiveQuanta.

Equations

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

Reduce

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

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

Equations

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

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

@[simp]

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

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

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

theorem FTheory.SU5.FiveQuanta.mem_reduce_iff {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (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.FiveQuanta.reduce_filter {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) (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.FiveQuanta.reduce_reduce {𝓩 : Type} [DecidableEq 𝓩] (x : FiveQuanta 𝓩) : x.reduce.reduce = x.reduce

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

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

Anomaly cancellation

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

The anomaly coefficent of a FiveQuanta is given by the pair of integers: (∑ᵢ qᵢ Nᵢ, ∑ᵢ 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, (Multiset.map (fun (x : 𝓩 × ℤ × ℤ) => x.2.2 • (x.1 * x.1)) F).sum)

@[simp]

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

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

ofChargesExpand

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

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

Equations

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

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

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

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

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

theorem FTheory.SU5.FiveQuanta.eq_sum_filter_of_mem_ofChargesExpand {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (F : FiveQuanta 𝓩) (h : F ∈ ofChargesExpand c) : F = Multiset.filter (fun (x : 𝓩 × ℤ × ℤ) => x.2 = (1, -1)) F + Multiset.filter (fun (x : 𝓩 × ℤ × ℤ) => x.2 = (0, 1)) F

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

theorem FTheory.SU5.FiveQuanta.exists_charges_of_mem_ofChargesExpand {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (F : FiveQuanta 𝓩) (h : F ∈ ofChargesExpand c) : ∃ (q1 : 𝓩) (q2 : 𝓩) (q3 : 𝓩) (q4 : 𝓩) (q5 : 𝓩) (q6 : 𝓩), F = {(q1, 1, -1), (q2, 1, -1), (q3, 1, -1), (q4, 0, 1), (q5, 0, 1), (q6, 0, 1)}

theorem FTheory.SU5.FiveQuanta.exists_charges_le_of_mem_ofChargesExpand (c : Finset ℤ) (F : FiveQuanta) (h : F ∈ ofChargesExpand c) : ∃ (q1 : ℤ) (q2 : ℤ) (q3 : ℤ) (q4 : ℤ) (q5 : ℤ) (q6 : ℤ), F = {(q1, 1, -1), (q2, 1, -1), (q3, 1, -1), (q4, 0, 1), (q5, 0, 1), (q6, 0, 1)} ∧ q1 ≤ q2 ∧ q2 ≤ q3 ∧ q4 ≤ q5 ∧ q5 ≤ q6

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

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

theorem FTheory.SU5.FiveQuanta.reduce_mem_elemsNoExotics_of_mem_ofChargesExpand {𝓩 : Type} [DecidableEq 𝓩] (c : Finset 𝓩) (F : FiveQuanta 𝓩) (h : F ∈ ofChargesExpand c) : F.reduce.toFluxesFive ∈ FluxesFive.elemsNoExotics

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