Matter

This module contains the data of the matter content of the SU(5) GUT model in F-theory with an additional U(1) symmetry.

References

Krippendorf, Schafer-Nameki and Wong. Froggatt-Nielson meets Mordell-Weil: A Phenomenological Survey of Global F-theory GUTs with U(1)s https://arxiv.org/pdf/1507.05961.

For conditions placed on the matter content, see: Krippendorf, Peña, Oehlmann, Ruehle. Rational F-theory GUTs without exotics https://arxiv.org/pdf/1401.5084.

@[reducible, inline]

abbrev FTheory.SU5U1.ChiralityFlux : Type

A type for the chirality flux of matter. This is induced by G₄-flux. This is often denoted M.

Equations

• FTheory.SU5U1.ChiralityFlux = ℤ

@[reducible, inline]

abbrev FTheory.SU5U1.HyperChargeFlux : Type

A type for the hypercharge flux associated with matter curves. This is often denote N.

Equations

• FTheory.SU5U1.HyperChargeFlux = ℤ

@[reducible, inline]

abbrev FTheory.SU5U1.QuantaBarFive (I : CodimensionOneConfig) : Type

The type of quanta associated with matter content in the 5-bar representation.

Equations

• FTheory.SU5U1.QuantaBarFive I = (FTheory.SU5U1.ChiralityFlux × FTheory.SU5U1.HyperChargeFlux × { x : ℤ // x ∈ I.allowedBarFiveCharges })

@[reducible, inline]

abbrev FTheory.SU5U1.QuantaBarFive.M {I : CodimensionOneConfig} (a : QuantaBarFive I) : ChiralityFlux

The ChiralityFlux quanta of a 5-bar representation.

Equations

• a.M = a.1

@[reducible, inline]

abbrev FTheory.SU5U1.QuantaBarFive.N {I : CodimensionOneConfig} (a : QuantaBarFive I) : HyperChargeFlux

The HyperChargeFlux quanta of a 5-bar representation.

Equations

• a.N = a.2.1

@[reducible, inline]

abbrev FTheory.SU5U1.QuantaBarFive.q {I : CodimensionOneConfig} (a : QuantaBarFive I) : { x : ℤ // x ∈ I.allowedBarFiveCharges }

The extra U(1) charge of a 5-bar representation.

Equations

• a.q = a.2.2

def FTheory.SU5U1.QuantaTen (I : CodimensionOneConfig) : Type

The type of quanta associated with matter content in the 10d representation.

Equations

• FTheory.SU5U1.QuantaTen I = (FTheory.SU5U1.ChiralityFlux × FTheory.SU5U1.HyperChargeFlux × { x : ℤ // x ∈ I.allowedTenCharges })

@[reducible, inline]

abbrev FTheory.SU5U1.QuantaTen.M {I : CodimensionOneConfig} (a : QuantaTen I) : ChiralityFlux

The ChiralityFlux quanta of a 10d representation.

Equations

• a.M = a.1

@[reducible, inline]

abbrev FTheory.SU5U1.QuantaTen.N {I : CodimensionOneConfig} (a : QuantaTen I) : HyperChargeFlux

The HyperChargeFlux quanta of a 10d representation.

Equations

• a.N = a.2.1

@[reducible, inline]

abbrev FTheory.SU5U1.QuantaTen.q {I : CodimensionOneConfig} (a : QuantaTen I) : { x : ℤ // x ∈ I.allowedTenCharges }

The extra U(1) charge of a 10d representation.

Equations

• a.q = a.2.2

structure FTheory.SU5U1.MatterContent (I : CodimensionOneConfig) : Type

The matter content, assumed to sit in the 5-bar or 10d representation of SU(5).

• quantaBarFive : Multiset (QuantaBarFive I)

  The chirality, charge and hyperChargeFlux associated with the 5-bar representations.

• quantaTen : Multiset (QuantaTen I)

  The chirality, charge and hyperChargeFlux associated with the 10d representations.

• chirality_charge_not_both_zero_bar_five (a : QuantaBarFive I) : a ∈ self.quantaBarFive → a.M = 0 → a.N ≠ 0

  There is no matter in the 5-bar representation with zero Chirality and HyperChargeFlux.

• chirality_charge_not_both_zero_ten (a : QuantaTen I) : a ∈ self.quantaTen → a.M = 0 → a.N ≠ 0

  There is no matter in the 10d representation with zero Chirality and HyperChargeFlux.

Gauge anomalies

https://arxiv.org/pdf/1401.5084

• Conditions (20) and (21) for the MSSM gauge group only.
• Condition (22) for the mixed anomaly between a single U(1) and the MSSM.
• Condition (23) for the mixed anomaly between two U(1)'s and the MSSM.

See also: arXiv:1209.4421

def FTheory.SU5U1.MatterContent.GaugeAnomalyMSSM {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The gauge anomalies coming from the SM gauge group.

These correspond to the conditions

• ∑ₐ Mₐ - ∑ᵢ Mᵢ = 0
• ∑ₐ Nₐ = 0
• ∑ᵢ Nᵢ = 0

where the sums are over the matter content in the 5-bar and 10d representations. Ref: See equation (20) and (21) of arXiv:1401.5084.

Equations

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

instance FTheory.SU5U1.MatterContent.instDecidableGaugeAnomalyMSSM {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.GaugeAnomalyMSSM

Equations

• 𝓜.instDecidableGaugeAnomalyMSSM = instDecidableAnd

def FTheory.SU5U1.MatterContent.GaugeAnomalyU1MSSM {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The mixed U(1)-MSSM gauge anomaly.

This condition corresponds to

∑ₐ qₐ Nₐ + ∑ᵢ qᵢ Nᵢ = 0

Ref: See equation (22) of arXiv:1401.5084.

Equations

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

instance FTheory.SU5U1.MatterContent.instDecidableGaugeAnomalyU1MSSM {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.GaugeAnomalyU1MSSM

Equations

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

def FTheory.SU5U1.MatterContent.GaugeAnomalyU1YU1U1 {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The mixed U(1)Y-U(1)-U(1) gauge anomaly.

This condition corresponds to

3 * ∑ₐ qₐ qₐ Nₐ + ∑ᵢ qᵢ qᵢ Nᵢ = 0

Ref: See equation (23) of arXiv:1401.5084.

Equations

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

instance FTheory.SU5U1.MatterContent.instDecidableGaugeAnomalyU1YU1U1 {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.GaugeAnomalyU1YU1U1

Equations

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

def FTheory.SU5U1.MatterContent.AnomalyFree {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Prop

The condition on matter content for it to be anomaly free.

Equations

• 𝓜.AnomalyFree = (𝓜.GaugeAnomalyMSSM ∧ 𝓜.GaugeAnomalyU1MSSM ∧ 𝓜.GaugeAnomalyU1YU1U1)

instance FTheory.SU5U1.MatterContent.instDecidableAnomalyFree {I : CodimensionOneConfig} (𝓜 : MatterContent I) : Decidable 𝓜.AnomalyFree

Equations

• 𝓜.instDecidableAnomalyFree = instDecidableAnd