# 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 #

theorem BilinForm.isSkewAdjoint_bracket {R : Type u} {M : Type v} [] [] [Module R M] (B : ) {f : } {g : } (hf : ) (hg : ) :
def skewAdjointLieSubalgebra {R : Type u} {M : Type v} [] [] [Module R M] (B : ) :

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

Instances For
def skewAdjointLieSubalgebraEquiv {R : Type u} {M : Type v} [] [] [Module R M] (B : ) {N : Type w} [] [Module R N] (e : N ≃ₗ[R] M) :
{ x // x skewAdjointLieSubalgebra (BilinForm.comp B e e) } ≃ₗ⁅R { x // }

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

Instances For
@[simp]
theorem skewAdjointLieSubalgebraEquiv_apply {R : Type u} {M : Type v} [] [] [Module R M] (B : ) {N : Type w} [] [Module R N] (e : N ≃ₗ[R] M) (f : { x // x skewAdjointLieSubalgebra (BilinForm.comp B e e) }) :
↑(↑() f) = ↑() f
@[simp]
theorem skewAdjointLieSubalgebraEquiv_symm_apply {R : Type u} {M : Type v} [] [] [Module R M] (B : ) {N : Type w} [] [Module R N] (e : N ≃ₗ[R] M) (f : { x // }) :
↑(↑() f) = ↑() f
theorem Matrix.lie_transpose {R : Type u} {n : Type w} [] [] [] (A : Matrix n n R) (B : Matrix n n R) :
theorem Matrix.isSkewAdjoint_bracket {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) {A : Matrix n n R} {B : Matrix n n R} (hA : ) (hB : ) :
def skewAdjointMatricesLieSubalgebra {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) :

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

Instances For
@[simp]
theorem mem_skewAdjointMatricesLieSubalgebra {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) (A : Matrix n n R) :
def skewAdjointMatricesLieSubalgebraEquiv {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) (P : Matrix n n R) (h : ) :
{ x // } ≃ₗ⁅R { x // }

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.

Instances For
theorem skewAdjointMatricesLieSubalgebraEquiv_apply {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) (P : Matrix n n R) (h : ) (A : { x // }) :
↑(↑() A) = P⁻¹ * A * P
def skewAdjointMatricesLieSubalgebraEquivTranspose {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) {m : Type w} [] [] (e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ (A : Matrix n n R), Matrix.transpose (e A) = e ()) :
{ x // } ≃ₗ⁅R { x // }

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

Instances For
@[simp]
theorem skewAdjointMatricesLieSubalgebraEquivTranspose_apply {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) {m : Type w} [] [] (e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ (A : Matrix n n R), Matrix.transpose (e A) = e ()) (A : { x // }) :
↑() = e A
theorem mem_skewAdjointMatricesLieSubalgebra_unit_smul {R : Type u} {n : Type w} [] [] [] (u : Rˣ) (J : Matrix n n R) (A : Matrix n n R) :