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

Equations
• = let __src := ; { toSubmodule := __src, lie_mem' := }
Instances For
def skewAdjointLieSubalgebraEquiv {R : Type u} {M : Type v} [] [] [Module R M] (B : ) {N : Type w} [] [Module R N] (e : N ≃ₗ[R] M) :
() ≃ₗ⁅R

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

Equations
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 : ()) :
() = e.lieConj 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 : ) :
(.symm f) = e.symm.lieConj f
theorem Matrix.lie_transpose {R : Type u} {n : Type w} [] [] [] (A : Matrix n n R) (B : Matrix n n R) :
A, B.transpose = B.transpose, A.transpose
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.

Equations
• = let __src := ; { toSubmodule := __src, lie_mem' := }
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 : ) :

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
Instances For
theorem skewAdjointMatricesLieSubalgebraEquiv_apply {R : Type u} {n : Type w} [] [] [] (J : Matrix n n R) (P : Matrix n n R) (h : ) (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), (e A).transpose = e A.transpose) :

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

Equations
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), (e A).transpose = e A.transpose) (A : ) :
() = 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) :