mathlib documentation


Lie algebras of skew-adjoint endomorphisms of a bilinear form #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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


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

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.


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.


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