Physlib.Particles.StandardModel.Basic

Imports

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

public import Physlib.SpaceAndTime.SpaceTime.Basic
public import Physlib.Meta.Linters.Sorry
public import Mathlib.RingTheory.RootsOfUnity.Complex

The Standard Model

This file defines the basic properties of the standard model in particle physics.

@[expose] public section

The unquotiented gauge group

The global gauge group of the Standard Model with no discrete quotients. The I in the Name is an indication of the statement that this has no discrete quotients.

abbrev GaugeGroupI : Type :=
  specialUnitaryGroup (Fin 3) ℂ × specialUnitaryGroup (Fin 2) ℂ × unitary ℂ

The underlying element of SU(3) of an element in GaugeGroupI.

def toSU3 : GaugeGroupI →* specialUnitaryGroup (Fin 3) ℂ where
  toFun g := g.1
  map_one' := rfl
  map_mul' _ _ := rfl

The underlying element of SU(2) of an element in GaugeGroupI.

def toSU2 : GaugeGroupI →* specialUnitaryGroup (Fin 2) ℂ where
  toFun g := g.2.1
  map_one' := rfl
  map_mul' _ _ := rfl

The underlying element of U(1) of an element in GaugeGroupI.

def toU1 : GaugeGroupI →* unitary ℂ where
  toFun g := g.2.2
  map_one' := rfl
  map_mul' _ _ := rfl

              @[ext]
lemma ext {g g' : GaugeGroupI} (hSU3 : toSU3 g = toSU3 g')
    (hSU2 : toSU2 g = toSU2 g') (hU1 : toU1 g = toU1 g') : g = g' :=
  Prod.ext hSU3 (Prod.ext hSU2 hU1)instance : Star GaugeGroupI where
  star g := (star g.1, star g.2.1, star g.2.2)lemma star_eq (g : GaugeGroupI) : star g = (star g.1, star g.2.1, star g.2.2) := rfl@[simp]
lemma star_toSU3 (g : GaugeGroupI) : toSU3 (star g) = star (toSU3 g) := rfl@[simp]
lemma star_toSU2 (g : GaugeGroupI) : toSU2 (star g) = star (toSU2 g) := rfl@[simp]
lemma star_toU1 (g : GaugeGroupI) : toU1 (star g) = star (toU1 g) := rflinstance : InvolutiveStar GaugeGroupI where
  star_involutive g := byg:GaugeGroupI⊢ star (star g) = g
    ext1hSU3g:GaugeGroupI⊢ toSU3 (star (star g)) = toSU3 ghSU2g:GaugeGroupI⊢ toSU2 (star (star g)) = toSU2 ghU1g:GaugeGroupI⊢ toU1 (star (star g)) = toU1 g <;>hSU3g:GaugeGroupI⊢ toSU3 (star (star g)) = toSU3 ghSU2g:GaugeGroupI⊢ toSU2 (star (star g)) = toSU2 ghU1g:GaugeGroupI⊢ toU1 (star (star g)) = toU1 g simpAll goals completed! 🐙@[simp]
lemma ofU1Subgroup_toSU3 (u1 : unitary ℂ) :
    toSU3 (ofU1Subgroup u1) = 1 := rfl

