mathlib documentation

algebra.lie.skew_adjoint

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

source
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) :
⁅f, g⁆ ∈ B.skew_adjoint_submodule
source
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) :
lie_subalgebra R (module.End 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
source
def skew_adjoint_lie_subalgebra_equiv {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) :
↥(skew_adjoint_lie_subalgebra (B.comp ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skew_adjoint_lie_subalgebra B)

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

Equations
source
@[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))) :
↑(⇑(skew_adjoint_lie_subalgebra_equiv B e) f) = ⇑(e.lie_conj) ↑f
source
@[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)) :
↑(⇑((skew_adjoint_lie_subalgebra_equiv B e).symm) f) = ⇑(e.symm.lie_conj) ↑f
source
theorem matrix.lie_transpose {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (A B : matrix n n R) :
⁅A, B⁆.transpose = ⁅B.transpose, A.transpose⁆
source
theorem matrix.is_skew_adjoint_bracket {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J A B : matrix n n R) (hA : A ∈ skew_adjoint_matrices_submodule J) (hB : B ∈ skew_adjoint_matrices_submodule J) :
⁅A, B⁆ ∈ skew_adjoint_matrices_submodule J
source
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) :
lie_subalgebra R (matrix n n R)

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

Equations
source
@[simp]
theorem mem_skew_adjoint_matrices_lie_subalgebra {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J A : matrix n n R) :
A ∈ skew_adjoint_matrices_lie_subalgebra J ↔ A ∈ skew_adjoint_matrices_submodule J
source
def skew_adjoint_matrices_lie_subalgebra_equiv {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J P : matrix n n R) (h : invertible P) :
↥(skew_adjoint_matrices_lie_subalgebra J) ≃ₗ⁅R⁆ ↥(skew_adjoint_matrices_lie_subalgebra ((P.transpose.mul J).mul 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
source
theorem skew_adjoint_matrices_lie_subalgebra_equiv_apply {R : Type u} {n : Type w} [comm_ring R] [decidable_eq n] [fintype n] (J P : matrix n n R) (h : invertible P) (A : ↥(skew_adjoint_matrices_lie_subalgebra J)) :
↑(⇑(skew_adjoint_matrices_lie_subalgebra_equiv J P h) A) = (P⁻¹.mul ↑A).mul P
source
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).transpose = ⇑e A.transpose) :
↥(skew_adjoint_matrices_lie_subalgebra J) ≃ₗ⁅R⁆ ↥(skew_adjoint_matrices_lie_subalgebra (⇑e J))

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

Equations
source
@[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).transpose = ⇑e A.transpose) (A : ↥(skew_adjoint_matrices_lie_subalgebra J)) :
↑(⇑(skew_adjoint_matrices_lie_subalgebra_equiv_transpose J e h) A) = ⇑e ↑A
source
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 : matrix n n R) :
A ∈ skew_adjoint_matrices_lie_subalgebra (u • J) ↔ A ∈ skew_adjoint_matrices_lie_subalgebra J