refactor: Higgs GaugeGroupI action to a Representation

Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -59,21 +59,21 @@ lemma ext_of_fst_snd {H1 H2 : TwoHiggsDoublet}
 
 noncomputable instance : SMul StandardModel.GaugeGroupI TwoHiggsDoublet where
   smul g H :=
-    { Φ1 := g • H.Φ1
-      Φ2 := g • H.Φ2 }
+    { Φ1 := StandardModel.HiggsVec.repGaugeGroupI g H.Φ1
+      Φ2 := StandardModel.HiggsVec.repGaugeGroupI g H.Φ2 }
 
 @[simp]
 lemma gaugeGroupI_smul_fst (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) :
-    (g • H).Φ1 = g • H.Φ1 := rfl
+    (g • H).Φ1 = StandardModel.HiggsVec.repGaugeGroupI g H.Φ1 := rfl
 
 @[simp]
 lemma gaugeGroupI_smul_snd (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) :
-    (g • H).Φ2 = g • H.Φ2 := rfl
+    (g • H).Φ2 = StandardModel.HiggsVec.repGaugeGroupI g H.Φ2 := rfl
 
 noncomputable instance : MulAction StandardModel.GaugeGroupI TwoHiggsDoublet where
   one_smul H := by
     ext <;> simp
   mul_smul g1 g2 H := by
-    ext <;> simp [mul_smul]
+    ext <;> simp [Module.End.mul_apply]
 
 end TwoHiggsDoublet

Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean

@@ -89,17 +89,17 @@ lemma gramMatrix_tr_nonneg (H : TwoHiggsDoublet) :
 
 lemma gaugeGroupI_exists_fst_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) :
     ∃ g : StandardModel.GaugeGroupI,
-      g • H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧
-      (g • H.Φ2) 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ ∧
-      ‖(g • H.Φ2) 1‖ = Real.sqrt (H.gramMatrix.det.re) / ‖H.Φ1‖ := by
+      HiggsVec.repGaugeGroupI g H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧
+      (HiggsVec.repGaugeGroupI g H.Φ2) 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ ∧
+      ‖(HiggsVec.repGaugeGroupI g H.Φ2) 1‖ = Real.sqrt (H.gramMatrix.det.re) / ‖H.Φ1‖ := by
   rw [gramMatrix_det_eq_real]
-  obtain ⟨g, h⟩ := (HiggsVec.mem_orbit_gaugeGroupI_iff (H.Φ1) (!₂[‖H.Φ1‖, 0] : HiggsVec)).mpr
-    (by simp [@PiLp.norm_eq_of_L2])
+  obtain ⟨g, h⟩ := (HiggsVec.exists_repGaugeGroupI_eq_iff_norm_eq (H.Φ1)
+    (!₂[‖H.Φ1‖, 0] : HiggsVec)).mpr (by simp [@PiLp.norm_eq_of_L2])
   use g
-  simp at h
   simp [h]
-  have h_fst : (g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ := by
-    have h2 : ⟪H.Φ1, H.Φ2⟫_ℂ = ⟪g • H.Φ1, g • H.Φ2⟫_ℂ := by
+  have h_fst : (HiggsVec.repGaugeGroupI g H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ := by
+    have h2 : ⟪H.Φ1, H.Φ2⟫_ℂ = ⟪HiggsVec.repGaugeGroupI g H.Φ1,
+        HiggsVec.repGaugeGroupI g H.Φ2⟫_ℂ := by
       simp
     rw [h] at h2
     conv_rhs at h2 =>
@@ -109,14 +109,16 @@ lemma gaugeGroupI_exists_fst_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) :
       simp_all
     field_simp
   apply And.intro h_fst
-  have hx : ‖g • H.Φ2‖ ^ 2 = ‖H.Φ2‖ ^ 2 := by
+  have hx : ‖HiggsVec.repGaugeGroupI g H.Φ2‖ ^ 2 = ‖H.Φ2‖ ^ 2 := by
     simp
   rw [PiLp.norm_sq_eq_of_L2] at hx
   simp at hx
-  have hx0 : ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2 := by
+  have hx0 : ‖(HiggsVec.repGaugeGroupI g H.Φ2).ofLp 1‖ ^ 2 =
+      ‖H.Φ2‖ ^ 2 - ‖(HiggsVec.repGaugeGroupI g H.Φ2).ofLp 0‖ ^ 2 := by
     rw [← hx]
     simp
-  have h0 : ‖(g • H.Φ2) 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2 := by
+  have h0 : ‖(HiggsVec.repGaugeGroupI g H.Φ2) 1‖ ^ 2 =
+      (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2 := by
     field_simp
     rw [hx0, h_fst]
     simp only [Fin.isValue, Complex.norm_div, Complex.norm_real, norm_norm]
@@ -133,18 +135,19 @@ lemma gaugeGroupI_exists_fst_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) :
   ring_nf
   · exact norm_ne_zero_iff.mpr h1
   · simpa using h1
-  · exact norm_nonneg ((g • H.Φ2).ofLp 1)
+  · exact norm_nonneg ((HiggsVec.repGaugeGroupI g H.Φ2).ofLp 1)
 
 lemma gaugeGroupI_exists_fst_eq_snd_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) :
     ∃ g : StandardModel.GaugeGroupI,
