structure Newton.SuNAlgebra (N : ℕ) : Type

Lie algebra su(N) of SU(N) N×N complex matrices A satisfying:

1. Traceless: Tr(A) = 0
2. Anti-Hermitian: A† = -A (where † denotes conjugate transpose)

• matrix : Matrix (Fin N) (Fin N) ℂ

  Matrix representation

• trace_zero : self.matrix.trace = 0

  Traceless condition

• anti_hermitian : self.matrix.conjTranspose = -self.matrix

  Anti-Hermitian condition: A† = -A

instance Newton.SuNAlgebra.instZero {N : ℕ} : Zero (SuNAlgebra N)

Zero element

Equations

• Newton.SuNAlgebra.instZero = { zero := { matrix := 0, trace_zero := ⋯, anti_hermitian := ⋯ } }

instance Newton.SuNAlgebra.instAdd {N : ℕ} : Add (SuNAlgebra N)

Addition

Equations

• Newton.SuNAlgebra.instAdd = { add := fun (A B : Newton.SuNAlgebra N) => { matrix := A.matrix + B.matrix, trace_zero := ⋯, anti_hermitian := ⋯ } }

instance Newton.SuNAlgebra.instNeg {N : ℕ} : Neg (SuNAlgebra N)

Negation

Equations

• Newton.SuNAlgebra.instNeg = { neg := fun (A : Newton.SuNAlgebra N) => { matrix := -A.matrix, trace_zero := ⋯, anti_hermitian := ⋯ } }

instance Newton.SuNAlgebra.instSub {N : ℕ} : Sub (SuNAlgebra N)

Subtraction

Equations

• Newton.SuNAlgebra.instSub = { sub := fun (A B : Newton.SuNAlgebra N) => A + -B }

instance Newton.SuNAlgebra.instSMulReal {N : ℕ} : SMul ℝ (SuNAlgebra N)

Real scalar multiplication (su(N) is a real vector space)

Equations

• Newton.SuNAlgebra.instSMulReal = { smul := fun (r : ℝ) (A : Newton.SuNAlgebra N) => { matrix := ↑r • A.matrix, trace_zero := ⋯, anti_hermitian := ⋯ } }

theorem Newton.SuNAlgebra.ext {N : ℕ} {A B : SuNAlgebra N} (h : A.matrix = B.matrix) : A = B

Equality via matrix equality

@[simp]

theorem Newton.SuNAlgebra.matrix_eq_iff {N : ℕ} {A B : SuNAlgebra N} : A.matrix = B.matrix ↔ A = B

SuNAlgebra equality is equivalent to matrix equality

theorem Newton.SuNAlgebra.ext_matrix {N : ℕ} {A : SuNAlgebra N} (h : A.matrix = 0) : A = 0

If matrix is zero, then the element is zero

@[simp]

theorem Newton.SuNAlgebra.zero_matrix {N : ℕ} : matrix 0 = 0

Zero element has zero matrix

@[simp]

theorem Newton.SuNAlgebra.add_matrix {N : ℕ} (A B : SuNAlgebra N) : (A + B).matrix = A.matrix + B.matrix

Addition is compatible with matrix addition

@[simp]

theorem Newton.SuNAlgebra.neg_matrix {N : ℕ} (A : SuNAlgebra N) : (-A).matrix = -A.matrix

Negation is compatible with matrix negation

@[simp]

theorem Newton.SuNAlgebra.smul_matrix {N : ℕ} (r : ℝ) (A : SuNAlgebra N) : (r • A).matrix = ↑r • A.matrix

Scalar multiplication is compatible with matrix scalar multiplication

@[simp]

theorem Newton.SuNAlgebra.sub_matrix {N : ℕ} (A B : SuNAlgebra N) : (A - B).matrix = A.matrix - B.matrix

Subtraction is compatible with matrix subtraction

instance Newton.SuNAlgebra.instAddCommGroup {N : ℕ} : AddCommGroup (SuNAlgebra N)

Additive commutative group instance

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Newton.SuNAlgebra.lie {N : ℕ} (A B : SuNAlgebra N) : SuNAlgebra N

