Quanta from charges and fluxes

Each FiveQuanta or TenQuanta has an underlying FluxesFive or FluxesTen and Multiset ℤ of charges.

In this file we define the fromParts function which takes a FluxesFive or FluxesTen and a Multiset ℤ of charges and returns a list of the allowed FiveQuanta or TenQuanta which can be formed from them.

We do this only in the very restrictive case when:

• fluxes has no exotics and has no zero fluxes
• charges lives in allowedBarFiveCharges or allowedBarTenCharges for a given CodimensionOneConfig.

FiveQuanta from parts

def FTheory.SU5U1.FiveQuanta.fromParts (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesFive) : List FiveQuanta

The list of FiveQuanta which arise from charges and fluxes. Note: This gives junk unless the charges correspond to a CodimensionOneConfig and fluxes has no exotics and no zero entries.

Equations

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

theorem FTheory.SU5U1.FiveQuanta.self_mem_fromParts_of_toCharges_toFluxesFive (I : CodimensionOneConfig) (F : FiveQuanta) (hf : F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedBarFiveCharges) : F ∈ fromParts I F.toCharges F.toFluxesFive

theorem FTheory.SU5U1.FiveQuanta.card_eq_charges_card_of_mem_fromParts (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesFive) (hf : fluxes.NoExotics ∧ fluxes.HasNoZero) (hc : ∀ s ∈ charges, s ∈ I.allowedBarFiveCharges) (F : FiveQuanta) : F ∈ fromParts I charges fluxes → Multiset.card F = charges.card

theorem FTheory.SU5U1.FiveQuanta.card_eq_fluxes_card_of_mem_fromParts (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesFive) (hf : fluxes.NoExotics ∧ fluxes.HasNoZero) (hc : ∀ s ∈ charges, s ∈ I.allowedBarFiveCharges) (F : FiveQuanta) : F ∈ fromParts I charges fluxes → Multiset.card F = Multiset.card fluxes

theorem FTheory.SU5U1.FiveQuanta.fromParts_eq_preimage (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesFive) (hf : fluxes.NoExotics ∧ fluxes.HasNoZero) (hc : ∀ s ∈ charges, s ∈ I.allowedBarFiveCharges) (F : FiveQuanta) : F.toCharges = charges ∧ F.toFluxesFive = fluxes ↔ F ∈ fromParts I charges fluxes

def FTheory.SU5U1.FiveQuanta.ofCharges (I : CodimensionOneConfig) (c : Multiset ℤ) : Multiset FiveQuanta

The multiset of FiveQuanta obtained from a mutliset of charges Multiset ℤ, which have a FluxesFive in FluxesFive.elemsNoExotics.

Equations

• FTheory.SU5U1.FiveQuanta.ofCharges I c = FTheory.SU5U1.FluxesFive.elemsNoExotics.bind fun (f : FTheory.SU5U1.FluxesFive) => ↑(FTheory.SU5U1.FiveQuanta.fromParts I c f)

theorem FTheory.SU5U1.FiveQuanta.mem_ofCharges_iff (I : CodimensionOneConfig) (charges : Multiset ℤ) (hc : ∀ s ∈ charges, s ∈ I.allowedBarFiveCharges) (F : FiveQuanta) : F ∈ ofCharges I charges ↔ F.toCharges = charges ∧ F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero

theorem FTheory.SU5U1.FiveQuanta.mem_ofCharges_self (I : CodimensionOneConfig) (c : FiveQuanta) (h : c.toFluxesFive.NoExotics) (hnz : c.toFluxesFive.HasNoZero) (hc : ∀ s ∈ c.toCharges, s ∈ I.allowedBarFiveCharges) : c ∈ ofCharges I c.toCharges

TenQuanta from parts

def FTheory.SU5U1.TenQuanta.fromParts (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesTen) : List TenQuanta

The list of TenQuanta which arise from charges and fluxes. Note: This gives junk unless charges the charges correspond to a CodimensionOneConfig and fluxes has no exotics and no zero entries.

Equations

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

theorem FTheory.SU5U1.TenQuanta.self_mem_fromParts_of_toCharges_toFluxesTen (I : CodimensionOneConfig) (F : TenQuanta) (hf : F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedTenCharges) : F ∈ fromParts I F.toCharges F.toFluxesTen

theorem FTheory.SU5U1.TenQuanta.card_eq_charges_card_of_mem_fromParts (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesTen) (hf : fluxes.NoExotics ∧ fluxes.HasNoZero) (hc : ∀ s ∈ charges, s ∈ I.allowedTenCharges) (F : TenQuanta) : F ∈ fromParts I charges fluxes → Multiset.card F = charges.card

theorem FTheory.SU5U1.TenQuanta.card_eq_fluxes_card_of_mem_fromParts (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesTen) (hf : fluxes.NoExotics ∧ fluxes.HasNoZero) (hc : ∀ s ∈ charges, s ∈ I.allowedTenCharges) (F : TenQuanta) : F ∈ fromParts I charges fluxes → Multiset.card F = Multiset.card fluxes

theorem FTheory.SU5U1.TenQuanta.fromParts_eq_preimage (I : CodimensionOneConfig) (charges : Multiset ℤ) (fluxes : FluxesTen) (hf : fluxes.NoExotics ∧ fluxes.HasNoZero) (hc : ∀ s ∈ charges, s ∈ I.allowedTenCharges) (F : TenQuanta) : F.toCharges = charges ∧ F.toFluxesTen = fluxes ↔ F ∈ fromParts I charges fluxes

def FTheory.SU5U1.TenQuanta.ofCharges (I : CodimensionOneConfig) (c : Multiset ℤ) : Multiset TenQuanta

The multiset of TenQuanta obtained from a mutliset of charges Multiset ℤ, which have a FluxesTen in FluxesTen.elemsNoExotics.

Equations

• FTheory.SU5U1.TenQuanta.ofCharges I c = FTheory.SU5U1.FluxesTen.elemsNoExotics.bind fun (f : FTheory.SU5U1.FluxesTen) => ↑(FTheory.SU5U1.TenQuanta.fromParts I c f)

theorem FTheory.SU5U1.TenQuanta.mem_ofCharges_iff (I : CodimensionOneConfig) (charges : Multiset ℤ) (hc : ∀ s ∈ charges, s ∈ I.allowedTenCharges) (F : TenQuanta) : F ∈ ofCharges I charges ↔ F.toCharges = charges ∧ F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero

theorem FTheory.SU5U1.TenQuanta.mem_ofCharges_self (I : CodimensionOneConfig) (c : TenQuanta) (h : c.toFluxesTen.NoExotics) (hnz : c.toFluxesTen.HasNoZero) (hc : ∀ s ∈ c.toCharges, s ∈ I.allowedTenCharges) : c ∈ ofCharges I c.toCharges

def FTheory.SU5U1.Quanta.ofCharges (I : CodimensionOneConfig) (c : Charges) : Multiset Quanta

The multiset of Quanta obtained from a Charges, which have a Fluxes which do not permit exotics.

Equations

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