Documentation

Mathlib.Algebra.Lie.SkewAdjoint

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 endomorphisms 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 LinearMap.BilinForm.isSkewAdjoint_bracket {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {f : Module.End R M} {g : Module.End R M} (hf : f ∈ LinearMap.skewAdjointSubmodule B) (hg : g ∈ LinearMap.skewAdjointSubmodule B) :
⁅f, g⁆ ∈ LinearMap.skewAdjointSubmodule B
source
def skewAdjointLieSubalgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) :
LieSubalgebra 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
Instances For
    source
    def skewAdjointLieSubalgebraEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {N : Type w} [AddCommGroup N] [Module R N] (e : N ≃ₗ[R] M) :
    ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e)) ≃ₗ⁅R⁆ ↥(skewAdjointLieSubalgebra B)

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

    Equations
    Instances For
      source
      @[simp]
      theorem skewAdjointLieSubalgebraEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {N : Type w} [AddCommGroup N] [Module R N] (e : N ≃ₗ[R] M) (f : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e))) :
      ↑((skewAdjointLieSubalgebraEquiv B e) f) = (LinearEquiv.lieConj e) ↑f
      source
      @[simp]
      theorem skewAdjointLieSubalgebraEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) {N : Type w} [AddCommGroup N] [Module R N] (e : N ≃ₗ[R] M) (f : ↥(skewAdjointLieSubalgebra B)) :
      ↑((LieEquiv.symm (skewAdjointLieSubalgebraEquiv B e)) f) = (LinearEquiv.lieConj (LinearEquiv.symm e)) ↑f
      source
      theorem Matrix.lie_transpose {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (A : Matrix n n R) (B : Matrix n n R) :
      Matrix.transpose ⁅A, B⁆ = ⁅Matrix.transpose B, Matrix.transpose A⁆
      source
      theorem Matrix.isSkewAdjoint_bracket {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) {A : Matrix n n R} {B : Matrix n n R} (hA : A ∈ skewAdjointMatricesSubmodule J) (hB : B ∈ skewAdjointMatricesSubmodule J) :
      ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J
      source
      def skewAdjointMatricesLieSubalgebra {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) :
      LieSubalgebra R (Matrix n n R)

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

      Equations
      Instances For
        source
        @[simp]
        theorem mem_skewAdjointMatricesLieSubalgebra {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) (A : Matrix n n R) :
        A ∈ skewAdjointMatricesLieSubalgebra J ↔ A ∈ skewAdjointMatricesSubmodule J
        source
        def skewAdjointMatricesLieSubalgebraEquiv {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) (P : Matrix n n R) (h : Invertible P) :
        ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (Matrix.transpose P * J * 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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem skewAdjointMatricesLieSubalgebraEquiv_apply {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) (P : Matrix n n R) (h : Invertible P) (A : ↥(skewAdjointMatricesLieSubalgebra J)) :
          ↑((skewAdjointMatricesLieSubalgebraEquiv J P h) A) = P⁻¹ * ↑A * P
          source
          def skewAdjointMatricesLieSubalgebraEquivTranspose {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) {m : Type w} [DecidableEq m] [Fintype m] (e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ (A : Matrix n n R), Matrix.transpose (e A) = e (Matrix.transpose A)) :
          ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (e J))

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

          Equations
          Instances For
            source
            @[simp]
            theorem skewAdjointMatricesLieSubalgebraEquivTranspose_apply {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (J : Matrix n n R) {m : Type w} [DecidableEq m] [Fintype m] (e : Matrix n n R ≃ₐ[R] Matrix m m R) (h : ∀ (A : Matrix n n R), Matrix.transpose (e A) = e (Matrix.transpose A)) (A : ↥(skewAdjointMatricesLieSubalgebra J)) :
            ↑((skewAdjointMatricesLieSubalgebraEquivTranspose J e h) A) = e ↑A
            source
            theorem mem_skewAdjointMatricesLieSubalgebra_unit_smul {R : Type u} {n : Type w} [CommRing R] [DecidableEq n] [Fintype n] (u : Rˣ) (J : Matrix n n R) (A : Matrix n n R) :
            A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J