Lie bracket [A, B] = AB - BA for SuNAlgebra

The Lie bracket of two su(N) elements is again in su(N). Uses Mathlib's Lie bracket on the underlying matrices.

Equations

• A.lie B = { matrix := ⁅A.matrix, B.matrix⁆, trace_zero := ⋯, anti_hermitian := ⋯ }

noncomputable instance Newton.instLieRingSuNAlgebra {N : ℕ} : LieRing (SuNAlgebra N)

LieRing instance for SuNAlgebra using Mathlib's Lie structure

Equations

• Newton.instLieRingSuNAlgebra = { toAddCommGroup := Newton.SuNAlgebra.instAddCommGroup, bracket := Newton.SuNAlgebra.lie, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

@[simp]

theorem Newton.SuNAlgebra.lie_matrix {N : ℕ} (A B : SuNAlgebra N) : ⁅A, B⁆.matrix = ⁅A.matrix, B.matrix⁆

Matrix representation of Lie bracket

theorem Newton.SuNAlgebra.lie_def {N : ℕ} (A B : SuNAlgebra N) : ⁅A, B⁆.matrix = A.matrix * B.matrix - B.matrix * A.matrix

Lie bracket expanded as commutator

theorem Newton.SuNAlgebra.jacobi_identity {N : ℕ} (A B C : SuNAlgebra N) : ⁅A, ⁅B, C⁆⁆ + ⁅B, ⁅C, A⁆⁆ + ⁅C, ⁅A, B⁆⁆ = 0

Jacobi identity follows from Mathlib's lie_jacobi

theorem Newton.SuNAlgebra.jacobi_identity_alt {N : ℕ} (A B C : SuNAlgebra N) : ⁅A, ⁅B, C⁆⁆ = ⁅⁅A, B⁆, C⁆ + ⁅B, ⁅A, C⁆⁆

Alternative form of Jacobi identity

theorem Newton.star_mul_self_re_nonneg (z : ℂ) : (star z * z).re ≥ 0

Real part of star z * z equals |z|² and is non-negative

theorem Newton.Complex.re_finset_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) : (∑ i ∈ s, f i).re = ∑ i ∈ s, (f i).re

Real part of a sum equals sum of real parts

theorem Newton.trace_conjTranspose_mul_self_re_nonneg {N : ℕ} (M : Matrix (Fin N) (Fin N) ℂ) : (M.conjTranspose * M).trace.re ≥ 0

Real part of Tr(A†A) is non-negative (diagonal elements of A†A are sums of |A_ij|²)

theorem Newton.trace_conjTranspose_mul_self_re_pos_of_ne_zero {N : ℕ} (M : Matrix (Fin N) (Fin N) ℂ) (hM : M ≠ 0) : (M.conjTranspose * M).trace.re > 0

For non-zero matrix, Tr(M†M) > 0

theorem Newton.SuNAlgebra.trace_square_nonpos {N : ℕ} (A : SuNAlgebra N) : (A.matrix * A.matrix).trace.re ≤ 0

Square of an su(N) element has non-positive trace (Tr(A²) ≤ 0)

noncomputable def Newton.killingForm {N : ℕ} [DecidableEq (Fin N)] (A B : SuNAlgebra N) : ℂ

Killing form: B(A, B) = Tr(AB)

Equations

• Newton.killingForm A B = (A.matrix * B.matrix).trace

theorem Newton.killingForm_symm {N : ℕ} [DecidableEq (Fin N)] (A B : SuNAlgebra N) : killingForm A B = killingForm B A

Killing form is symmetric

theorem Newton.killingForm_add_left {N : ℕ} [DecidableEq (Fin N)] (A B C : SuNAlgebra N) : killingForm (A + B) C = killingForm A C + killingForm B C

Bilinearity of Killing form (left)

theorem Newton.killingForm_add_right {N : ℕ} [DecidableEq (Fin N)] (A B C : SuNAlgebra N) : killingForm A (B + C) = killingForm A B + killingForm A C

Bilinearity of Killing form (right)