Lie Ideals

This file defines Lie ideals, which are Lie submodules of a Lie algebra over itself. They are defined as a special case of LieSubmodule, and inherit much of their structure from it.

We also prove some basic properties of Lie ideals, including how they behave under Lie algebra homomorphisms (map, comap) and how they relate to the lattice structure on Lie submodules.

Main definitions

• LieIdeal
• LieIdeal.map
• LieIdeal.comap

Tags

Lie algebra, ideal, submodule, Lie submodule

@[reducible, inline]

abbrev LieIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Type v

An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself.

theorem lie_mem_right (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x y : L) (h : y ∈ I) : ⁅x, y⁆ ∈ I

theorem lie_mem_left (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x y : L) (h : x ∈ I) : ⁅x, y⁆ ∈ I

def LieIdeal.toLieSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieSubalgebra R L

An ideal of a Lie algebra is a Lie subalgebra.

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

@[simp]

theorem LieIdeal.coe_toLieSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↑(toLieSubalgebra R L I) = ↑I

@[simp]

theorem LieIdeal.toLieSubalgebra_toSubmodule (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : (toLieSubalgebra R L I).toSubmodule = ↑I

instance LieIdeal.lieRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieRing ↥I

An ideal of L is a Lie subalgebra of L, so it is a Lie ring.

instance LieIdeal.lieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra R ↥I

Transfer the LieAlgebra instance from the coercion LieIdeal → LieSubalgebra.

instance LieIdeal.lieRingModule (M : Type w) [AddCommGroup M] {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] : LieRingModule (↥I) M

Transfer the LieRingModule instance from the coercion LieIdeal → LieSubalgebra.

@[simp]

theorem LieIdeal.coe_bracket_of_module (M : Type w) [AddCommGroup M] {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] (x : ↥I) (m : M) : ⁅x, m⁆ = ⁅↑x, m⁆

instance LieIdeal.lieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] (I : LieIdeal R L) : LieModule R (↥I) M

Transfer the LieModule instance from the coercion LieIdeal → LieSubalgebra.

instance instIsLieTowerSubtypeMemLieSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [LieRingModule L M] [LieAlgebra R L] (I : LieIdeal R L) : IsLieTower (↥I) L M

