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 BilinForm.isSkewAdjoint_bracket {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : BilinForm R M) {f : Module.End R M} {g : Module.End R M} (hf : f ∈ BilinForm.skewAdjointSubmodule B) (hg : g ∈ BilinForm.skewAdjointSubmodule B) : ⁅f, g⁆ ∈ BilinForm.skewAdjointSubmodule B

def skewAdjointLieSubalgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : 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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

theorem Matrix.isSkewAdjoint_bracket {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) {A : Matrix n n R} {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

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

@[simp]

theorem mem_skewAdjointMatricesLieSubalgebra {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) (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 : Matrix n n R) (P : Matrix n n R) (h : Invertible P) : ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (Matrix.transpose P * 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

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

theorem skewAdjointMatricesLieSubalgebraEquiv_apply {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) (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), Matrix.transpose (e A) = e (Matrix.transpose A)) : ↥(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

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

@[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), Matrix.transpose (e A) = e (Matrix.transpose A)) (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 : Matrix n n R) (A : Matrix n n R) : A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J