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)}

instance FTheory.SU5U1.instDecidableEqCodimensionOneConfig : DecidableEq CodimensionOneConfig

Equations

• FTheory.SU5U1.instDecidableEqCodimensionOneConfig x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance FTheory.SU5U1.CodimensionOneConfig.instFintype : Fintype CodimensionOneConfig

Equations

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

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}

instance FTheory.SU5U1.CodimensionOneConfig.instFintypeSubtypeIntMemFinsetAllowedBarFiveCharges (I : CodimensionOneConfig) : Fintype { x : ℤ // x ∈ I.allowedBarFiveCharges }

Equations

• FTheory.SU5U1.CodimensionOneConfig.same.instFintypeSubtypeIntMemFinsetAllowedBarFiveCharges = inferInstance
• FTheory.SU5U1.CodimensionOneConfig.nearestNeighbor.instFintypeSubtypeIntMemFinsetAllowedBarFiveCharges = inferInstance
• FTheory.SU5U1.CodimensionOneConfig.nextToNearestNeighbor.instFintypeSubtypeIntMemFinsetAllowedBarFiveCharges = inferInstance

def FTheory.SU5U1.CodimensionOneConfig.allowedBarFiveChargesList : CodimensionOneConfig → List ℤ

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

Equations

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

@[simp]

theorem FTheory.SU5U1.CodimensionOneConfig.mem_allowedBarFiveChargesList_iff {I : CodimensionOneConfig} (x : ℤ) : x ∈ I.allowedBarFiveChargesList ↔ x ∈ I.allowedBarFiveCharges

theorem FTheory.SU5U1.CodimensionOneConfig.allowedBarFiveChargesList_nodup (I : CodimensionOneConfig) : I.allowedBarFiveChargesList.Nodup

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}

instance FTheory.SU5U1.CodimensionOneConfig.instFintypeSubtypeIntMemFinsetAllowedTenCharges (I : CodimensionOneConfig) : Fintype { x : ℤ // x ∈ I.allowedTenCharges }

Equations

• FTheory.SU5U1.CodimensionOneConfig.same.instFintypeSubtypeIntMemFinsetAllowedTenCharges = inferInstance
• FTheory.SU5U1.CodimensionOneConfig.nearestNeighbor.instFintypeSubtypeIntMemFinsetAllowedTenCharges = inferInstance
• FTheory.SU5U1.CodimensionOneConfig.nextToNearestNeighbor.instFintypeSubtypeIntMemFinsetAllowedTenCharges = inferInstance

def FTheory.SU5U1.CodimensionOneConfig.allowedTenChargesList : CodimensionOneConfig → List ℤ

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

Equations

• FTheory.SU5U1.CodimensionOneConfig.same.allowedTenChargesList = [-3, -2, -1, 0, 1, 2, 3]
• FTheory.SU5U1.CodimensionOneConfig.nearestNeighbor.allowedTenChargesList = [-12, -7, -2, 3, 8, 13]
• FTheory.SU5U1.CodimensionOneConfig.nextToNearestNeighbor.allowedTenChargesList = [-9, -4, 1, 6, 11]

@[simp]

theorem FTheory.SU5U1.CodimensionOneConfig.mem_allowedTenChargesList_iff {I : CodimensionOneConfig} (x : ℤ) : x ∈ I.allowedTenChargesList ↔ x ∈ I.allowedTenCharges

theorem FTheory.SU5U1.CodimensionOneConfig.allowedTenChargesList_nodup (I : CodimensionOneConfig) : I.allowedTenChargesList.Nodup

Multisets of charges

def FTheory.SU5U1.CodimensionOneConfig.fiveChargeMultisetToList (I : CodimensionOneConfig) (S : Multiset ℤ) : List ℤ

Given a multiset S : Multiset ℤ for which all elements are members of I.allowedBarFiveCharges, fiveChargeMultisetToList I S is a computable list whose underlying multiset is S.

Equations

• I.fiveChargeMultisetToList S = List.flatMap (fun (x : ℤ) => List.replicate (Multiset.count x S) x) I.allowedBarFiveChargesList

def FTheory.SU5U1.CodimensionOneConfig.tenChargeMultisetToList (I : CodimensionOneConfig) (S : Multiset ℤ) : List ℤ

Given a multiset S : Multiset ℤ for which all elements are members of I.allowedTenCharges, tenChargeMultisetToList I S is a computable list whose underlying multiset is S.

Equations

• I.tenChargeMultisetToList S = List.flatMap (fun (x : ℤ) => List.replicate (Multiset.count x S) x) I.allowedTenChargesList

theorem FTheory.SU5U1.CodimensionOneConfig.fiveChargeMultisetToList_mem_iff {I : CodimensionOneConfig} {S : Multiset ℤ} {a : ℤ} : a ∈ I.fiveChargeMultisetToList S ↔ a ∈ S ∧ a ∈ I.allowedBarFiveCharges

theorem FTheory.SU5U1.CodimensionOneConfig.tenChargeMultisetToList_mem_iff {I : CodimensionOneConfig} {S : Multiset ℤ} {a : ℤ} : a ∈ I.tenChargeMultisetToList S ↔ a ∈ S ∧ a ∈ I.allowedTenCharges

theorem FTheory.SU5U1.CodimensionOneConfig.fiveChargeMultisetToList_count {I : CodimensionOneConfig} {S : Multiset ℤ} {a : ℤ} (hmem : a ∈ I.allowedBarFiveCharges) : List.count a (I.fiveChargeMultisetToList S) = Multiset.count a S

theorem FTheory.SU5U1.CodimensionOneConfig.tenChargeMultisetToList_count {I : CodimensionOneConfig} {S : Multiset ℤ} {a : ℤ} (hmem : a ∈ I.allowedTenCharges) : List.count a (I.tenChargeMultisetToList S) = Multiset.count a S

theorem FTheory.SU5U1.CodimensionOneConfig.coe_fiveChargeMultisetToList_of_all_mem (I : CodimensionOneConfig) (S : Multiset ℤ) (hs : ∀ s ∈ S, s ∈ I.allowedBarFiveCharges) : ↑(I.fiveChargeMultisetToList S) = S

theorem FTheory.SU5U1.CodimensionOneConfig.coe_tenChargeMultisetToList_of_all_mem (I : CodimensionOneConfig) (S : Multiset ℤ) (hs : ∀ s ∈ S, s ∈ I.allowedTenCharges) : ↑(I.tenChargeMultisetToList S) = S

theorem FTheory.SU5U1.CodimensionOneConfig.fiveChargeMultisetToList_length (I : CodimensionOneConfig) (S : Multiset ℤ) (hs : ∀ s ∈ S, s ∈ I.allowedBarFiveCharges) : (I.fiveChargeMultisetToList S).length = S.card

theorem FTheory.SU5U1.CodimensionOneConfig.tenChargeMultisetToList_length (I : CodimensionOneConfig) (S : Multiset ℤ) (hs : ∀ s ∈ S, s ∈ I.allowedTenCharges) : (I.tenChargeMultisetToList S).length = S.card