PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.ChargeSpectrum.OfFieldLabel

Charges assocaited with a field label #

i. Overview #

Recall that a FieldLabel is one of the seven possible superfields in the SU(5) GUT, corresponding to the fields present and their conjugates.

Given a charge spectrum x : ChargeSpectrum 𝓩, we are intrested in the finite set of charges carried by representations associated with a given FieldLabel.

Results in this module will be used to find the charges associated with terms in the potential.

ii. Key results #

iii. Table of contents #

iv. References #

There are no known references for the results in this file.

A. Charges associated with a field label #

We first define ofFieldLabel, which given a charge spectrum x : ChargeSpectrum 𝓩 and a FieldLabel, returns the finite set of charges associated with representations corresponding to that FieldLabel.

source
def SuperSymmetry.SU5.ChargeSpectrum.ofFieldLabel {𝓩 : Type} [InvolutiveNeg 𝓩] (x : ChargeSpectrum 𝓩) :
FieldLabel → Finset 𝓩

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

Equations
Instances For

    A.1. The field labels for the empty charge spectrum #

    We show that the charges associated with any field label for the empty charge spectrum is empty. This follows directly from the definition.

    source
    @[simp]
    theorem SuperSymmetry.SU5.ChargeSpectrum.ofFieldLabel_empty {𝓩 : Type} [InvolutiveNeg 𝓩] (F : FieldLabel) :
    ∅.ofFieldLabel F = ∅

    ofFieldLabel ∅ F is empty for any field label F.

    A.2. Monotonicity of ofFieldLabel #

    We show that the function ofFieldLabel is monotone in the charge spectrum, with relation to the subset relation. That is for a fixed field label F, if x ⊆ y are charge spectra, then ofFieldLabel x F ⊆ ofFieldLabel y F.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.ofFieldLabel_mono {𝓩 : Type} [InvolutiveNeg 𝓩] {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) (F : FieldLabel) :
    x.ofFieldLabel F ⊆ y.ofFieldLabel F

    The function ofFieldLabel is monotone in the charge spectrum.

    A.3. Membership of conjugate charegs #

    We show that a charge is a member of the finite sets associated with a field label if and only if its negative is a member of the finite set associated with the conjugate field label.

    source
    @[simp]
    theorem SuperSymmetry.SU5.ChargeSpectrum.mem_ofFieldLabel_fiveHd {𝓩 : Type} [InvolutiveNeg 𝓩] (x : 𝓩) (y : ChargeSpectrum 𝓩) :
    x ∈ y.ofFieldLabel FieldLabel.fiveHd ↔ -x ∈ y.ofFieldLabel FieldLabel.fiveBarHd
    source
    @[simp]
    theorem SuperSymmetry.SU5.ChargeSpectrum.mem_ofFieldLabel_fiveHu {𝓩 : Type} [InvolutiveNeg 𝓩] (x : 𝓩) (y : ChargeSpectrum 𝓩) :
    x ∈ y.ofFieldLabel FieldLabel.fiveHu ↔ -x ∈ y.ofFieldLabel FieldLabel.fiveBarHu
    source
    @[simp]
    theorem SuperSymmetry.SU5.ChargeSpectrum.mem_ofFieldLabel_fiveMatter {𝓩 : Type} [InvolutiveNeg 𝓩] (x : 𝓩) (y : ChargeSpectrum 𝓩) :
    x ∈ y.ofFieldLabel FieldLabel.fiveMatter ↔ -x ∈ y.ofFieldLabel FieldLabel.fiveBarMatter

    A.4. Extensionality of charge spectra via ofFieldLabel #

    We whow that two charge spectra are equal if they are equal on all field labels.

    This extensionality lemma is actually overkill in most cases, as there are a lot more direct ways to show that two charge spectra are equal.

    source
    theorem SuperSymmetry.SU5.ChargeSpectrum.ext_ofFieldLabel {𝓩 : Type} [InvolutiveNeg 𝓩] {x y : ChargeSpectrum 𝓩} (h : ∀ (F : FieldLabel), x.ofFieldLabel F = y.ofFieldLabel F) :
    x = y

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