-      g • H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧
-      g • H.Φ2 = (!₂[⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖, √(H.gramMatrix.det.re) / ‖H.Φ1‖] : HiggsVec) := by
+      HiggsVec.repGaugeGroupI g H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧
+      HiggsVec.repGaugeGroupI g H.Φ2 =
+        (!₂[⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖, √(H.gramMatrix.det.re) / ‖H.Φ1‖] : HiggsVec) := by
   obtain ⟨g, h_fst, h_snd_0, h_snd_1⟩ := gaugeGroupI_exists_fst_eq h1
-  obtain ⟨k, h1, h2, h3⟩ := HiggsVec.gaugeGroupI_smul_phase_snd (g • H.Φ2)
+  obtain ⟨k, h1, h2, h3⟩ := HiggsVec.repGaugeGroupI_phase_snd (HiggsVec.repGaugeGroupI g H.Φ2)
   use k * g
   apply And.intro
-  · rw [mul_smul, h_fst, h3]
-  · rw [mul_smul]
+  · rw [HiggsVec.repGaugeGroupI_mul_apply, h_fst, h3]
+  · rw [HiggsVec.repGaugeGroupI_mul_apply]
     ext i
     fin_cases i
     · simp
@@ -162,10 +165,10 @@ lemma mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) :
     simp [← hg]
   by_cases Φ1_zero : H1.Φ1 = 0
   · intro h
-    obtain ⟨g1, hg1⟩ := (HiggsVec.mem_orbit_gaugeGroupI_iff (H1.Φ2) (!₂[‖H1.Φ2‖, 0] : HiggsVec)).mpr
-      (by simp [@PiLp.norm_eq_of_L2])
-    obtain ⟨g2, hg2⟩ := (HiggsVec.mem_orbit_gaugeGroupI_iff (H2.Φ2) (!₂[‖H2.Φ2‖, 0] : HiggsVec)).mpr
-      (by simp [@PiLp.norm_eq_of_L2])
+    obtain ⟨g1, hg1⟩ := (HiggsVec.exists_repGaugeGroupI_eq_iff_norm_eq (H1.Φ2)
+      (!₂[‖H1.Φ2‖, 0] : HiggsVec)).mpr (by simp [@PiLp.norm_eq_of_L2])
+    obtain ⟨g2, hg2⟩ := (HiggsVec.exists_repGaugeGroupI_eq_iff_norm_eq (H2.Φ2)
+      (!₂[‖H2.Φ2‖, 0] : HiggsVec)).mpr (by simp [@PiLp.norm_eq_of_L2])
     use g1⁻¹ * g2
     simp only
     ext:1
@@ -175,9 +178,8 @@ lemma mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) :
         rw [← eq_fst_norm_of_eq_gramMatrix h]
       simp [Φ1_zero] at hnorm
       simp [hnorm]
