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

Adjoint ad action: ad(A)(B) = [A, B]

The ad action of su(N) element A on another element B. This defines the map B ↦ [A, B].

Equations

• Newton.adjointAd A B = ⁅A, B⁆

theorem Newton.adjointAd.add {N : ℕ} (A B C : SuNAlgebra N) : adjointAd A (B + C) = adjointAd A B + adjointAd A C

ad action preserves addition: ad(A)(B + C) = ad(A)(B) + ad(A)(C)

theorem Newton.adjointAd.smul {N : ℕ} (A : SuNAlgebra N) (r : ℝ) (B : SuNAlgebra N) : adjointAd A (r • B) = r • adjointAd A B

ad action preserves scalar multiplication: ad(A)(r • B) = r • ad(A)(B)

@[simp]

theorem Newton.adjointAd.zero {N : ℕ} (A : SuNAlgebra N) : adjointAd A 0 = 0

ad action preserves zero: ad(A)(0) = 0

@[simp]

theorem Newton.adjointAd.zero_left {N : ℕ} (B : SuNAlgebra N) : adjointAd 0 B = 0

ad action of zero is the zero map: ad(0)(B) = 0

@[simp]

theorem Newton.adjointAd.self {N : ℕ} (A : SuNAlgebra N) : adjointAd A A = 0

ad action on self is zero: ad(A)(A) = 0

theorem Newton.adjointAd.antisymm {N : ℕ} (A B : SuNAlgebra N) : adjointAd A B = -adjointAd B A

Antisymmetry of ad action: ad(A)(B) = -ad(B)(A)

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

Leibniz rule for ad action (derivation property)

ad(A)([B, C]) = [ad(A)(B), C] + [B, ad(A)(C)]

This follows directly from the Jacobi identity.

theorem Newton.adjointAd_bracket {N : ℕ} (A B C : SuNAlgebra N) : adjointAd ⁅A, B⁆ C = adjointAd A (adjointAd B C) - adjointAd B (adjointAd A C)

Composition rule for ad action

[[A, B], C] = [A, [B, C]] - [B, [A, C]]

This is a fundamental property of the adjoint representation of Lie algebras.

theorem Newton.adjointAd_add_left {N : ℕ} (A B C : SuNAlgebra N) : adjointAd (A + B) C = adjointAd A C + adjointAd B C

Left linearity of ad action: ad(A + B) = ad(A) + ad(B)

theorem Newton.adjointAd_smul_left {N : ℕ} (r : ℝ) (A B : SuNAlgebra N) : adjointAd (r • A) B = r • adjointAd A B

Left scalar multiplication of ad action: ad(r • A) = r • ad(A)

theorem Newton.killingForm_via_ad {N : ℕ} [DecidableEq (Fin N)] (A B : SuNAlgebra N) : killingForm A B = (A.matrix * B.matrix).trace

Killing form expressed via ad action

The relation B(X, Y) = Tr(XY) holds.

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

Double application of ad action: ad(A)(ad(A)(B)) = [A, [A, B]]

Equations

• Newton.adjointAd2 A B = Newton.adjointAd A (Newton.adjointAd A B)

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

Expansion of ad(A)^2(B) = [A, [A, B]]

@[simp]

theorem Newton.adjointAd2_self {N : ℕ} (A : SuNAlgebra N) : adjointAd2 A A = 0

ad(A)^2(A) = 0 (from Jacobi identity)