Lie algebras of skew-adjoint endomorphisms of a bilinear form
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) :
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
- skew_adjoint_lie_subalgebra B = {carrier := B.skew_adjoint_submodule.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}
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
@[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.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) :
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
- skew_adjoint_matrices_lie_subalgebra J = {carrier := (skew_adjoint_matrices_submodule J).carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := _}
@[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) :
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 : is_unit 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 : matrix n n R)
(h : is_unit P)
(A : ↥(skew_adjoint_matrices_lie_subalgebra J)) :
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.
@[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)) :
theorem
mem_skew_adjoint_matrices_lie_subalgebra_unit_smul
{R : Type u}
{n : Type w}
[comm_ring R]
[decidable_eq n]
[fintype n]
(u : units R)
(J A : matrix n n R) :