-    · simp [mul_smul]
-      refine inv_smul_eq_iff.mpr ?_
-      simp at hg1 hg2
+    · simp
+      refine (HiggsVec.repGaugeGroupI_inv_apply_eq_iff _ _ _).mpr ?_
       simp [hg1, hg2]
       exact eq_snd_norm_of_eq_gramMatrix h.symm
   · intro h
@@ -192,12 +194,12 @@ lemma mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) :
     use g1⁻¹ * g2
     simp only
     ext:1
-    · simp [mul_smul]
-      refine inv_smul_eq_iff.mpr ?_
+    · simp
+      refine (HiggsVec.repGaugeGroupI_inv_apply_eq_iff _ _ _).mpr ?_
       simp [H1_Φ1, H2_Φ1]
       apply eq_fst_norm_of_eq_gramMatrix h.symm
-    · simp [mul_smul]
-      refine inv_smul_eq_iff.mpr ?_
+    · simp
+      refine (HiggsVec.repGaugeGroupI_inv_apply_eq_iff _ _ _).mpr ?_
       simp [H1_Φ2, H2_Φ2]
       apply And.intro
       · congr 1

Physlib/Particles/StandardModel/HiggsBoson/Basic.lean

@@ -32,8 +32,9 @@ In this module we define the Higgs field and prove some basic properties.
   - A.3. Orthonormal basis
   - A.4. Generating Higgs vectors from real numbers
   - A.5. Action of the gauge group on `HiggsVec`
-    - A.5.1. Definition of the action
+    - A.5.1. Definition of the representation
     - A.5.2. Unitary nature of the action
+    - A.5.3. Group properties of the representation applied to vectors
   - A.6. The Gauge orbit of a Higgs vector
     - A.6.1. The rotation matrix to ofReal
     - A.6.2. Members of orbits
@@ -160,43 +161,37 @@ The gauge group of the Standard Model acts on `HiggsVec` by matrix multiplicatio
 
 /-!
 
-#### A.5.1. Definition of the action
+#### A.5.1. Definition of the representation
 
 -/
 
-instance : SMul StandardModel.GaugeGroupI HiggsVec where
-  smul g φ := WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)
+/-- The representation of the gauge group `GaugeGroupI` on `HiggsVec`: the `SU(2)`
+  factor acts by matrix multiplication, and the `U(1)` factor by scalar
+  multiplication with its third power. -/
+def repGaugeGroupI : Representation ℂ GaugeGroupI HiggsVec where
+  toFun g :=
+    { toFun φ := WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)
+      map_add' φ ψ := by simp [mulVec_add, smul_add]
+      map_smul' c φ := by simp [mulVec_smul, smul_comm c] }
+  map_one' := by
+    ext φ
+    simp
+  map_mul' g₁ g₂ := by
+    ext φ
+    simp [Module.End.mul_apply, smul_smul, mulVec_mulVec, mul_pow, mul_comm]
 
-lemma gaugeGroupI_smul_eq (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
-    g • φ = (WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)) := rfl
+lemma repGaugeGroupI_apply (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
+    repGaugeGroupI g φ = (WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)) := rfl
 
-lemma gaugeGroupI_smul_eq_U1_mul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
-    g • φ = (WithLp.toLp 2 <| g.toSU2.1 *ᵥ (g.toU1 ^ 3 • φ.ofLp)) := by
-  rw [gaugeGroupI_smul_eq, ← mulVec_smul]
+lemma repGaugeGroupI_apply_eq_U1_mul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
+    repGaugeGroupI g φ = (WithLp.toLp 2 <| g.toSU2.1 *ᵥ (g.toU1 ^ 3 • φ.ofLp)) := by
+  rw [repGaugeGroupI_apply, ← mulVec_smul]
 
-lemma gaugeGroupI_smul_eq_U1_smul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
-    g • φ = (WithLp.toLp 2 <| (g.toU1 ^ 3 • g.toSU2.1) *ᵥ φ.ofLp) := by
-  rw [gaugeGroupI_smul_eq]
+lemma repGaugeGroupI_apply_eq_U1_smul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
+    repGaugeGroupI g φ = (WithLp.toLp 2 <| (g.toU1 ^ 3 • g.toSU2.1) *ᵥ φ.ofLp) := by
+  rw [repGaugeGroupI_apply]
   rw [Matrix.smul_mulVec]
 
