Quanta of representations

In SU(5) × U(1) F-theory theory, each 5-bar and 10d representation carries with it 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.

@[reducible, inline]

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

The quanta associated with the representations in a SU(5) x U(1) F-theory. This contains the value of the charges and the flux intergers (M, N) for the 5-bar matter content and the 10d matter content, and the charges of the Hd and Hu particles (there values of (M,N) are not included as they are forced to be (0, 1) and (0, -1) respectively.

Equations

• FTheory.SU5.Quanta 𝓩 = (Option 𝓩 × Option 𝓩 × FTheory.SU5.FiveQuanta 𝓩 × FTheory.SU5.TenQuanta 𝓩)

instance FTheory.SU5.Quanta.instDecidableEq {𝓩 : Type} [DecidableEq 𝓩] : DecidableEq (Quanta 𝓩)

Equations

• FTheory.SU5.Quanta.instDecidableEq = inferInstanceAs (DecidableEq (Option 𝓩 × Option 𝓩 × FTheory.SU5.FiveQuanta 𝓩 × FTheory.SU5.TenQuanta 𝓩))

def FTheory.SU5.Quanta.toCharges {𝓩 : Type} [DecidableEq 𝓩] (x : Quanta 𝓩) : SuperSymmetry.SU5.Charges 𝓩

The underlying Charges of a Quanta.

Equations

• x.toCharges = (x.1, x.2.1, x.2.2.1.toCharges.toFinset, x.2.2.2.toCharges.toFinset)

Reduce

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

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

Equations

• x.reduce = (x.1, x.2.1, x.2.2.1.reduce, x.2.2.2.reduce)

Anomaly cancellation conditions

There are two anomaly cancellation conditions in the SU(5)×U(1) model which involve the U(1) charges. These are

• ∑ᵢ qᵢ Nᵢ + ∑ₐ qₐ Nₐ = 0 where the first sum is over all 5-bar represenations and the second is over all 10d representations.
• ∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar represenations and the second is over all 10d representations.

According to arXiv:1401.5084 it is unclear whether this second condition should necessarily be imposed.

def FTheory.SU5.Quanta.HdAnomalyCoefficent {𝓩 : Type} [CommRing 𝓩] (qHd : Option 𝓩) : 𝓩 × 𝓩

The pair of anomaly cancellation coefficents associated with the Hd particle.

Equations

• FTheory.SU5.Quanta.HdAnomalyCoefficent none = (0, 0)
• FTheory.SU5.Quanta.HdAnomalyCoefficent (some qHd_2) = (qHd_2, qHd_2 ^ 2)

@[simp]

theorem FTheory.SU5.Quanta.HdAnomalyCoefficent_map {𝓩 𝓩1 : Type} [CommRing 𝓩] [CommRing 𝓩1] (f : 𝓩 →+* 𝓩1) (qHd : Option 𝓩) : HdAnomalyCoefficent (Option.map (⇑f) qHd) = (f.prodMap f) (HdAnomalyCoefficent qHd)

def FTheory.SU5.Quanta.HuAnomalyCoefficent {𝓩 : Type} [CommRing 𝓩] (qHu : Option 𝓩) : 𝓩 × 𝓩

The pair of anomaly cancellation coefficents associated with the Hu particle.

Equations

• FTheory.SU5.Quanta.HuAnomalyCoefficent none = (0, 0)
• FTheory.SU5.Quanta.HuAnomalyCoefficent (some qHd_1) = (-qHd_1, -qHd_1 ^ 2)

@[simp]

theorem FTheory.SU5.Quanta.HuAnomalyCoefficent_map {𝓩 𝓩1 : Type} [CommRing 𝓩] [CommRing 𝓩1] (f : 𝓩 →+* 𝓩1) (qHu : Option 𝓩) : HuAnomalyCoefficent (Option.map (⇑f) qHu) = (f.prodMap f) (HuAnomalyCoefficent qHu)

def FTheory.SU5.Quanta.AnomalyCancellation {𝓩 : Type} [CommRing 𝓩] (qHd qHu : Option 𝓩) (F : FiveQuanta 𝓩) (T : TenQuanta 𝓩) : Prop

The anomaly cancellation conditions on quanta making up the fields present in the theory. This corresponds to the conditions that:

• ∑ᵢ qᵢ Nᵢ + ∑ₐ qₐ Nₐ = 0 where the first sum is over all 5-bar represenations and the second is over all 10d representations.
• ∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar represenations and the second is over all 10d representations.

Equations

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

instance FTheory.SU5.Quanta.instDecidableAnomalyCancellationOfDecidableEq {𝓩 : Type} {qHd qHu : Option 𝓩} {F : FiveQuanta 𝓩} {T : TenQuanta 𝓩} [CommRing 𝓩] [DecidableEq 𝓩] : Decidable (AnomalyCancellation qHd qHu F T)

Equations

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

theorem FTheory.SU5.Quanta.anomalyCoefficent_snd_eq_zero_of_anomalyCancellation {𝓩 : Type} [CommRing 𝓩] {qHd qHu : Option 𝓩} {F : FiveQuanta 𝓩} {T : TenQuanta 𝓩} (h : AnomalyCancellation qHd qHu F T) : (HdAnomalyCoefficent qHd).2 + (HuAnomalyCoefficent qHu).2 + F.anomalyCoefficent.2 + T.anomalyCoefficent.2 = 0

ofChargesExpand

def FTheory.SU5.Quanta.ofChargesExpand {𝓩 : Type} [DecidableEq 𝓩] (c : SuperSymmetry.SU5.Charges 𝓩) : Multiset (Quanta 𝓩)

Given a finite set of charges c the Quanta with fluxes {(1, -1), (1, -1), (1, -1), (0, 1), (0, 1), (0, 1)} for the 5-bar matter content and fluxes {(1, 0), (1, 0), (1, 0)} or {(1, 1), (1, -1), (1, 0)} for the 10d matter content, and finite set of charges equal to c.

These quanta reduce to all viable quanta.

Equations

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