Quanta of representations

i. Overview

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.

ii. Key results

• Quanta : The structure containing the quantum numbers of the 5-bar and 10d representations, as well as the charges of the Hd and Hu particles.
• Quanta.liftCharge : Lifting a ChargeSpectrum to a multiset of Quanta which have no chiral exotics and no zero fluxes.
• Quanta.AnomalyCancellation : The anomaly cancellation conditions on a Quanta.

iii. Table of contents

• A. The Quanta structure
  • A.1. Repr instance on Quanta
  • A.2. Extensionality lemma
  • A.3. Decidable equality instance
  • A.4. Map to the underlying ChargeSpectrum
• B. The reduction of a Quanta
• C. Lifting a charge spectrum to quanta with no exotics or zero fluxes
  • C.1. Simplification of membership in the liftCharge multiset
  • C.2. Charge spectrum of a lifted quanta
• D. Anomaly cancellation conditions
  • D.1. The anomaly coefficient of Hd
  • D.2. The anomaly coefficient of Hu
  • D.3. The anomaly cancellation condition propositions
    • D.3.1. The propositions are decidable

iv. References

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

A. The Quanta structure

structure 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 integers (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.

• qHd : Option 𝓩

  The charge of the Hd matter field.

• qHu : Option 𝓩

  The negative charge of the Hu matter field. In other words the charge of the Hu considered as a 5-bar field.

• F : FiveQuanta 𝓩

  The quanta carried by the 5-bar matter fields.

• T : TenQuanta 𝓩

  The quanta carried by the 10d matter fields.

A.1. Repr instance on Quanta

unsafe instance FTheory.SU5.Quanta.instRepr {𝓩 : Type} [Repr 𝓩] : Repr (Quanta 𝓩)

Equations

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

A.2. Extensionality lemma

theorem FTheory.SU5.Quanta.ext {𝓩 : Type} {x y : Quanta 𝓩} (h1 : x.qHd = y.qHd) (h2 : x.qHu = y.qHu) (h3 : x.F = y.F) (h4 : x.T = y.T) : x = y

theorem FTheory.SU5.Quanta.ext_iff {𝓩 : Type} {x y : Quanta 𝓩} : x = y ↔ x.qHd = y.qHd ∧ x.qHu = y.qHu ∧ x.F = y.F ∧ x.T = y.T

A.3. Decidable equality instance

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

Equations

• x.instDecidableEq y = decidable_of_iff (x.qHd = y.qHd ∧ x.qHu = y.qHu ∧ x.F = y.F ∧ x.T = y.T) ⋯

A.4. Map to the underlying ChargeSpectrum

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

The underlying ChargeSpectrum of a Quanta.

Equations

• x.toCharges = { qHd := x.qHd, qHu := x.qHu, Q5 := x.F.toCharges.toFinset, Q10 := x.T.toCharges.toFinset }

theorem FTheory.SU5.Quanta.toCharges_qHd {𝓩 : Type} [DecidableEq 𝓩] (x : Quanta 𝓩) : x.toCharges.qHd = x.qHd

theorem FTheory.SU5.Quanta.toCharges_qHu {𝓩 : Type} [DecidableEq 𝓩] (x : Quanta 𝓩) : x.toCharges.qHu = x.qHu

B. The reduction of a Quanta

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

Equations

• x.reduce = { qHd := x.qHd, qHu := x.qHu, F := x.F.reduce, T := x.T.reduce }

C. Lifting a charge spectrum to quanta with no exotics or zero fluxes

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

Lifting a charge spectrum to quanta which do not have exotics and which have no zero flux.

Equations

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

C.1. Simplification of membership in the liftCharge multiset

theorem FTheory.SU5.Quanta.mem_liftCharge_iff {𝓩 : Type} [DecidableEq 𝓩] {c : SuperSymmetry.SU5.ChargeSpectrum 𝓩} {x : Quanta 𝓩} : x ∈ liftCharge c ↔ x.qHd = c.qHd ∧ x.qHu = c.qHu ∧ x.F ∈ FiveQuanta.liftCharge c.Q5 ∧ x.T ∈ TenQuanta.liftCharge c.Q10

C.2. Charge spectrum of a lifted quanta

theorem FTheory.SU5.Quanta.toCharges_of_mem_liftCharge {𝓩 : Type} [DecidableEq 𝓩] {c : SuperSymmetry.SU5.ChargeSpectrum 𝓩} {x : Quanta 𝓩} (h : x ∈ liftCharge c) : x.toCharges = c

D. 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 representations and the second is over all 10d representations.
• ∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar representations and the second is over all 10d representations.

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

D.1. The anomaly coefficient of Hd

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

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

Equations

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

@[simp]

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

D.2. The anomaly coefficient of Hu

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

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

Equations

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

@[simp]

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

D.3. The anomaly cancellation condition propositions

def FTheory.SU5.Quanta.LinearAnomalyCancellation {𝓩 : Type} [CommRing 𝓩] (Q : Quanta 𝓩) : Prop

The linear anomaly cancellation condition, corresponding to ∑ᵢ qᵢ Nᵢ + ∑ₐ qₐ Nₐ = 0 where the first sum is over all 5-bar representations and the second is over all 10d representations.

Equations

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

def FTheory.SU5.Quanta.QuarticAnomalyCancellation {𝓩 : Type} [CommRing 𝓩] (Q : Quanta 𝓩) : Prop

The quartic anomaly cancellation condition, corresponding to ∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0 where the first sum is over all 5-bar representations and the second is over all 10d representations.

Equations

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

D.3.1. The propositions are decidable

instance FTheory.SU5.Quanta.instDecidableLinearAnomalyCancellationOfDecidableEq {𝓩 : Type} [CommRing 𝓩] [DecidableEq 𝓩] (Q : Quanta 𝓩) : Decidable Q.LinearAnomalyCancellation

Equations

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

instance FTheory.SU5.Quanta.instDecidableQuarticAnomalyCancellationOfDecidableEq {𝓩 : Type} [CommRing 𝓩] [DecidableEq 𝓩] (Q : Quanta 𝓩) : Decidable Q.QuarticAnomalyCancellation

Equations

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