Lie subalgebras

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

Main definitions

• LieSubalgebra
• LieSubalgebra.incl
• LieSubalgebra.map
• LieHom.range
• LieEquiv.ofInjective
• LieEquiv.ofEq
• LieEquiv.ofSubalgebras

Tags

lie algebra, lie subalgebra

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

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.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : R) {x : L} : x ∈ self.carrier → c • x ∈ self.carrier
• lie_mem' {x y : L} : x ∈ self.carrier → y ∈ self.carrier → ⁅x, y⁆ ∈ self.carrier

  A Lie subalgebra is closed under Lie bracket.

@[implicit_reducible]

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

The zero algebra is a subalgebra of any Lie algebra.

Equations

• instZeroLieSubalgebra R L = { zero := { toSubmodule := 0, lie_mem' := ⋯ } }

@[implicit_reducible]

instance instInhabitedLieSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Inhabited (LieSubalgebra R L)

Equations

• instInhabitedLieSubalgebra R L = { default := 0 }

@[implicit_reducible]

instance instCoeLieSubalgebraSubmodule (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Coe (LieSubalgebra R L) (Submodule R L)

Equations

• instCoeLieSubalgebraSubmodule R L = { coe := LieSubalgebra.toSubmodule }

@[implicit_reducible]

instance LieSubalgebra.instSetLike (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : SetLike (LieSubalgebra R L) L

Equations

• LieSubalgebra.instSetLike R L = { coe := fun (L' : LieSubalgebra R L) => L'.carrier, coe_injective' := ⋯ }

@[implicit_reducible]

instance LieSubalgebra.instPartialOrder (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : PartialOrder (LieSubalgebra R L)

Equations

• LieSubalgebra.instPartialOrder R L = PartialOrder.ofSetLike (LieSubalgebra R L) L

instance LieSubalgebra.instAddSubgroupClass (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : AddSubgroupClass (LieSubalgebra R L) L

instance LieSubalgebra.instSMulMemClass (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : SMulMemClass (LieSubalgebra R L) R L

@[implicit_reducible]

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

• LieSubalgebra.lieRing R L L' = { toAddCommGroup := AddSubgroupClass.toAddCommGroup L', bracket := fun (x y : ↥L') => ⟨⁅↑x, ↑y⁆, ⋯⟩, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

@[implicit_reducible]

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

• LieSubalgebra.instModuleSubtypeMemOfIsScalarTower R L L' = L'.module'

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'

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'

instance LieSubalgebra.instIsNoetherianSubtypeMem (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) [IsNoetherian R L] : IsNoetherian R ↥L'

instance LieSubalgebra.instIsArtinianSubtypeMem (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) [IsArtinian R L] : IsArtinian R ↥L'

@[implicit_reducible]

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

• LieSubalgebra.lieAlgebra R L L' = { toModule := LieSubalgebra.instModuleSubtypeMemOfIsScalarTower R L L', lie_smul := ⋯ }

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 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 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 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'

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 ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • 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₃ }.carrier → y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, 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_toSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) {x : L} : x ∈ L'.toSubmodule ↔ x ∈ L'

@[simp]

theorem LieSubalgebra.mem_mk_iff' {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (p : Submodule R L) (h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier) {x : L} : x ∈ { toSubmodule := p, lie_mem' := h } ↔ x ∈ p

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 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 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₁' 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₁' 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 ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • 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₃ }.carrier → y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, 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.toSubmodule_mk {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (p : Submodule R L) (h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, 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₁' L₂' : LieSubalgebra R L) : ↑L₁' = ↑L₂' ↔ L₁' = L₂'

theorem LieSubalgebra.toSubmodule_injective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Injective toSubmodule

@[simp]

theorem LieSubalgebra.toSubmodule_inj {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L₁' L₂' : LieSubalgebra R L) : L₁'.toSubmodule = L₂'.toSubmodule ↔ L₁' = L₂'

theorem LieSubalgebra.coe_toSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (L' : LieSubalgebra R L) : ↑L'.toSubmodule = ↑L'

@[implicit_reducible]

instance LieSubalgebra.instBracketSubtypeMem {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] : Bracket (↥L') M

Equations

• L'.instBracketSubtypeMem = { bracket := fun (x : ↥L') (m : M) => ⁅↑x, m⁆ }

@[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.instIsLieTowerSubtypeMem {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] : IsLieTower (↥L') L M

@[implicit_reducible]

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

• L'.lieRingModule = { toBracket := L'.instBracketSubtypeMem, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

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.

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' = { toLinearMap := ↑f, map_lie' := ⋯ }

@[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 = { toLinearMap := L'.subtype, map_lie' := ⋯ }

@[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' = { toLinearMap := L'.subtype, map_lie' := ⋯ }

@[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₂) : LieSubalgebra R L₂

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

Equations

• f.range = { toSubmodule := (↑f).range, lie_mem' := ⋯ }

@[simp]

theorem LieHom.coe_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₂) : ↑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 = { toLinearMap := (↑f).rangeRestrict, map_lie' := ⋯ }

@[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

• f.equivRangeOfInjective h = LieEquiv.ofBijective f.rangeRestrict ⋯

@[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 ∈ p → y ∈ p → ⁅x, 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) : LieSubalgebra R L₂

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

Equations

• LieSubalgebra.map f K = { toSubmodule := Submodule.map (↑f) K.toSubmodule, lie_mem' := ⋯ }

@[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 ∈ map f K ↔ ∃ y ∈ K, 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 ∈ 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₂) : LieSubalgebra R L

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

Equations

• LieSubalgebra.comap f K₂ = { toSubmodule := Submodule.comap (↑f) K₂.toSubmodule, lie_mem' := ⋯ }

@[simp]

theorem LieSubalgebra.mem_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₂) {x : L} : x ∈ comap f K₂ ↔ f x ∈ K₂

@[implicit_reducible]

instance LieSubalgebra.instPartialOrder_1 {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : PartialOrder (LieSubalgebra R L)

Equations

• One or more equations did not get rendered due to their size.

theorem LieSubalgebra.le_def {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : K ≤ K' ↔ ↑K ⊆ ↑K'

@[simp]

theorem LieSubalgebra.toSubmodule_le_toSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : K.toSubmodule ≤ K'.toSubmodule ↔ K ≤ K'

@[implicit_reducible]

instance LieSubalgebra.instBot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Bot (LieSubalgebra 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_toSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ⊥.toSubmodule = ⊥

@[simp]

theorem LieSubalgebra.toSubmodule_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : K.toSubmodule = ⊥ ↔ K = ⊥

@[simp]

theorem LieSubalgebra.mem_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : x ∈ ⊥ ↔ x = 0

@[implicit_reducible]

instance LieSubalgebra.instTop {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Top (LieSubalgebra 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_toSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ⊤.toSubmodule = ⊤

@[simp]

theorem LieSubalgebra.toSubmodule_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : K.toSubmodule = ⊤ ↔ K = ⊤

@[simp]

theorem LieSubalgebra.mem_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : x ∈ ⊤

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₂) : f.range = LieSubalgebra.map f ⊤

@[implicit_reducible]

instance LieSubalgebra.instMin {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Min (LieSubalgebra R L)

Equations

• LieSubalgebra.instMin = { min := fun (K K' : LieSubalgebra R L) => let __src := K.toSubmodule ⊓ K'.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ } }

@[implicit_reducible]

instance LieSubalgebra.instInfSet {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : InfSet (LieSubalgebra R L)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieSubalgebra.coe_inf {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : ↑(K ⊓ K') = ↑K ∩ ↑K'

@[simp]

theorem LieSubalgebra.sInf_toSubmodule {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 | ∃ s ∈ S, s.toSubmodule = x}

@[simp]

theorem LieSubalgebra.coe_sInf {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (S : Set (LieSubalgebra R L)) : ↑(sInf S) = ⋂ s ∈ S, ↑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)

@[implicit_reducible]

instance LieSubalgebra.completeLattice {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : CompleteLattice (LieSubalgebra R L)

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

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance LieSubalgebra.instAdd {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Add (LieSubalgebra R L)

Equations

• LieSubalgebra.instAdd = { add := max }

@[implicit_reducible]

instance LieSubalgebra.instZero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Zero (LieSubalgebra R L)

Equations

• LieSubalgebra.instZero = { zero := ⊥ }

@[implicit_reducible]

instance LieSubalgebra.addCommMonoid {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : AddCommMonoid (LieSubalgebra R L)

Equations

• One or more equations did not get rendered due to their size.

instance LieSubalgebra.instIsOrderedAddMonoid {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : IsOrderedAddMonoid (LieSubalgebra R L)

instance LieSubalgebra.instCanonicallyOrderedAdd {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : CanonicallyOrderedAdd (LieSubalgebra R L)

@[simp]

theorem LieSubalgebra.add_eq_sup {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K K' : LieSubalgebra R L) : K + K' = K ⊔ K'

@[simp]

theorem LieSubalgebra.inf_toSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K 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 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 = ⊥ ↔ ∀ x ∈ K, x = 0

instance LieSubalgebra.subsingleton_of_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Subsingleton (LieSubalgebra R ↥⊥)

theorem LieSubalgebra.subsingleton_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : Subsingleton ↥⊥

@[simp]

theorem LieSubalgebra.disjoint_toSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} : Disjoint K.toSubmodule K'.toSubmodule ↔ Disjoint K K'

instance LieSubalgebra.wellFoundedGT_of_noetherian (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : WellFoundedGT (LieSubalgebra R L)

def LieSubalgebra.inclusion {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K 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

• LieSubalgebra.inclusion h = { toLinearMap := Submodule.inclusion h, map_lie' := ⋯ }

@[simp]

theorem LieSubalgebra.coe_inclusion {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K) : ↑((inclusion h) x) = ↑x

theorem LieSubalgebra.inclusion_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K) : (inclusion h) x = ⟨↑x, ⋯⟩

theorem LieSubalgebra.inclusion_injective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : Function.Injective ⇑(inclusion h)

def LieSubalgebra.ofLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : LieSubalgebra R ↥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

• LieSubalgebra.ofLe h = (LieSubalgebra.inclusion h).range

@[simp]

theorem LieSubalgebra.mem_ofLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K') : x ∈ ofLe h ↔ ↑x ∈ K

theorem LieSubalgebra.ofLe_eq_comap_incl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : ofLe h = comap K'.incl K

@[simp]

theorem LieSubalgebra.coe_ofLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : (ofLe h).toSubmodule = (Submodule.inclusion h).range

noncomputable def LieSubalgebra.equivOfLe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') : ↥K ≃ₗ⁅R⁆ ↥(ofLe h)

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

Equations

• LieSubalgebra.equivOfLe h = (LieSubalgebra.inclusion h).equivRangeOfInjective ⋯

@[simp]

theorem LieSubalgebra.equivOfLe_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K) : (equivOfLe h) x = ⟨(inclusion h) x, ⋯⟩

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₂} : map f K ≤ K' ↔ K ≤ comap f K'

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₂} : GaloisConnection (map f) (comap f)

def LieSubalgebra.lieSpan (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (s : Set L) : LieSubalgebra R L

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

Equations

• LieSubalgebra.lieSpan R L s = sInf {N : LieSubalgebra R L | s ⊆ ↑N}

theorem LieSubalgebra.mem_lieSpan {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} {x : L} : x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

theorem LieSubalgebra.subset_lieSpan {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} : s ⊆ ↑(lieSpan R L s)

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 ≤ (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} : lieSpan R L s ≤ K ↔ s ⊆ ↑K

theorem LieSubalgebra.lieSpan_mono {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s t : Set L} (h : s ⊆ t) : lieSpan R L s ≤ lieSpan R L t

theorem LieSubalgebra.lieSpan_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : lieSpan R L ↑K = K

theorem LieSubalgebra.coe_lieSpan_submodule_eq_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {p : Submodule R L} : (lieSpan R L ↑p).toSubmodule = p ↔ ∃ (K : LieSubalgebra R L), K.toSubmodule = p

theorem LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} (hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0) : (lieSpan R L s).toSubmodule = Submodule.span R s

def LieSubalgebra.gi (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : GaloisInsertion (lieSpan R L) SetLike.coe

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

Equations

• LieSubalgebra.gi R L = { choice := fun (s : Set L) (x : ↑(LieSubalgebra.lieSpan R L s) ≤ s) => LieSubalgebra.lieSpan R L s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

@[simp]

theorem LieSubalgebra.span_empty (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : lieSpan R L ∅ = ⊥

@[simp]

theorem LieSubalgebra.span_univ (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : lieSpan R L Set.univ = ⊤

theorem LieSubalgebra.span_union (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (s t : Set L) : lieSpan R L (s ∪ t) = lieSpan R L s ⊔ lieSpan R L t

theorem LieSubalgebra.span_iUnion (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Sort u_1} (s : ι → Set L) : lieSpan R L (⋃ (i : ι), s i) = ⨆ (i : ι), 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 : (x : L) → x ∈ lieSpan R L s → Prop} (mem : ∀ (x : L) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p x hx → p y hy → p (x + y) ⋯) (smul : ∀ (a : R) (x : L) (hx : x ∈ lieSpan R L s), p x hx → p (a • x) ⋯) {x : L} (lie : ∀ (x y : L) (hx : x ∈ lieSpan R L s) (hy : y ∈ lieSpan R L s), p x hx → p y hy → p ⁅x, y⁆ ⋯) (hx : x ∈ lieSpan R L s) : p x hx

An induction principle for span membership. If p holds for 0 and all elements of s, and is preserved under addition, scalar multiplication and the Lie bracket, then p holds for all elements of the Lie algebra spanned by s.

@[simp]

theorem LieSubalgebra.lieSpan_neg (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} : lieSpan R L (-s) = lieSpan R L s

@[simp]

theorem LieSubalgebra.lieSpan_lieSpan_coe_preimage {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} : lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) = ⊤

theorem LieSubalgebra.comap_lieSpan_range_eq (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {ι : Type u_1} (f : ι → ↥K) : comap K.incl (lieSpan R L (Set.range (Subtype.val ∘ f))) = lieSpan R (↥K) (Set.range f)

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

• LieEquiv.ofInjective f h = { toLinearMap := ↑(LinearEquiv.ofInjective ↑f ⋯), map_lie' := ⋯, invFun := (LinearEquiv.ofInjective ↑f ⋯).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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₁) : ↑((ofInjective f h) x) = f x

def LieEquiv.ofEq {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (L₁' L₁'' : LieSubalgebra R L₁) (h : ↑L₁' = ↑L₁'') : ↥L₁' ≃ₗ⁅R⁆ ↥L₁''

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieEquiv.ofEq_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (L L' : LieSubalgebra R L₁) (h : ↑L = ↑L') (x : ↥L) : ↑((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

• One or more equations did not get rendered due to their size.

@[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₁'') : ↑((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.

@[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₁') : ↑((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₂') : ↑((ofSubalgebras L₁' L₂' e h).symm x) = e.symm ↑x