Quanta into list

The types FiveQuanta and TenQuanta are defined as multisets, but in some instances it is good to have them as lists. Usually turning a multiset into a list is done using choice, and therefore is not computable. However, in the cases when NoExotics and HasNoZero hold, and all the charges in the FiveQuanta and TenQuanta correspond to some CodimensionOneConfig then possible elements of FluxesFive and FluxesTen are known. Thus we can use those elements to construct a list of the fluxes from multisets, in a way which is computable. This file provides the definitions and lemmas needed to do this.

FiveQuanta to lists

def FTheory.SU5U1.FiveQuanta.allowedElems (I : CodimensionOneConfig) : List (ℤ × ℤ × ℤ)

The allowed elements of a FiveQuanta for which the underlying FluxesFive obeys NoExotics and HasNoZero and for which the charges are determined by a CodimensionOneConfig.

Equations

• FTheory.SU5U1.FiveQuanta.allowedElems I = List.flatMap (fun (x : ℤ) => List.map (fun (y : ℤ × ℤ) => (x, y.1, y.2)) FTheory.SU5U1.FluxesFive.allowedPairs) I.allowedBarFiveChargesList

theorem FTheory.SU5U1.FiveQuanta.mem_allowedElems_of_mem {I : CodimensionOneConfig} (F : FiveQuanta) (hf : F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedBarFiveCharges) (x : ℤ × ℤ × ℤ) (h : x ∈ F) : x ∈ allowedElems I

def FTheory.SU5U1.FiveQuanta.toList (I : CodimensionOneConfig) (F : FiveQuanta) : List (ℤ × ℤ × ℤ)

A list from a FiveQuanta which when the underlying FluxesFive obeys NoExotics and HasNoZero, and the charges are determined by a CodimensionOneConfig, is a list whose underlying multiset is the FiveQuanta. Otherwise this list produces junk.

Equations

• FTheory.SU5U1.FiveQuanta.toList I F = List.flatMap (fun (x : ℤ × ℤ × ℤ) => List.replicate (Multiset.count x F) x) (FTheory.SU5U1.FiveQuanta.allowedElems I)

theorem FTheory.SU5U1.FiveQuanta.mem_allowedElems_of_mem_toList (I : CodimensionOneConfig) (F : FiveQuanta) (x : ℤ × ℤ × ℤ) (h : x ∈ toList I F) : x ∈ allowedElems I

theorem FTheory.SU5U1.FiveQuanta.snd_mem_allowedPairs_of_mem_toList (I : CodimensionOneConfig) (F : FiveQuanta) (x : ℤ × ℤ × ℤ) (h : x ∈ toList I F) : x.2 ∈ FluxesFive.allowedPairs

theorem FTheory.SU5U1.FiveQuanta.mem_toList_iff {I : CodimensionOneConfig} (F : FiveQuanta) (hf : F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedBarFiveCharges) {a : ℤ × ℤ × ℤ} : a ∈ toList I F ↔ a ∈ F

theorem FTheory.SU5U1.FiveQuanta.toList_count {I : CodimensionOneConfig} {F : FiveQuanta} {a : ℤ × ℤ × ℤ} (hf : F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedBarFiveCharges) (hmema : a ∈ allowedElems I) : List.count a (toList I F) = Multiset.count a F

theorem FTheory.SU5U1.FiveQuanta.coe_toList {I : CodimensionOneConfig} {F : FiveQuanta} (hf : F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedBarFiveCharges) : ↑(toList I F) = F

theorem FTheory.SU5U1.FiveQuanta.toList_prod_fst_eq {I : CodimensionOneConfig} {F : FiveQuanta} (hf : F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedBarFiveCharges) : List.map Prod.fst (toList I F) = I.fiveChargeMultisetToList F.toCharges

theorem FTheory.SU5U1.FiveQuanta.toList_prod_snd_perm {I : CodimensionOneConfig} {F : FiveQuanta} (hf : F.toFluxesFive.NoExotics ∧ F.toFluxesFive.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedBarFiveCharges) : (List.map Prod.snd (toList I F)).Perm F.toFluxesFive.toList

TenQuanta to lists

def FTheory.SU5U1.TenQuanta.allowedElems (I : CodimensionOneConfig) : List (ℤ × ℤ × ℤ)

The allowed elements of a FiveQuanta for which the underlying FluxesFive obeys NoExotics and HasNoZero and for which the charges are determined by a CodimensionOneConfig.

Equations

• FTheory.SU5U1.TenQuanta.allowedElems I = List.flatMap (fun (x : ℤ) => List.map (fun (y : ℤ × ℤ) => (x, y.1, y.2)) FTheory.SU5U1.FluxesTen.allowedPairs) I.allowedTenChargesList

theorem FTheory.SU5U1.TenQuanta.mem_allowedElems_of_mem {I : CodimensionOneConfig} (F : TenQuanta) (hf : F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedTenCharges) (x : ℤ × ℤ × ℤ) (h : x ∈ F) : x ∈ allowedElems I

def FTheory.SU5U1.TenQuanta.toList (I : CodimensionOneConfig) (F : TenQuanta) : List (ℤ × ℤ × ℤ)

A list from a TenQuanta which when the underlying FluxesTen obeys NoExotics and HasNoZero, and the charges are determined by a CodimensionOneConfig, is a list whose underlying multiset is the TenQuanta. Otherwise this list produces junk.

Equations

• FTheory.SU5U1.TenQuanta.toList I F = List.flatMap (fun (x : ℤ × ℤ × ℤ) => List.replicate (Multiset.count x F) x) (FTheory.SU5U1.TenQuanta.allowedElems I)

theorem FTheory.SU5U1.TenQuanta.mem_allowedElems_of_mem_toList (I : CodimensionOneConfig) (F : TenQuanta) (x : ℤ × ℤ × ℤ) (h : x ∈ toList I F) : x ∈ allowedElems I

theorem FTheory.SU5U1.TenQuanta.snd_mem_allowedPairs_of_mem_toList (I : CodimensionOneConfig) (F : TenQuanta) (x : ℤ × ℤ × ℤ) (h : x ∈ toList I F) : x.2 ∈ FluxesTen.allowedPairs

theorem FTheory.SU5U1.TenQuanta.mem_toList_iff {I : CodimensionOneConfig} (F : TenQuanta) (hf : F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedTenCharges) {a : ℤ × ℤ × ℤ} : a ∈ toList I F ↔ a ∈ F

theorem FTheory.SU5U1.TenQuanta.toList_count {I : CodimensionOneConfig} {F : TenQuanta} {a : ℤ × ℤ × ℤ} (hf : F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedTenCharges) (hmema : a ∈ allowedElems I) : List.count a (toList I F) = Multiset.count a F

theorem FTheory.SU5U1.TenQuanta.coe_toList {I : CodimensionOneConfig} {F : TenQuanta} (hf : F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedTenCharges) : ↑(toList I F) = F

theorem FTheory.SU5U1.TenQuanta.toList_prod_fst_eq {I : CodimensionOneConfig} {F : TenQuanta} (hf : F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedTenCharges) : List.map Prod.fst (toList I F) = I.tenChargeMultisetToList F.toCharges

theorem FTheory.SU5U1.TenQuanta.toList_prod_snd_perm {I : CodimensionOneConfig} {F : TenQuanta} (hf : F.toFluxesTen.NoExotics ∧ F.toFluxesTen.HasNoZero) (hc : ∀ s ∈ F.toCharges, s ∈ I.allowedTenCharges) : (List.map Prod.snd (toList I F)).Perm F.toFluxesTen.toList