Lie algebras of skew-adjoint endomorphisms of a bilinear form

When a module carries a bilinear form, the Lie algebra of endomorphisms of the module contains a distinguished Lie subalgebra: the skew-adjoint endomorphisms. Such subalgebras are important because they provide a simple, explicit construction of the so-called classical Lie algebras.

This file defines the Lie subalgebra of skew-adjoint endomorphisms cut out by a bilinear form on a module and proves some basic related results. It also provides the corresponding definitions and results for the Lie algebra of square matrices.

Main definitions

• skewAdjointLieSubalgebra
• skewAdjointLieSubalgebraEquiv
• skewAdjointMatricesLieSubalgebra
• skewAdjointMatricesLieSubalgebraEquiv

Tags

lie algebra, skew-adjoint, bilinear form

theorem LinearMap.BilinForm.isSkewAdjoint_bracket {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {f g : Module.End R M} (hf : f ∈ LinearMap.skewAdjointSubmodule B) (hg : g ∈ LinearMap.skewAdjointSubmodule B) : ⁅f, g⁆ ∈ LinearMap.skewAdjointSubmodule B

def skewAdjointLieSubalgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : LieSubalgebra R (Module.End R M)

Given an R-module M, equipped with a bilinear form, the skew-adjoint endomorphisms form a Lie subalgebra of the Lie algebra of endomorphisms.

Equations

• skewAdjointLieSubalgebra B = { toSubmodule := LinearMap.skewAdjointSubmodule B, lie_mem' := ⋯ }

def skewAdjointLieSubalgebraEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {N : Type w} [AddCommGroup N] [Module R N] (e : N ≃ₗ[R] M) : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)

An equivalence of modules with bilinear forms gives equivalence of Lie algebras of skew-adjoint endomorphisms.

Equations

• skewAdjointLieSubalgebraEquiv B e = LieEquiv.ofSubalgebras (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) (skewAdjointLieSubalgebra B) e.lieConj ⋯

@[simp]

theorem skewAdjointLieSubalgebraEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {N : Type w} [AddCommGroup N] [Module R N] (e : N ≃ₗ[R] M) (f : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e))) : ↑((skewAdjointLieSubalgebraEquiv B e) f) = e.lieConj ↑f

@[simp]

theorem skewAdjointLieSubalgebraEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {N : Type w} [AddCommGroup N] [Module R N] (e : N ≃ₗ[R] M) (f : ↥(skewAdjointLieSubalgebra B)) : ↑((skewAdjointLieSubalgebraEquiv B e).symm f) = e.symm.lieConj ↑f

theorem Matrix.lie_transpose {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (A B : Matrix n n R) : ⁅A, B⁆.transpose = ⁅B.transpose, A.transpose⁆

theorem Matrix.isSkewAdjoint_bracket {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) {A B : Matrix n n R} (hA : A ∈ skewAdjointMatricesSubmodule J) (hB : B ∈ skewAdjointMatricesSubmodule J) : ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J

def skewAdjointMatricesLieSubalgebra {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) : LieSubalgebra R (Matrix n n R)

The Lie subalgebra of skew-adjoint square matrices corresponding to a square matrix J.

Equations

• skewAdjointMatricesLieSubalgebra J = { toSubmodule := skewAdjointMatricesSubmodule J, lie_mem' := ⋯ }

@[simp]

theorem mem_skewAdjointMatricesLieSubalgebra {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J A : Matrix n n R) : A ∈ skewAdjointMatricesLieSubalgebra J ↔ A ∈ skewAdjointMatricesSubmodule J

def skewAdjointMatricesLieSubalgebraEquiv {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J P : Matrix n n R) (h : Invertible P) : ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (P.transpose * J * P))

An invertible matrix P gives a Lie algebra equivalence between those endomorphisms that are skew-adjoint with respect to a square matrix J and those with respect to PᵀJP.

Equations

• skewAdjointMatricesLieSubalgebraEquiv J P h = LieEquiv.ofSubalgebras (skewAdjointMatricesLieSubalgebra J) (skewAdjointMatricesLieSubalgebra (P.transpose * J * P)) (P.lieConj h).symm ⋯

theorem skewAdjointMatricesLieSubalgebraEquiv_apply {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J P : Matrix n n R) (h : Invertible P) (A : ↥(skewAdjointMatricesLieSubalgebra J)) : ↑((skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P

def skewAdjointMatricesLieSubalgebraEquivTranspose {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) {m : Type w} [DecidableEq m] [Fintype m] (e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ (A : Matrix n n R), (e A).transpose = e A.transpose) : ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (e J))

An equivalence of matrix algebras commuting with the transpose endomorphisms restricts to an equivalence of Lie algebras of skew-adjoint matrices.

Equations

• skewAdjointMatricesLieSubalgebraEquivTranspose J e h = LieEquiv.ofSubalgebras (skewAdjointMatricesLieSubalgebra J) (skewAdjointMatricesLieSubalgebra (e J)) e.toLieEquiv ⋯

@[simp]

theorem skewAdjointMatricesLieSubalgebraEquivTranspose_apply {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) {m : Type w} [DecidableEq m] [Fintype m] (e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ (A : Matrix n n R), (e A).transpose = e A.transpose) (A : ↥(skewAdjointMatricesLieSubalgebra J)) : ↑((skewAdjointMatricesLieSubalgebraEquivTranspose J e h) A) = e ↑A

theorem mem_skewAdjointMatricesLieSubalgebra_unit_smul {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (u : Rˣ) (J A : Matrix n n R) : A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J