@[simp]
lemma ofU1Subgroup_toSU2 (u1 : unitary ℂ) :
    toSU2 (ofU1Subgroup u1) = ⟨!![star (u1 ^ 3 : unitary ℂ), 0;0, (u1 ^ 3 : unitary ℂ)], byu1:↥(unitary ℂ)⊢ !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ∈ ↑(unitaryGroup (Fin 2) ℂ)
    simp only [SetLike.mem_coe]u1:↥(unitary ℂ)⊢ !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ∈ unitaryGroup (Fin 2) ℂ
    rw [mem_unitaryGroup_iff'u1:↥(unitary ℂ)⊢ star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] = 1u1:↥(unitary ℂ)⊢ star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] = 1]u1:↥(unitary ℂ)⊢ star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] = 1
    funext i ju1:↥(unitary ℂ)i:Fin 2j:Fin 2⊢ (star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)]) i j = 1 i j
    rw [Matrix.mul_applyu1:↥(unitary ℂ)i:Fin 2j:Fin 2⊢ ∑ j_1, star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] i j_1 * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j_1 j = 1 i ju1:↥(unitary ℂ)i:Fin 2j:Fin 2⊢ ∑ j_1, star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] i j_1 * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j_1 j = 1 i j]u1:↥(unitary ℂ)i:Fin 2j:Fin 2⊢ ∑ j_1, star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] i j_1 * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j_1 j = 1 i j
    fin_cases i«0»u1:↥(unitary ℂ)j:Fin 2⊢ ∑ j_1, star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨0, ⋯⟩) j_1 * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j_1 j =
  1 ((fun i => i) ⟨0, ⋯⟩) j«1»u1:↥(unitary ℂ)j:Fin 2⊢ ∑ j_1, star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨1, ⋯⟩) j_1 * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j_1 j =
  1 ((fun i => i) ⟨1, ⋯⟩) j <;>«0»u1:↥(unitary ℂ)j:Fin 2⊢ ∑ j_1, star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨0, ⋯⟩) j_1 * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j_1 j =
  1 ((fun i => i) ⟨0, ⋯⟩) j«1»u1:↥(unitary ℂ)j:Fin 2⊢ ∑ j_1, star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨1, ⋯⟩) j_1 * !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j_1 j =
  1 ((fun i => i) ⟨1, ⋯⟩) j fin_cases j«1».«0»u1:↥(unitary ℂ)⊢ ∑ j,
    star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨1, ⋯⟩) j *
      !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j ((fun i => i) ⟨0, ⋯⟩) =
  1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»u1:↥(unitary ℂ)⊢ ∑ j,
    star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨1, ⋯⟩) j *
      !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j ((fun i => i) ⟨1, ⋯⟩) =
  1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) <;>«0».«0»u1:↥(unitary ℂ)⊢ ∑ j,
    star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨0, ⋯⟩) j *
      !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j ((fun i => i) ⟨0, ⋯⟩) =
  1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1»u1:↥(unitary ℂ)⊢ ∑ j,
    star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨0, ⋯⟩) j *
      !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j ((fun i => i) ⟨1, ⋯⟩) =
  1 ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«1».«0»u1:↥(unitary ℂ)⊢ ∑ j,
    star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨1, ⋯⟩) j *
      !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j ((fun i => i) ⟨0, ⋯⟩) =
  1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»u1:↥(unitary ℂ)⊢ ∑ j,
    star !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ((fun i => i) ⟨1, ⋯⟩) j *
      !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] j ((fun i => i) ⟨1, ⋯⟩) =
  1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) simp [conj_mul']All goals completed! 🐙, byu1:↥(unitary ℂ)⊢ !![star ↑(u1 ^ 3), 0; 0, ↑(u1 ^ 3)] ∈ ↑(MonoidHom.mker detMonoidHom)
    simp only [RCLike.star_def, SetLike.mem_coe, MonoidHom.mem_mker, coe_detMonoidHom,
      det_fin_two_of, conj_mul', mul_zero, sub_zero]u1:↥(unitary ℂ)⊢ ↑‖↑(u1 ^ 3)‖ ^ 2 = 1
    simpAll goals completed! 🐙⟩ := rfl@[simp]
lemma ofU1Subgroup_toU1 (u1 : unitary ℂ) :
    toU1 (ofU1Subgroup u1) = u1 := rfl

The ℤ₆ quotient

              @[simp]
lemma gaugeGroupℤ₆UnitaryOfRoot_coe (α : rootsOfUnity 6 ℂ) :
    (gaugeGroupℤ₆UnitaryOfRoot α : ℂ) = ((α : ℂˣ) : ℂ) := rfllemma gaugeGroupℤ₆SU3OfRoot_eq_mul_id (α : rootsOfUnity 6 ℂ) :
    (gaugeGroupℤ₆SU3OfRoot α).1 = ((α : ℂˣ) : ℂ) ^ 2 • 1 := byα:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) = ↑↑α ^ 2 • 1
  ext i jα:↥(rootsOfUnity 6 ℂ)i:Fin 3j:Fin 3⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) i j = (↑↑α ^ 2 • 1) i j
  fin_cases i«0»α:↥(rootsOfUnity 6 ℂ)j:Fin 3⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨0, ⋯⟩) j = (↑↑α ^ 2 • 1) ((fun i => i) ⟨0, ⋯⟩) j«1»α:↥(rootsOfUnity 6 ℂ)j:Fin 3⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨1, ⋯⟩) j = (↑↑α ^ 2 • 1) ((fun i => i) ⟨1, ⋯⟩) j«2»α:↥(rootsOfUnity 6 ℂ)j:Fin 3⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) j = (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) j <;>«0»α:↥(rootsOfUnity 6 ℂ)j:Fin 3⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨0, ⋯⟩) j = (↑↑α ^ 2 • 1) ((fun i => i) ⟨0, ⋯⟩) j«1»α:↥(rootsOfUnity 6 ℂ)j:Fin 3⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨1, ⋯⟩) j = (↑↑α ^ 2 • 1) ((fun i => i) ⟨1, ⋯⟩) j«2»α:↥(rootsOfUnity 6 ℂ)j:Fin 3⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) j = (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) j fin_cases j«2».«0»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) <;>«0».«0»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«0».«2»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«1».«0»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«1».«2»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)«2».«0»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«2».«1»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«2».«2»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU3OfRoot α) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) =
  (↑↑α ^ 2 • 1) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) simp [gaugeGroupℤ₆SU3OfRoot]All goals completed! 🐙lemma gaugeGroupℤ₆SU3OfRoot_toEuclideanLin_apply (α : rootsOfUnity 6 ℂ)
    (v : EuclideanSpace ℂ (Fin 3)) :
    (gaugeGroupℤ₆SU3OfRoot α).1.toEuclideanLin v = ((α : ℂˣ) : ℂ) ^ 2 • v := byα:↥(rootsOfUnity 6 ℂ)v:EuclideanSpace ℂ (Fin 3)⊢ (toEuclideanLin ↑(gaugeGroupℤ₆SU3OfRoot α)) v = ↑↑α ^ 2 • v
  simp [gaugeGroupℤ₆SU3OfRoot, Matrix.scalar_apply, toLpLin_apply]All goals completed! 🐙lemma gaugeGroupℤ₆SU2OfRoot_eq_mul_id (α : rootsOfUnity 6 ℂ) :
    (gaugeGroupℤ₆SU2OfRoot α).1 = star ((α : ℂˣ) : ℂ) ^ 3 • 1 := byα:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) = star ↑↑α ^ 3 • 1
  ext i jα:↥(rootsOfUnity 6 ℂ)i:Fin 2j:Fin 2⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) i j = (star ↑↑α ^ 3 • 1) i j
  fin_cases i«0»α:↥(rootsOfUnity 6 ℂ)j:Fin 2⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨0, ⋯⟩) j = (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨0, ⋯⟩) j«1»α:↥(rootsOfUnity 6 ℂ)j:Fin 2⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨1, ⋯⟩) j = (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨1, ⋯⟩) j <;>«0»α:↥(rootsOfUnity 6 ℂ)j:Fin 2⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨0, ⋯⟩) j = (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨0, ⋯⟩) j«1»α:↥(rootsOfUnity 6 ℂ)j:Fin 2⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨1, ⋯⟩) j = (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨1, ⋯⟩) j fin_cases j«1».«0»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) <;>«0».«0»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)«1».«0»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) =
  (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«1».«1»α:↥(rootsOfUnity 6 ℂ)⊢ ↑(gaugeGroupℤ₆SU2OfRoot α) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) =
  (star ↑↑α ^ 3 • 1) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) simp [gaugeGroupℤ₆SU2OfRoot]All goals completed! 🐙lemma gaugeGroupℤ₆SU2OfRoot_toEuclideanLin_apply (α : rootsOfUnity 6 ℂ)
    (v : EuclideanSpace ℂ (Fin 2)) :
    (gaugeGroupℤ₆SU2OfRoot α).1.toEuclideanLin v = star ((α : ℂˣ) : ℂ) ^ 3 • v := byα:↥(rootsOfUnity 6 ℂ)v:EuclideanSpace ℂ (Fin 2)⊢ (toEuclideanLin ↑(gaugeGroupℤ₆SU2OfRoot α)) v = star ↑↑α ^ 3 • v
  simp [gaugeGroupℤ₆SU2OfRoot, Matrix.scalar_apply, toLpLin_apply]All goals completed! 🐙@[simp]