instance instIsLieTowerSubtypeMemLieSubmodule_1 (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [LieRingModule L M] [LieAlgebra R L] (I : LieIdeal R L) : IsLieTower L (↥I) M

theorem LieSubalgebra.exists_lieIdeal_coe_eq_iff (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : (∃ (I : LieIdeal R L), LieIdeal.toLieSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K

theorem LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {K' : LieSubalgebra R L} (h : K ≤ K') : (∃ (I : LieIdeal R ↥K'), LieIdeal.toLieSubalgebra R (↥K') I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

@[simp]

theorem LieIdeal.top_toLieSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : toLieSubalgebra R L ⊤ = ⊤

def LieIdeal.map {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') (I : LieIdeal R L) : LieIdeal R L'

A morphism of Lie algebras f : L → L' pushes forward Lie ideals of L to Lie ideals of L'.

Note that unlike LieSubmodule.map, we must take the lieSpan of the image. Mathematically this is because although f makes L' into a Lie module over L, in general the L submodules of L' are not the same as the ideals of L'.

def LieIdeal.comap {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') (J : LieIdeal R L') : LieIdeal R L

A morphism of Lie algebras f : L → L' pulls back Lie ideals of L' to Lie ideals of L.

Note that f makes L' into a Lie module over L (turning f into a morphism of Lie modules) and so this is a special case of LieSubmodule.comap but we do not exploit this fact.

@[simp]

theorem LieIdeal.map_toSubmodule {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') (I : LieIdeal R L) (h : ↑(map f I) = ⇑f '' ↑I) : ↑(map f I) = Submodule.map ↑f ↑I

@[simp]

theorem LieIdeal.comap_toSubmodule {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') (J : LieIdeal R L') : ↑(comap f J) = Submodule.comap ↑f ↑J

theorem LieIdeal.map_le {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') (I : LieIdeal R L) (J : LieIdeal R L') : map f I ≤ J ↔ ⇑f '' ↑I ⊆ ↑J

theorem LieIdeal.mem_map {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'} {I : LieIdeal R L} {x : L} (hx : x ∈ I) : f x ∈ map f I

@[simp]

theorem LieIdeal.mem_comap {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'} {J : LieIdeal R L'} {x : L} : x ∈ comap f J ↔ f x ∈ J

theorem LieIdeal.map_le_iff_le_comap {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'} {I : LieIdeal R L} {J : LieIdeal R L'} : map f I ≤ J ↔ I ≤ comap f J

theorem LieIdeal.gc_map_comap {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') : GaloisConnection (map f) (comap f)

@[simp]

theorem LieIdeal.map_sup {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'} {I I₂ : LieIdeal R L} : map f (I ⊔ I₂) = map f I ⊔ map f I₂

theorem LieIdeal.map_comap_le {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'} {J : LieIdeal R L'} : map f (comap f J) ≤ J

theorem LieIdeal.comap_map_le {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'} {I : LieIdeal R L} : I ≤ comap f (map f I)

See also LieIdeal.map_comap_eq.

theorem LieIdeal.map_mono {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'} : Monotone (map f)

theorem LieIdeal.comap_mono {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'} : Monotone (comap f)

theorem LieIdeal.map_of_image {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'} {I : LieIdeal R L} {J : LieIdeal R L'} (h : ⇑f '' ↑I = ↑J) : map f I = J

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

Note that this is not a special case of LieSubmodule.subsingleton_of_bot. Indeed, given I : LieIdeal R L, in general the two lattices LieIdeal R I and LieSubmodule R L I are different (though the latter does naturally inject into the former).

In other words, in general, ideals of I, regarded as a Lie algebra in its own right, are not the same as ideals of L contained in I.

def LieHom.ker {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') : LieIdeal R L

The kernel of a morphism of Lie algebras, as an ideal in the domain.

def LieHom.idealRange {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') : LieIdeal R L'

The range of a morphism of Lie algebras as an ideal in the codomain.

theorem LieHom.idealRange_eq_lieSpan_range {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') : f.idealRange = LieSubmodule.lieSpan R L' ↑f.range

theorem LieHom.idealRange_eq_map {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') : f.idealRange = LieIdeal.map f ⊤

def LieHom.IsIdealMorphism {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') : Prop

The condition that the range of a morphism of Lie algebras is an ideal.

theorem LieHom.isIdealMorphism_def {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') : f.IsIdealMorphism ↔ LieIdeal.toLieSubalgebra R L' f.idealRange = f.range

theorem LieHom.IsIdealMorphism.eq {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'} (hf : f.IsIdealMorphism) : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range

theorem LieHom.isIdealMorphism_iff {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') : f.IsIdealMorphism ↔ ∀ (x : L') (y : L), ∃ (z : L), ⁅x, f y⁆ = f z

theorem LieHom.range_subset_idealRange {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') : ↑f.range ⊆ ↑f.idealRange

theorem LieHom.map_le_idealRange {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') (I : LieIdeal R L) : LieIdeal.map f I ≤ f.idealRange

theorem LieHom.ker_le_comap {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') (J : LieIdeal R L') : f.ker ≤ LieIdeal.comap f J

@[simp]

theorem LieHom.ker_toSubmodule {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') : ↑f.ker = LinearMap.ker ↑f

@[simp]

theorem LieHom.mem_ker {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'} {x : L} : x ∈ f.ker ↔ f x = 0

theorem LieHom.mem_idealRange {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') (x : L) : f x ∈ f.idealRange

@[simp]

theorem LieHom.mem_idealRange_iff {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 : f.IsIdealMorphism) {y : L'} : y ∈ f.idealRange ↔ ∃ (x : L), f x = y

theorem LieHom.le_ker_iff {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') (I : LieIdeal R L) : I ≤ f.ker ↔ ∀ x ∈ I, f x = 0

theorem LieHom.ker_eq_bot {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') : f.ker = ⊥ ↔ Function.Injective ⇑f

@[simp]

theorem LieHom.range_toSubmodule {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') : f.range.toSubmodule = LinearMap.range ↑f

theorem LieHom.range_eq_top {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') : f.range = ⊤ ↔ Function.Surjective ⇑f

@[simp]

theorem LieHom.idealRange_eq_top_of_surjective {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.Surjective ⇑f) : f.idealRange = ⊤

theorem LieHom.isIdealMorphism_of_surjective {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.Surjective ⇑f) : f.IsIdealMorphism

@[simp]

theorem LieIdeal.map_eq_bot_iff {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'} {I : LieIdeal R L} : map f I = ⊥ ↔ I ≤ f.ker

theorem LieIdeal.coe_map_of_surjective {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'} {I : LieIdeal R L} (h : Function.Surjective ⇑f) : ↑(map f I) = Submodule.map ↑f ↑I

theorem LieIdeal.mem_map_of_surjective {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'} {I : LieIdeal R L} {y : L'} (h₁ : Function.Surjective ⇑f) (h₂ : y ∈ map f I) : ∃ (x : ↥I), f ↑x = y

theorem LieIdeal.bot_of_map_eq_bot {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'} {I : LieIdeal R L} (h₁ : Function.Injective ⇑f) (h₂ : map f I = ⊥) : I = ⊥

def LieIdeal.inclusion {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : ↥I₁ →ₗ⁅R⁆ ↥I₂

Given two nested Lie ideals I₁ ⊆ I₂, the inclusion I₁ ↪ I₂ is a morphism of Lie algebras.

@[simp]

theorem LieIdeal.coe_inclusion {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) (x : ↥I₁) : ↑((inclusion h) x) = ↑x

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

theorem LieIdeal.inclusion_injective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : Function.Injective ⇑(inclusion h)

theorem LieIdeal.map_sup_ker_eq_map {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'} {I : LieIdeal R L} : map f (I ⊔ f.ker) = map f I

@[simp]

theorem LieIdeal.map_sup_ker_eq_map' {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'} {I : LieIdeal R L} : map f I ⊔ map f f.ker = map f I

@[simp]

theorem LieIdeal.map_comap_eq {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'} {J : LieIdeal R L'} (h : f.IsIdealMorphism) : map f (comap f J) = f.idealRange ⊓ J

@[simp]

theorem LieIdeal.comap_map_eq {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'} {I : LieIdeal R L} (h : ↑(map f I) = ⇑f '' ↑I) : comap f (map f I) = I ⊔ f.ker

def LieIdeal.incl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↥I →ₗ⁅R⁆ L

Regarding an ideal I as a subalgebra, the inclusion map into its ambient space is a morphism of Lie algebras.

@[simp]

theorem LieIdeal.incl_range {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.range = toLieSubalgebra R L I

@[simp]

theorem LieIdeal.incl_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : ↥I) : I.incl x = ↑x

@[simp]

theorem LieIdeal.incl_coe {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↑I.incl = (toLieSubalgebra R L I).subtype

theorem LieIdeal.incl_injective {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Function.Injective ⇑I.incl

@[simp]

theorem LieIdeal.comap_incl_self {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : comap I.incl I = ⊤

@[simp]

theorem LieIdeal.ker_incl {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.ker = ⊥

@[simp]

theorem LieIdeal.incl_idealRange {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.idealRange = I

theorem LieIdeal.incl_isIdealMorphism {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.incl.IsIdealMorphism

@[simp]

theorem LieIdeal.comap_incl_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I I₂ : LieIdeal R L} : comap I.incl I₂ = ⊤ ↔ I ≤ I₂

@[simp]

theorem LieIdeal.comap_incl_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I I₂ : LieIdeal R L} : comap I.incl I₂ = ⊥ ↔ Disjoint I I₂

def LieIdeal.topEquiv {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ↥⊤ ≃ₗ⁅R⁆ L

The natural equivalence between the 'top' Lie ideal and the enclosing Lie algebra. This is the Lie ideal version of Submodule.topEquiv.

theorem LieIdeal.topEquiv_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x : ↥⊤) : topEquiv x = ↑x