Allowed charges

For an SU(5) GUT model in F-theory with an additional U(1) symmetry, this module gives the possible charges of the matter fields.

References

Lawrie, Schafer-Nameki and Wong. F-theory and All Things Rational: Surveying U(1) Symmetries with Rational Sections https://arxiv.org/pdf/1504.05593. Page 6.

TODO

The results in this file are currently stated, but not proved.

inductive FTheory.SU5U1.CodimensionOneConfig : Type

The distinct codimension one configurations of the zero-section (σ₀) relativity to the additional rational section (σ₁s).

• same : CodimensionOneConfig

  σ₀ and σ₁ intersect the same ℙ¹ of the I₅ Kodaira fiber. This is sometimes denoted I₅^{(01)}

• nearestNeighbor : CodimensionOneConfig

  σ₀ and σ₁ intersect the nearest neighbor ℙ¹s of the I₅ Kodaira fiber. This is sometimes denoted I₅^{(0|1)}

• nextToNearestNeighbor : CodimensionOneConfig

  σ₀ and σ₁ intersect the next to nearest neighbor ℙ¹s of the I₅ Kodaira fiber. This is sometimes denoted I₅^{(0||1)}

def FTheory.SU5U1.CodimensionOneConfig.allowedBarFiveCharges : CodimensionOneConfig → Finset ℤ

The allowed U(1)-charges of matter in the 5-bar representation of SU(5) given a CodimensionOneConfig.

Equations

• FTheory.SU5U1.CodimensionOneConfig.same.allowedBarFiveCharges = {-3, -2, -1, 0, 1, 2, 3}
• FTheory.SU5U1.CodimensionOneConfig.nearestNeighbor.allowedBarFiveCharges = {-14, -9, -4, 1, 6, 11}
• FTheory.SU5U1.CodimensionOneConfig.nextToNearestNeighbor.allowedBarFiveCharges = {-13, -8, -3, 2, 7, 12}

def FTheory.SU5U1.CodimensionOneConfig.allowedTenCharges : CodimensionOneConfig → Finset ℤ

The allowed U(1)-charges of matter in the 10d representation of SU(5) given a CodimensionOneConfig.

Equations

• FTheory.SU5U1.CodimensionOneConfig.same.allowedTenCharges = {-3, -2, -1, 0, 1, 2, 3}
• FTheory.SU5U1.CodimensionOneConfig.nearestNeighbor.allowedTenCharges = {-12, -7, -2, 3, 8, 13}
• FTheory.SU5U1.CodimensionOneConfig.nextToNearestNeighbor.allowedTenCharges = {-9, -4, 1, 6, 11}