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
SuperSymmetry.SU5.Charges.ofFieldLabel
{𝓩 : Type}
[InvolutiveNeg 𝓩]
(x : Charges 𝓩)
:
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' := ⋯ } x.1.toFinset
- x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveHu = Finset.map { toFun := Neg.neg, inj' := ⋯ } x.2.1.toFinset
- x.ofFieldLabel SuperSymmetry.SU5.FieldLabel.fiveMatter = Finset.map { toFun := Neg.neg, inj' := ⋯ } x.2.2.1
Instances For
@[simp]
theorem
SuperSymmetry.SU5.Charges.ofFieldLabel_empty
{𝓩 : Type}
[InvolutiveNeg 𝓩]
(F : FieldLabel)
:
theorem
SuperSymmetry.SU5.Charges.ofFieldLabel_mono
{𝓩 : Type}
[InvolutiveNeg 𝓩]
{x y : Charges 𝓩}
(h : x ⊆ y)
(F : FieldLabel)
:
@[simp]
theorem
SuperSymmetry.SU5.Charges.mem_ofFieldLabel_fiveHd
{𝓩 : Type}
[InvolutiveNeg 𝓩]
(x : 𝓩)
(y : Charges 𝓩)
:
@[simp]
theorem
SuperSymmetry.SU5.Charges.mem_ofFieldLabel_fiveHu
{𝓩 : Type}
[InvolutiveNeg 𝓩]
(x : 𝓩)
(y : Charges 𝓩)
:
@[simp]
theorem
SuperSymmetry.SU5.Charges.mem_ofFieldLabel_fiveMatter
{𝓩 : Type}
[InvolutiveNeg 𝓩]
(x : 𝓩)
(y : Charges 𝓩)
:
theorem
SuperSymmetry.SU5.Charges.ext_ofFieldLabel
{𝓩 : Type}
[InvolutiveNeg 𝓩]
{x y : Charges 𝓩}
(h : ∀ (F : FieldLabel), x.ofFieldLabel F = y.ofFieldLabel F)
:
Two charges are equal if they are equal on all field labels.