lemma gaugeGroupℤ₆OfRoot_toSU3 (α : rootsOfUnity 6 ℂ) :
    GaugeGroupI.toSU3 (gaugeGroupℤ₆OfRoot α) = gaugeGroupℤ₆SU3OfRoot α := rfl@[simp]
lemma gaugeGroupℤ₆OfRoot_toSU2 (α : rootsOfUnity 6 ℂ) :
    GaugeGroupI.toSU2 (gaugeGroupℤ₆OfRoot α) = gaugeGroupℤ₆SU2OfRoot α := rfl@[simp]
lemma gaugeGroupℤ₆OfRoot_toU1 (α : rootsOfUnity 6 ℂ) :
    GaugeGroupI.toU1 (gaugeGroupℤ₆OfRoot α) = gaugeGroupℤ₆UnitaryOfRoot α := rfl

lemma gaugeGroupℤ₆OfRoot_mem_center (α : rootsOfUnity 6 ℂ) :
    gaugeGroupℤ₆OfRoot α ∈ Subgroup.center GaugeGroupI := byα:↥(rootsOfUnity 6 ℂ)⊢ gaugeGroupℤ₆OfRoot α ∈ Subgroup.center GaugeGroupI
  rw [Subgroup.mem_center_iffα:↥(rootsOfUnity 6 ℂ)⊢ ∀ (g : GaugeGroupI), g * gaugeGroupℤ₆OfRoot α = gaugeGroupℤ₆OfRoot α * gα:↥(rootsOfUnity 6 ℂ)⊢ ∀ (g : GaugeGroupI), g * gaugeGroupℤ₆OfRoot α = gaugeGroupℤ₆OfRoot α * g]α:↥(rootsOfUnity 6 ℂ)⊢ ∀ (g : GaugeGroupI), g * gaugeGroupℤ₆OfRoot α = gaugeGroupℤ₆OfRoot α * g
  intro gα:↥(rootsOfUnity 6 ℂ)g:GaugeGroupI⊢ g * gaugeGroupℤ₆OfRoot α = gaugeGroupℤ₆OfRoot α * g
  refine GaugeGroupI.ext ?_ ?_ (mul_comm _ _)refine_1α:↥(rootsOfUnity 6 ℂ)g:GaugeGroupI⊢ GaugeGroupI.toSU3 (g * gaugeGroupℤ₆OfRoot α) = GaugeGroupI.toSU3 (gaugeGroupℤ₆OfRoot α * g)refine_2α:↥(rootsOfUnity 6 ℂ)g:GaugeGroupI⊢ GaugeGroupI.toSU2 (g * gaugeGroupℤ₆OfRoot α) = GaugeGroupI.toSU2 (gaugeGroupℤ₆OfRoot α * g) <;>refine_1α:↥(rootsOfUnity 6 ℂ)g:GaugeGroupI⊢ GaugeGroupI.toSU3 (g * gaugeGroupℤ₆OfRoot α) = GaugeGroupI.toSU3 (gaugeGroupℤ₆OfRoot α * g)refine_2α:↥(rootsOfUnity 6 ℂ)g:GaugeGroupI⊢ GaugeGroupI.toSU2 (g * gaugeGroupℤ₆OfRoot α) = GaugeGroupI.toSU2 (gaugeGroupℤ₆OfRoot α * g) ext i jrefine_2α:↥(rootsOfUnity 6 ℂ)g:GaugeGroupIi:Fin 2j:Fin 2⊢ ↑(GaugeGroupI.toSU2 (g * gaugeGroupℤ₆OfRoot α)) i j = ↑(GaugeGroupI.toSU2 (gaugeGroupℤ₆OfRoot α * g)) i j <;>refine_1α:↥(rootsOfUnity 6 ℂ)g:GaugeGroupIi:Fin 3j:Fin 3⊢ ↑(GaugeGroupI.toSU3 (g * gaugeGroupℤ₆OfRoot α)) i j = ↑(GaugeGroupI.toSU3 (gaugeGroupℤ₆OfRoot α * g)) i jrefine_2α:↥(rootsOfUnity 6 ℂ)g:GaugeGroupIi:Fin 2j:Fin 2⊢ ↑(GaugeGroupI.toSU2 (g * gaugeGroupℤ₆OfRoot α)) i j = ↑(GaugeGroupI.toSU2 (gaugeGroupℤ₆OfRoot α * g)) i j
    simp [map_mul, gaugeGroupℤ₆SU3OfRoot, gaugeGroupℤ₆SU2OfRoot, Matrix.scalar_apply, mul_comm]All goals completed! 🐙@[simp]
