Documentation

Mathlib.Algebra.Lie.Subalgebra

Lie subalgebras #

This file defines Lie subalgebras of a Lie algebra and provides basic related definitions and results.

Main definitions #

Tags #

lie algebra, lie subalgebra

structure LieSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] extends Submodule :

A Lie subalgebra of a Lie algebra is submodule that is closed under the Lie bracket. This is a sufficient condition for the subset itself to form a Lie algebra.

  • carrier : Set L
  • add_mem' : ∀ {a b : L}, a self.carrierb self.carriera + b self.carrier
  • zero_mem' : 0 self.carrier
  • smul_mem' : ∀ (c : R) {x : L}, x self.carrierc x self.carrier
  • lie_mem' : ∀ {x y : L}, x self.carriery self.carrierx, y self.carrier

    A Lie subalgebra is closed under Lie bracket.

Instances For
    theorem LieSubalgebra.lie_mem' {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (self : LieSubalgebra R L) {x : L} {y : L} :
    x self.carriery self.carrierx, y self.carrier

    A Lie subalgebra is closed under Lie bracket.

    instance instZeroLieSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

    The zero algebra is a subalgebra of any Lie algebra.

    Equations
    Equations
    instance instCoeLieSubalgebraSubmodule (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    Equations
    instance LieSubalgebra.instSetLike (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    Equations
    Equations
    • =
    instance LieSubalgebra.lieRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
    LieRing L'

    A Lie subalgebra forms a new Lie ring.

    Equations
    instance LieSubalgebra.instModuleSubtypeMemOfIsScalarTower (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {R₁ : Type u_1} [Semiring R₁] [SMul R₁ R] [Module R₁ L] [IsScalarTower R₁ R L] (L' : LieSubalgebra R L) :
    Module R₁ L'

    A Lie subalgebra inherits module structures from L.

    Equations
    instance LieSubalgebra.instIsCentralScalarSubtypeMem (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {R₁ : Type u_1} [Semiring R₁] [SMul R₁ R] [SMul R₁ᵐᵒᵖ R] [Module R₁ L] [Module R₁ᵐᵒᵖ L] [IsScalarTower R₁ R L] [IsScalarTower R₁ᵐᵒᵖ R L] [IsCentralScalar R₁ L] (L' : LieSubalgebra R L) :
    IsCentralScalar R₁ L'
    Equations
    • =
    instance LieSubalgebra.instIsScalarTowerSubtypeMem (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {R₁ : Type u_1} [Semiring R₁] [SMul R₁ R] [Module R₁ L] [IsScalarTower R₁ R L] (L' : LieSubalgebra R L) :
    IsScalarTower R₁ R L'
    Equations
    • =
    Equations
    • =
    instance LieSubalgebra.lieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
    LieAlgebra R L'

    A Lie subalgebra forms a new Lie algebra.

    Equations
    @[simp]
    theorem LieSubalgebra.zero_mem {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
    0 L'
    theorem LieSubalgebra.add_mem {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} {y : L} :
    x L'y L'x + y L'
    theorem LieSubalgebra.sub_mem {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} {y : L} :
    x L'y L'x - y L'
    theorem LieSubalgebra.smul_mem {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (t : R) {x : L} (h : x L') :
    t x L'
    theorem LieSubalgebra.lie_mem {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} {y : L} (hx : x L') (hy : y L') :
    x, y L'
    theorem LieSubalgebra.mem_carrier {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} :
    x L'.carrier x L'
    @[simp]
    theorem LieSubalgebra.mem_mk_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set L) (h₁ : ∀ {a b : L}, a Sb Sa + b S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : L}, x { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrierc x { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x y : L}, x { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carriery { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrierx, y { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) {x : L} :
    x { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } x S
    @[simp]
    theorem LieSubalgebra.mem_coe_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} :
    x L'.toSubmodule x L'
    theorem LieSubalgebra.mem_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} :
    x L' x L'
    @[simp]
    theorem LieSubalgebra.coe_bracket {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (x : L') (y : L') :
    x, y = x, y
    theorem LieSubalgebra.ext_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (x : L') (y : L') :
    x = y x = y
    theorem LieSubalgebra.coe_zero_iff_zero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) (x : L') :
    x = 0 x = 0
    theorem LieSubalgebra.ext {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' : LieSubalgebra R L) (L₂' : LieSubalgebra R L) (h : ∀ (x : L), x L₁' x L₂') :
    L₁' = L₂'
    theorem LieSubalgebra.ext_iff' {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' : LieSubalgebra R L) (L₂' : LieSubalgebra R L) :
    L₁' = L₂' ∀ (x : L), x L₁' x L₂'
    @[simp]
    theorem LieSubalgebra.mk_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set L) (h₁ : ∀ {a b : L}, a Sb Sa + b S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : L}, x { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrierc x { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x y : L}, x { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carriery { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrierx, y { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) :
    { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } = S
    theorem LieSubalgebra.coe_to_submodule_mk {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (p : Submodule R L) (h : ∀ {x y : L}, x p.carriery p.carrierx, y p.carrier) :
    { toSubmodule := p, lie_mem' := h }.toSubmodule = p
    theorem LieSubalgebra.coe_injective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
    Function.Injective SetLike.coe
    theorem LieSubalgebra.coe_set_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' : LieSubalgebra R L) (L₂' : LieSubalgebra R L) :
    L₁' = L₂' L₁' = L₂'
    theorem LieSubalgebra.to_submodule_injective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
    Function.Injective LieSubalgebra.toSubmodule
    @[simp]
    theorem LieSubalgebra.coe_to_submodule_eq_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' : LieSubalgebra R L) (L₂' : LieSubalgebra R L) :
    L₁'.toSubmodule = L₂'.toSubmodule L₁' = L₂'
    theorem LieSubalgebra.coe_to_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
    L'.toSubmodule = L'
    instance LieSubalgebra.lieRingModule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] :
    LieRingModule (L') M

    Given a Lie algebra L containing a Lie subalgebra L' ⊆ L, together with a Lie ring module M of L, we may regard M as a Lie ring module of L' by restriction.

    Equations
    @[simp]
    theorem LieSubalgebra.coe_bracket_of_module {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] (x : L') (m : M) :
    x, m = x, m
    instance LieSubalgebra.lieModule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] [Module R M] [LieModule R L M] :
    LieModule R (L') M

    Given a Lie algebra L containing a Lie subalgebra L' ⊆ L, together with a Lie module M of L, we may regard M as a Lie module of L' by restriction.

    Equations
    • =
    def LieModuleHom.restrictLie {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type w} [AddCommGroup M] [LieRingModule L M] {N : Type w₁} [AddCommGroup N] [LieRingModule L N] [Module R N] [Module R M] (f : M →ₗ⁅R,L N) (L' : LieSubalgebra R L) :
    M →ₗ⁅R,L' N

    An L-equivariant map of Lie modules M → N is L'-equivariant for any Lie subalgebra L' ⊆ L.

    Equations
    • f.restrictLie L' = let __src := f; { toLinearMap := __src, map_lie' := }
    Instances For
      @[simp]
      theorem LieModuleHom.coe_restrictLie {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {M : Type w} [AddCommGroup M] [LieRingModule L M] {N : Type w₁} [AddCommGroup N] [LieRingModule L N] [Module R N] [Module R M] (f : M →ₗ⁅R,L N) :
      (f.restrictLie L') = f
      def LieSubalgebra.incl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
      L' →ₗ⁅R L

      The embedding of a Lie subalgebra into the ambient space as a morphism of Lie algebras.

      Equations
      • L'.incl = let __src := L'.subtype; { toLinearMap := __src, map_lie' := }
      Instances For
        @[simp]
        theorem LieSubalgebra.coe_incl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
        L'.incl = Subtype.val
        def LieSubalgebra.incl' {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
        L' →ₗ⁅R,L' L

        The embedding of a Lie subalgebra into the ambient space as a morphism of Lie modules.

        Equations
        • L'.incl' = let __src := L'.subtype; { toLinearMap := __src, map_lie' := }
        Instances For
          @[simp]
          theorem LieSubalgebra.coe_incl' {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) :
          L'.incl' = Subtype.val
          def LieHom.range {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :

          The range of a morphism of Lie algebras is a Lie subalgebra.

          Equations
          • f.range = let __src := LinearMap.range f; { toSubmodule := __src, lie_mem' := }
          Instances For
            @[simp]
            theorem LieHom.range_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
            f.range = Set.range f
            @[simp]
            theorem LieHom.mem_range {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (x : L₂) :
            x f.range ∃ (y : L), f y = x
            theorem LieHom.mem_range_self {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (x : L) :
            f x f.range
            def LieHom.rangeRestrict {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
            L →ₗ⁅R f.range

            We can restrict a morphism to a (surjective) map to its range.

            Equations
            • f.rangeRestrict = let __src := (f).rangeRestrict; { toLinearMap := __src, map_lie' := }
            Instances For
              @[simp]
              theorem LieHom.rangeRestrict_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (x : L) :
              f.rangeRestrict x = f x,
              theorem LieHom.surjective_rangeRestrict {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
              Function.Surjective f.rangeRestrict
              noncomputable def LieHom.equivRangeOfInjective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (h : Function.Injective f) :
              L ≃ₗ⁅R f.range

              A Lie algebra is equivalent to its range under an injective Lie algebra morphism.

              Equations
              Instances For
                @[simp]
                theorem LieHom.equivRangeOfInjective_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (h : Function.Injective f) (x : L) :
                (f.equivRangeOfInjective h) x = f x,
                theorem Submodule.exists_lieSubalgebra_coe_eq_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (p : Submodule R L) :
                (∃ (K : LieSubalgebra R L), K.toSubmodule = p) ∀ (x y : L), x py px, y p
                @[simp]
                theorem LieSubalgebra.incl_range {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) :
                K.incl.range = K
                def LieSubalgebra.map {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (K : LieSubalgebra R L) :

                The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the codomain.

                Equations
                Instances For
                  @[simp]
                  theorem LieSubalgebra.mem_map {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (K : LieSubalgebra R L) (x : L₂) :
                  x LieSubalgebra.map f K yK, f y = x
                  theorem LieSubalgebra.mem_map_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (K : LieSubalgebra R L) (e : L ≃ₗ⁅R L₂) (x : L₂) :
                  x LieSubalgebra.map e.toLieHom K x Submodule.map (e.toLinearEquiv) K.toSubmodule
                  def LieSubalgebra.comap {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (K₂ : LieSubalgebra R L₂) :

                  The preimage of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the domain.

                  Equations
                  Instances For
                    Equations
                    theorem LieSubalgebra.le_def {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (K' : LieSubalgebra R L) :
                    K K' K K'
                    @[simp]
                    theorem LieSubalgebra.coe_submodule_le_coe_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (K' : LieSubalgebra R L) :
                    K.toSubmodule K'.toSubmodule K K'
                    instance LieSubalgebra.instBot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    Equations
                    • LieSubalgebra.instBot = { bot := 0 }
                    @[simp]
                    theorem LieSubalgebra.bot_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    = {0}
                    @[simp]
                    theorem LieSubalgebra.bot_coe_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    .toSubmodule =
                    @[simp]
                    theorem LieSubalgebra.mem_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
                    x x = 0
                    instance LieSubalgebra.instTop {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    Equations
                    • LieSubalgebra.instTop = { top := let __src := ; { toSubmodule := __src, lie_mem' := } }
                    @[simp]
                    theorem LieSubalgebra.top_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    = Set.univ
                    @[simp]
                    theorem LieSubalgebra.top_coe_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    .toSubmodule =
                    @[simp]
                    theorem LieSubalgebra.mem_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
                    theorem LieHom.range_eq_map {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
                    instance LieSubalgebra.instInf {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    Equations
                    • LieSubalgebra.instInf = { inf := fun (K K' : LieSubalgebra R L) => let __src := K.toSubmodule K'.toSubmodule; { toSubmodule := __src, lie_mem' := } }
                    instance LieSubalgebra.instInfSet {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    @[simp]
                    theorem LieSubalgebra.inf_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (K' : LieSubalgebra R L) :
                    (K K') = K K'
                    @[simp]
                    theorem LieSubalgebra.sInf_coe_to_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set (LieSubalgebra R L)) :
                    (sInf S).toSubmodule = sInf {x : Submodule R L | sS, s.toSubmodule = x}
                    @[simp]
                    theorem LieSubalgebra.sInf_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set (LieSubalgebra R L)) :
                    (sInf S) = sS, s
                    theorem LieSubalgebra.sInf_glb {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set (LieSubalgebra R L)) :
                    IsGLB S (sInf S)

                    The set of Lie subalgebras of a Lie algebra form a complete lattice.

                    We provide explicit values for the fields bot, top, inf to get more convenient definitions than we would otherwise obtain from completeLatticeOfInf.

                    Equations
                    instance LieSubalgebra.instAdd {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    Equations
                    • LieSubalgebra.instAdd = { add := Sup.sup }
                    instance LieSubalgebra.instZero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
                    Equations
                    • LieSubalgebra.instZero = { zero := }
                    Equations
                    Equations
                    • LieSubalgebra.instCanonicallyOrderedAddCommMonoid = let __src := LieSubalgebra.addCommMonoid; let __src_1 := LieSubalgebra.completeLattice; CanonicallyOrderedAddCommMonoid.mk
                    @[simp]
                    theorem LieSubalgebra.add_eq_sup {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (K' : LieSubalgebra R L) :
                    K + K' = K K'
                    @[simp]
                    theorem LieSubalgebra.inf_coe_to_submodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (K' : LieSubalgebra R L) :
                    (K K').toSubmodule = K.toSubmodule K'.toSubmodule
                    @[simp]
                    theorem LieSubalgebra.mem_inf {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) (K' : LieSubalgebra R L) (x : L) :
                    x K K' x K x K'
                    theorem LieSubalgebra.eq_bot_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) :
                    K = xK, x = 0
                    Equations
                    • =
                    theorem LieSubalgebra.wellFounded_of_noetherian (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] :
                    WellFounded fun (x x_1 : LieSubalgebra R L) => x > x_1
                    def LieSubalgebra.inclusion {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') :
                    K →ₗ⁅R K'

                    Given two nested Lie subalgebras K ⊆ K', the inclusion K ↪ K' is a morphism of Lie algebras.

                    Equations
                    Instances For
                      @[simp]
                      theorem LieSubalgebra.coe_inclusion {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') (x : K) :
                      ((LieSubalgebra.inclusion h) x) = x
                      theorem LieSubalgebra.inclusion_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') (x : K) :
                      (LieSubalgebra.inclusion h) x = x,
                      def LieSubalgebra.ofLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') :

                      Given two nested Lie subalgebras K ⊆ K', we can view K as a Lie subalgebra of K', regarded as Lie algebra in its own right.

                      Equations
                      Instances For
                        @[simp]
                        theorem LieSubalgebra.mem_ofLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') (x : K') :
                        theorem LieSubalgebra.ofLe_eq_comap_incl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') :
                        @[simp]
                        theorem LieSubalgebra.coe_ofLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') :
                        noncomputable def LieSubalgebra.equivOfLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') :

                        Given nested Lie subalgebras K ⊆ K', there is a natural equivalence from K to its image in K'.

                        Equations
                        Instances For
                          @[simp]
                          theorem LieSubalgebra.equivOfLe_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K K') (x : K) :
                          theorem LieSubalgebra.map_le_iff_le_comap {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] {f : L →ₗ⁅R L₂} {K : LieSubalgebra R L} {K' : LieSubalgebra R L₂} :
                          theorem LieSubalgebra.gc_map_comap {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] {f : L →ₗ⁅R L₂} :
                          def LieSubalgebra.lieSpan (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (s : Set L) :

                          The Lie subalgebra of a Lie algebra L generated by a subset s ⊆ L.

                          Equations
                          Instances For
                            theorem LieSubalgebra.mem_lieSpan {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {x : L} :
                            x LieSubalgebra.lieSpan R L s ∀ (K : LieSubalgebra R L), s Kx K
                            theorem LieSubalgebra.subset_lieSpan {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} :
                            theorem LieSubalgebra.submodule_span_le_lieSpan {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} :
                            Submodule.span R s (LieSubalgebra.lieSpan R L s).toSubmodule
                            theorem LieSubalgebra.lieSpan_le {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {K : LieSubalgebra R L} :
                            theorem LieSubalgebra.lieSpan_mono {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {t : Set L} (h : s t) :
                            theorem LieSubalgebra.lieSpan_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) :
                            theorem LieSubalgebra.coe_lieSpan_submodule_eq_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {p : Submodule R L} :
                            (LieSubalgebra.lieSpan R L p).toSubmodule = p ∃ (K : LieSubalgebra R L), K.toSubmodule = p
                            def LieSubalgebra.gi (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

                            lieSpan forms a Galois insertion with the coercion from LieSubalgebra to Set.

                            Equations
                            Instances For
                              @[simp]
                              theorem LieSubalgebra.span_univ (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
                              theorem LieSubalgebra.span_iUnion (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Sort u_1} (s : ιSet L) :
                              LieSubalgebra.lieSpan R L (⋃ (i : ι), s i) = ⨆ (i : ι), LieSubalgebra.lieSpan R L (s i)
                              theorem LieSubalgebra.lieSpan_induction (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {p : LProp} {x : L} (h : x LieSubalgebra.lieSpan R L s) (mem : xs, p x) (zero : p 0) (smul : ∀ (r : R) {x : L}, p xp (r x)) (add : ∀ (x y : L), p xp yp (x + y)) (lie : ∀ (x y : L), p xp yp x, y) :
                              p x

                              If a predicate p is true on some set s ⊆ L, true for 0, stable by scalar multiplication, by addition and by Lie bracket, then the predicate is true on the Lie span of s. (Since s can be empty, and the Lie span always contains 0, the assumption that p 0 holds cannot be removed.)

                              noncomputable def LieEquiv.ofInjective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : Function.Injective f) :
                              L₁ ≃ₗ⁅R f.range

                              An injective Lie algebra morphism is an equivalence onto its range.

                              Equations
                              Instances For
                                @[simp]
                                theorem LieEquiv.ofInjective_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : Function.Injective f) (x : L₁) :
                                ((LieEquiv.ofInjective f h) x) = f x
                                def LieEquiv.ofEq {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (L₁' : LieSubalgebra R L₁) (L₁'' : LieSubalgebra R L₁) (h : L₁' = L₁'') :
                                L₁' ≃ₗ⁅R L₁''

                                Lie subalgebras that are equal as sets are equivalent as Lie algebras.

                                Equations
                                • LieEquiv.ofEq L₁' L₁'' h = let __src := LinearEquiv.ofEq L₁'.toSubmodule L₁''.toSubmodule ; { toLinearMap := __src, map_lie' := , invFun := __src.invFun, left_inv := , right_inv := }
                                Instances For
                                  @[simp]
                                  theorem LieEquiv.ofEq_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (L : LieSubalgebra R L₁) (L' : LieSubalgebra R L₁) (h : L = L') (x : L) :
                                  ((LieEquiv.ofEq L L' h) x) = x
                                  def LieEquiv.lieSubalgebraMap {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁'' : LieSubalgebra R L₁) (e : L₁ ≃ₗ⁅R L₂) :
                                  L₁'' ≃ₗ⁅R (LieSubalgebra.map e.toLieHom L₁'')

                                  An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image.

                                  Equations
                                  • LieEquiv.lieSubalgebraMap L₁'' e = let __src := e.toLinearEquiv.submoduleMap L₁''.toSubmodule; { toLinearMap := __src, map_lie' := , invFun := __src.invFun, left_inv := , right_inv := }
                                  Instances For
                                    @[simp]
                                    theorem LieEquiv.lieSubalgebraMap_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁'' : LieSubalgebra R L₁) (e : L₁ ≃ₗ⁅R L₂) (x : L₁'') :
                                    ((LieEquiv.lieSubalgebraMap L₁'' e) x) = e x
                                    def LieEquiv.ofSubalgebras {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') :
                                    L₁' ≃ₗ⁅R L₂'

                                    An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem LieEquiv.ofSubalgebras_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : L₁') :
                                      ((LieEquiv.ofSubalgebras L₁' L₂' e h) x) = e x
                                      @[simp]
                                      theorem LieEquiv.ofSubalgebras_symm_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : LieSubalgebra R L₁) (L₂' : LieSubalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : L₂') :
                                      ((LieEquiv.ofSubalgebras L₁' L₂' e h).symm x) = e.symm x