-instance : MulAction StandardModel.GaugeGroupI HiggsVec where
-  one_smul φ := by simp [gaugeGroupI_smul_eq]
-  mul_smul g₁ g₂ φ := by
-    simp [gaugeGroupI_smul_eq, mulVec_smul, smul_smul, mulVec_mulVec, mul_pow]
-
-instance : DistribMulAction StandardModel.GaugeGroupI HiggsVec where
-  smul_zero g := by simp [gaugeGroupI_smul_eq_U1_smul_SU2]
-  smul_add g φ ψ := by simp [gaugeGroupI_smul_eq_U1_smul_SU2, mulVec_add]
-
-TODO "Change the action of `GaugeGroupI` on `HiggsVec` to be a representation
-  rather than a `MulAction`."
-
-instance : SMulCommClass ℂ GaugeGroupI HiggsVec where
-  smul_comm r g φ := by simp [gaugeGroupI_smul_eq, mulVec_smul, smul_comm r]
-
-instance : SMulCommClass ℝ GaugeGroupI HiggsVec where
-  smul_comm r g φ := by simp [gaugeGroupI_smul_eq, mulVec_smul, smul_comm r]
-
 /-!
 
 #### A.5.2. Unitary nature of the action
@@ -207,18 +202,36 @@ The action of `StandardModel.GaugeGroupI` on `HiggsVec` is unitary.
 open InnerProductSpace
 
 @[simp]
-lemma gaugeGroupI_smul_inner (g : StandardModel.GaugeGroupI) (φ ψ : HiggsVec) :
-    ⟪g • φ, g • ψ⟫_ℂ = ⟪φ, ψ⟫_ℂ := by
-  rw [gaugeGroupI_smul_eq, gaugeGroupI_smul_eq, EuclideanSpace.inner_toLp_toLp,
+lemma repGaugeGroupI_inner (g : StandardModel.GaugeGroupI) (φ ψ : HiggsVec) :
+    ⟪repGaugeGroupI g φ, repGaugeGroupI g ψ⟫_ℂ = ⟪φ, ψ⟫_ℂ := by
+  rw [repGaugeGroupI_apply, repGaugeGroupI_apply, EuclideanSpace.inner_toLp_toLp,
     EuclideanSpace.inner_eq_star_dotProduct, Submonoid.smul_def, Submonoid.smul_def, star_smul,
     smul_dotProduct, dotProduct_smul, smul_smul, Unitary.mul_star_self_of_mem (g.toU1 ^ 3).2,
     one_smul, star_mulVec, dotProduct_comm, dotProduct_mulVec, vecMul_vecMul,
     ← star_eq_conjTranspose, mem_unitaryGroup_iff'.mp g.toSU2.2.1, vecMul_one, dotProduct_comm]
 
 @[simp]
-lemma gaugeGroupI_smul_norm (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
-    ‖g • φ‖ = ‖φ‖ := by
-  rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), norm_eq_sqrt_re_inner (𝕜 := ℂ), gaugeGroupI_smul_inner]
+lemma repGaugeGroupI_norm (g : StandardModel.GaugeGroupI) (φ : HiggsVec) :
+    ‖repGaugeGroupI g φ‖ = ‖φ‖ := by
+  rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), norm_eq_sqrt_re_inner (𝕜 := ℂ), repGaugeGroupI_inner]
+
+/-!
+
+#### A.5.3. Group properties of the representation applied to vectors
+
+-/
+
+lemma repGaugeGroupI_mul_apply (g₁ g₂ : StandardModel.GaugeGroupI) (φ : HiggsVec) :
+    repGaugeGroupI (g₁ * g₂) φ = repGaugeGroupI g₁ (repGaugeGroupI g₂ φ) := by
+  rw [map_mul, Module.End.mul_apply]
+
+lemma repGaugeGroupI_inv_apply_eq_iff (g : StandardModel.GaugeGroupI) (φ ψ : HiggsVec) :
+    repGaugeGroupI g⁻¹ φ = ψ ↔ φ = repGaugeGroupI g ψ := by
+  constructor
+  · rintro rfl
+    rw [Representation.self_inv_apply]
+  · rintro rfl
+    rw [Representation.inv_self_apply]
 
 /-!
 