lemma gaugeGroupℤ₆Hom_apply (α : rootsOfUnity 6 ℂ) :
    gaugeGroupℤ₆Hom α = gaugeGroupℤ₆OfRoot α := rfl@[simp]
lemma gaugeGroupℤ₆Hom_toSU3 (α : rootsOfUnity 6 ℂ) :
    GaugeGroupI.toSU3 (gaugeGroupℤ₆Hom α) = gaugeGroupℤ₆SU3OfRoot α := rfl@[simp]
lemma gaugeGroupℤ₆Hom_toSU2 (α : rootsOfUnity 6 ℂ) :
    GaugeGroupI.toSU2 (gaugeGroupℤ₆Hom α) = gaugeGroupℤ₆SU2OfRoot α := rfl@[simp]
lemma gaugeGroupℤ₆Hom_toU1 (α : rootsOfUnity 6 ℂ) :
    GaugeGroupI.toU1 (gaugeGroupℤ₆Hom α) = gaugeGroupℤ₆UnitaryOfRoot α := rfllemma gaugeGroupℤ₆OfRoot_mem (α : rootsOfUnity 6 ℂ) :
    gaugeGroupℤ₆OfRoot α ∈ gaugeGroupℤ₆SubGroup :=
  ⟨α, rfl⟩lemma mem_gaugeGroupℤ₆SubGroup_iff (g : GaugeGroupI) :
    g ∈ gaugeGroupℤ₆SubGroup ↔ ∃ α : rootsOfUnity 6 ℂ, gaugeGroupℤ₆OfRoot α = g := byg:GaugeGroupI⊢ g ∈ gaugeGroupℤ₆SubGroup ↔ ∃ α, gaugeGroupℤ₆OfRoot α = g
  simp [gaugeGroupℤ₆SubGroup]All goals completed! 🐙lemma gaugeGroupℤ₆SubGroup_le_center :
    gaugeGroupℤ₆SubGroup ≤ Subgroup.center GaugeGroupI := by⊢ gaugeGroupℤ₆SubGroup ≤ Subgroup.center GaugeGroupI
  rintro g ⟨α, rfl⟩α:↥(rootsOfUnity 6 ℂ)⊢ gaugeGroupℤ₆Hom α ∈ Subgroup.center GaugeGroupI
  exact gaugeGroupℤ₆OfRoot_mem_center αAll goals completed! 🐙instance gaugeGroupℤ₆SubGroup_normal : gaugeGroupℤ₆SubGroup.Normal where
  conj_mem n hn g := byn:GaugeGroupIhn:n ∈ gaugeGroupℤ₆SubGroupg:GaugeGroupI⊢ g * n * g⁻¹ ∈ gaugeGroupℤ₆SubGroup
    rwa [Subgroup.mem_center_iff.mp (gaugeGroupℤ₆SubGroup_le_center hn) g,n:GaugeGroupIhn:n ∈ gaugeGroupℤ₆SubGroupg:GaugeGroupI⊢ n * g * g⁻¹ ∈ gaugeGroupℤ₆SubGroup
      mul_inv_cancel_rightn:GaugeGroupIhn:n ∈ gaugeGroupℤ₆SubGroupg:GaugeGroupI⊢ n ∈ gaugeGroupℤ₆SubGroup]n:GaugeGroupIhn:n ∈ gaugeGroupℤ₆SubGroupg:GaugeGroupI⊢ n ∈ gaugeGroupℤ₆SubGroup

The smallest possible gauge group of the Standard Model, i.e., the quotient of GaugeGroupI by the ℤ₆-subgroup gaugeGroupℤ₆SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

def GaugeGroupℤ₆ : Type :=
  GaugeGroupI ⧸ gaugeGroupℤ₆SubGroup

@[simp]
lemma mk_gaugeGroupℤ₆OfRoot (α : rootsOfUnity 6 ℂ) :
    mk (gaugeGroupℤ₆OfRoot α) = 1 :=
  (QuotientGroup.eq_one_iff _).mpr (gaugeGroupℤ₆OfRoot_mem α)

The ℤ₂ quotient

              @[simp]
