Commutators of linear maps

This file defines commutators of linear operators, and proves a few useful properties of them.

Main definitions

• LinearMap.commutator: The commutator [A,B] := AB-BA of two linear operators A, B.
• LinearMap.commutatorBilin: The commutator [⬝,⬝] as a bilinear map on the space of linear maps.

def LinearMap.commutator {𝕜 : Type u_1} [Semiring 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (A B : V →ₗ[𝕜] V) : V →ₗ[𝕜] V

Commutator [A,B] := AB-BA of two linear operators A, B.

Equations

• A.commutator B = A * B - B * A

theorem LinearMap.commutator_comm {𝕜 : Type u_1} [Semiring 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (A B : V →ₗ[𝕜] V) : A.commutator B = -B.commutator A

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

theorem LinearMap.mul_eq_mul_add_commutator {𝕜 : Type u_1} [Semiring 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (A B : V →ₗ[𝕜] V) : A * B = B * A + A.commutator B

theorem LinearMap.commutator_pair {𝕜 : Type u_1} [Semiring 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (A B C : V →ₗ[𝕜] V) : (A * B).commutator C = A * B.commutator C + A.commutator C * B

[AB,C] = A[B,C] + [A,C]B

theorem LinearMap.commutator_pair' {𝕜 : Type u_1} [Semiring 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (A B C : V →ₗ[𝕜] V) : A.commutator (B * C) = B * A.commutator C + A.commutator B * C

[A,BC] = B[A,C] + [A,B]C

@[simp]

theorem LinearMap.commutator_smul_one {𝕜 : Type u_3} [Field 𝕜] (V : Type u_4) [AddCommGroup V] [Module 𝕜 V] (A : V →ₗ[𝕜] V) (c : 𝕜) : A.commutator (c • 1) = 0

@[simp]

theorem LinearMap.smul_one_commutator {𝕜 : Type u_3} [Field 𝕜] (V : Type u_4) [AddCommGroup V] [Module 𝕜 V] (A : V →ₗ[𝕜] V) (c : 𝕜) : (c • 1).commutator A = 0

noncomputable def LinearMap.commutatorBilin {𝕜 : Type u_1} [Field 𝕜] (V : Type u_2) [AddCommGroup V] [Module 𝕜 V] : (V →ₗ[𝕜] V) →ₗ[𝕜] (V →ₗ[𝕜] V) →ₗ[𝕜] V →ₗ[𝕜] V

Commutator [⬝,⬝] as a bilinear map on the space of linear maps.

Equations

• LinearMap.commutatorBilin V = { toFun := fun (A : V →ₗ[𝕜] V) => { toFun := fun (B : V →ₗ[𝕜] V) => A.commutator B, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.commutatorBilin_apply₂ {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (A B : V →ₗ[𝕜] V) : ((commutatorBilin V) A) B = A.commutator B

def LinearMap.algebraCommutator' (𝕜 : Type u_1) {A : Type u_2} [CommSemiring 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) : A →ₗ[𝕜] A

Commutator with a fixed element in a 𝕜-algebra as a 𝕜-linear map.

Equations

• LinearMap.algebraCommutator' 𝕜 a = { toFun := fun (b : A) => a * b - b * a, map_add' := ⋯, map_smul' := ⋯ }

theorem LinearMap.algebraCommutator'_apply (𝕜 : Type u_1) {A : Type u_2} [CommSemiring 𝕜] [Ring A] [Algebra 𝕜 A] (a b : A) : (algebraCommutator' 𝕜 a) b = a * b - b * a

def LinearMap.algebraCommutator (𝕜 : Type u_1) {A : Type u_2} [CommSemiring 𝕜] [Ring A] [Algebra 𝕜 A] : A →ₗ[𝕜] A →ₗ[𝕜] A

Commutator in a 𝕜-algebra as a 𝕜-bilinear linear map.

Equations

• LinearMap.algebraCommutator 𝕜 = { toFun := LinearMap.algebraCommutator' 𝕜, map_add' := ⋯, map_smul' := ⋯ }