Quanta of representations

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.

@[reducible, inline]

abbrev FTheory.SU5U1.FiveQuanta : Type

The quanta of 5-bar representations corresponding to a multiset of (q, M, N) for each partcile. (M, N) are defined in the FluxesFive module.

Equations

• FTheory.SU5U1.FiveQuanta = Multiset (ℤ × ℤ × ℤ)

def FTheory.SU5U1.FiveQuanta.toFluxesFive (x : FiveQuanta) : FluxesFive

The underlying FluxesFive from a FiveQuanta.

Equations

• x.toFluxesFive = Multiset.map Prod.snd x

def FTheory.SU5U1.FiveQuanta.toCharges (x : FiveQuanta) : Multiset ℤ

The underlying Multiset charges from a FiveQuanta.

Equations

• x.toCharges = Multiset.map Prod.fst x

@[reducible, inline]

abbrev FTheory.SU5U1.TenQuanta : Type

The quanta of w0d representations corresponding to a multiset of (q, M, N) for each partcile. (M, N) are defined in the FluxesFive module.

Equations

• FTheory.SU5U1.TenQuanta = Multiset (ℤ × ℤ × ℤ)

def FTheory.SU5U1.TenQuanta.toFluxesTen (x : TenQuanta) : FluxesTen

The underlying FluxesTen from a TenQuanta.

Equations

• x.toFluxesTen = Multiset.map Prod.snd x

def FTheory.SU5U1.TenQuanta.toCharges (x : TenQuanta) : Multiset ℤ

The underlying Multiset charges from a TenQuanta.

Equations

• x.toCharges = Multiset.map Prod.fst x

@[reducible, inline]

abbrev FTheory.SU5U1.Quanta : 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 intergers (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.

Equations

• FTheory.SU5U1.Quanta = (Option ℤ × Option ℤ × FTheory.SU5U1.FiveQuanta × FTheory.SU5U1.TenQuanta)

instance FTheory.SU5U1.Quanta.instDecidableEq : DecidableEq Quanta

Equations

• FTheory.SU5U1.Quanta.instDecidableEq = instDecidableEqProd

def FTheory.SU5U1.Quanta.toCharges (x : Quanta) : Charges

The underlying Charges of a Quanta.

Equations

• x.toCharges = (x.1, x.2.1, x.2.2.1.toCharges.toFinset, x.2.2.2.toCharges.toFinset)