Physlib.Particles.StandardModel.Representations

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Analysis.Complex.Basic
public import Mathlib.LinearAlgebra.UnitaryGroup
public import Physlib.Meta.TODO.Basic

Representations appearing in the Standard Model

This file defines the basic representations which appear in the Standard Model.

@[expose] public section

The 2d representation of U(1) with charge 3 as a map from U(1) to unitaryGroup (Fin 2) ℂ.


@[simps!]
noncomputable def repU1Map (g : unitary ℂ) : unitaryGroup (Fin 2) ℂ :=
  ⟨g ^ 3 • 1, byg:↥(unitary ℂ)⊢ g ^ 3 • 1 ∈ unitaryGroup (Fin 2) ℂ
    rw [mem_unitaryGroup_iff,g:↥(unitary ℂ)⊢ g ^ 3 • 1 * star (g ^ 3 • 1) = 1g:↥(unitary ℂ)⊢ ⟨↑g, ⋯⟩ ^ 3 • star (⟨↑g, ⋯⟩ ^ 3 • 1) = 1 smul_one_mul,g:↥(unitary ℂ)⊢ g ^ 3 • star (g ^ 3 • 1) = 1g:↥(unitary ℂ)⊢ ⟨↑g, ⋯⟩ ^ 3 • star (⟨↑g, ⋯⟩ ^ 3 • 1) = 1 show g = ⟨g.1, g.prop⟩ from rflg:↥(unitary ℂ)⊢ ⟨↑g, ⋯⟩ ^ 3 • star (⟨↑g, ⋯⟩ ^ 3 • 1) = 1g:↥(unitary ℂ)⊢ ⟨↑g, ⋯⟩ ^ 3 • star (⟨↑g, ⋯⟩ ^ 3 • 1) = 1]g:↥(unitary ℂ)⊢ ⟨↑g, ⋯⟩ ^ 3 • star (⟨↑g, ⋯⟩ ^ 3 • 1) = 1
    simp only [SubmonoidClass.mk_pow, Submonoid.mk_smul, star_smul, star_pow, RCLike.star_def,
      star_one]g:↥(unitary ℂ)⊢ ↑g ^ 3 • (starRingEnd ℂ) ↑g ^ 3 • 1 = 1
    rw [smul_smul,g:↥(unitary ℂ)⊢ (↑g ^ 3 * (starRingEnd ℂ) ↑g ^ 3) • 1 = 1g:↥(unitary ℂ)⊢ (↑g * (starRingEnd ℂ) ↑g) ^ 3 • 1 = 1 ← mul_powg:↥(unitary ℂ)⊢ (↑g * (starRingEnd ℂ) ↑g) ^ 3 • 1 = 1g:↥(unitary ℂ)⊢ (↑g * (starRingEnd ℂ) ↑g) ^ 3 • 1 = 1]g:↥(unitary ℂ)⊢ (↑g * (starRingEnd ℂ) ↑g) ^ 3 • 1 = 1
    rw [← star_def,g:↥(unitary ℂ)⊢ (↑g * star ↑g) ^ 3 • 1 = 1g:↥(unitary ℂ)⊢ 1 ^ 3 • 1 = 1 (Unitary.mem_iff.mp g.prop).2g:↥(unitary ℂ)⊢ 1 ^ 3 • 1 = 1g:↥(unitary ℂ)⊢ 1 ^ 3 • 1 = 1]g:↥(unitary ℂ)⊢ 1 ^ 3 • 1 = 1
    simp only [one_pow, one_smul]All goals completed! 🐙⟩

The 2d representation of U(1) with charge 3 as a homomorphism from U(1) to unitaryGroup (Fin 2) ℂ.

@[simps!]
noncomputable def repU1 : unitary ℂ →* unitaryGroup (Fin 2) ℂ where
  toFun g := repU1Map g
  map_mul' g h := byg:↥(unitary ℂ)h:↥(unitary ℂ)⊢ repU1Map (g * h) = repU1Map g * repU1Map h
    simp only [repU1Map, Submonoid.mk_mul_mk, mul_smul_one, smul_smul, mul_comm, ← mul_pow]All goals completed! 🐙
  map_one' := by⊢ repU1Map 1 = 1
    simp only [repU1Map, one_pow, one_smul, Submonoid.mk_eq_one]All goals completed! 🐙

The fundamental representation of SU(2) as a homomorphism to unitaryGroup (Fin 2) ℂ.

@[simps!]
def fundamentalSU2 : specialUnitaryGroup (Fin 2) ℂ →* unitaryGroup (Fin 2) ℂ where
  toFun g := ⟨g.1, g.prop.1⟩
  map_mul' _ _ := Subtype.ext rfl
  map_one' := Subtype.ext rfl

lemma repU1_fundamentalSU2_commute (u1 : unitary ℂ) (g : specialUnitaryGroup (Fin 2) ℂ) :
    repU1 u1 * fundamentalSU2 g = fundamentalSU2 g * repU1 u1 := byu1:↥(unitary ℂ)g:↥(specialUnitaryGroup (Fin 2) ℂ)⊢ repU1 u1 * fundamentalSU2 g = fundamentalSU2 g * repU1 u1
  apply Subtype.extu1:↥(unitary ℂ)g:↥(specialUnitaryGroup (Fin 2) ℂ)⊢ ↑(repU1 u1 * fundamentalSU2 g) = ↑(fundamentalSU2 g * repU1 u1)
  simpAll goals completed! 🐙

TODO "Define a structure capturing the fermionic content of the Standard Model, with all fermions
  expressed as left-handed Weyl fermions (`Fermion.LeftHandedWeyl`) and including all three
  families. The structure should carry a `Module ℂ` instance together with a representation of the
  Lorentz group and a representation of the global gauge group `GaugeGroupI` (built from `repU1`
  and `fundamentalSU2`)."