structure Newton.SUNGroup (N : ℕ) : Type

Element of SU(N) group N×N complex matrix g satisfying:

1. Unitary: g g† = 1
2. Determinant one: det(g) = 1

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

  Matrix representation

• unitary : self.matrix * self.matrix.conjTranspose = 1

  Unitary condition: g g† = 1

• det_one : self.matrix.det = 1

  Special condition: det(g) = 1

theorem Newton.SUNGroup.ext {N : ℕ} {g h : SUNGroup N} (hm : g.matrix = h.matrix) : g = h

SUNGroup equality is matrix equality

theorem Newton.SUNGroup.unitary' {N : ℕ} (g : SUNGroup N) : g.matrix.conjTranspose * g.matrix = 1

Alternative form of unitary condition: g† g = 1

instance Newton.SUNGroup.instOne {N : ℕ} : One (SUNGroup N)

Identity element

Equations

• Newton.SUNGroup.instOne = { one := { matrix := 1, unitary := ⋯, det_one := ⋯ } }

instance Newton.SUNGroup.instMul {N : ℕ} : Mul (SUNGroup N)

Multiplication

Equations

• Newton.SUNGroup.instMul = { mul := fun (g h : Newton.SUNGroup N) => { matrix := g.matrix * h.matrix, unitary := ⋯, det_one := ⋯ } }

noncomputable instance Newton.SUNGroup.instInv {N : ℕ} : Inv (SUNGroup N)

Inverse element

Equations

• Newton.SUNGroup.instInv = { inv := fun (g : Newton.SUNGroup N) => { matrix := g.matrix.conjTranspose, unitary := ⋯, det_one := ⋯ } }

@[simp]

theorem Newton.SUNGroup.one_matrix {N : ℕ} : matrix 1 = 1

Matrix of identity element

@[simp]

theorem Newton.SUNGroup.mul_matrix {N : ℕ} (g h : SUNGroup N) : (g * h).matrix = g.matrix * h.matrix

Matrix of multiplication

@[simp]

theorem Newton.SUNGroup.inv_matrix {N : ℕ} (g : SUNGroup N) : g⁻¹.matrix = g.matrix.conjTranspose

Matrix of inverse element

@[simp]

theorem Newton.SUNGroup.mul_one {N : ℕ} (g : SUNGroup N) : g * 1 = g

Right identity law

@[simp]

theorem Newton.SUNGroup.one_mul {N : ℕ} (g : SUNGroup N) : 1 * g = g

Left identity law

@[simp]

theorem Newton.SUNGroup.mul_inv {N : ℕ} (g : SUNGroup N) : g * g⁻¹ = 1

Right inverse law

@[simp]

theorem Newton.SUNGroup.inv_mul {N : ℕ} (g : SUNGroup N) : g⁻¹ * g = 1

Left inverse law

theorem Newton.SUNGroup.mul_assoc {N : ℕ} (g h k : SUNGroup N) : g * h * k = g * (h * k)

Associativity of multiplication

noncomputable def Newton.adjointAction {N : ℕ} (g : SUNGroup N) (A : SuNAlgebra N) : SuNAlgebra N

Adjoint action: g A g⁻¹ = g A g† Adjoint action of SU(N) element g on su(N) element A. The result is again an element of su(N).

Equations

• Newton.adjointAction g A = { matrix := g.matrix * A.matrix * g.matrix.conjTranspose, trace_zero := ⋯, anti_hermitian := ⋯ }

@[simp]

theorem Newton.adjointAction.one_action {N : ℕ} (A : SuNAlgebra N) : adjointAction 1 A = A

Adjoint action by identity is the identity map

theorem Newton.adjointAction.compose {N : ℕ} (g h : SUNGroup N) (A : SuNAlgebra N) : adjointAction (g * h) A = adjointAction g (adjointAction h A)

Composition rule for adjoint action: Ad(gh)(A) = Ad(g)(Ad(h)(A))

theorem Newton.adjointAction.add {N : ℕ} (g : SUNGroup N) (A B : SuNAlgebra N) : adjointAction g (A + B) = adjointAction g A + adjointAction g B

Adjoint action preserves addition

@[simp]

theorem Newton.adjointAction.zero {N : ℕ} (g : SUNGroup N) : adjointAction g 0 = 0

Adjoint action preserves zero

theorem Newton.adjointAction.bracket {N : ℕ} (g : SUNGroup N) (A B : SuNAlgebra N) : adjointAction g ⁅A, B⁆ = ⁅adjointAction g A, adjointAction g B⁆

Adjoint action preserves Lie bracket