@@ -270,12 +283,12 @@ def toRealGroupElem (φ : HiggsVec) : GaugeGroupI :=
     rw [← mul_conj, ← mul_conj]
     ring
 
-lemma toRealGroupElem_smul_self (φ : HiggsVec) :
-    (toRealGroupElem φ) • φ = ofReal (‖φ‖ ^ 2) := by
+lemma toRealGroupElem_apply_self (φ : HiggsVec) :
+    repGaugeGroupI (toRealGroupElem φ) φ = ofReal (‖φ‖ ^ 2) := by
   by_cases hφ : φ = 0
   · ext i
     fin_cases i <;> simp [hφ, toRealGroupElem, ofReal]
-  rw [gaugeGroupI_smul_eq]
+  rw [repGaugeGroupI_apply]
   have h0' : (‖φ‖ ^ 2 : ℂ) = φ 0 * (starRingEnd ℂ) (φ 0) + φ 1 * (starRingEnd ℂ) (φ 1) := by
     rw [← ofReal_pow, ← @real_inner_self_eq_norm_sq]
     simp only [Fin.isValue, mul_conj, PiLp.inner_apply, Complex.inner, ofReal_re,
@@ -301,16 +314,18 @@ Higgs vectors with the same norm.
 
 -/
 
-lemma mem_orbit_gaugeGroupI_iff (φ : HiggsVec) (ψ : HiggsVec) :
-    ψ ∈ MulAction.orbit GaugeGroupI φ ↔ ‖ψ‖ = ‖φ‖ := by
+/-- Two Higgs vectors are in the same gauge orbit (i.e. related by `repGaugeGroupI`)
+  if and only if they have the same norm. -/
+lemma exists_repGaugeGroupI_eq_iff_norm_eq (φ : HiggsVec) (ψ : HiggsVec) :
+    (∃ g : GaugeGroupI, repGaugeGroupI g φ = ψ) ↔ ‖ψ‖ = ‖φ‖ := by
   constructor
   · rintro ⟨g, rfl⟩
     simp
   · intro h
     use (toRealGroupElem ψ)⁻¹ * toRealGroupElem (φ)
-    simp only
-    rw [← smul_smul, toRealGroupElem_smul_self φ, ← h, ← toRealGroupElem_smul_self ψ]
-    exact inv_smul_smul _ ψ
+    rw [map_mul, Module.End.mul_apply, toRealGroupElem_apply_self φ, ← h,
+      ← toRealGroupElem_apply_self ψ, ← Module.End.mul_apply, ← map_mul,
+      inv_mul_cancel, map_one, Module.End.one_apply]
 
 /-!
 
@@ -324,7 +339,7 @@ The items in this section are marked as `informal_lemma` as they are not yet for
 -/
 
 /-- The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the
-stability group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the
+stability group of `repGaugeGroupI` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the
 `SU(3) × U(1)` subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` with the embedding given by
 `(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`.
 -/
@@ -333,8 +348,8 @@ informal_lemma stability_group_single where
   tag := "6V2MD"
 
 /-- The subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` which preserves every `HiggsVec` by the
-action of `StandardModel.HiggsVec.rep` is given by `SU(3) × ℤ₆` where `ℤ₆` is the subgroup of
-`SU(2) × U(1)` with elements `(α^(-3) * I₂, α)` where `α` is a sixth root of unity.
+action of `StandardModel.HiggsVec.repGaugeGroupI` is given by `SU(3) × ℤ₆` where `ℤ₆` is the
+subgroup of `SU(2) × U(1)` with elements `(α^(-3) * I₂, α)` where `α` is a sixth root of unity.
 -/
 informal_lemma stability_group where
   deps := [``HiggsVec]
@@ -346,10 +361,10 @@ informal_lemma stability_group where
 
 -/
 
-lemma ofU1Subgroup_smul_eq_smul (g : unitary ℂ) (φ : HiggsVec) :
-    (StandardModel.GaugeGroupI.ofU1Subgroup g) • φ =
+lemma ofU1Subgroup_repGaugeGroupI_apply (g : unitary ℂ) (φ : HiggsVec) :
+    repGaugeGroupI (StandardModel.GaugeGroupI.ofU1Subgroup g) φ =
     (WithLp.toLp 2 <| !![1, 0; 0, g.1 ^ 6] *ᵥ φ.ofLp) := by
-  rw [gaugeGroupI_smul_eq_U1_smul_SU2]
+  rw [repGaugeGroupI_apply_eq_U1_smul_SU2]
   simp only [GaugeGroupI.ofU1Subgroup_toU1, GaugeGroupI.ofU1Subgroup_toSU2, SubmonoidClass.coe_pow,
     star_pow, RCLike.star_def, smul_of, smul_cons, smul_zero, smul_empty, cons_mulVec,
     cons_dotProduct, zero_mul, dotProduct_of_isEmpty, add_zero, zero_add, empty_mulVec, one_mul,
@@ -362,17 +377,17 @@ lemma ofU1Subgroup_smul_eq_smul (g : unitary ℂ) (φ : HiggsVec) :
   · show (g : ℂ) ^ 3 * (g : ℂ) ^ 3 = (g : ℂ) ^ 6
     ring
 
-lemma gaugeGroupI_smul_phase_snd (φ : HiggsVec) :
+lemma repGaugeGroupI_phase_snd (φ : HiggsVec) :
     ∃ g : StandardModel.GaugeGroupI,
-      (g • φ).ofLp 1 = ‖(φ.ofLp 1)‖ ∧
-      (∀ φ1 : HiggsVec, (g • φ1).ofLp 0 = φ1.ofLp 0) ∧
-      (∀ a : ℝ, g • (!₂[a, 0] : HiggsVec) = (!₂[a, 0] : HiggsVec)) := by
+      (repGaugeGroupI g φ).ofLp 1 = ‖(φ.ofLp 1)‖ ∧
+      (∀ φ1 : HiggsVec, (repGaugeGroupI g φ1).ofLp 0 = φ1.ofLp 0) ∧
+      (∀ a : ℝ, repGaugeGroupI g (!₂[a, 0] : HiggsVec) = (!₂[a, 0] : HiggsVec)) := by
   let θ := arg (φ 1)
   refine ⟨StandardModel.GaugeGroupI.ofU1Subgroup ⟨Complex.exp (-I * θ / 6), by
     simp [Unitary.mem_iff, ← Complex.exp_conj, ← Complex.exp_add, Complex.conj_ofNat]
     ring_nf
     simp⟩, ?_, ?_, ?_⟩
-  · rw [ofU1Subgroup_smul_eq_smul]
+  · rw [ofU1Subgroup_repGaugeGroupI_apply]
     simp only [Fin.isValue, neg_mul, cons_mulVec, cons_dotProduct, one_mul, zero_mul,
       dotProduct_of_isEmpty, add_zero, zero_add, empty_mulVec, cons_val_one, cons_val_fin_one]
     rw [show vecHead (vecTail φ.ofLp) = φ.ofLp 1 from rfl]
@@ -382,10 +397,10 @@ lemma gaugeGroupI_smul_phase_snd (φ : HiggsVec) :
     ring_nf
     simp
   · intro φ
-    simp [ofU1Subgroup_smul_eq_smul, vecHead]
+    simp [ofU1Subgroup_repGaugeGroupI_apply, vecHead]
   · intro a
     ext i
-    fin_cases i <;> simp [ofU1Subgroup_smul_eq_smul]
+    fin_cases i <;> simp [ofU1Subgroup_repGaugeGroupI_apply]
 
 
 /-!
@@ -738,7 +753,8 @@ TODO "Define the global gauge action on HiggsField."
 TODO "Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)"
 TODO "Prove invariance of potential under global gauge action."
 
-/-- The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`. -/
+/-- The action of `gaugeTransformI` on `HiggsField` acting pointwise through
+  `HiggsVec.repGaugeGroupI`. -/
 informal_definition gaugeAction where
   deps := [``gaugeTransformI]
   tag := "6V2NP"