lemma gaugeGroupℤ₂OfRoot_toSU3 (α : rootsOfUnity 2 ℂ) :
    GaugeGroupI.toSU3 (gaugeGroupℤ₂OfRoot α) =
      gaugeGroupℤ₆SU3OfRoot (gaugeGroupℤ₂RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₂OfRoot_toSU2 (α : rootsOfUnity 2 ℂ) :
    GaugeGroupI.toSU2 (gaugeGroupℤ₂OfRoot α) =
      gaugeGroupℤ₆SU2OfRoot (gaugeGroupℤ₂RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₂OfRoot_toU1 (α : rootsOfUnity 2 ℂ) :
    GaugeGroupI.toU1 (gaugeGroupℤ₂OfRoot α) =
      gaugeGroupℤ₆UnitaryOfRoot (gaugeGroupℤ₂RootToℤ₆Root α) := rfllemma gaugeGroupℤ₂OfRoot_mem_center (α : rootsOfUnity 2 ℂ) :
    gaugeGroupℤ₂OfRoot α ∈ Subgroup.center GaugeGroupI :=
  gaugeGroupℤ₆OfRoot_mem_center (gaugeGroupℤ₂RootToℤ₆Root α)@[simp]
lemma gaugeGroupℤ₂Hom_apply (α : rootsOfUnity 2 ℂ) :
    gaugeGroupℤ₂Hom α = gaugeGroupℤ₂OfRoot α := rfl@[simp]
lemma gaugeGroupℤ₂Hom_toSU3 (α : rootsOfUnity 2 ℂ) :
    GaugeGroupI.toSU3 (gaugeGroupℤ₂Hom α) =
      gaugeGroupℤ₆SU3OfRoot (gaugeGroupℤ₂RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₂Hom_toSU2 (α : rootsOfUnity 2 ℂ) :
    GaugeGroupI.toSU2 (gaugeGroupℤ₂Hom α) =
      gaugeGroupℤ₆SU2OfRoot (gaugeGroupℤ₂RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₂Hom_toU1 (α : rootsOfUnity 2 ℂ) :
    GaugeGroupI.toU1 (gaugeGroupℤ₂Hom α) =
      gaugeGroupℤ₆UnitaryOfRoot (gaugeGroupℤ₂RootToℤ₆Root α) := rfllemma gaugeGroupℤ₂OfRoot_mem (α : rootsOfUnity 2 ℂ) :
    gaugeGroupℤ₂OfRoot α ∈ gaugeGroupℤ₂SubGroup :=
  ⟨α, rfl⟩lemma mem_gaugeGroupℤ₂SubGroup_iff (g : GaugeGroupI) :
    g ∈ gaugeGroupℤ₂SubGroup ↔ ∃ α : rootsOfUnity 2 ℂ, gaugeGroupℤ₂OfRoot α = g := byg:GaugeGroupI⊢ g ∈ gaugeGroupℤ₂SubGroup ↔ ∃ α, gaugeGroupℤ₂OfRoot α = g
  simp [gaugeGroupℤ₂SubGroup]All goals completed! 🐙lemma gaugeGroupℤ₂SubGroup_le_gaugeGroupℤ₆SubGroup :
    gaugeGroupℤ₂SubGroup ≤ gaugeGroupℤ₆SubGroup := by⊢ gaugeGroupℤ₂SubGroup ≤ gaugeGroupℤ₆SubGroup
  rintro g ⟨α, rfl⟩α:↥(rootsOfUnity 2 ℂ)⊢ gaugeGroupℤ₂Hom α ∈ gaugeGroupℤ₆SubGroup
  exact gaugeGroupℤ₆OfRoot_mem (gaugeGroupℤ₂RootToℤ₆Root α)All goals completed! 🐙lemma gaugeGroupℤ₂SubGroup_le_center :
    gaugeGroupℤ₂SubGroup ≤ Subgroup.center GaugeGroupI :=
  gaugeGroupℤ₂SubGroup_le_gaugeGroupℤ₆SubGroup.trans gaugeGroupℤ₆SubGroup_le_centerinstance gaugeGroupℤ₂SubGroup_normal : gaugeGroupℤ₂SubGroup.Normal where
  conj_mem n hn g := byn:GaugeGroupIhn:n ∈ gaugeGroupℤ₂SubGroupg:GaugeGroupI⊢ g * n * g⁻¹ ∈ gaugeGroupℤ₂SubGroup
    rwa [Subgroup.mem_center_iff.mp (gaugeGroupℤ₂SubGroup_le_center hn) g,n:GaugeGroupIhn:n ∈ gaugeGroupℤ₂SubGroupg:GaugeGroupI⊢ n * g * g⁻¹ ∈ gaugeGroupℤ₂SubGroup
      mul_inv_cancel_rightn:GaugeGroupIhn:n ∈ gaugeGroupℤ₂SubGroupg:GaugeGroupI⊢ n ∈ gaugeGroupℤ₂SubGroup]n:GaugeGroupIhn:n ∈ gaugeGroupℤ₂SubGroupg:GaugeGroupI⊢ n ∈ gaugeGroupℤ₂SubGroup

The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of GaugeGroupI by the ℤ₂-subgroup gaugeGroupℤ₂SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

def GaugeGroupℤ₂ : Type :=
  GaugeGroupI ⧸ gaugeGroupℤ₂SubGroup

@[simp]
lemma mk_gaugeGroupℤ₂OfRoot (α : rootsOfUnity 2 ℂ) :
    mk (gaugeGroupℤ₂OfRoot α) = 1 :=
  (QuotientGroup.eq_one_iff _).mpr (gaugeGroupℤ₂OfRoot_mem α)

The ℤ₃ quotient

              @[simp]
lemma gaugeGroupℤ₃OfRoot_toSU3 (α : rootsOfUnity 3 ℂ) :
    GaugeGroupI.toSU3 (gaugeGroupℤ₃OfRoot α) =
      gaugeGroupℤ₆SU3OfRoot (gaugeGroupℤ₃RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₃OfRoot_toSU2 (α : rootsOfUnity 3 ℂ) :
    GaugeGroupI.toSU2 (gaugeGroupℤ₃OfRoot α) =
      gaugeGroupℤ₆SU2OfRoot (gaugeGroupℤ₃RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₃OfRoot_toU1 (α : rootsOfUnity 3 ℂ) :
    GaugeGroupI.toU1 (gaugeGroupℤ₃OfRoot α) =
      gaugeGroupℤ₆UnitaryOfRoot (gaugeGroupℤ₃RootToℤ₆Root α) := rfllemma gaugeGroupℤ₃OfRoot_mem_center (α : rootsOfUnity 3 ℂ) :
    gaugeGroupℤ₃OfRoot α ∈ Subgroup.center GaugeGroupI :=
  gaugeGroupℤ₆OfRoot_mem_center (gaugeGroupℤ₃RootToℤ₆Root α)@[simp]
lemma gaugeGroupℤ₃Hom_apply (α : rootsOfUnity 3 ℂ) :
    gaugeGroupℤ₃Hom α = gaugeGroupℤ₃OfRoot α := rfl@[simp]
lemma gaugeGroupℤ₃Hom_toSU3 (α : rootsOfUnity 3 ℂ) :
    GaugeGroupI.toSU3 (gaugeGroupℤ₃Hom α) =
      gaugeGroupℤ₆SU3OfRoot (gaugeGroupℤ₃RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₃Hom_toSU2 (α : rootsOfUnity 3 ℂ) :
    GaugeGroupI.toSU2 (gaugeGroupℤ₃Hom α) =
      gaugeGroupℤ₆SU2OfRoot (gaugeGroupℤ₃RootToℤ₆Root α) := rfl@[simp]
lemma gaugeGroupℤ₃Hom_toU1 (α : rootsOfUnity 3 ℂ) :
    GaugeGroupI.toU1 (gaugeGroupℤ₃Hom α) =
      gaugeGroupℤ₆UnitaryOfRoot (gaugeGroupℤ₃RootToℤ₆Root α) := rfllemma gaugeGroupℤ₃OfRoot_mem (α : rootsOfUnity 3 ℂ) :
    gaugeGroupℤ₃OfRoot α ∈ gaugeGroupℤ₃SubGroup :=
  ⟨α, rfl⟩lemma mem_gaugeGroupℤ₃SubGroup_iff (g : GaugeGroupI) :
    g ∈ gaugeGroupℤ₃SubGroup ↔ ∃ α : rootsOfUnity 3 ℂ, gaugeGroupℤ₃OfRoot α = g := byg:GaugeGroupI⊢ g ∈ gaugeGroupℤ₃SubGroup ↔ ∃ α, gaugeGroupℤ₃OfRoot α = g
  simp [gaugeGroupℤ₃SubGroup]All goals completed! 🐙lemma gaugeGroupℤ₃SubGroup_le_gaugeGroupℤ₆SubGroup :
    gaugeGroupℤ₃SubGroup ≤ gaugeGroupℤ₆SubGroup := by⊢ gaugeGroupℤ₃SubGroup ≤ gaugeGroupℤ₆SubGroup
  rintro g ⟨α, rfl⟩α:↥(rootsOfUnity 3 ℂ)⊢ gaugeGroupℤ₃Hom α ∈ gaugeGroupℤ₆SubGroup
  exact gaugeGroupℤ₆OfRoot_mem (gaugeGroupℤ₃RootToℤ₆Root α)All goals completed! 🐙lemma gaugeGroupℤ₃SubGroup_le_center :
    gaugeGroupℤ₃SubGroup ≤ Subgroup.center GaugeGroupI :=
  gaugeGroupℤ₃SubGroup_le_gaugeGroupℤ₆SubGroup.trans gaugeGroupℤ₆SubGroup_le_centerinstance gaugeGroupℤ₃SubGroup_normal : gaugeGroupℤ₃SubGroup.Normal where
  conj_mem n hn g := byn:GaugeGroupIhn:n ∈ gaugeGroupℤ₃SubGroupg:GaugeGroupI⊢ g * n * g⁻¹ ∈ gaugeGroupℤ₃SubGroup
    rwa [Subgroup.mem_center_iff.mp (gaugeGroupℤ₃SubGroup_le_center hn) g,n:GaugeGroupIhn:n ∈ gaugeGroupℤ₃SubGroupg:GaugeGroupI⊢ n * g * g⁻¹ ∈ gaugeGroupℤ₃SubGroup
      mul_inv_cancel_rightn:GaugeGroupIhn:n ∈ gaugeGroupℤ₃SubGroupg:GaugeGroupI⊢ n ∈ gaugeGroupℤ₃SubGroup]n:GaugeGroupIhn:n ∈ gaugeGroupℤ₃SubGroupg:GaugeGroupI⊢ n ∈ gaugeGroupℤ₃SubGroup

The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of GaugeGroupI by the ℤ₃-subgroup gaugeGroupℤ₃SubGroup.

See https://math.ucr.edu/home/baez/guts.pdf

def GaugeGroupℤ₃ : Type :=
  GaugeGroupI ⧸ gaugeGroupℤ₃SubGroup

@[simp]
lemma mk_gaugeGroupℤ₃OfRoot (α : rootsOfUnity 3 ℂ) :
    mk (gaugeGroupℤ₃OfRoot α) = 1 :=
  (QuotientGroup.eq_one_iff _).mpr (gaugeGroupℤ₃OfRoot_mem α)

Gauge groups from quotient choices

Specifies the allowed quotients of SU(3) x SU(2) x U(1) which give a valid gauge group of the Standard Model.

The element of GaugeGroupQuot corresponding to the quotient of the full SM gauge group by the sub-group ℤ₆.

The element of GaugeGroupQuot corresponding to the quotient of the full SM gauge group by the sub-group ℤ₂.

The element of GaugeGroupQuot corresponding to the quotient of the full SM gauge group by the sub-group ℤ₃.

The element of GaugeGroupQuot corresponding to the full SM gauge group.

              inductive GaugeGroupQuot : Type  | ℤ₆ : GaugeGroupQuot  | ℤ₂ : GaugeGroupQuot  | ℤ₃ : GaugeGroupQuot  | I : GaugeGroupQuot
deriving Fintype, DecidableEq

The (global) gauge group of the Standard Model given a choice of quotient, i.e., the map from GaugeGroupQuot to Type which gives the gauge group of the Standard Model for a given choice of quotient.

See https://math.ucr.edu/home/baez/guts.pdf

def GaugeGroup : GaugeGroupQuot → Type
  | .ℤ₆ => GaugeGroupℤ₆
  | .ℤ₂ => GaugeGroupℤ₂
  | .ℤ₃ => GaugeGroupℤ₃
  | .I => GaugeGroupI

TODO "Define the unbroken gauge group using the Higgs field."

The subgroup attached to a gauge-group quotient choice lies in the center of GaugeGroupI.

lemma subgroup_le_center (q : GaugeGroupQuot) :
    subgroup q ≤ Subgroup.center GaugeGroupI := byq:GaugeGroupQuot⊢ q.subgroup ≤ Subgroup.center GaugeGroupI
  cases qℤ₆⊢ ℤ₆.subgroup ≤ Subgroup.center GaugeGroupIℤ₂⊢ ℤ₂.subgroup ≤ Subgroup.center GaugeGroupIℤ₃⊢ ℤ₃.subgroup ≤ Subgroup.center GaugeGroupII⊢ I.subgroup ≤ Subgroup.center GaugeGroupI
  ·ℤ₆⊢ ℤ₆.subgroup ≤ Subgroup.center GaugeGroupI exact gaugeGroupℤ₆SubGroup_le_centerAll goals completed! 🐙
  ·ℤ₂⊢ ℤ₂.subgroup ≤ Subgroup.center GaugeGroupI exact gaugeGroupℤ₂SubGroup_le_centerAll goals completed! 🐙
  ·ℤ₃⊢ ℤ₃.subgroup ≤ Subgroup.center GaugeGroupI exact gaugeGroupℤ₃SubGroup_le_centerAll goals completed! 🐙
  ·I⊢ I.subgroup ≤ Subgroup.center GaugeGroupI exact bot_leAll goals completed! 🐙

The subgroup attached to a gauge-group quotient choice is normal in GaugeGroupI.

instance subgroup_normal (q : GaugeGroupQuot) : (subgroup q).Normal := byq:GaugeGroupQuot⊢ q.subgroup.Normal
  cases qℤ₆⊢ ℤ₆.subgroup.Normalℤ₂⊢ ℤ₂.subgroup.Normalℤ₃⊢ ℤ₃.subgroup.NormalI⊢ I.subgroup.Normal
  ·ℤ₆⊢ ℤ₆.subgroup.Normal exact gaugeGroupℤ₆SubGroup_normalAll goals completed! 🐙
  ·ℤ₂⊢ ℤ₂.subgroup.Normal exact gaugeGroupℤ₂SubGroup_normalAll goals completed! 🐙
  ·ℤ₃⊢ ℤ₃.subgroup.Normal exact gaugeGroupℤ₃SubGroup_normalAll goals completed! 🐙
  ·I⊢ I.subgroup.Normal exact Subgroup.normal_botAll goals completed! 🐙

              

lemma subgroup_le_subgroup_ℤ₆ (q : GaugeGroupQuot) : subgroup q ≤ gaugeGroupℤ₆SubGroup := byq:GaugeGroupQuot⊢ q.subgroup ≤ gaugeGroupℤ₆SubGroup
  cases qℤ₆⊢ ℤ₆.subgroup ≤ gaugeGroupℤ₆SubGroupℤ₂⊢ ℤ₂.subgroup ≤ gaugeGroupℤ₆SubGroupℤ₃⊢ ℤ₃.subgroup ≤ gaugeGroupℤ₆SubGroupI⊢ I.subgroup ≤ gaugeGroupℤ₆SubGroup
  ·ℤ₆⊢ ℤ₆.subgroup ≤ gaugeGroupℤ₆SubGroup exact le_rflAll goals completed! 🐙
  ·ℤ₂⊢ ℤ₂.subgroup ≤ gaugeGroupℤ₆SubGroup exact gaugeGroupℤ₂SubGroup_le_gaugeGroupℤ₆SubGroupAll goals completed! 🐙
  ·ℤ₃⊢ ℤ₃.subgroup ≤ gaugeGroupℤ₆SubGroup exact gaugeGroupℤ₃SubGroup_le_gaugeGroupℤ₆SubGroupAll goals completed! 🐙
  ·I⊢ I.subgroup ≤ gaugeGroupℤ₆SubGroup intro g hgIg:GaugeGroupIhg:g ∈ I.subgroup⊢ g ∈ gaugeGroupℤ₆SubGroup
    change g ∈ (⊥ : Subgroup GaugeGroupI) at hgIg:GaugeGroupIhg:g ∈ ⊥⊢ g ∈ gaugeGroupℤ₆SubGroup
    rw [Subgroup.mem_botIg:GaugeGroupIhg:g = 1⊢ g ∈ gaugeGroupℤ₆SubGroupIg:GaugeGroupIhg:g = 1⊢ g ∈ gaugeGroupℤ₆SubGroup] at hgIg:GaugeGroupIhg:g = 1⊢ g ∈ gaugeGroupℤ₆SubGroup
    simp [hg]All goals completed! 🐙@[simp]
lemma quotientMap_I_apply (g : GaugeGroupI) :
    quotientMap .I g = g := rfl@[simp]
lemma quotientMap_ℤ₆_gaugeGroupℤ₆OfRoot (α : rootsOfUnity 6 ℂ) :
    quotientMap .ℤ₆ (gaugeGroupℤ₆OfRoot α) = 1 :=
  GaugeGroupℤ₆.mk_gaugeGroupℤ₆OfRoot α@[simp]
lemma quotientMap_ℤ₂_gaugeGroupℤ₂OfRoot (α : rootsOfUnity 2 ℂ) :
    quotientMap .ℤ₂ (gaugeGroupℤ₂OfRoot α) = 1 :=
  GaugeGroupℤ₂.mk_gaugeGroupℤ₂OfRoot α@[simp]
lemma quotientMap_ℤ₃_gaugeGroupℤ₃OfRoot (α : rootsOfUnity 3 ℂ) :
    quotientMap .ℤ₃ (gaugeGroupℤ₃OfRoot α) = 1 :=
  GaugeGroupℤ₃.mk_gaugeGroupℤ₃OfRoot α

The kernel of the quotient map is the subgroup selected by the quotient choice.

lemma mem_subgroup_iff_quotientMap_eq_one (q : GaugeGroupQuot) (g : GaugeGroupI) :
    g ∈ subgroup q ↔ quotientMap q g = 1 := byq:GaugeGroupQuotg:GaugeGroupI⊢ g ∈ q.subgroup ↔ q.quotientMap g = 1
  cases qℤ₆g:GaugeGroupI⊢ g ∈ ℤ₆.subgroup ↔ ℤ₆.quotientMap g = 1ℤ₂g:GaugeGroupI⊢ g ∈ ℤ₂.subgroup ↔ ℤ₂.quotientMap g = 1ℤ₃g:GaugeGroupI⊢ g ∈ ℤ₃.subgroup ↔ ℤ₃.quotientMap g = 1Ig:GaugeGroupI⊢ g ∈ I.subgroup ↔ I.quotientMap g = 1
  case I =>g:GaugeGroupI⊢ g ∈ I.subgroup ↔ I.quotientMap g = 1 exact Subgroup.mem_botAll goals completed! 🐙
  all_goals exact (QuotientGroup.eq_one_iff g).symmAll goals completed! 🐙

Two representatives have the same image under the selected quotient map exactly when their quotient lies in the subgroup selected by the quotient choice.

lemma quotientMap_eq_iff (q : GaugeGroupQuot) (g h : GaugeGroupI) :
    quotientMap q g = quotientMap q h ↔ g / h ∈ subgroup q := byq:GaugeGroupQuotg:GaugeGroupIh:GaugeGroupI⊢ q.quotientMap g = q.quotientMap h ↔ g / h ∈ q.subgroup
  cases qℤ₆g:GaugeGroupIh:GaugeGroupI⊢ ℤ₆.quotientMap g = ℤ₆.quotientMap h ↔ g / h ∈ ℤ₆.subgroupℤ₂g:GaugeGroupIh:GaugeGroupI⊢ ℤ₂.quotientMap g = ℤ₂.quotientMap h ↔ g / h ∈ ℤ₂.subgroupℤ₃g:GaugeGroupIh:GaugeGroupI⊢ ℤ₃.quotientMap g = ℤ₃.quotientMap h ↔ g / h ∈ ℤ₃.subgroupIg:GaugeGroupIh:GaugeGroupI⊢ I.quotientMap g = I.quotientMap h ↔ g / h ∈ I.subgroup
  case I =>g:GaugeGroupIh:GaugeGroupI⊢ I.quotientMap g = I.quotientMap h ↔ g / h ∈ I.subgroup exact (Subgroup.mem_bot.trans div_eq_one).symmAll goals completed! 🐙
  all_goals exact QuotientGroup.eq_iff_div_memAll goals completed! 🐙

Smoothness structure on the gauge group.

The gauge group GaugeGroupI is a Lie group.

informal_lemma gaugeGroupI_lie where
  deps := [``GaugeGroupI]
  tag := "6V2HL"

For every q in GaugeGroupQuot the group GaugeGroup q is a Lie group.

informal_lemma gaugeGroup_lie where
  deps := [``GaugeGroup]
  tag := "6V2HR"

Gauge bundles and transformations

The trivial principal bundle over SpaceTime with structure group GaugeGroupI.

informal_definition gaugeBundleI where
  deps := [``GaugeGroupI, ``SpaceTime]
  tag := "6V2HX"

A global section of gaugeBundleI.

informal_definition gaugeTransformI where
  deps := [``gaugeBundleI]
  tag := "6V2H5"