Charges associated with a potential term

Given a potential term T, and a charge x : Charges, we can extract the set of charges associated with instances of that potential term.

def FTheory.SU5U1.Charges.ofPotentialTerm (x : Charges) (T : SuperSymmetry.SU5.PotentialTerm) : Multiset ℤ

Given a charges x : Charges associated to the representations, and a potential term T, the charges associated with instances of that potential term.

Equations

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

theorem FTheory.SU5U1.Charges.ofPotentialTerm_subset_of_subset {x y : Charges} (h : x ⊆ y) (T : SuperSymmetry.SU5.PotentialTerm) : x.ofPotentialTerm T ⊆ y.ofPotentialTerm T

def FTheory.SU5U1.Charges.ofPotentialTerm' (y : Charges) (T : SuperSymmetry.SU5.PotentialTerm) : Multiset ℤ

Given a charges x : Charges associated to the representations, and a potential term T, the charges associated with instances of that potential term.

This is a more explicit form of PotentialTerm, which has the benifit that it is quick with decide, but it is not defined based on more fundamental concepts, like ofPotentialTerm is.

Equations

• One or more equations did not get rendered due to their size.
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.μ = Multiset.map (fun (x : ℤ × ℤ) => x.1 - x.2) (y.1.toFinset.product y.2.1.toFinset).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.β = Multiset.map (fun (x : ℤ × ℤ) => -x.1 + x.2) (y.2.1.toFinset.product y.2.2.1).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.Λ = Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 + x.2.1 + x.2.2) (y.2.2.1.product (y.2.2.1.product y.2.2.2)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.W3 = Multiset.map (fun (x : ℤ × ℤ × ℤ) => -x.1 - x.1 + x.2.1 + x.2.2) (y.2.1.toFinset.product (y.2.2.1.product y.2.2.1)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.W4 = Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 - x.2.1 - x.2.1 + x.2.2) (y.1.toFinset.product (y.2.1.toFinset.product y.2.2.1)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.K1 = Multiset.map (fun (x : ℤ × ℤ × ℤ) => -x.1 + x.2.1 + x.2.2) (y.2.2.1.product (y.2.2.2.product y.2.2.2)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.K2 = Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 + x.2.1 + x.2.2) (y.1.toFinset.product (y.2.1.toFinset.product y.2.2.2)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.topYukawa = Multiset.map (fun (x : ℤ × ℤ × ℤ) => -x.1 + x.2.1 + x.2.2) (y.2.1.toFinset.product (y.2.2.2.product y.2.2.2)).val
• y.ofPotentialTerm' SuperSymmetry.SU5.PotentialTerm.bottomYukawa = Multiset.map (fun (x : ℤ × ℤ × ℤ) => x.1 + x.2.1 + x.2.2) (y.1.toFinset.product (y.2.2.1.product y.2.2.2)).val

theorem FTheory.SU5U1.Charges.ofPotentialTerm_subset_ofPotentialTerm' {x : Charges} (T : SuperSymmetry.SU5.PotentialTerm) : x.ofPotentialTerm T ⊆ x.ofPotentialTerm' T

theorem FTheory.SU5U1.Charges.ofPotentialTerm'_subset_ofPotentialTerm {x : Charges} (T : SuperSymmetry.SU5.PotentialTerm) : x.ofPotentialTerm' T ⊆ x.ofPotentialTerm T

theorem FTheory.SU5U1.Charges.mem_ofPotentialTerm_iff_mem_ofPotentialTerm {T : SuperSymmetry.SU5.PotentialTerm} {n : ℤ} {y : Charges} : n ∈ y.ofPotentialTerm T ↔ n ∈ y.ofPotentialTerm' T