Allowed charges

i. Overview

Within SU(5) F-theory with 10d and 5-bar matter fields there are constraints on the allowed U(1) charges the fields can have. These constraints are determined in arXiv:1504.05593. They are related to the distinct configurations of the zero-section (σ₀) relativity to the additional rational section (σ₁s) in codimension one fiber. For our purposes here, we currently just state the constraints found in arXiv:1504.05593, and leave the proof and derivation of these constraints to future work.

ii. Key results

• CodimensionOneConfig : The distinct configurations of the zero-section (σ₀) relativity to the additional rational section (σ₁s) in the codimension one fiber, I₅.
• CodimensionOneConfig.allowedBarFiveCharges : The allowed U(1)-charges of matter in the 5-bar representation of SU(5) given a CodimensionOneConfig.
• CodimensionOneConfig.allowedTenCharges : The allowed U(1)-charges of matter in the 10d representation of SU(5) given a CodimensionOneConfig.

iii. Table of contents

• A. The distinct section configurations
  • A.1. The finiteness of the set of configurations
• B. The allowed charges given a configuration
  • B.1. The allowed charges of the 5-bar matter
  • B.2. The allowed charges of the 10d matter
  • B.3. The finiteness of the allowed charges

iv. References

The main reference for the material in this section is the paper:

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.

• See also footnote 4 of 1507.05961

A. The distinct section configurations

inductive FTheory.SU5.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.SU5.instDecidableEqCodimensionOneConfig : DecidableEq CodimensionOneConfig

Equations

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

A.1. The finiteness of the set of configurations

instance FTheory.SU5.CodimensionOneConfig.instFintype : Fintype CodimensionOneConfig

Equations

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

B. The allowed charges given a configuration

B.1. The allowed charges of the 5-bar matter

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

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

Equations

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

B.2. The allowed charges of the 10d matter

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

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

Equations

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

B.3. The finiteness of the allowed charges

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

Equations

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

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

Equations

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