From 1b2c54c6387716a0b761de126ecc5c22b4a4a370 Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 25 Jul 2026 19:23:16 +0400 Subject: [PATCH 1/7] feat(down-singlet): add target space Co-authored-by: ChatGPT --- .../StandardModel/Fermions/DownSinglet.lean | 111 ++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 Physlib/Particles/StandardModel/Fermions/DownSinglet.lean diff --git a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean new file mode 100644 index 000000000..e6c6f8743 --- /dev/null +++ b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean @@ -0,0 +1,111 @@ +/- +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.Basic +/-! +# Down-type singlets + +## i. Overview + +The Standard Model down-type singlet is a right-handed Weyl spinor in the `(3, 1)_{-2}` +representation. Here charges are normalized as `6Y`, so `-2` is the usual hypercharge +`Y = -1/3`. + +`DownSinglet` is the target vector space of one down-type quark multiplet. Its Weyl factor +carries the Lorentz index and its three-dimensional factor carries the colour index. The absence +of a weak factor makes it an `SU(2)` singlet. + +The Lorentz and gauge actions are first defined separately. The gauge action is then computed on a +basis, used to identify its kernel, and descended to each supported global form of the Standard +Model gauge group. + +## ii. Key results + +- `DownSinglet` : the target space of the `(3, 1)_{-2}` multiplet. +- `repLorentzGroup` : the right-handed Lorentz action. +- `repGaugeGroupI` : the action of the unquotiented gauge group. +- `repGaugeGroupI_tmul_basis_eq_sum` : the gauge action in a tensor-product basis. +- `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 down-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 section + +namespace StandardModel + +open TensorProduct + +/-! + +## A. The down-singlet space + +The Weyl factor carries the right-handed Lorentz index, while +`EuclideanSpace ℂ (Fin 3)` carries the colour index. +-/ + +/-- The target vector space of one Standard Model down-type singlet quark. +It carries the `(3, 1)_{-2}` representation of the gauge group. -/ +@[ext] +structure DownSinglet where + /-- The right-handed Weyl spinor with its colour index. -/ + val : Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3) + +namespace DownSinglet + +/-! + +## B. Linear structure + +`DownSinglet` wraps its tensor-product carrier as a distinct type. The equivalences below identify +the two types and transport the additive and complex module structures to `DownSinglet`. +-/ + +/-- Identifies a down-type singlet with its underlying tensor-product value. -/ +def valEquiv : DownSinglet ≃ Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3) where + toFun := val + invFun := fun m => ⟨m⟩ + +instance : AddCommGroup DownSinglet := Equiv.addCommGroup valEquiv + +instance : Module ℂ DownSinglet := Equiv.module ℂ valEquiv + +/-- The linear identification with the underlying tensor product. -/ +def valLinEquiv : DownSinglet ≃ₗ[ℂ] + Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3) where + toFun := val + invFun := fun m => ⟨m⟩ + map_add' := by intros; rfl + map_smul' := by intros; rfl + +@[simp] +lemma valLinEquiv_apply (d : DownSinglet) : valLinEquiv d = d.val := rfl + +lemma valLinEquiv_symm_apply + (m : Fermion.RightHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3)) : + valLinEquiv.symm m = ⟨m⟩ := rfl + +@[simp] +lemma val_add (d₁ d₂ : DownSinglet) : (d₁ + d₂).val = d₁.val + d₂.val := rfl + +@[simp] +lemma val_smul (r : ℂ) (d : DownSinglet) : (r • d).val = r • d.val := rfl + +end DownSinglet + +end StandardModel From 38c7845d21de1d00a1550c4cf8b7321e5d5f2d19 Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 25 Jul 2026 19:24:23 +0400 Subject: [PATCH 2/7] feat(down-singlet): add Lorentz representation Co-authored-by: ChatGPT --- .../StandardModel/Fermions/DownSinglet.lean | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean index e6c6f8743..55639f353 100644 --- a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean +++ b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean @@ -106,6 +106,29 @@ lemma val_add (d₁ d₂ : DownSinglet) : (d₁ + d₂).val = d₁.val + d₂.va @[simp] lemma val_smul (r : ℂ) (d : DownSinglet) : (r • d).val = r • d.val := rfl +/-! + +## C. Lorentz action + +The Lorentz group acts on the right-handed Weyl factor and leaves the colour index fixed. +-/ + +open Matrix MatrixGroups + +open Representation in +/-- The right-handed Lorentz representation on down-type singlet quarks. -/ +noncomputable def repLorentzGroup : Representation ℂ (SL(2,ℂ)) DownSinglet where + toFun Λ := valLinEquiv.symm ∘ₗ + TensorProduct.map (Fermion.RightHandedWeyl.rep Λ) + (trivial ℂ (SL(2,ℂ)) (EuclideanSpace ℂ (Fin 3)) Λ) ∘ₗ + valLinEquiv + map_one' := by + ext d + simp [Module.End.one_eq_id] + map_mul' Λ₁ Λ₂ := by + ext1 d + simp [TensorProduct.map_map, Module.End.mul_eq_comp] + end DownSinglet end StandardModel From 87d372bcbbf653bb812a8d9abb1102602a887999 Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 25 Jul 2026 19:26:11 +0400 Subject: [PATCH 3/7] feat(down-singlet): add gauge representation Co-authored-by: ChatGPT --- .../StandardModel/Fermions/DownSinglet.lean | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean index 55639f353..1f450d597 100644 --- a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean +++ b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean @@ -129,6 +129,40 @@ noncomputable def repLorentzGroup : Representation ℂ (SL(2,ℂ)) DownSinglet w ext1 d simp [TensorProduct.map_map, Module.End.mul_eq_comp] +/-! + +## D. Gauge action + +The `SU(3)` component acts on the colour index, while the `SU(2)` component acts trivially. The +`U(1)` action is `star z ^ 2`; since `z` is unitary, `star z = z⁻¹`, so this represents charge +`-2`. + +The tensor and basis formulas below expose the coefficients used to compare actions and compute the +kernel. +-/ + +/-- The `(3, 1)_{-2}` action of the unquotiented Standard Model gauge group. -/ +noncomputable def repGaugeGroupI : Representation ℂ GaugeGroupI DownSinglet where + toFun g := valLinEquiv.symm ∘ₗ + TensorProduct.map + (LinearMap.id (M := Fermion.RightHandedWeyl)) + g.toSU3.1.toEuclideanLin ∘ₗ + LinearMap.lsmul ℂ _ (star g.toU1.1 ^ 2 : ℂ) ∘ₗ + valLinEquiv + map_one' := by + ext d + simp [valLinEquiv_symm_apply] + map_mul' g₁ g₂ := by + ext d + simp [smul_smul, mul_comm, TensorProduct.map_map, valLinEquiv_symm_apply] + ring_nf + +/-- The gauge action on a pure spinor–colour tensor. -/ +lemma repGaugeGroupI_tmul (g : GaugeGroupI) (ψ : Fermion.RightHandedWeyl) + (v : EuclideanSpace ℂ (Fin 3)) : + repGaugeGroupI g ⟨ψ ⊗ₜ v⟩ = + ⟨(star g.toU1.1 ^ 2) • ψ ⊗ₜ g.toSU3.1.toEuclideanLin v⟩ := rfl + end DownSinglet end StandardModel From 69b0833bd8b2e228777ce5b01cde66b0e93f631a Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 25 Jul 2026 19:36:54 +0400 Subject: [PATCH 4/7] feat(down-singlet): add basis and equality lemmas Co-authored-by: ChatGPT --- .../StandardModel/Fermions/DownSinglet.lean | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean index 1f450d597..66bfe0d7c 100644 --- a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean +++ b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean @@ -163,6 +163,59 @@ lemma repGaugeGroupI_tmul (g : GaugeGroupI) (ψ : Fermion.RightHandedWeyl) repGaugeGroupI g ⟨ψ ⊗ₜ v⟩ = ⟨(star g.toU1.1 ^ 2) • ψ ⊗ₜ g.toSU3.1.toEuclideanLin v⟩ := rfl +open Fermion in +/-- Expands the gauge action in the spinor–colour basis. -/ +lemma repGaugeGroupI_tmul_basis_eq_sum (g : GaugeGroupI) (k : Fin 2) (i : Fin 3) : + repGaugeGroupI g + ⟨RightHandedWeyl.basis k ⊗ₜ[ℂ] EuclideanSpace.basisFun (Fin 3) ℂ i⟩ = + ∑ i' : Fin 3, (star g.toU1.1 ^ 2 * g.toSU3.1 i' i) • + (⟨RightHandedWeyl.basis k ⊗ₜ[ℂ] + EuclideanSpace.basisFun (Fin 3) ℂ i'⟩ : DownSinglet) := by + apply valLinEquiv.injective + apply (((RightHandedWeyl.basis).tensorProduct + (EuclideanSpace.basisFun (Fin 3) ℂ).toBasis)).repr.injective + ext ⟨⟨k, l⟩, m⟩ + simp only [EuclideanSpace.basisFun_apply, repGaugeGroupI_tmul, valLinEquiv_apply, map_smul, + Finsupp.coe_smul, Pi.smul_apply, Module.Basis.tensorProduct_repr_tmul_apply, + OrthonormalBasis.coe_toBasis_repr_apply, EuclideanSpace.basisFun_repr, ofLp_toLpLin, + PiLp.ofLp_single, toLin'_apply, mulVec_single, MulOpposite.op_one, col_apply, one_smul, + Module.Basis.repr_self, smul_eq_mul, map_sum, Finsupp.coe_finsetSum, Finset.sum_apply, + PiLp.single_apply, ite_mul, one_mul, zero_mul, mul_ite, mul_zero, Finset.sum_ite_eq, + Finset.mem_univ, ↓reduceIte] + ring + +open Fermion in +/-- Two gauge elements induce the same action exactly when their hypercharge–colour coefficients +agree. -/ +lemma repGaugeGroupI_eq_iff_mul_eq {g₁ g₂ : GaugeGroupI} : + repGaugeGroupI g₁ = repGaugeGroupI g₂ ↔ ∀ i i', + star g₁.toU1.1 ^ 2 * g₁.toSU3.1 i' i = + star g₂.toU1.1 ^ 2 * g₂.toSU3.1 i' i := by + let b := RightHandedWeyl.basis.tensorProduct + (EuclideanSpace.basisFun (Fin 3) ℂ).toBasis + constructor + · intro h i i' + have h' := congrFun (congrArg (fun f => f.1) h) + ⟨RightHandedWeyl.basis 0 ⊗ₜ[ℂ] EuclideanSpace.basisFun (Fin 3) ℂ i⟩ + simp only [Fin.isValue, LinearMap.coe_toAddHom, repGaugeGroupI_tmul_basis_eq_sum] at h' + replace h' := congrArg b.repr (congrArg valLinEquiv h') + simpa [Module.Basis.tensorProduct_repr_tmul_apply, -Fin.sum_univ_two, b] using + congrArg (fun f => f (0, i')) h' + · intro h + apply (valLinEquiv.symm.eq_comp_toLinearMap_iff + (repGaugeGroupI g₁) (repGaugeGroupI g₂)).mp + apply b.ext + rintro ⟨k, i⟩ + have h₁ := repGaugeGroupI_tmul_basis_eq_sum g₁ k i + have h₂ := repGaugeGroupI_tmul_basis_eq_sum g₂ k i + simp only [EuclideanSpace.basisFun_apply] at h₁ h₂ + simp [valLinEquiv_symm_apply, h₁, h₂, b] + apply Finset.sum_congr rfl + intro i' _ + have hi' : (starRingEnd ℂ) g₁.toU1.1 ^ 2 * g₁.toSU3.1 i' i = + (starRingEnd ℂ) g₂.toU1.1 ^ 2 * g₂.toSU3.1 i' i := h i i' + rw [hi'] + end DownSinglet end StandardModel From a488d7fe33b6d2b2be6aab46da5ca72087bc937c Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 25 Jul 2026 19:40:37 +0400 Subject: [PATCH 5/7] feat(down-singlet): characterize the gauge kernel Co-authored-by: ChatGPT --- .../StandardModel/Fermions/DownSinglet.lean | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean index 66bfe0d7c..f5d9957dc 100644 --- a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean +++ b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean @@ -216,6 +216,41 @@ lemma repGaugeGroupI_eq_iff_mul_eq {g₁ g₂ : GaugeGroupI} : (starRingEnd ℂ) g₂.toU1.1 ^ 2 * g₂.toSU3.1 i' i := h i i' rw [hi'] +/-! + +## E. Kernel of the gauge action + +An element acts trivially when its colour action is scalar and that scalar cancels its `U(1)` +phase. Its weak component is unrestricted because the down-type singlet is an `SU(2)` singlet. +-/ + +/-- Characterizes the full-group elements acting trivially on the down-type singlet. -/ +lemma mem_repGaugeGroupI_ker_iff_eq {g : GaugeGroupI} : + g ∈ repGaugeGroupI.ker ↔ ∃ a : ℂ, + g.toSU3.1 = a • 1 ∧ a * star g.toU1.1 ^ 2 = 1 := by + rw [MonoidHom.mem_ker, ← MonoidHom.map_one repGaugeGroupI, repGaugeGroupI_eq_iff_mul_eq] + constructor + · intro h + have hc : star g.toU1.1 ^ 2 ≠ 0 := by + apply pow_ne_zero + rw [star_ne_zero] + intro hzero + have hu := Unitary.star_mul_self_of_mem g.toU1.2 + simp [hzero] at hu + use g.toSU3.1 0 0 + simp only [map_one, OneMemClass.coe_one, Fin.forall_fin_succ, Fin.isValue, + Fin.succ_zero_eq_one, IsEmpty.forall_iff, and_true, one_apply_eq, ne_eq, + one_ne_zero, not_false_eq_true, one_apply_ne, mul_eq_zero, zero_ne_one, + Fin.succ_one_eq_two, Fin.reduceEq, star_one, one_pow, one_mul] at h + refine ⟨?_, ?_⟩ + · ext i j + fin_cases i <;> fin_cases j <;> simp <;> grind + · grind + · rintro ⟨a, h₁, h₂⟩ i i' + simp only [Matrix.smul_apply, smul_eq_mul, h₁, map_one, OneMemClass.coe_one, + star_one, one_pow, one_mul] + linear_combination h₂ * (1 : Matrix _ _ ℂ) i' i + end DownSinglet end StandardModel From 179068d5fc0717f8dd7bb5ad238f376c5001fd74 Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 25 Jul 2026 19:42:28 +0400 Subject: [PATCH 6/7] feat(down-singlet): descend the representation to gauge quotients Co-authored-by: ChatGPT --- .../StandardModel/Fermions/DownSinglet.lean | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean index f5d9957dc..246f2ed65 100644 --- a/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean +++ b/Physlib/Particles/StandardModel/Fermions/DownSinglet.lean @@ -251,6 +251,42 @@ lemma mem_repGaugeGroupI_ker_iff_eq {g : GaugeGroupI} : star_one, one_pow, one_mul] linear_combination h₂ * (1 : Matrix _ _ ℂ) i' i +/-! + +## F. Descent to quotient gauge groups + +A representation descends through a quotient when the quotient subgroup lies in its kernel. For +the central `ℤ₆`, the colour phase is `x²` while the charge `-2` phase is `(star x)² = x⁻²`, so +their product is one. +-/ + +/-- The central `ℤ₆` subgroup acts trivially on `(3, 1)_{-2}`. -/ +lemma gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI : + GaugeGroupQuot.subgroup .ℤ₆ ≤ repGaugeGroupI.ker := by + simp only [GaugeGroupQuot.subgroup, gaugeGroupℤ₆SubGroup, SetLike.le_def, + MonoidHom.mem_range, gaugeGroupℤ₆Hom_apply, Subtype.exists, + mem_repGaugeGroupI_ker_iff_eq, forall_exists_index] + rintro g x hx ⟨rfl⟩ + use x ^ 2 + simp only [gaugeGroupℤ₆OfRoot_toSU3, gaugeGroupℤ₆SU3OfRoot_eq_mul_id, + gaugeGroupℤ₆OfRoot_toU1, gaugeGroupℤ₆UnitaryOfRoot_coe, true_and, RCLike.star_def, + Complex.conj_rootsOfUnity hx, Units.val_inv_eq_inv_val, inv_pow] + field_simp + +/-- Every supported quotient subgroup acts trivially on the down-type singlet. -/ +lemma gaugeGroup_subgroup_le_ker_repGaugeGroupI (Q : GaugeGroupQuot) : + Q.subgroup ≤ repGaugeGroupI.ker := Q.subgroup_le_subgroup_ℤ₆.trans + gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI + +/-- The `(3, 1)_{-2}` representation for every supported global form of the +Standard Model gauge group. -/ +noncomputable def repGaugeGroup : (Q : GaugeGroupQuot) → + Representation ℂ (GaugeGroup Q) DownSinglet + | .I => repGaugeGroupI + | .ℤ₆ => QuotientGroup.lift _ repGaugeGroupI (gaugeGroup_subgroup_le_ker_repGaugeGroupI .ℤ₆) + | .ℤ₂ => QuotientGroup.lift _ repGaugeGroupI (gaugeGroup_subgroup_le_ker_repGaugeGroupI .ℤ₂) + | .ℤ₃ => QuotientGroup.lift _ repGaugeGroupI (gaugeGroup_subgroup_le_ker_repGaugeGroupI .ℤ₃) + end DownSinglet end StandardModel From 3043e23d497d1ae0f0c175db552046bf3d9cad8f Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 25 Jul 2026 19:44:11 +0400 Subject: [PATCH 7/7] feat(down-singlet): register the module Co-authored-by: ChatGPT --- Physlib.lean | 1 + Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib.lean b/Physlib.lean index a0450d782..085779556 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -188,6 +188,7 @@ public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lem public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.LinearParameterization public import Physlib.Particles.StandardModel.AnomalyCancellation.Permutations public import Physlib.Particles.StandardModel.Basic +public import Physlib.Particles.StandardModel.Fermions.DownSinglet public import Physlib.Particles.StandardModel.Fermions.QuarkDoublet public import Physlib.Particles.StandardModel.Fermions.UpSinglet public import Physlib.Particles.StandardModel.HiggsBoson.Basic diff --git a/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean b/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean index 9ea6f7f1d..5445e8cfc 100644 --- a/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean +++ b/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean @@ -29,7 +29,6 @@ open TensorProduct TODO "Add other fermions similar to this file with the names: - UpSinglet (3, 1)_{4} (right-handed) - - DownSinglet (3, 1)_{-2} (right-handed) - LeptonDoublet (1, 2)_{-3} (left-handed) - LeptonSinglet (1, 1)_{-6} (right-handed)"