Charges assocated with field labels

Given a field label F, and a charge x : Charges, we can extract the set of charges associated with that field label. This is done by the function ofFieldLabel, which returns a Finset ℤ.

def FTheory.SU5U1.Charges.ofFieldLabel (x : Charges) : SuperSymmetry.SU5.FieldLabel → Finset ℤ

Given an x : Charges, the charges associated with a given FieldLabel.

Equations

• x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveBarHd = x.1.toFinset
• x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveBarHu = x.2.1.toFinset
• x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveBarMatter = x.2.2.1
• x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.tenMatter = x.2.2.2
• x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveHd = Finset.map { toFun := Neg.neg, inj' := FTheory.SU5U1.Charges.ofFieldLabel._proof_1 } x.1.toFinset
• x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveHu = Finset.map { toFun := Neg.neg, inj' := FTheory.SU5U1.Charges.ofFieldLabel._proof_1 } x.2.1.toFinset
• x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveMatter = Finset.map { toFun := Neg.neg, inj' := FTheory.SU5U1.Charges.ofFieldLabel._proof_1 } x.2.2.1

@[simp]

theorem FTheory.SU5U1.Charges.mem_ofFieldLabel_fiveHd (x : ℤ) (y : Charges) : x ∈ y.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveHd ↔ -x ∈ y.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveBarHd

@[simp]

theorem FTheory.SU5U1.Charges.mem_ofFieldLabel_fiveHu (x : ℤ) (y : Charges) : x ∈ y.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveHu ↔ -x ∈ y.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveBarHu

@[simp]

theorem FTheory.SU5U1.Charges.mem_ofFieldLabel_fiveMatter (x : ℤ) (y : Charges) : x ∈ y.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveMatter ↔ -x ∈ y.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveBarMatter

theorem FTheory.SU5U1.Charges.ofFieldLabel_subset_of_subset {x y : Charges} (h : x ⊆ y) (F : SuperSymmetry.SU5.FieldLabel) : x.ofFieldLabel F ⊆ y.ofFieldLabel F

theorem FTheory.SU5U1.Charges.ext_ofFieldLabel {x y : Charges} (h : ∀ (F : SuperSymmetry.SU5.FieldLabel), x.ofFieldLabel F = y.ofFieldLabel F) : x = y

Two charges are equal if they are equal on all field labels.