mathlib documentation

algebra.lie.skew_adjoint

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.

Main definitions #

Tags #

lie algebra, skew-adjoint, bilinear form

theorem bilin_form.is_skew_adjoint_bracket {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (B : bilin_form R M) (f g : module.End R 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] [add_comm_group M] [module R M] (B : bilin_form 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

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] [add_comm_group M] [module R M] (B : bilin_form R M) {N : Type w} [add_comm_group N] [module R 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] [add_comm_group M] [module R M] (B : bilin_form R M) {N : Type w} [add_comm_group N] [module R N] (e : N ≃ₗ[R] M) (f : (skew_adjoint_lie_subalgebra B)) :
theorem matrix.lie_transpose {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (A B : matrix n n R) :
def skew_adjoint_matrices_lie_subalgebra {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J : matrix n n R) :

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

Equations

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
def skew_adjoint_matrices_lie_subalgebra_equiv_transpose {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J : matrix n n R) {m : Type w} [decidable_eq m] [fintype m] (e : matrix n n R ≃ₐ[R] matrix m m R) (h : ∀ (A : matrix n n R), (e A) = e A) :

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 : matrix n n R) {m : Type w} [decidable_eq m] [fintype m] (e : matrix n n R ≃ₐ[R] matrix m m R) (h : ∀ (A : matrix n n R), (e A) = e A) (A : (skew_adjoint_matrices_lie_subalgebra J)) :