Documentation

Mathlib.Algebra.Lie.CartanSubalgebra

Cartan subalgebras #

Cartan subalgebras are one of the most important concepts in Lie theory. We define them here. The standard example is the set of diagonal matrices in the Lie algebra of matrices.

Main definitions #

Tags #

lie subalgebra, normalizer, idealizer, cartan subalgebra

source
def LieSubmodule.IsUcsLimit {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_1} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :
Prop

Given a Lie module M of a Lie algebra L, LieSubmodule.IsUcsLimit is the proposition that a Lie submodule N ⊆ M is the limiting value for the upper central series.

This is a characteristic property of Cartan subalgebras with the roles of L, M, N played by H, L, H, respectively. See LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit.

Equations
Instances For
    source
    class LieSubalgebra.IsCartanSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) :
    Prop

    A Cartan subalgebra is a nilpotent, self-normalizing subalgebra.

    A splitting Cartan subalgebra can be defined by mixing in LieModule.IsTriangularizable R H L.

    Instances
      source
      theorem LieSubalgebra.IsCartanSubalgebra.nilpotent {R : Type u} {L : Type v} :
      ∀ {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L} {H : LieSubalgebra R L} [self : H.IsCartanSubalgebra], LieAlgebra.IsNilpotent R ↥H
      source
      theorem LieSubalgebra.IsCartanSubalgebra.self_normalizing {R : Type u} {L : Type v} :
      ∀ {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L} {H : LieSubalgebra R L} [self : H.IsCartanSubalgebra], H.normalizer = H
      source
      instance LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
      LieAlgebra.IsNilpotent R ↥H
      Equations
      • ⋯ = ⋯
      source
      @[simp]
      theorem LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
      H.toLieSubmodule.normalizer = H.toLieSubmodule
      source
      @[simp]
      theorem LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] (k : ℕ) :
      LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
      source
      theorem LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) :
      H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit
      source
      theorem LieSubalgebra.ne_bot_of_isCartanSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
      H ≠ ⊥
      source
      @[instance 500]
      instance LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [Nontrivial L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
      Nontrivial ↥H
      Equations
      • ⋯ = ⋯
      source
      @[simp]
      theorem LieIdeal.normalizer_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :
      (lieIdealSubalgebra R L I).normalizer = ⊤
      source
      instance LieAlgebra.top_isCartanSubalgebra_of_nilpotent {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] :
      ⊤.IsCartanSubalgebra

      A nilpotent Lie algebra is its own Cartan subalgebra.

      Equations
      • ⋯ = ⋯