Imports
/-
Copyright (c) 2026 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 Physlib.Particles.BeyondTheStandardModel.TwoHDM.GramMatrixThe gauge torus acting on Higgs vectors
The maximal torus of the gauge group acting on a Higgs doublet is the group of diagonal phase
rotations diag(a, b) of the two components. We realise it using
the SU(2) Cartan element diag(a, ā) (constructed here as gaugeCartan), and
the existing ofU1Subgroup, whose action is diag(1, μ).
Together these realise an arbitrary diagonal phase diag(a, b), which is the symmetry underlying
the charge-balancing ("Condition A") of the effective potential on the orbit representatives.
@[expose] public section@[simp]
lemma gaugeCartan_toU1 (a : unitary ℂ) : (gaugeCartan a).toU1 = 1 := rfl@[simp]
lemma gaugeCartan_toSU2_coe (a : unitary ℂ) :
((gaugeCartan a).toSU2 : Matrix (Fin 2) (Fin 2) ℂ) = !![(a : ℂ), 0; 0, (star a : ℂ)] := rfl
The Cartan element acts as the diagonal matrix diag(a, ā).
All goals completed! 🐙