Imports
/-
Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nathaneal Sajan
-/
module
public import Physlib.Particles.StandardModel.Basic
public import Physlib.Relativity.Tensors.ComplexTensor.BasicCharged-lepton singlets
i. Overview
The Standard Model charged-lepton singlet is a right-handed Weyl spinor in the (1, 1)_{-6}
representation. Here charges are normalized as 6Y, so -6 is the usual hypercharge
Y = -1.
LeptonSinglet is the target vector space of one charged-lepton singlet. Its only index is
the Lorentz index carried by the Weyl spinor.
The Lorentz and gauge actions are first defined separately. The gauge action is then computed on an arbitrary spinor, used to identify its kernel, and descended to each supported global form of the Standard Model gauge group.
ii. Key results
LeptonSinglet : the target space of the (1, 1)_{-6} multiplet.
repLorentzGroup : the right-handed Lorentz action.
repGaugeGroupI : the action of the unquotiented gauge group.
repGaugeGroupI_apply : the gauge action on a spinor.
mem_repGaugeGroupI_ker_iff_eq : the kernel of the full-group action.
gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI : triviality of the central ℤ₆.
repGaugeGroup : the action descended to every supported gauge-group quotient.
iii. Table of contents
A. The charged-lepton-singlet space
B. Linear structure
C. Lorentz action
D. Gauge action
E. Kernel of the gauge action
F. Descent to quotient gauge groups
@[expose] public sectionA. The charged-lepton-singlet space
The Weyl spinor carries the right-handed Lorentz index, and it is the whole of the multiplet: a charged-lepton singlet has no colour index and no weak-isospin index.
The target vector space of one Standard Model charged-lepton singlet.
It carries the (1, 1)_{-6} representation of the gauge group.
The right-handed Weyl spinor.
@[ext]
structure LeptonSinglet where val : Fermion.RightHandedWeylB. Linear structure
The wrapper distinguishes charged-lepton singlets from other isomorphic vector spaces. The following equivalences transfer the linear structure of the Weyl-spinor space and expose that model when defining representations.
Identifies a charged-lepton singlet with its underlying Weyl spinor.
def valEquiv : LeptonSinglet ≃ Fermion.RightHandedWeyl where
toFun := val
invFun := fun m => ⟨m⟩instance : AddCommGroup LeptonSinglet := Equiv.addCommGroup valEquivinstance : Module ℂ LeptonSinglet := Equiv.module ℂ valEquivThe linear identification with the underlying Weyl-spinor space.
def valLinEquiv : LeptonSinglet ≃ₗ[ℂ] Fermion.RightHandedWeyl where
toFun := val
invFun := fun m => ⟨m⟩
map_add' := ⊢ ∀ (x y : LeptonSinglet), (x + y).val = x.val + y.val x✝:LeptonSinglety✝:LeptonSinglet⊢ (x✝ + y✝).val = x✝.val + y✝.val; All goals completed! 🐙
map_smul' := ⊢ ∀ (m : ℂ) (x : LeptonSinglet), (m • x).val = (RingHom.id ℂ) m • x.val m✝:ℂx✝:LeptonSinglet⊢ (m✝ • x✝).val = (RingHom.id ℂ) m✝ • x✝.val; All goals completed! 🐙@[simp]
lemma valLinEquiv_apply (l : LeptonSinglet) : valLinEquiv l = l.val := rfllemma valLinEquiv_symm_apply (m : Fermion.RightHandedWeyl) :
valLinEquiv.symm m = ⟨m⟩ := rfl@[simp]
lemma val_add (l₁ l₂ : LeptonSinglet) : (l₁ + l₂).val = l₁.val + l₂.val := rfl@[simp]
lemma val_smul (r : ℂ) (l : LeptonSinglet) : (r • l).val = r • l.val := rflC. Lorentz action
The Lorentz group acts through the right-handed Weyl representation, transported along the identification of a charged-lepton singlet with its spinor.
D. Gauge action
The colour and weak factors act trivially, so the gauge group acts only through hypercharge.
The U(1) action is star z ^ 6; since z is unitary, star z = z⁻¹, so this represents
charge -6.
The formulas below expose the scalar used to compare actions and compute the kernel.
The gauge group acts on a charged-lepton singlet by the hypercharge scalar alone.
lemma repGaugeGroupI_apply (g : GaugeGroupI) (ψ : Fermion.RightHandedWeyl) :
repGaugeGroupI g ⟨ψ⟩ = ⟨(star g.toU1.1 ^ 6) • ψ⟩ := rflE. Kernel of the gauge action
An element acts trivially exactly when its hypercharge scalar is one. Its colour and weak components are unrestricted, since neither appears in the action.
Characterizes the full-group elements acting trivially on the charged-lepton singlet.
g:GaugeGroupI⊢ star ↑(GaugeGroupI.toU1 g) ^ 6 = star ↑(GaugeGroupI.toU1 1) ^ 6 ↔ star ↑(GaugeGroupI.toU1 g) ^ 6 = 1
All goals completed! 🐙F. Descent to quotient gauge groups
A representation descends through a quotient when the quotient subgroup lies in its kernel.
The U(1) component of a central element is a sixth root of unity, so conjugating and raising
to the sixth power gives one, and charge -6 therefore acts trivially.
The central ℤ₆ subgroup acts trivially on (1, 1)_{-6}.
lemma gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI :
GaugeGroupQuot.subgroup .ℤ₆ ≤ repGaugeGroupI.ker := ⊢ GaugeGroupQuot.ℤ₆.subgroup ≤ MonoidHom.ker repGaugeGroupI
⊢ ∀ ⦃x : GaugeGroupI⦄ (x_1 : ℂˣ) (x_2 : x_1 ∈ rootsOfUnity 6 ℂ),
gaugeGroupℤ₆OfRoot ⟨x_1, x_2⟩ = x → star ↑(GaugeGroupI.toU1 x) ^ 6 = 1
x:ℂˣhx:x ∈ rootsOfUnity 6 ℂ⊢ star ↑(GaugeGroupI.toU1 (gaugeGroupℤ₆OfRoot ⟨x, hx⟩)) ^ 6 = 1
x:ℂˣhx:x ∈ rootsOfUnity 6 ℂ⊢ star ↑x ^ 6 = 1
x:ℂˣhx:x ∈ rootsOfUnity 6 ℂhx6:↑x ^ 6 = 1⊢ star ↑x ^ 6 = 1
All goals completed! 🐙Every supported quotient subgroup acts trivially on the charged-lepton singlet.
lemma gaugeGroup_subgroup_le_ker_repGaugeGroupI (Q : GaugeGroupQuot) :
Q.subgroup ≤ repGaugeGroupI.ker := Q.subgroup_le_subgroup_ℤ₆.trans
gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI