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

## Tags #

lie algebra, skew-adjoint, bilinear form

theorem bilin_form.is_skew_adjoint_bracket {R : Type u} {M : Type v} [comm_ring R] [ M] (B : M) (f g : M) (hf : f B.skew_adjoint_submodule) (hg : g B.skew_adjoint_submodule) :
def skew_adjoint_lie_subalgebra {R : Type u} {M : Type v} [comm_ring R] [ M] (B : M) :
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
def skew_adjoint_lie_subalgebra_equiv {R : Type u} {M : Type v} [comm_ring R] [ M] (B : M) {N : Type w} [ N] (e : N ≃ₗ[R] M) :

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

Equations
@[simp]
theorem skew_adjoint_lie_subalgebra_equiv_apply {R : Type u} {M : Type v} [comm_ring R] [ M] (B : M) {N : Type w} [ N] (e : N ≃ₗ[R] M) (f : (skew_adjoint_lie_subalgebra (B.comp e e))) :
@[simp]
theorem skew_adjoint_lie_subalgebra_equiv_symm_apply {R : Type u} {M : Type v} [comm_ring R] [ M] (B : M) {N : Type w} [ N] (e : N ≃ₗ[R] M) (f : ) :
theorem matrix.lie_transpose {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (A B : n R) :
theorem matrix.is_skew_adjoint_bracket {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J A B : n R) (hA : A ) (hB : B ) :
def skew_adjoint_matrices_lie_subalgebra {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J : n R) :
(matrix n n R)

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

Equations
@[simp]
theorem mem_skew_adjoint_matrices_lie_subalgebra {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J A : n R) :
def skew_adjoint_matrices_lie_subalgebra_equiv {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J P : n R) (h : invertible 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
theorem skew_adjoint_matrices_lie_subalgebra_equiv_apply {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J P : n R) (h : invertible P)  :
A) = (P⁻¹.mul A).mul P
def skew_adjoint_matrices_lie_subalgebra_equiv_transpose {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J : n R) {m : Type w} [decidable_eq m] [fintype m] (e : n R ≃ₐ[R] m R) (h : ∀ (A : 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
@[simp]
theorem skew_adjoint_matrices_lie_subalgebra_equiv_transpose_apply {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J : n R) {m : Type w} [decidable_eq m] [fintype m] (e : n R ≃ₐ[R] m R) (h : ∀ (A : n R), (e A).transpose = e A.transpose)  :
= e A
theorem mem_skew_adjoint_matrices_lie_subalgebra_unit_smul {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (u : Rˣ) (J A : n R) :