Help formalizing some properties of a group

Stream: general

[Joseph Tooby-Smith]

I'm soliciting help formalizing some properties of a specific group as part of HepLean. The results I would like formalizing are those under the HepLean.StandardModel.Basic heading here, they are also those in the part of this dependency graph connected to the StandardModel.GaugeGroupI node.

If anyone would be willing to help that would be great? (Anyone should feel welcome to help formalize any of the other nodes there aswell)

I note that I don't expect any of these results to be too hard to formalize. What I really want to know is if the informal_lemma and infromal_definition structures used to write them down are useful and followable by someone other than myself, and what would help improve them. See here for a related discussion.

[Floris van Doorn]

So is this roughly what you're after for the very first definition (still contains some sorries)?

import Mathlib.Data.Complex.Exponential
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.LinearAlgebra.Matrix.ToLin

noncomputable section
namespace StandardModel

open scoped Real
open Manifold Matrix Complex ComplexConjugate

/-- 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 ℂ

def α : unitary ℂ := ⟨exp (I * π / 3), sorry⟩

instance {ι} [Fintype ι] [DecidableEq ι] : SMul (unitary ℂ) (specialUnitaryGroup ι ℂ) :=
  ⟨fun a b ↦ ⟨a • b, sorry⟩⟩

def gaugeGroupℤ₆SubGroup : Subgroup GaugeGroupIˣ :=
  .zpowers <| IsUnit.unit (a := (α ^ 2 • 1, α ^ (-3 : ℤ) • 1, α)) sorry

Note that I don't have time to seriously help, but I wanted to take a look what kind of thing you are doing.

[Floris van Doorn]

What I expect will be helpful is even more precise mathematical definitions. For example here I wasn't immediately sure if "with elements" meant "generated by". Also, isn't α^(-3) equal to -1? In gaugeGroupℤ₃SubGroup I believe there are 2 choices you can make. Do you care which one?

[Joseph Tooby-Smith]

Hi @Floris van Doorn thanks for this, and thanks for your comment and for taking a look :).

By "with elements" I really meant that the subgroup ℤ₆ of GaugeGroupIˣ consisting of the six elements of the form (α ^ 2 • 1, α ^ (-3 : ℤ) • 1, α) where α is a sixth root of unity. But I understand that this wasn't clear, and I thank you for pointing this out.

I believe the definition you have is (trivially) equivalent to what I wanted however.

[Floris van Doorn]

Ah, fair. Now I understand what you mean, and why there is an α ^ (-3) there.