From 2c01cd813eaae5941409dc1074199681e0ed1637 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Oct 2026 09:29:14 +0100
Subject: [PATCH 1/6] feat: Add Adjiont

---
 Physlib.lean                                  |   1 +
 .../SpecialUnitary/LieAlgebra/Adjoint.lean    | 276 ++++++++++++++++++
 .../SpecialUnitary/LieAlgebra/Basic.lean      | 104 ++++++-
 3 files changed, 379 insertions(+), 2 deletions(-)
 create mode 100644 Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean

diff --git a/Physlib.lean b/Physlib.lean
index 87110cdd32..efdb2cc98f 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -139,6 +139,7 @@ public import Physlib.Mathematics.ForMathlib.SchurTriangulation
 public import Physlib.Mathematics.ForMathlib.Trigonometry.SinSq
 public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh
 public import Physlib.Mathematics.Groups.SO3.Basic
+public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Adjoint
 public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Basic
 public import Physlib.Mathematics.InnerProductSpace.Adjoint
 public import Physlib.Mathematics.InnerProductSpace.Basic
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
new file mode 100644
index 0000000000..3f41b3996e
--- /dev/null
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
@@ -0,0 +1,276 @@
+/-
+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.Mathematics.Groups.SpecialUnitary.LieAlgebra.Basic
+public import Mathlib.Analysis.Complex.Basic
+public import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
+public import Mathlib.LinearAlgebra.Matrix.PosDef
+public import Mathlib.RepresentationTheory.Intertwining
+/-!
+
+# The adjoint representation of `SU(n)`
+
+## i. Overview
+
+We define the adjont representation of `SU(n)` on its Lie algebra `su(n)` and its complexification.
+The adjoint is defined by conjugation, `x ↦ g x g†`.
+
+The contraction `adjointContr` of two real adjoint indices is the trace form `x ⊗ y ↦ tr (x y)` on
+`su(n)`, which is real since `x` and `y` are hermitian, and invariant under the adjoint action by
+the cyclicity of the trace. It is symmetric, and nondegenerate since `tr (x x†) = 0` forces
+`x = 0` (B.1). The contraction `adjointℂContr` of two complex adjoint indices is its
+complexification. On the underlying matrices it is the trace form `A ⊗ B ↦ tr (A B)`, and it is
+again symmetric and nondegenerate (B.2).
+
+## ii. Key results
+
+- `SULieAlgebra.adjoint` : the adjoint representation on `su(n)`.
+- `SULieAlgebra.adjoint_lie` : the adjoint representation preserves the bracket.
+- `SULieAlgebra.adjointℂ` : the adjoint representation on the complexification.
+- `SULieAlgebra.adjointℂ_lie` : the complex adjoint representation preserves the bracket.
+- `SULieAlgebra.adjointContr` : the contraction of two real adjoint indices.
+- `SULieAlgebra.adjointContr_flip_injective` : the real contraction is nondegenerate.
+- `SULieAlgebra.adjointℂContr` : the contraction of two complex adjoint indices.
+- `SULieAlgebra.toMatrixℂ_adjointℂ` : on matrices the adjoint action is conjugation.
+- `SULieAlgebra.adjointℂContr_tmul` : the contraction is the trace form on matrices.
+- `SULieAlgebra.adjointℂContr_flip_injective` : the complex contraction is nondegenerate.
+
+## iii. Table of contents
+
+- A. The adjoint representation
+  - A.1. The real adjoint representation
+  - A.2. The complex adjoint representation
+- B. The contraction of adjoint indices
+  - B.1. The real case
+  - B.2. The complex case
+
+## iv. References
+
+* None.
+
+-/
+
+@[expose] public section
+
+open Matrix TensorProduct ComplexStarModule
+open scoped ComplexOrder
+
+namespace SULieAlgebra
+
+/-!
+
+## A. The adjoint representation
+
+-/
+
+/-!
+
+### A.1. The real adjoint representation
+
+-/
+
+/-- The adjoint representation `x ↦ g x g†` of `SU(n)` on its real Lie algebra `su(n)`. -/
+noncomputable def adjoint {n : ℕ} :
+    Representation ℝ (specialUnitaryGroup (Fin n) ℂ) (SULieAlgebra n ℂ) :=
+  conj.comp (Submonoid.inclusion specialUnitaryGroup_le_unitaryGroup)
+
+/-- The underlying matrix of `adjoint g x` is `g x g†`. -/
+@[simp]
+lemma adjoint_val {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) (x : SULieAlgebra n ℂ) :
+    (adjoint g x).1 = g.1 * x.1 * star g.1 := rfl
+
+/-- The adjoint representation preserves the bracket, so `SU(n)` acts on `su(n)` by Lie algebra
+  automorphisms. -/
+lemma adjoint_lie {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) (x y : SULieAlgebra n ℂ) :
+    adjoint g ⁅x, y⁆ = ⁅adjoint g x, adjoint g y⁆ :=
+  conj_lie _ x y
+
+/-!
+
+### A.2. The complex adjoint representation
+
+-/
+
+/-- The adjoint representation of `SU(n)` on the complexification `ℂ ⊗[ℝ] su(n)`: the
+  complexification of the adjoint representation `adjoint` on `su(n)`. -/
+noncomputable def adjointℂ {n : ℕ} :
+    Representation ℂ (specialUnitaryGroup (Fin n) ℂ) (Complexification n) :=
+  (Module.End.baseChangeHom ℝ ℂ (SULieAlgebra n ℂ) : Module.End ℝ _ →* Module.End ℂ _).comp
+    adjoint
+
+@[simp]
+lemma adjointℂ_tmul {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) (z : ℂ) (x : SULieAlgebra n ℂ) :
+    adjointℂ g (z ⊗ₜ x) = z ⊗ₜ adjoint g x := rfl
+
+/-- The complex adjoint representation preserves the bracket of the complexification, so `SU(n)`
+  acts on `ℂ ⊗[ℝ] su(n)` by Lie algebra automorphisms. -/
+lemma adjointℂ_lie {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) (A B : Complexification n) :
+    adjointℂ g ⁅A, B⁆ = ⁅adjointℂ g A, adjointℂ g B⁆ := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z x =>
+    induction B using TensorProduct.inductionOn with
+    | tmul w y =>
+      rw [LieAlgebra.ExtendScalars.bracket_tmul, adjointℂ_tmul, adjointℂ_tmul, adjointℂ_tmul,
+        LieAlgebra.ExtendScalars.bracket_tmul, adjoint_lie]
+    | add B B' hB hB' =>
+      rw [lie_add (L := Complexification n), map_add, hB, hB', map_add,
+        lie_add (L := Complexification n)]
+  | add A A' hA hA' =>
+    rw [add_lie (L := Complexification n), map_add, hA, hA', map_add,
+      add_lie (L := Complexification n)]
+
+/-- The adjoint representation conjugates the matrix, `M ↦ g M g†`. -/
+@[simp]
+lemma toMatrixℂ_adjointℂ {n} (g : specialUnitaryGroup (Fin n) ℂ) (A : Complexification n) :
+    toMatrixℂ (adjointℂ g A) = g.1 * toMatrixℂ A * star g.1 := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z x =>
+    rw [adjointℂ_tmul, toMatrixℂ_tmul, toMatrixℂ_tmul, adjoint_val, Matrix.mul_smul,
+      Matrix.smul_mul]
+  | add A B hA hB => rw [map_add, map_add, hA, hB, map_add, Matrix.mul_add, Matrix.add_mul]
+
+lemma toMatrixℂ_adjointℂ_trace {n} (g : specialUnitaryGroup (Fin n) ℂ) (A : Complexification n) :
+    (toMatrixℂ (adjointℂ g A)).trace = (toMatrixℂ A).trace := by
+  rw [toMatrixℂ_adjointℂ, Matrix.trace_mul_cycle, Matrix.trace_mul_cycle, Matrix.mul_assoc,
+    (mem_specialUnitaryGroup_iff.mp g.2).1.1, Matrix.mul_one]
+
+/-!
+
+## B. The contraction of adjoint indices
+
+### B.1. The real case
+
+-/
+
+/-- The contraction of two real adjoint indices: the trace form `x ⊗ y ↦ tr (x y)` on `su(n)`,
+  which is real since `x` and `y` are hermitian. -/
+noncomputable def adjointContr {n : ℕ} : ((adjoint (n := n)).tprod adjoint).IntertwiningMap
+    (Representation.trivial ℝ (specialUnitaryGroup (Fin n) ℂ) ℝ) where
+  toLinearMap := TensorProduct.lift <|
+    LinearMap.mk₂ ℝ (fun x y : SULieAlgebra n ℂ => (x.1 * y.1).trace.re)
+      (fun x x' y => by simp [add_mul, trace_add])
+      (fun r x y => by simp)
+      (fun x y y' => by simp [mul_add, trace_add])
+      (fun r x y => by simp)
+  isIntertwining' g := TensorProduct.ext' fun x y => by
+    have hg : star g.1 * g.1 = 1 := (mem_specialUnitaryGroup_iff.mp g.2).1.1
+    simp only [LinearMap.comp_apply, Representation.tprod_apply, TensorProduct.map_tmul,
+      Representation.trivial_apply, lift.tmul, LinearMap.mk₂_apply, adjoint_val]
+    rw [show g.1 * x.1 * star g.1 * (g.1 * y.1 * star g.1) = g.1 * (x.1 * y.1) * star g.1 by
+      simp only [Matrix.mul_assoc]
+      rw [← Matrix.mul_assoc (star g.1), hg, Matrix.one_mul],
+      Matrix.trace_mul_cycle, hg, Matrix.one_mul]
+
+/-- The real contraction is the real part of the trace, `x ⊗ y ↦ re tr (x y)`. -/
+@[simp]
+lemma adjointContr_tmul {n : ℕ} (x y : SULieAlgebra n ℂ) :
+    adjointContr (x ⊗ₜ y) = (x.1 * y.1).trace.re := rfl
+
+/-- The trace `tr (x y)` of two elements of `su(n)` is real, equal to their contraction. -/
+lemma ofReal_adjointContr_tmul {n : ℕ} (x y : SULieAlgebra n ℂ) :
+    (adjointContr (x ⊗ₜ y) : ℂ) = (x.1 * y.1).trace := by
+  rw [adjointContr_tmul]
+  refine Complex.conj_eq_iff_re.1 ?_
+  change star (x.1 * y.1).trace = _
+  rw [← trace_conjTranspose, conjTranspose_mul, ← star_eq_conjTranspose,
+    ← star_eq_conjTranspose, x.star_val_eq, y.star_val_eq, trace_mul_comm]
+
+lemma adjointContr_symm {n : ℕ} (x y : SULieAlgebra n ℂ) :
+    adjointContr (x ⊗ₜ y) = adjointContr (y ⊗ₜ x) := by
+  rw [adjointContr_tmul, adjointContr_tmul, trace_mul_comm]
+
+lemma adjointContr_separating_left {n : ℕ} (x : SULieAlgebra n ℂ)
+    (hx : ∀ y, adjointContr (x ⊗ₜ y) = 0) : x = 0 := by
+  have h : (x.1 * x.1ᴴ).trace = 0 := by
+    rw [← star_eq_conjTranspose, x.star_val_eq, ← ofReal_adjointContr_tmul, hx,
+      Complex.ofReal_zero]
+  exact Subtype.ext (trace_mul_conjTranspose_self_eq_zero_iff.mp h)
+
+lemma adjointContr_separating_right {n : ℕ} (y : SULieAlgebra n ℂ)
+    (hy : ∀ x, adjointContr (x ⊗ₜ y) = 0) : y = 0 :=
+  adjointContr_separating_left y fun x => by rw [adjointContr_symm, hy]
+
+/-- The real contraction separates `su(n)`: `y ↦ (x ↦ re tr (x y))` is injective. -/
+lemma adjointContr_flip_injective {n : ℕ} :
+    Function.Injective (TensorProduct.curry (adjointContr (n := n)).toLinearMap).flip := by
+  intro w w' h
+  refine sub_eq_zero.1 (adjointContr_separating_right _ fun x => ?_)
+  have hx := LinearMap.congr_fun h x
+  simp only [LinearMap.flip_apply, TensorProduct.curry_apply] at hx
+  rw [tmul_sub, map_sub, sub_eq_zero]
+  exact hx
+
+/-!
+
+### B.2. The complex case
+
+-/
+
+/-- The contraction of two complex adjoint indices: the complexification of the real contraction
+  `adjointContr`. -/
+noncomputable def adjointℂContr {n : ℕ} : ((adjointℂ (n := n)).tprod adjointℂ).IntertwiningMap
+    (Representation.trivial ℂ (specialUnitaryGroup (Fin n) ℂ) ℂ) where
+  toLinearMap := TensorProduct.lift <| LinearMap.BilinForm.baseChange ℂ <|
+    TensorProduct.curry (adjointContr (n := n)).toLinearMap
+  isIntertwining' g := TensorProduct.ext' fun A B => by
+    simp only [LinearMap.comp_apply, Representation.tprod_apply, TensorProduct.map_tmul,
+      Representation.trivial_apply]
+    induction A using TensorProduct.inductionOn with
+    | tmul z x =>
+      induction B using TensorProduct.inductionOn with
+      | tmul w y =>
+        have h := Representation.IntertwiningMap.isIntertwining _ _ (adjointContr (n := n)) g
+          (x ⊗ₜ y)
+        simp only [Representation.tprod_apply, TensorProduct.map_tmul,
+          Representation.trivial_apply] at h
+        simp only [adjointℂ_tmul, lift.tmul, LinearMap.BilinForm.baseChange_tmul,
+          TensorProduct.curry_apply, Representation.IntertwiningMap.toLinearMap_apply, h]
+      | add B B' hB hB' => rw [map_add, tmul_add, map_add, hB, hB', tmul_add, map_add]
+    | add A A' hA hA' => rw [map_add, add_tmul, map_add, hA, hA', add_tmul, map_add]
+
+/-- The contraction is the trace form, `A ⊗ B ↦ tr (A B)`. -/
+lemma adjointℂContr_tmul (A B : Complexification n) :
+    adjointℂContr (A ⊗ₜ B) = (toMatrixℂ A * toMatrixℂ B).trace := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z x =>
+    induction B using TensorProduct.inductionOn with
+    | tmul w y =>
+      change TensorProduct.lift _ ((z ⊗ₜ x) ⊗ₜ (w ⊗ₜ y)) = _
+      rw [lift.tmul, LinearMap.BilinForm.baseChange_tmul, TensorProduct.curry_apply,
+        Representation.IntertwiningMap.toLinearMap_apply, Complex.real_smul,
+        ofReal_adjointContr_tmul, toMatrixℂ_tmul, toMatrixℂ_tmul, Matrix.smul_mul,
+        Matrix.mul_smul, trace_smul, trace_smul, smul_eq_mul, smul_eq_mul]
+      ring
+    | add B B' hB hB' => rw [tmul_add, map_add, hB, hB', map_add, Matrix.mul_add, trace_add]
+  | add A A' hA hA' => rw [add_tmul, map_add, hA, hA', map_add, Matrix.add_mul, trace_add]
+
+lemma adjointℂContr_symm {n} (A B : Complexification n) :
+    adjointℂContr (A ⊗ₜ B) = adjointℂContr (B ⊗ₜ A) := by
+  rw [adjointℂContr_tmul, adjointℂContr_tmul, Matrix.trace_mul_comm]
+
+lemma adjointℂContr_separating_left {n} (A : Complexification n)
+    (hA : ∀ B, adjointℂContr (A ⊗ₜ B) = 0) : A = 0 := by
+  have h := hA (ofTracelessℂ (toMatrixℂ A)ᴴ
+    (by rw [trace_conjTranspose, trace_toMatrixℂ, star_zero]))
+  rw [adjointℂContr_tmul, toMatrixℂ_ofTracelessℂ, trace_mul_conjTranspose_self_eq_zero_iff] at h
+  exact toMatrixℂ_injective (h.trans (map_zero _).symm)
+
+lemma adjointℂContr_separating_right {n} (B : Complexification n)
+    (hB : ∀ A, adjointℂContr (A ⊗ₜ B) = 0) : B = 0 :=
+  adjointℂContr_separating_left B fun A => by rw [adjointℂContr_symm, hB]
+
+/-- The contraction separates the complexification: `B ↦ (A ↦ tr (A B))` is injective. -/
+lemma adjointℂContr_flip_injective :
+    Function.Injective (TensorProduct.curry (adjointℂContr (n := n)).toLinearMap).flip := by
+  intro w w' h
+  refine sub_eq_zero.1 (adjointℂContr_separating_right _ fun A => ?_)
+  have hA := LinearMap.congr_fun h A
+  simp only [LinearMap.flip_apply, TensorProduct.curry_apply] at hA
+  rw [tmul_sub, map_sub, sub_eq_zero]
+  exact hA
+
+end SULieAlgebra
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
index 342c0bf1b6..2006597cd2 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
@@ -26,12 +26,19 @@ This file makes the traceless hermitian matrices into a real Lie algebra with th
 entries in any commutative `*`-ring `R` that is both a real and a complex `*`-algebra, as
 `SULieAlgebra n R`; the Lie algebra `su(n)` itself is `SULieAlgebra n ℂ`.
 
+Sending `z ⊗ x` to the matrix `z x` identifies the complexification `ℂ ⊗[ℝ] su(n)` with the
+traceless complex matrices. The inverse writes a traceless matrix `M` as `ℜ M + i ℑ M`, its real
+and imaginary parts `ℜ M` and `ℑ M` being traceless hermitian.
+
 ## ii. Key results
 
 - `SULieAlgebra n R` : traceless hermitian `n × n` matrices over `R`, as a real Lie algebra.
 - `SULieAlgebra.conj` : the representation `x ↦ U x U†` of the unitary group.
 - `SULieAlgebra.conj_lie` : conjugation by a unitary matrix preserves the bracket.
 - `SULieAlgebra.Complexification n` : the complexification `ℂ ⊗[ℝ] su(n)`.
+- `SULieAlgebra.toMatrixℂ` : the underlying matrix of an element of the complexification.
+- `SULieAlgebra.toMatrixℂ_injective`, `SULieAlgebra.range_toMatrixℂ` : the complexification is
+  the traceless complex matrices.
 
 ## iii. Table of contents
 
@@ -40,6 +47,9 @@ entries in any commutative `*`-ring `R` that is both a real and a complex `*`-al
 - C. The bracket
 - D. Conjugation preserves the bracket
 - E. The complexification
+  - E.1. The underlying matrix of the complexification
+  - E.2. The element with a given traceless matrix
+  - E.3. The injectivity and surjectivity of the matrix map
 
 ## iv. References
 
@@ -49,7 +59,7 @@ entries in any commutative `*`-ring `R` that is both a real and a complex `*`-al
 
 @[expose] public section
 
-open Matrix
+open Matrix TensorProduct ComplexStarModule
 
 /-!
 
@@ -194,8 +204,98 @@ lemma conj_lie (U : unitaryGroup (Fin n) R) (x y : SULieAlgebra n R) :
 
 -/
 
-open TensorProduct in
 /-- The complexification `ℂ ⊗[ℝ] su(n)` of `su(n)`, a complex Lie algebra. -/
 abbrev Complexification (n : ℕ) : Type := ℂ ⊗[ℝ] SULieAlgebra n ℂ
 
+/-!
+
+### E.1. The underlying matrix of the complexification
+
+-/
+
+/-- The underlying matrix of an element of the complexification, `z ⊗ x ↦ z x`. -/
+noncomputable def toMatrixℂ : Complexification n →ₗ[ℂ] Matrix (Fin n) (Fin n) ℂ :=
+  (SULieAlgebra.submodule n ℂ).subtype.liftBaseChange ℂ
+
+@[simp]
+lemma toMatrixℂ_tmul (z : ℂ) (x : SULieAlgebra n ℂ) : toMatrixℂ (z ⊗ₜ x) = z • x.1 := rfl
+
+/-- The underlying matrix of an element of the complexification is traceless. -/
+lemma trace_toMatrixℂ (A : Complexification n) : (toMatrixℂ A).trace = 0 := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z x => rw [toMatrixℂ_tmul, Matrix.trace_smul, x.trace_val_eq_zero, smul_zero]
+  | add A B hA hB => rw [map_add, Matrix.trace_add, hA, hB, add_zero]
+
+/-!
+
+### E.2. The element with a given traceless matrix
+
+-/
+
+/-- The element `1 ⊗ ℜ M + i ⊗ ℑ M` of the complexification with the traceless matrix `M`. -/
+noncomputable def ofTracelessℂ (M : Matrix (Fin n) (Fin n) ℂ) (hM : M.trace = 0) :
+    Complexification n :=
+  1 ⊗ₜ ofMatrix (ℜ M) (selfAdjoint.mem_iff.mp (ℜ M).2) (by
+      simp [realPart_apply_coe, trace_smul, trace_add, star_eq_conjTranspose,
+        trace_conjTranspose, hM]) +
+    Complex.I ⊗ₜ ofMatrix (ℑ M) (selfAdjoint.mem_iff.mp (ℑ M).2) (by
+      simp [imaginaryPart_apply_coe, trace_smul, trace_sub, star_eq_conjTranspose,
+        trace_conjTranspose, hM])
+
+/-- The matrix of `ofTracelessℂ M` is `M = ℜ M + i ℑ M`. -/
+@[simp]
+lemma toMatrixℂ_ofTracelessℂ (M : Matrix (Fin n) (Fin n) ℂ) (hM : M.trace = 0) :
+    toMatrixℂ (ofTracelessℂ M hM) = M := by
+  rw [ofTracelessℂ, map_add, toMatrixℂ_tmul, toMatrixℂ_tmul, one_smul, val_ofMatrix,
+    val_ofMatrix, realPart_add_I_smul_imaginaryPart]
+
+/-- `ofTracelessℂ` is additive. -/
+lemma ofTracelessℂ_add (M N : Matrix (Fin n) (Fin n) ℂ) (hM : M.trace = 0) (hN : N.trace = 0)
+    (hMN : (M + N).trace = 0) :
+    ofTracelessℂ (M + N) hMN = ofTracelessℂ M hM + ofTracelessℂ N hN := by
+  rw [ofTracelessℂ, ofTracelessℂ, ofTracelessℂ, add_add_add_comm, ← tmul_add, ← tmul_add]
+  congr 2 <;> exact Subtype.ext (by simp)
+
+/-- An element of the complexification is recovered from its matrix. -/
+@[simp]
+lemma ofTracelessℂ_toMatrixℂ (A : Complexification n) :
+    ofTracelessℂ (toMatrixℂ A) (trace_toMatrixℂ A) = A := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z x =>
+    have hre : ∀ h₁ h₂, ofMatrix (ℜ (z • x.1)) h₁ h₂ = z.re • x := fun _ _ => Subtype.ext (by
+      simp [realPart_smul, IsSelfAdjoint.coe_realPart x.star_val_eq,
+        IsSelfAdjoint.imaginaryPart x.star_val_eq])
+    have him : ∀ h₁ h₂, ofMatrix (ℑ (z • x.1)) h₁ h₂ = z.im • x := fun _ _ => Subtype.ext (by
+      simp [imaginaryPart_smul, IsSelfAdjoint.coe_realPart x.star_val_eq,
+        IsSelfAdjoint.imaginaryPart x.star_val_eq])
+    rw [ofTracelessℂ]
+    simp only [toMatrixℂ_tmul, hre, him]
+    rw [← smul_tmul, ← smul_tmul, ← add_tmul, Complex.real_smul, Complex.real_smul, mul_one,
+      Complex.re_add_im]
+  | add A B hA hB =>
+    calc _ = ofTracelessℂ (toMatrixℂ A + toMatrixℂ B)
+          (by rw [← map_add]; exact trace_toMatrixℂ _) := by
+          congr 1
+          exact map_add _ _ _
+      _ = A + B := by rw [ofTracelessℂ_add _ _ (trace_toMatrixℂ A) (trace_toMatrixℂ B), hA, hB]
+
+/-!
+
+### E.3. The injectivity and surjectivity of the matrix map
+
+-/
+
+/-- An element of the complexification is determined by its matrix. -/
+lemma toMatrixℂ_injective : Function.Injective (toMatrixℂ (n := n)) := fun A B h => by
+  rw [← ofTracelessℂ_toMatrixℂ A, ← ofTracelessℂ_toMatrixℂ B]
+  congr 1
+
+/-- The matrices of elements of the complexification are exactly the traceless matrices. -/
+lemma range_toMatrixℂ :
+    LinearMap.range (toMatrixℂ (n := n)) = LinearMap.ker (Matrix.traceLinearMap (Fin n) ℂ ℂ) := by
+  ext M
+  rw [LinearMap.mem_range, LinearMap.mem_ker, Matrix.traceLinearMap_apply]
+  exact ⟨fun ⟨A, hA⟩ => hA ▸ trace_toMatrixℂ A,
+    fun hM => ⟨ofTracelessℂ M hM, toMatrixℂ_ofTracelessℂ M hM⟩⟩
+
 end SULieAlgebra

From 57daae4236f84536df644662706ad97220e1fef5 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Oct 2026 09:48:22 +0100
Subject: [PATCH 2/6] feat: More adjoint lemmas

---
 .../SpecialUnitary/LieAlgebra/Adjoint.lean    | 115 +++++++++++++++---
 .../SpecialUnitary/LieAlgebra/Basic.lean      |  38 ++++++
 2 files changed, 136 insertions(+), 17 deletions(-)

diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
index 3f41b3996e..f76640a65d 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
@@ -1,7 +1,7 @@
 /-
 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
+Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith
 -/
 module
 
@@ -10,33 +10,43 @@ public import Mathlib.Analysis.Complex.Basic
 public import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
 public import Mathlib.LinearAlgebra.Matrix.PosDef
 public import Mathlib.RepresentationTheory.Intertwining
+public import Physlib.Meta.Linters.Sorry
 /-!
 
 # The adjoint representation of `SU(n)`
 
+The adjoint representation of `SU(n)` and its complexification, defined as `x ↦ g x g†`.
 ## i. Overview
 
 We define the adjont representation of `SU(n)` on its Lie algebra `su(n)` and its complexification.
-The adjoint is defined by conjugation, `x ↦ g x g†`.
+The adjoint is defined by conjugation, `x ↦ g x g†`. It preserves the bracket, and its kernel is
+the centre of `SU(n)`, the scalar matrices (A).
 
 The contraction `adjointContr` of two real adjoint indices is the trace form `x ⊗ y ↦ tr (x y)` on
 `su(n)`, which is real since `x` and `y` are hermitian, and invariant under the adjoint action by
-the cyclicity of the trace. It is symmetric, and nondegenerate since `tr (x x†) = 0` forces
-`x = 0` (B.1). The contraction `adjointℂContr` of two complex adjoint indices is its
-complexification. On the underlying matrices it is the trace form `A ⊗ B ↦ tr (A B)`, and it is
-again symmetric and nondegenerate (B.2).
+the cyclicity of the trace. It is symmetric, invariant under the bracket, and positive definite
+since `tr (x x) = tr (x x†)` vanishes only for `x = 0` (B.1).
+
+The contraction `adjointℂContr` of two complex adjoint indices is its complexification. On the
+underlying matrices it is the trace form `A ⊗ B ↦ tr (A B)`, and it is again symmetric, invariant
+under the bracket and nondegenerate (B.2).
 
 ## ii. Key results
 
 - `SULieAlgebra.adjoint` : the adjoint representation on `su(n)`.
 - `SULieAlgebra.adjoint_lie` : the adjoint representation preserves the bracket.
+- `SULieAlgebra.adjoint_eq_one_iff` : the kernel of the adjoint representation is the centre.
 - `SULieAlgebra.adjointℂ` : the adjoint representation on the complexification.
 - `SULieAlgebra.adjointℂ_lie` : the complex adjoint representation preserves the bracket.
+- `SULieAlgebra.adjointℂ_eq_one_iff` : the kernel of the complex adjoint representation is the
+  centre.
 - `SULieAlgebra.adjointContr` : the contraction of two real adjoint indices.
-- `SULieAlgebra.adjointContr_flip_injective` : the real contraction is nondegenerate.
+- `SULieAlgebra.adjointContr_lie` : the real contraction is invariant under the bracket.
+- `SULieAlgebra.adjointContr_self_pos` : the real contraction is positive definite.
 - `SULieAlgebra.adjointℂContr` : the contraction of two complex adjoint indices.
 - `SULieAlgebra.toMatrixℂ_adjointℂ` : on matrices the adjoint action is conjugation.
 - `SULieAlgebra.adjointℂContr_tmul` : the contraction is the trace form on matrices.
+- `SULieAlgebra.adjointℂContr_lie` : the complex contraction is invariant under the bracket.
 - `SULieAlgebra.adjointℂContr_flip_injective` : the complex contraction is nondegenerate.
 
 ## iii. Table of contents
@@ -89,6 +99,31 @@ lemma adjoint_lie {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) (x y : SULieAl
     adjoint g ⁅x, y⁆ = ⁅adjoint g x, adjoint g y⁆ :=
   conj_lie _ x y
 
+/-- The kernel of the adjoint representation is the centre of `SU(n)`: `g` acts trivially exactly
+  when it is a scalar matrix `c 1`. -/
+lemma adjoint_eq_one_iff {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) :
+    adjoint g = 1 ↔ ∃ c : ℂ, g.1 = c • 1 := by
+  have hg := (mem_specialUnitaryGroup_iff.mp g.2).1
+  constructor
+  · intro h
+    -- `g x g† = x` for all `x`, so `g` commutes with `su(n)` and hence with every matrix
+    have hx (x : SULieAlgebra n ℂ) : Commute g.1 x.1 := by
+      have hx := congrArg Subtype.val (LinearMap.congr_fun h x)
+      rw [adjoint_val, Module.End.one_apply] at hx
+      calc g.1 * x.1 = g.1 * x.1 * star g.1 * g.1 := by
+            rw [Matrix.mul_assoc _ (star g.1), hg.1, Matrix.mul_one]
+        _ = x.1 * g.1 := by rw [hx]
+    have hcen : g.1 ∈ Set.center (Matrix (Fin n) (Fin n) ℂ) :=
+      Semigroup.mem_center_iff.mpr fun N => (commute_of_forall_commute_val hx N).symm.eq
+    rw [Matrix.center_eq_range] at hcen
+    obtain ⟨c, hc⟩ := hcen
+    exact ⟨c, by rw [← hc, Matrix.scalar_apply, Matrix.smul_one_eq_diagonal]⟩
+  · rintro ⟨c, hc⟩
+    refine LinearMap.ext fun x => Subtype.ext ?_
+    have hcomm : g.1 * x.1 = x.1 * g.1 := by
+      rw [hc, Matrix.smul_mul, Matrix.mul_smul, Matrix.one_mul, Matrix.mul_one]
+    rw [adjoint_val, Module.End.one_apply, hcomm, Matrix.mul_assoc, hg.2, Matrix.mul_one]
+
 /-!
 
 ### A.2. The complex adjoint representation
@@ -123,6 +158,18 @@ lemma adjointℂ_lie {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) (A B : Comp
     rw [add_lie (L := Complexification n), map_add, hA, hA', map_add,
       add_lie (L := Complexification n)]
 
+/-- The kernel of the complex adjoint representation is the centre of `SU(n)`, as for the real
+  adjoint representation. -/
+lemma adjointℂ_eq_one_iff {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) :
+    adjointℂ g = 1 ↔ ∃ c : ℂ, g.1 = c • 1 := by
+  rw [← adjoint_eq_one_iff]
+  refine ⟨fun h => LinearMap.ext fun x => Subtype.ext ?_, fun h => ?_⟩
+  · have hx := congrArg toMatrixℂ (LinearMap.congr_fun h (1 ⊗ₜ x))
+    rwa [adjointℂ_tmul, Module.End.one_apply, toMatrixℂ_tmul, toMatrixℂ_tmul, one_smul,
+      one_smul] at hx
+  · change Module.End.baseChangeHom ℝ ℂ _ (adjoint g) = 1
+    rw [h, map_one]
+
 /-- The adjoint representation conjugates the matrix, `M ↦ g M g†`. -/
 @[simp]
 lemma toMatrixℂ_adjointℂ {n} (g : specialUnitaryGroup (Fin n) ℂ) (A : Complexification n) :
@@ -170,6 +217,12 @@ noncomputable def adjointContr {n : ℕ} : ((adjoint (n := n)).tprod adjoint).In
 lemma adjointContr_tmul {n : ℕ} (x y : SULieAlgebra n ℂ) :
     adjointContr (x ⊗ₜ y) = (x.1 * y.1).trace.re := rfl
 
+/-- The adjoint representation preserves the real contraction, so `SU(n)` acts on `su(n)` by
+  isometries. -/
+lemma adjointContr_adjoint {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) (x y : SULieAlgebra n ℂ) :
+    adjointContr (adjoint g x ⊗ₜ adjoint g y) = adjointContr (x ⊗ₜ y) :=
+  Representation.IntertwiningMap.isIntertwining _ _ adjointContr g (x ⊗ₜ y)
+
 /-- The trace `tr (x y)` of two elements of `su(n)` is real, equal to their contraction. -/
 lemma ofReal_adjointContr_tmul {n : ℕ} (x y : SULieAlgebra n ℂ) :
     (adjointContr (x ⊗ₜ y) : ℂ) = (x.1 * y.1).trace := by
@@ -183,12 +236,35 @@ lemma adjointContr_symm {n : ℕ} (x y : SULieAlgebra n ℂ) :
     adjointContr (x ⊗ₜ y) = adjointContr (y ⊗ₜ x) := by
   rw [adjointContr_tmul, adjointContr_tmul, trace_mul_comm]
 
+/-- The real contraction is invariant under the bracket, `tr (⁅x, y⁆ z) = tr (x ⁅y, z⁆)`; in terms
+  of generators, the structure constants `tr (T^a ⁅T^b, T^c⁆)` are totally antisymmetric. -/
+lemma adjointContr_lie {n : ℕ} (x y z : SULieAlgebra n ℂ) :
+    adjointContr (⁅x, y⁆ ⊗ₜ z) = adjointContr (x ⊗ₜ ⁅y, z⁆) := by
+  rw [adjointContr_tmul, adjointContr_tmul, val_bracket, val_bracket, Matrix.smul_mul,
+    Matrix.mul_smul, trace_smul, trace_smul, sub_mul, mul_sub, trace_sub, trace_sub,
+    Matrix.mul_assoc, Matrix.mul_assoc, trace_mul_comm y.1 (x.1 * z.1), Matrix.mul_assoc]
+
+/-- The real contraction is positive semidefinite: `tr (x x) = tr (x x†) ≥ 0`. -/
+lemma adjointContr_self_nonneg {n : ℕ} (x : SULieAlgebra n ℂ) : 0 ≤ adjointContr (x ⊗ₜ x) := by
+  have h := (posSemidef_self_mul_conjTranspose x.1).trace_nonneg
+  rw [← star_eq_conjTranspose, x.star_val_eq, ← ofReal_adjointContr_tmul] at h
+  exact Complex.zero_le_real.mp h
+
+/-- The real contraction of `x` with itself vanishes only for `x = 0`. -/
+lemma adjointContr_self_eq_zero_iff {n : ℕ} (x : SULieAlgebra n ℂ) :
+    adjointContr (x ⊗ₜ x) = 0 ↔ x = 0 := by
+  refine ⟨fun hx => Subtype.ext (trace_mul_conjTranspose_self_eq_zero_iff.mp ?_),
+    fun hx => by rw [hx, zero_tmul, map_zero]⟩
+  rw [← star_eq_conjTranspose, x.star_val_eq, ← ofReal_adjointContr_tmul, hx, Complex.ofReal_zero]
+
+/-- The real contraction is positive definite, making it an inner product on `su(n)`. -/
+lemma adjointContr_self_pos {n : ℕ} {x : SULieAlgebra n ℂ} (hx : x ≠ 0) :
+    0 < adjointContr (x ⊗ₜ x) :=
+  (adjointContr_self_nonneg x).lt_of_ne fun h => hx ((adjointContr_self_eq_zero_iff x).mp h.symm)
+
 lemma adjointContr_separating_left {n : ℕ} (x : SULieAlgebra n ℂ)
-    (hx : ∀ y, adjointContr (x ⊗ₜ y) = 0) : x = 0 := by
-  have h : (x.1 * x.1ᴴ).trace = 0 := by
-    rw [← star_eq_conjTranspose, x.star_val_eq, ← ofReal_adjointContr_tmul, hx,
-      Complex.ofReal_zero]
-  exact Subtype.ext (trace_mul_conjTranspose_self_eq_zero_iff.mp h)
+    (hx : ∀ y, adjointContr (x ⊗ₜ y) = 0) : x = 0 :=
+  (adjointContr_self_eq_zero_iff x).mp (hx x)
 
 lemma adjointContr_separating_right {n : ℕ} (y : SULieAlgebra n ℂ)
     (hy : ∀ x, adjointContr (x ⊗ₜ y) = 0) : y = 0 :=
@@ -223,12 +299,9 @@ noncomputable def adjointℂContr {n : ℕ} : ((adjointℂ (n := n)).tprod adjoi
     | tmul z x =>
       induction B using TensorProduct.inductionOn with
       | tmul w y =>
-        have h := Representation.IntertwiningMap.isIntertwining _ _ (adjointContr (n := n)) g
-          (x ⊗ₜ y)
-        simp only [Representation.tprod_apply, TensorProduct.map_tmul,
-          Representation.trivial_apply] at h
         simp only [adjointℂ_tmul, lift.tmul, LinearMap.BilinForm.baseChange_tmul,
-          TensorProduct.curry_apply, Representation.IntertwiningMap.toLinearMap_apply, h]
+          TensorProduct.curry_apply, Representation.IntertwiningMap.toLinearMap_apply,
+          adjointContr_adjoint]
       | add B B' hB hB' => rw [map_add, tmul_add, map_add, hB, hB', tmul_add, map_add]
     | add A A' hA hA' => rw [map_add, add_tmul, map_add, hA, hA', add_tmul, map_add]
 
@@ -252,6 +325,14 @@ lemma adjointℂContr_symm {n} (A B : Complexification n) :
     adjointℂContr (A ⊗ₜ B) = adjointℂContr (B ⊗ₜ A) := by
   rw [adjointℂContr_tmul, adjointℂContr_tmul, Matrix.trace_mul_comm]
 
+/-- The complex contraction is invariant under the bracket, `tr (⁅A, B⁆ C) = tr (A ⁅B, C⁆)`. -/
+lemma adjointℂContr_lie {n} (A B C : Complexification n) :
+    adjointℂContr (⁅A, B⁆ ⊗ₜ C) = adjointℂContr (A ⊗ₜ ⁅B, C⁆) := by
+  rw [adjointℂContr_tmul, adjointℂContr_tmul, toMatrixℂ_lie, toMatrixℂ_lie, Matrix.smul_mul,
+    Matrix.mul_smul, trace_smul, trace_smul, sub_mul, mul_sub, trace_sub, trace_sub,
+    Matrix.mul_assoc, Matrix.mul_assoc, trace_mul_comm (toMatrixℂ B) (toMatrixℂ A * toMatrixℂ C),
+    Matrix.mul_assoc]
+
 lemma adjointℂContr_separating_left {n} (A : Complexification n)
     (hA : ∀ B, adjointℂContr (A ⊗ₜ B) = 0) : A = 0 := by
   have h := hA (ofTracelessℂ (toMatrixℂ A)ᴴ
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
index 2006597cd2..4c2a25035b 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
@@ -37,6 +37,7 @@ and imaginary parts `ℜ M` and `ℑ M` being traceless hermitian.
 - `SULieAlgebra.conj_lie` : conjugation by a unitary matrix preserves the bracket.
 - `SULieAlgebra.Complexification n` : the complexification `ℂ ⊗[ℝ] su(n)`.
 - `SULieAlgebra.toMatrixℂ` : the underlying matrix of an element of the complexification.
+- `SULieAlgebra.toMatrixℂ_lie` : the matrix of a bracket is `i` times the commutator.
 - `SULieAlgebra.toMatrixℂ_injective`, `SULieAlgebra.range_toMatrixℂ` : the complexification is
   the traceless complex matrices.
 
@@ -226,6 +227,27 @@ lemma trace_toMatrixℂ (A : Complexification n) : (toMatrixℂ A).trace = 0 :=
   | tmul z x => rw [toMatrixℂ_tmul, Matrix.trace_smul, x.trace_val_eq_zero, smul_zero]
   | add A B hA hB => rw [map_add, Matrix.trace_add, hA, hB, add_zero]
 
+/-- The matrix of a bracket is `i` times the commutator of the matrices, `[A, B] ↦ i (A B - B A)`,
+  as in `su(n)` itself. -/
+lemma toMatrixℂ_lie (A B : Complexification n) :
+    toMatrixℂ ⁅A, B⁆ = Complex.I • (toMatrixℂ A * toMatrixℂ B - toMatrixℂ B * toMatrixℂ A) := by
+  induction A using TensorProduct.inductionOn with
+  | tmul z x =>
+    induction B using TensorProduct.inductionOn with
+    | tmul w y =>
+      rw [LieAlgebra.ExtendScalars.bracket_tmul, toMatrixℂ_tmul, toMatrixℂ_tmul, toMatrixℂ_tmul,
+        val_bracket]
+      simp only [Matrix.smul_mul, Matrix.mul_smul]
+      module
+    | add B B' hB hB' =>
+      rw [lie_add (L := Complexification n), map_add, hB, hB', map_add, Matrix.mul_add,
+        Matrix.add_mul]
+      module
+  | add A A' hA hA' =>
+    rw [add_lie (L := Complexification n), map_add, hA, hA', map_add, Matrix.mul_add,
+      Matrix.add_mul]
+    module
+
 /-!
 
 ### E.2. The element with a given traceless matrix
@@ -298,4 +320,20 @@ lemma range_toMatrixℂ :
   exact ⟨fun ⟨A, hA⟩ => hA ▸ trace_toMatrixℂ A,
     fun hM => ⟨ofTracelessℂ M hM, toMatrixℂ_ofTracelessℂ M hM⟩⟩
 
+/-- A matrix commuting with every element of `su(n)` commutes with every matrix: it commutes with
+  the traceless matrices, which `su(n)` spans over `ℂ`, and with the identity. -/
+lemma commute_of_forall_commute_val {M : Matrix (Fin n) (Fin n) ℂ}
+    (h : ∀ x : SULieAlgebra n ℂ, Commute M x.1) (N : Matrix (Fin n) (Fin n) ℂ) : Commute M N := by
+  have hA (A : Complexification n) : Commute M (toMatrixℂ A) := by
+    induction A using TensorProduct.inductionOn with
+    | tmul z x => exact toMatrixℂ_tmul z x ▸ (h x).smul_right z
+    | add A B hA hB => exact map_add toMatrixℂ A B ▸ hA.add_right hB
+  rcases Nat.eq_zero_or_pos n with rfl | hn
+  · exact Subsingleton.elim (M * N) (N * M)
+  have hN : (N - (N.trace / n) • (1 : Matrix (Fin n) (Fin n) ℂ)).trace = 0 := by
+    rw [Matrix.trace_sub, Matrix.trace_smul, Matrix.trace_one, Fintype.card_fin, smul_eq_mul,
+      div_mul_cancel₀ _ (by exact_mod_cast hn.ne'), sub_self]
+  have h1 := toMatrixℂ_ofTracelessℂ _ hN ▸ hA (ofTracelessℂ _ hN)
+  simpa using h1.add_right ((Commute.one_right M).smul_right (N.trace / n))
+
 end SULieAlgebra

From 88c2ee966efc0eb6eab42acca66b0a75a9ca9844 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Oct 2026 09:49:36 +0100
Subject: [PATCH 3/6] Update Basic.lean

---
 .../Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
index 4c2a25035b..64794f660f 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
@@ -320,6 +320,12 @@ lemma range_toMatrixℂ :
   exact ⟨fun ⟨A, hA⟩ => hA ▸ trace_toMatrixℂ A,
     fun hM => ⟨ofTracelessℂ M hM, toMatrixℂ_ofTracelessℂ M hM⟩⟩
 
+/-!
+
+### E.4. Commuting with all elements of `su(n)`
+
+-/
+
 /-- A matrix commuting with every element of `su(n)` commutes with every matrix: it commutes with
   the traceless matrices, which `su(n)` spans over `ℂ`, and with the identity. -/
 lemma commute_of_forall_commute_val {M : Matrix (Fin n) (Fin n) ℂ}

From abe13da5f75ed337cef478c622453ccbae7edce4 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Oct 2026 11:11:07 +0100
Subject: [PATCH 4/6] feat: Add results

---
 .../SpecialUnitary/LieAlgebra/Adjoint.lean    | 91 ++++++++++++++++---
 .../SpecialUnitary/LieAlgebra/Basic.lean      | 34 ++++++-
 2 files changed, 108 insertions(+), 17 deletions(-)

diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
index f76640a65d..275e57c6a2 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
@@ -5,17 +5,17 @@ Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith
 -/
 module
 
-public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Basic
 public import Mathlib.Analysis.Complex.Basic
 public import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
 public import Mathlib.LinearAlgebra.Matrix.PosDef
 public import Mathlib.RepresentationTheory.Intertwining
-public import Physlib.Meta.Linters.Sorry
+public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Basic
 /-!
 
 # The adjoint representation of `SU(n)`
 
 The adjoint representation of `SU(n)` and its complexification, defined as `x ↦ g x g†`.
+
 ## i. Overview
 
 We define the adjont representation of `SU(n)` on its Lie algebra `su(n)` and its complexification.
@@ -34,20 +34,12 @@ under the bracket and nondegenerate (B.2).
 ## ii. Key results
 
 - `SULieAlgebra.adjoint` : the adjoint representation on `su(n)`.
-- `SULieAlgebra.adjoint_lie` : the adjoint representation preserves the bracket.
-- `SULieAlgebra.adjoint_eq_one_iff` : the kernel of the adjoint representation is the centre.
 - `SULieAlgebra.adjointℂ` : the adjoint representation on the complexification.
-- `SULieAlgebra.adjointℂ_lie` : the complex adjoint representation preserves the bracket.
-- `SULieAlgebra.adjointℂ_eq_one_iff` : the kernel of the complex adjoint representation is the
-  centre.
+- `SULieAlgebra.adjoint_eq_iff` : the adjoint representation is faithful modulo the centre.
 - `SULieAlgebra.adjointContr` : the contraction of two real adjoint indices.
-- `SULieAlgebra.adjointContr_lie` : the real contraction is invariant under the bracket.
-- `SULieAlgebra.adjointContr_self_pos` : the real contraction is positive definite.
 - `SULieAlgebra.adjointℂContr` : the contraction of two complex adjoint indices.
-- `SULieAlgebra.toMatrixℂ_adjointℂ` : on matrices the adjoint action is conjugation.
-- `SULieAlgebra.adjointℂContr_tmul` : the contraction is the trace form on matrices.
-- `SULieAlgebra.adjointℂContr_lie` : the complex contraction is invariant under the bracket.
-- `SULieAlgebra.adjointℂContr_flip_injective` : the complex contraction is nondegenerate.
+- `SULieAlgebra.adjointContr_self_pos` : the real contraction is positive definite.
+- `SULieAlgebra.adjointℂContr_nondegenerate` : the complex contraction is nondegenerate.
 
 ## iii. Table of contents
 
@@ -124,6 +116,23 @@ lemma adjoint_eq_one_iff {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) :
       rw [hc, Matrix.smul_mul, Matrix.mul_smul, Matrix.one_mul, Matrix.mul_one]
     rw [adjoint_val, Module.End.one_apply, hcomm, Matrix.mul_assoc, hg.2, Matrix.mul_one]
 
+/-- Two elements of `SU(n)` have the same adjoint action exactly when they differ by a scalar:
+  the adjoint representation is faithful on `SU(n)` modulo its centre. -/
+lemma adjoint_eq_iff {n : ℕ} (g h : specialUnitaryGroup (Fin n) ℂ) :
+    adjoint g = adjoint h ↔ ∃ c : ℂ, g.1 = c • h.1 := by
+  have hh := (mem_specialUnitaryGroup_iff.mp h.2).1
+  have hval : (g * h⁻¹).1 = g.1 * star h.1 := rfl
+  have key : adjoint g = adjoint h ↔ adjoint (g * h⁻¹) = 1 := by
+    constructor
+    · intro hgh
+      rw [map_mul, hgh, ← map_mul, mul_inv_cancel, map_one]
+    · intro h1
+      rw [← one_mul (adjoint h), ← h1, ← map_mul, inv_mul_cancel_right]
+  rw [key, adjoint_eq_one_iff, hval]
+  refine exists_congr fun c => ⟨fun hc => ?_, fun hc => ?_⟩
+  · rw [← Matrix.mul_one g.1, ← hh.1, ← Matrix.mul_assoc, hc, Matrix.smul_mul, Matrix.one_mul]
+  · rw [hc, Matrix.smul_mul, hh.2]
+
 /-!
 
 ### A.2. The complex adjoint representation
@@ -170,6 +179,17 @@ lemma adjointℂ_eq_one_iff {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ) :
   · change Module.End.baseChangeHom ℝ ℂ _ (adjoint g) = 1
     rw [h, map_one]
 
+/-- Two elements of `SU(n)` have the same complex adjoint action exactly when they differ by a
+  scalar, as for the real adjoint representation. -/
+lemma adjointℂ_eq_iff {n : ℕ} (g h : specialUnitaryGroup (Fin n) ℂ) :
+    adjointℂ g = adjointℂ h ↔ ∃ c : ℂ, g.1 = c • h.1 := by
+  rw [← adjoint_eq_iff]
+  refine ⟨fun hgh => LinearMap.ext fun x => Subtype.ext ?_, fun hgh => ?_⟩
+  · have hx := congrArg toMatrixℂ (LinearMap.congr_fun hgh (1 ⊗ₜ x))
+    rwa [adjointℂ_tmul, adjointℂ_tmul, toMatrixℂ_tmul, toMatrixℂ_tmul, one_smul, one_smul] at hx
+  · change Module.End.baseChangeHom ℝ ℂ _ (adjoint g) = Module.End.baseChangeHom ℝ ℂ _ (adjoint h)
+    rw [hgh]
+
 /-- The adjoint representation conjugates the matrix, `M ↦ g M g†`. -/
 @[simp]
 lemma toMatrixℂ_adjointℂ {n} (g : specialUnitaryGroup (Fin n) ℂ) (A : Complexification n) :
@@ -180,6 +200,15 @@ lemma toMatrixℂ_adjointℂ {n} (g : specialUnitaryGroup (Fin n) ℂ) (A : Comp
       Matrix.smul_mul]
   | add A B hA hB => rw [map_add, map_add, hA, hB, map_add, Matrix.mul_add, Matrix.add_mul]
 
+/-- The adjoint action of a diagonal element of `SU(n)` scales the entry at `(x, y)` of the
+  matrix by `d x * star (d y)`. -/
+lemma toMatrixℂ_adjointℂ_apply_of_diagonal {n} {g : specialUnitaryGroup (Fin n) ℂ}
+    {d : Fin n → ℂ} (hg : g.1 = diagonal d) (A : Complexification n) (x y : Fin n) :
+    toMatrixℂ (adjointℂ g A) x y = d x * star (d y) * toMatrixℂ A x y := by
+  rw [toMatrixℂ_adjointℂ, hg, star_eq_conjTranspose, diagonal_conjTranspose, mul_diagonal,
+    diagonal_mul, Pi.star_apply]
+  ring
+
 lemma toMatrixℂ_adjointℂ_trace {n} (g : specialUnitaryGroup (Fin n) ℂ) (A : Complexification n) :
     (toMatrixℂ (adjointℂ g A)).trace = (toMatrixℂ A).trace := by
   rw [toMatrixℂ_adjointℂ, Matrix.trace_mul_cycle, Matrix.trace_mul_cycle, Matrix.mul_assoc,
@@ -280,6 +309,16 @@ lemma adjointContr_flip_injective {n : ℕ} :
   rw [tmul_sub, map_sub, sub_eq_zero]
   exact hx
 
+/-- The real contraction, as a bilinear form, is symmetric. -/
+lemma adjointContr_isSymm {n : ℕ} :
+    LinearMap.BilinForm.IsSymm (TensorProduct.curry (adjointContr (n := n)).toLinearMap) :=
+  ⟨fun x y => adjointContr_symm x y⟩
+
+/-- The real contraction, as a bilinear form, is nondegenerate. -/
+lemma adjointContr_nondegenerate {n : ℕ} :
+    (TensorProduct.curry (adjointContr (n := n)).toLinearMap).Nondegenerate :=
+  ⟨fun x hx => adjointContr_separating_left x hx, fun y hy => adjointContr_separating_right y hy⟩
+
 /-!
 
 ### B.2. The complex case
@@ -305,6 +344,14 @@ noncomputable def adjointℂContr {n : ℕ} : ((adjointℂ (n := n)).tprod adjoi
       | add B B' hB hB' => rw [map_add, tmul_add, map_add, hB, hB', tmul_add, map_add]
     | add A A' hA hA' => rw [map_add, add_tmul, map_add, hA, hA', add_tmul, map_add]
 
+/-- The adjoint representation preserves the complex contraction. -/
+lemma adjointℂContr_adjointℂ {n : ℕ} (g : specialUnitaryGroup (Fin n) ℂ)
+    (A B : Complexification n) :
+    adjointℂContr (adjointℂ g A ⊗ₜ adjointℂ g B) = adjointℂContr (A ⊗ₜ B) := by
+  have h := Representation.IntertwiningMap.isIntertwining _ _ (adjointℂContr (n := n)) g (A ⊗ₜ B)
+  simpa only [Representation.tprod_apply, TensorProduct.map_tmul, Representation.trivial_apply]
+    using h
+
 /-- The contraction is the trace form, `A ⊗ B ↦ tr (A B)`. -/
 lemma adjointℂContr_tmul (A B : Complexification n) :
     adjointℂContr (A ⊗ₜ B) = (toMatrixℂ A * toMatrixℂ B).trace := by
@@ -321,6 +368,13 @@ lemma adjointℂContr_tmul (A B : Complexification n) :
     | add B B' hB hB' => rw [tmul_add, map_add, hB, hB', map_add, Matrix.mul_add, trace_add]
   | add A A' hA hA' => rw [add_tmul, map_add, hA, hA', map_add, Matrix.add_mul, trace_add]
 
+/-- On the real elements `1 ⊗ x` of the complexification the complex contraction is the real
+  contraction, so the two agree on real gauge fields. -/
+lemma adjointℂContr_one_tmul {n : ℕ} (x y : SULieAlgebra n ℂ) :
+    adjointℂContr ((1 ⊗ₜ x) ⊗ₜ (1 ⊗ₜ y)) = adjointContr (x ⊗ₜ y) := by
+  rw [adjointℂContr_tmul, toMatrixℂ_tmul, toMatrixℂ_tmul, one_smul, one_smul,
+    ofReal_adjointContr_tmul]
+
 lemma adjointℂContr_symm {n} (A B : Complexification n) :
     adjointℂContr (A ⊗ₜ B) = adjointℂContr (B ⊗ₜ A) := by
   rw [adjointℂContr_tmul, adjointℂContr_tmul, Matrix.trace_mul_comm]
@@ -354,4 +408,15 @@ lemma adjointℂContr_flip_injective :
   rw [tmul_sub, map_sub, sub_eq_zero]
   exact hA
 
+/-- The complex contraction, as a bilinear form, is symmetric. -/
+lemma adjointℂContr_isSymm {n : ℕ} :
+    LinearMap.BilinForm.IsSymm (TensorProduct.curry (adjointℂContr (n := n)).toLinearMap) :=
+  ⟨fun A B => adjointℂContr_symm A B⟩
+
+/-- The complex contraction, as a bilinear form, is nondegenerate. -/
+lemma adjointℂContr_nondegenerate {n : ℕ} :
+    (TensorProduct.curry (adjointℂContr (n := n)).toLinearMap).Nondegenerate :=
+  ⟨fun A hA => adjointℂContr_separating_left A hA,
+    fun B hB => adjointℂContr_separating_right B hB⟩
+
 end SULieAlgebra
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
index 64794f660f..3059bc9faf 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
@@ -5,13 +5,11 @@ Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith
 -/
 module
 
-public import Mathlib.Algebra.Lie.Basic
 public import Mathlib.Algebra.Lie.BaseChange
-public import Mathlib.Algebra.Star.SelfAdjoint
-public import Mathlib.LinearAlgebra.Matrix.Trace
+public import Mathlib.LinearAlgebra.Complex.Module
+public import Mathlib.LinearAlgebra.Matrix.FiniteDimensional
 public import Mathlib.LinearAlgebra.UnitaryGroup
 public import Mathlib.RepresentationTheory.Basic
-public import Mathlib.LinearAlgebra.Complex.Module
 /-!
 
 # The Lie algebra `su(n)` in the hermitian presentation
@@ -40,6 +38,8 @@ and imaginary parts `ℜ M` and `ℑ M` being traceless hermitian.
 - `SULieAlgebra.toMatrixℂ_lie` : the matrix of a bracket is `i` times the commutator.
 - `SULieAlgebra.toMatrixℂ_injective`, `SULieAlgebra.range_toMatrixℂ` : the complexification is
   the traceless complex matrices.
+- `SULieAlgebra.finrank_eq`, `SULieAlgebra.finrank_complexification` : `su(n)` and its
+  complexification have dimension `n² - 1`.
 
 ## iii. Table of contents
 
@@ -51,6 +51,8 @@ and imaginary parts `ℜ M` and `ℑ M` being traceless hermitian.
   - E.1. The underlying matrix of the complexification
   - E.2. The element with a given traceless matrix
   - E.3. The injectivity and surjectivity of the matrix map
+  - E.4. Commuting with all elements of `su(n)`
+- F. The dimension
 
 ## iv. References
 
@@ -342,4 +344,28 @@ lemma commute_of_forall_commute_val {M : Matrix (Fin n) (Fin n) ℂ}
   have h1 := toMatrixℂ_ofTracelessℂ _ hN ▸ hA (ofTracelessℂ _ hN)
   simpa using h1.add_right ((Commute.one_right M).smul_right (N.trace / n))
 
+/-!
+
+## F. The dimension
+
+-/
+
+/-- The complexification `ℂ ⊗[ℝ] su(n)` has complex dimension `n² - 1`: it is the traceless
+  matrices, and the trace is onto. -/
+lemma finrank_complexification : Module.finrank ℂ (Complexification n) = n ^ 2 - 1 := by
+  rw [← LinearMap.finrank_range_of_inj toMatrixℂ_injective, range_toMatrixℂ]
+  rcases Nat.eq_zero_or_pos n with rfl | hn
+  · exact Module.finrank_zero_of_subsingleton
+  have hsurj : LinearMap.range (Matrix.traceLinearMap (Fin n) ℂ ℂ) = ⊤ :=
+    LinearMap.range_eq_top.2 fun c => ⟨single ⟨0, hn⟩ ⟨0, hn⟩ c, by simp⟩
+  have h := LinearMap.finrank_range_add_finrank_ker (Matrix.traceLinearMap (Fin n) ℂ ℂ)
+  rw [hsurj, finrank_top, Module.finrank_matrix, Fintype.card_fin, Module.finrank_self] at h
+  rw [sq]
+  omega
+
+/-- `su(n)` has real dimension `n² - 1`, the dimension of its complexification. -/
+lemma finrank_eq : Module.finrank ℝ (SULieAlgebra n ℂ) = n ^ 2 - 1 := by
+  rw [← Module.finrank_baseChange (R := ℂ)]
+  exact finrank_complexification
+
 end SULieAlgebra

From 8f7cb85fc3e545d3d0e5c6bf06985540520b2571 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 6 Oct 2026 11:45:47 +0100
Subject: [PATCH 5/6] feat: Add relation to killing forms

---
 .../SpecialUnitary/LieAlgebra/Adjoint.lean    | 73 ++++++++++++++++++-
 1 file changed, 71 insertions(+), 2 deletions(-)

diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
index 275e57c6a2..12de8cf0af 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
@@ -5,8 +5,9 @@ Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith
 -/
 module
 
+public import Mathlib.Algebra.Lie.TraceForm
 public import Mathlib.Analysis.Complex.Basic
-public import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
+public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.LinearAlgebra.Matrix.PosDef
 public import Mathlib.RepresentationTheory.Intertwining
 public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Basic
@@ -40,6 +41,8 @@ under the bracket and nondegenerate (B.2).
 - `SULieAlgebra.adjointℂContr` : the contraction of two complex adjoint indices.
 - `SULieAlgebra.adjointContr_self_pos` : the real contraction is positive definite.
 - `SULieAlgebra.adjointℂContr_nondegenerate` : the complex contraction is nondegenerate.
+- `SULieAlgebra.adjointContr_eq_killingForm` : the contraction is `-1 / (2n)` times the Killing
+  form.
 
 ## iii. Table of contents
 
@@ -49,6 +52,7 @@ under the bracket and nondegenerate (B.2).
 - B. The contraction of adjoint indices
   - B.1. The real case
   - B.2. The complex case
+  - B.3. The Killing form
 
 ## iv. References
 
@@ -58,7 +62,7 @@ under the bracket and nondegenerate (B.2).
 
 @[expose] public section
 
-open Matrix TensorProduct ComplexStarModule
+open Matrix TensorProduct ComplexStarModule Kronecker LieAlgebra
 open scoped ComplexOrder
 
 namespace SULieAlgebra
@@ -419,4 +423,69 @@ lemma adjointℂContr_nondegenerate {n : ℕ} :
   ⟨fun A hA => adjointℂContr_separating_left A hA,
     fun B hB => adjointℂContr_separating_right B hB⟩
 
+/-!
+
+### B.3. The Killing form
+
+-/
+
+/-- The contraction is the Killing form on the complexified Lie
+  algebra, up to a factor of `-1/(2n)`. -/
+lemma adjointℂContr_eq_killingForm {n : ℕ} (A B : Complexification n) :
+    adjointℂContr (A ⊗ₜ B) = -(1 / (2 * (n : ℂ))) * killingForm ℂ (Complexification n) A B := by
+  set K : Matrix (Fin n × Fin n) (Fin n × Fin n) ℂ :=
+    -(1 ⊗ₖ (toMatrixℂ A * toMatrixℂ B) - (toMatrixℂ B)ᵀ ⊗ₖ toMatrixℂ A
+      - (toMatrixℂ A)ᵀ ⊗ₖ toMatrixℂ B + (toMatrixℂ B * toMatrixℂ A)ᵀ ⊗ₖ 1)
+  let e : Matrix (Fin n) (Fin n) ℂ ≃ₗ[ℂ] (Fin n × Fin n → ℂ) :=
+    LinearEquiv.ofBijective ⟨⟨vec, vec_add⟩, vec_smul⟩ vec_bijective
+  set F := e.symm.conj (toLin' K)
+  have hF (M : Matrix (Fin n) (Fin n) ℂ) :
+      F M = -(toMatrixℂ A * (toMatrixℂ B * M - M * toMatrixℂ B)
+        - (toMatrixℂ B * M - M * toMatrixℂ B) * toMatrixℂ A) := by
+    apply e.injective
+    simp only [F, e, LinearEquiv.conj_apply, LinearMap.comp_apply, LinearEquiv.coe_coe,
+      LinearEquiv.symm_symm, LinearEquiv.apply_symm_apply, LinearEquiv.ofBijective_apply,
+      LinearMap.coe_mk, AddHom.coe_mk, toLin'_apply, K, neg_mulVec, sub_mulVec, add_mulVec,
+      kronecker_mulVec_vec, transpose_transpose, transpose_one, Matrix.mul_one, Matrix.one_mul,
+      ← vec_sub, ← vec_add, ← vec_neg]
+    congr 1
+    noncomm_ring
+  have h1 : toMatrixℂ ∘ₗ (ad ℂ (Complexification n) A ∘ₗ ad ℂ (Complexification n) B)
+      = F ∘ₗ toMatrixℂ := by
+    refine LinearMap.ext fun M => ?_
+    simp only [LinearMap.comp_apply, ad_apply, toMatrixℂ_lie, hF, Matrix.mul_smul,
+      Matrix.smul_mul, ← smul_sub, smul_smul, Complex.I_mul_I, neg_one_smul]
+  obtain ⟨π, hπ⟩ := LinearMap.exists_leftInverse_of_injective toMatrixℂ
+    (LinearMap.ker_eq_bot.2 toMatrixℂ_injective)
+  have h2 : (toMatrixℂ ∘ₗ π) ∘ₗ F = F := by
+    refine LinearMap.ext fun M => ?_
+    have hM : (F M).trace = 0 := by
+      rw [hF, trace_neg, trace_sub, trace_mul_comm, sub_self, neg_zero]
+    rw [LinearMap.comp_apply, LinearMap.comp_apply, ← toMatrixℂ_ofTracelessℂ (F M) hM,
+      ← LinearMap.comp_apply π, hπ, LinearMap.id_apply]
+  have hK : killingForm ℂ (Complexification n) A B = -(2 * n) * adjointℂContr (A ⊗ₜ B) := by
+    rw [killingForm_apply_apply, ← LinearMap.id_comp (ad ℂ (Complexification n) A ∘ₗ _), ← hπ,
+      LinearMap.comp_assoc, h1, LinearMap.trace_comp_comm', LinearMap.comp_assoc,
+      ← Module.End.mul_eq_comp, LinearMap.trace_mul_comm, Module.End.mul_eq_comp, h2,
+      adjointℂContr_tmul]
+    simp only [F, LinearMap.trace_conj', trace_toLin'_eq, K, trace_neg, trace_sub, trace_add,
+      trace_kronecker, trace_one, trace_transpose, trace_toMatrixℂ, Fintype.card_fin, mul_zero,
+      trace_mul_comm (toMatrixℂ B)]
+    ring
+  rw [hK]
+  rcases Nat.eq_zero_or_pos n with rfl | hn
+  · simp [adjointℂContr_tmul, Matrix.trace]
+  · have : (n : ℂ) ≠ 0 := by exact_mod_cast hn.ne'
+    field_simp
+
+/-- The contraction is the Killing form on the Lie algebra, up to a factor of `-1/(2n)`. -/
+lemma adjointContr_eq_killingForm {n : ℕ} (x y : SULieAlgebra n ℂ) :
+    adjointContr (x ⊗ₜ y) = -(1 / (2 * (n : ℝ))) * killingForm ℝ (SULieAlgebra n ℂ) x y := by
+  have h := adjointℂContr_eq_killingForm (1 ⊗ₜ x) (1 ⊗ₜ y)
+  rw [adjointℂContr_one_tmul, killingForm, LieModule.traceForm_baseChange,
+    LinearMap.BilinForm.baseChange_tmul, mul_one, Complex.real_smul, mul_one] at h
+  apply Complex.ofReal_injective
+  push_cast
+  exact h
+
 end SULieAlgebra

From 53a3519bb962f79aca8d92e3a9a1394938c685d0 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 7 Oct 2026 06:54:02 +0100
Subject: [PATCH 6/6] refactor: Address review comments

---
 Physlib.lean                                  |   1 +
 .../SpecialUnitary/LieAlgebra/Adjoint.lean    |  72 +-----------
 .../SpecialUnitary/LieAlgebra/Basic.lean      |  31 ++++-
 .../LieAlgebra/KillingForm.lean               | 107 ++++++++++++++++++
 4 files changed, 140 insertions(+), 71 deletions(-)
 create mode 100644 Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/KillingForm.lean

diff --git a/Physlib.lean b/Physlib.lean
index efdb2cc98f..1b82405029 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -141,6 +141,7 @@ public import Physlib.Mathematics.ForMathlib.Trigonometry.Tanh
 public import Physlib.Mathematics.Groups.SO3.Basic
 public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Adjoint
 public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Basic
+public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.KillingForm
 public import Physlib.Mathematics.InnerProductSpace.Adjoint
 public import Physlib.Mathematics.InnerProductSpace.Basic
 public import Physlib.Mathematics.InnerProductSpace.Calculus
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
index 12de8cf0af..0c36332242 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Adjoint.lean
@@ -5,8 +5,8 @@ Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith
 -/
 module
 
-public import Mathlib.Algebra.Lie.TraceForm
 public import Mathlib.Analysis.Complex.Basic
+public import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.LinearAlgebra.Matrix.PosDef
 public import Mathlib.RepresentationTheory.Intertwining
@@ -41,8 +41,6 @@ under the bracket and nondegenerate (B.2).
 - `SULieAlgebra.adjointℂContr` : the contraction of two complex adjoint indices.
 - `SULieAlgebra.adjointContr_self_pos` : the real contraction is positive definite.
 - `SULieAlgebra.adjointℂContr_nondegenerate` : the complex contraction is nondegenerate.
-- `SULieAlgebra.adjointContr_eq_killingForm` : the contraction is `-1 / (2n)` times the Killing
-  form.
 
 ## iii. Table of contents
 
@@ -52,7 +50,6 @@ under the bracket and nondegenerate (B.2).
 - B. The contraction of adjoint indices
   - B.1. The real case
   - B.2. The complex case
-  - B.3. The Killing form
 
 ## iv. References
 
@@ -62,7 +59,7 @@ under the bracket and nondegenerate (B.2).
 
 @[expose] public section
 
-open Matrix TensorProduct ComplexStarModule Kronecker LieAlgebra
+open Matrix TensorProduct ComplexStarModule
 open scoped ComplexOrder
 
 namespace SULieAlgebra
@@ -423,69 +420,4 @@ lemma adjointℂContr_nondegenerate {n : ℕ} :
   ⟨fun A hA => adjointℂContr_separating_left A hA,
     fun B hB => adjointℂContr_separating_right B hB⟩
 
-/-!
-
-### B.3. The Killing form
-
--/
-
-/-- The contraction is the Killing form on the complexified Lie
-  algebra, up to a factor of `-1/(2n)`. -/
-lemma adjointℂContr_eq_killingForm {n : ℕ} (A B : Complexification n) :
-    adjointℂContr (A ⊗ₜ B) = -(1 / (2 * (n : ℂ))) * killingForm ℂ (Complexification n) A B := by
-  set K : Matrix (Fin n × Fin n) (Fin n × Fin n) ℂ :=
-    -(1 ⊗ₖ (toMatrixℂ A * toMatrixℂ B) - (toMatrixℂ B)ᵀ ⊗ₖ toMatrixℂ A
-      - (toMatrixℂ A)ᵀ ⊗ₖ toMatrixℂ B + (toMatrixℂ B * toMatrixℂ A)ᵀ ⊗ₖ 1)
-  let e : Matrix (Fin n) (Fin n) ℂ ≃ₗ[ℂ] (Fin n × Fin n → ℂ) :=
-    LinearEquiv.ofBijective ⟨⟨vec, vec_add⟩, vec_smul⟩ vec_bijective
-  set F := e.symm.conj (toLin' K)
-  have hF (M : Matrix (Fin n) (Fin n) ℂ) :
-      F M = -(toMatrixℂ A * (toMatrixℂ B * M - M * toMatrixℂ B)
-        - (toMatrixℂ B * M - M * toMatrixℂ B) * toMatrixℂ A) := by
-    apply e.injective
-    simp only [F, e, LinearEquiv.conj_apply, LinearMap.comp_apply, LinearEquiv.coe_coe,
-      LinearEquiv.symm_symm, LinearEquiv.apply_symm_apply, LinearEquiv.ofBijective_apply,
-      LinearMap.coe_mk, AddHom.coe_mk, toLin'_apply, K, neg_mulVec, sub_mulVec, add_mulVec,
-      kronecker_mulVec_vec, transpose_transpose, transpose_one, Matrix.mul_one, Matrix.one_mul,
-      ← vec_sub, ← vec_add, ← vec_neg]
-    congr 1
-    noncomm_ring
-  have h1 : toMatrixℂ ∘ₗ (ad ℂ (Complexification n) A ∘ₗ ad ℂ (Complexification n) B)
-      = F ∘ₗ toMatrixℂ := by
-    refine LinearMap.ext fun M => ?_
-    simp only [LinearMap.comp_apply, ad_apply, toMatrixℂ_lie, hF, Matrix.mul_smul,
-      Matrix.smul_mul, ← smul_sub, smul_smul, Complex.I_mul_I, neg_one_smul]
-  obtain ⟨π, hπ⟩ := LinearMap.exists_leftInverse_of_injective toMatrixℂ
-    (LinearMap.ker_eq_bot.2 toMatrixℂ_injective)
-  have h2 : (toMatrixℂ ∘ₗ π) ∘ₗ F = F := by
-    refine LinearMap.ext fun M => ?_
-    have hM : (F M).trace = 0 := by
-      rw [hF, trace_neg, trace_sub, trace_mul_comm, sub_self, neg_zero]
-    rw [LinearMap.comp_apply, LinearMap.comp_apply, ← toMatrixℂ_ofTracelessℂ (F M) hM,
-      ← LinearMap.comp_apply π, hπ, LinearMap.id_apply]
-  have hK : killingForm ℂ (Complexification n) A B = -(2 * n) * adjointℂContr (A ⊗ₜ B) := by
-    rw [killingForm_apply_apply, ← LinearMap.id_comp (ad ℂ (Complexification n) A ∘ₗ _), ← hπ,
-      LinearMap.comp_assoc, h1, LinearMap.trace_comp_comm', LinearMap.comp_assoc,
-      ← Module.End.mul_eq_comp, LinearMap.trace_mul_comm, Module.End.mul_eq_comp, h2,
-      adjointℂContr_tmul]
-    simp only [F, LinearMap.trace_conj', trace_toLin'_eq, K, trace_neg, trace_sub, trace_add,
-      trace_kronecker, trace_one, trace_transpose, trace_toMatrixℂ, Fintype.card_fin, mul_zero,
-      trace_mul_comm (toMatrixℂ B)]
-    ring
-  rw [hK]
-  rcases Nat.eq_zero_or_pos n with rfl | hn
-  · simp [adjointℂContr_tmul, Matrix.trace]
-  · have : (n : ℂ) ≠ 0 := by exact_mod_cast hn.ne'
-    field_simp
-
-/-- The contraction is the Killing form on the Lie algebra, up to a factor of `-1/(2n)`. -/
-lemma adjointContr_eq_killingForm {n : ℕ} (x y : SULieAlgebra n ℂ) :
-    adjointContr (x ⊗ₜ y) = -(1 / (2 * (n : ℝ))) * killingForm ℝ (SULieAlgebra n ℂ) x y := by
-  have h := adjointℂContr_eq_killingForm (1 ⊗ₜ x) (1 ⊗ₜ y)
-  rw [adjointℂContr_one_tmul, killingForm, LieModule.traceForm_baseChange,
-    LinearMap.BilinForm.baseChange_tmul, mul_one, Complex.real_smul, mul_one] at h
-  apply Complex.ofReal_injective
-  push_cast
-  exact h
-
 end SULieAlgebra
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
index 3059bc9faf..efa66b74d1 100644
--- a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/Basic.lean
@@ -38,6 +38,8 @@ and imaginary parts `ℜ M` and `ℑ M` being traceless hermitian.
 - `SULieAlgebra.toMatrixℂ_lie` : the matrix of a bracket is `i` times the commutator.
 - `SULieAlgebra.toMatrixℂ_injective`, `SULieAlgebra.range_toMatrixℂ` : the complexification is
   the traceless complex matrices.
+- `SULieAlgebra.equivTraceKer` : the linear equivalence between the complexification and the
+  traceless complex matrices.
 - `SULieAlgebra.finrank_eq`, `SULieAlgebra.finrank_complexification` : `su(n)` and its
   complexification have dimension `n² - 1`.
 
@@ -52,6 +54,7 @@ and imaginary parts `ℜ M` and `ℑ M` being traceless hermitian.
   - E.2. The element with a given traceless matrix
   - E.3. The injectivity and surjectivity of the matrix map
   - E.4. Commuting with all elements of `su(n)`
+  - E.5. Linear equivalences
 - F. The dimension
 
 ## iv. References
@@ -346,12 +349,38 @@ lemma commute_of_forall_commute_val {M : Matrix (Fin n) (Fin n) ℂ}
 
 /-!
 
+### E.5. Linear equivalences
+
+-/
+
+/-- The linear equivalence between the complexification of `su(n)` and the traceless complex
+  matrices, sending an element to its matrix. -/
+noncomputable def equivTraceKer :
+    Complexification n ≃ₗ[ℂ] LinearMap.ker (Matrix.traceLinearMap (Fin n) ℂ ℂ) where
+  toFun A := ⟨toMatrixℂ A, trace_toMatrixℂ A⟩
+  invFun M := ofTracelessℂ M.1 M.2
+  map_add' A B := Subtype.ext (map_add _ A B)
+  map_smul' z A := Subtype.ext (map_smul _ z A)
+  left_inv := ofTracelessℂ_toMatrixℂ
+  right_inv _ := Subtype.ext (toMatrixℂ_ofTracelessℂ _ _)
+
+/-- The matrix of `equivTraceKer A` is the matrix of `A`. -/
+@[simp]
+lemma val_equivTraceKer (A : Complexification n) : (equivTraceKer A).1 = toMatrixℂ A := rfl
+
+/-- The matrix of `equivTraceKer.symm M` is `M`. -/
+@[simp]
+lemma toMatrixℂ_equivTraceKer_symm (M : LinearMap.ker (traceLinearMap (Fin n) ℂ ℂ)) :
+    toMatrixℂ (equivTraceKer.symm M) = M.1 := toMatrixℂ_ofTracelessℂ _ M.2
+
+/-!
+
 ## F. The dimension
 
 -/
 
 /-- The complexification `ℂ ⊗[ℝ] su(n)` has complex dimension `n² - 1`: it is the traceless
-  matrices, and the trace is onto. -/
+  matrices, and the trace is onto for `0 < n`. -/
 lemma finrank_complexification : Module.finrank ℂ (Complexification n) = n ^ 2 - 1 := by
   rw [← LinearMap.finrank_range_of_inj toMatrixℂ_injective, range_toMatrixℂ]
   rcases Nat.eq_zero_or_pos n with rfl | hn
diff --git a/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/KillingForm.lean b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/KillingForm.lean
new file mode 100644
index 0000000000..eecd7be7eb
--- /dev/null
+++ b/Physlib/Mathematics/Groups/SpecialUnitary/LieAlgebra/KillingForm.lean
@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jinzheng Li, Nathaneal Sajan, Joseph Tooby-Smith
+-/
+module
+
+public import Mathlib.Algebra.Lie.TraceForm
+public import Physlib.Mathematics.Groups.SpecialUnitary.LieAlgebra.Adjoint
+/-!
+
+# The Killing form of `su(n)`
+
+The Killing form of `su(n)` and its complexification, and its relation to the adjoint contraction.
+
+## i. Overview
+
+The Killing form `K(A, B) = tr (ad A ∘ ad B)` of the complexification is computed by transporting
+`ad A ∘ ad B` to the matrices, where it is `M ↦ -[A, [B, M]]`, the sign coming from the factor `i`
+in the bracket. Its trace is `-2n tr (A B)` (A).
+
+The contractions `adjointℂContr` and `adjointContr` of adjoint indices are therefore `-1 / (2n)`
+times the Killing forms of the complexification and of `su(n)` (B).
+
+## ii. Key results
+
+- `SULieAlgebra.killingForm_eq_trace` : the Killing form of the complexification is `-2n` times
+  the trace form.
+- `SULieAlgebra.adjointℂContr_eq_killingForm` : the complex contraction is `-1 / (2n)` times the
+  Killing form.
+- `SULieAlgebra.adjointContr_eq_killingForm` : the real contraction is `-1 / (2n)` times the
+  Killing form.
+
+## iii. Table of contents
+
+- A. The Killing form as a trace
+- B. The contraction as the Killing form
+
+## iv. References
+
+* None.
+
+-/
+
+@[expose] public section
+
+open Matrix TensorProduct Kronecker LieAlgebra
+
+namespace SULieAlgebra
+
+/-!
+
+## A. The Killing form as a trace
+
+-/
+
+/-- The Killing form of the complexification is the trace form of the matrices,
+  `K(A, B) = -2n tr (A B)`. The sign comes from the factor `i` in the bracket, which makes
+  `ad A ∘ ad B` the map `M ↦ -[A, [B, M]]`. -/
+lemma killingForm_eq_trace {n : ℕ} (A B : Complexification n) :
+    killingForm ℂ (Complexification n) A B = - (2 * n) * (toMatrixℂ A * toMatrixℂ B).trace := by
+  let e : Matrix (Fin n) (Fin n) ℂ ≃ₗ[ℂ] (Fin n × Fin n → ℂ) :=
+    .ofBijective ⟨⟨vec, vec_add⟩, vec_smul⟩ vec_bijective
+  let F := e.symm.conj <| toLin' <| -(1 ⊗ₖ (toMatrixℂ A * toMatrixℂ B)
+    - (toMatrixℂ B)ᵀ ⊗ₖ toMatrixℂ A - (toMatrixℂ A)ᵀ ⊗ₖ toMatrixℂ B
+    + (toMatrixℂ B * toMatrixℂ A)ᵀ ⊗ₖ 1)
+  have hF (M) : F M = -(toMatrixℂ A * (toMatrixℂ B * M - M * toMatrixℂ B)
+      - (toMatrixℂ B * M - M * toMatrixℂ B) * toMatrixℂ A) := e.symm_apply_eq.2 <| by
+    simp [e, kronecker_mulVec_vec, ← vec_sub, ← vec_add, ← vec_neg, vec_inj]
+    noncomm_ring
+  have hF' (M) : F M ∈ LinearMap.ker (traceLinearMap (Fin n) ℂ ℂ) := by
+    simp [hF, trace_mul_comm (toMatrixℂ A)]
+  have h1 : equivTraceKer.conj (ad ℂ _ A ∘ₗ ad ℂ _ B) = F.restrict fun M _ => hF' M :=
+    LinearMap.ext fun M => Subtype.ext <| by
+      simp [hF, toMatrixℂ_lie, ← smul_sub, smul_smul]
+  rw [killingForm_apply_apply, ← LinearMap.trace_conj' _ equivTraceKer, h1,
+    LinearMap.trace_restrict_eq_of_forall_mem _ _ hF']
+  simp [F, trace_kronecker, -transpose_mul, trace_mul_comm (toMatrixℂ B), trace_toMatrixℂ]
+  ring
+
+/-!
+
+## B. The contraction as the Killing form
+
+-/
+
+/-- The contraction is the Killing form on the complexified Lie
+  algebra, up to a factor of `-1/(2n)`. -/
+lemma adjointℂContr_eq_killingForm {n : ℕ} (A B : Complexification n) :
+    adjointℂContr (A ⊗ₜ B) = -(1 / (2 * (n : ℂ))) * killingForm ℂ (Complexification n) A B := by
+  rw [killingForm_eq_trace, adjointℂContr_tmul]
+  rcases Nat.eq_zero_or_pos n with rfl | hn
+  · simp [Matrix.trace]
+  · have : (n : ℂ) ≠ 0 := by exact_mod_cast hn.ne'
+    field_simp
+
+/-- The contraction is the Killing form on the Lie algebra, up to a factor of `-1/(2n)`. -/
+lemma adjointContr_eq_killingForm {n : ℕ} (x y : SULieAlgebra n ℂ) :
+    adjointContr (x ⊗ₜ y) = -(1 / (2 * (n : ℝ))) * killingForm ℝ (SULieAlgebra n ℂ) x y := by
+  have h := adjointℂContr_eq_killingForm (1 ⊗ₜ x) (1 ⊗ₜ y)
+  rw [adjointℂContr_one_tmul, killingForm, LieModule.traceForm_baseChange,
+    LinearMap.BilinForm.baseChange_tmul, mul_one, Complex.real_smul, mul_one] at h
+  apply Complex.ofReal_injective
+  push_cast
+  exact h
+
+end SULieAlgebra