feat: Add down singlets

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

Physlib/Particles/StandardModel/Fermions/DownSinglet.lean

@@ -0,0 +1,292 @@
+/-
+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
+
+/-!
+
+## 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]
+
+/-!
+
+## 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
+
+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']
+
+/-!
+
+## 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
+
+/-!
+
+## 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

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)"