Lie submodules of a Lie algebra

In this file we define Lie submodules and Lie ideals, we construct the lattice structure on Lie submodules and we use it to define various important operations, notably the Lie span of a subset of a Lie module.

Main definitions

• LieSubmodule
• LieSubmodule.wellFounded_of_noetherian
• LieSubmodule.lieSpan
• LieSubmodule.map
• LieSubmodule.comap
• LieIdeal
• LieIdeal.map
• LieIdeal.comap

Tags

lie algebra, lie submodule, lie ideal, lattice structure

structure LieSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] extends Submodule : Type w

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

• carrier : Set M
• add_mem' : ∀ {a b : M}, a ∈ (↑self).carrier → b ∈ (↑self).carrier → a + b ∈ (↑self).carrier
• zero_mem' : 0 ∈ (↑self).carrier
• smul_mem' : ∀ (c : R) {x : M}, x ∈ (↑self).carrier → c • x ∈ (↑self).carrier
• lie_mem : ∀ {x : L} {m : M}, m ∈ (↑self).carrier → ⁅x, m⁆ ∈ (↑self).carrier

theorem LieSubmodule.lie_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (self : LieSubmodule R L M) {x : L} {m : M} : m ∈ (↑self).carrier → ⁅x, m⁆ ∈ (↑self).carrier

instance LieSubmodule.instSetLike {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : SetLike (LieSubmodule R L M) M

Equations

• LieSubmodule.instSetLike = { coe := fun (s : LieSubmodule R L M) => (↑s).carrier, coe_injective' := ⋯ }

instance LieSubmodule.instAddSubgroupClass {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : AddSubgroupClass (LieSubmodule R L M) M

Equations

• ⋯ = ⋯

instance LieSubmodule.instSMulMemClass {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : SMulMemClass (LieSubmodule R L M) R M

Equations

• ⋯ = ⋯

instance LieSubmodule.instZero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Zero (LieSubmodule R L M)

The zero module is a Lie submodule of any Lie module.

Equations

• LieSubmodule.instZero = { zero := let __src := 0; { toSubmodule := __src, lie_mem := ⋯ } }

instance LieSubmodule.instInhabited {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Inhabited (LieSubmodule R L M)

Equations

• LieSubmodule.instInhabited = { default := 0 }

instance LieSubmodule.coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : CoeOut (LieSubmodule R L M) (Submodule R M)

Equations

• LieSubmodule.coeSubmodule = { coe := LieSubmodule.toSubmodule }

instance LieSubmodule.instCanLiftSubmoduleLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : CanLift (Submodule R M) (LieSubmodule R L M) (fun (x : LieSubmodule R L M) => ↑x) fun (N : Submodule R M) => ∀ {x : L} {m : M}, m ∈ N → ⁅x, m⁆ ∈ N

Equations

• ⋯ = ⋯

theorem LieSubmodule.coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : ↑↑N = ↑N

@[simp]

theorem LieSubmodule.mem_carrier {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} : x ∈ (↑N).carrier ↔ x ∈ ↑N

theorem LieSubmodule.mem_mk_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : M}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x : L} {m : M}, m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) {x : M} : x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄ } ↔ x ∈ S

@[simp]

theorem LieSubmodule.mem_mk_iff' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (p : Submodule R M) (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier) {x : M} : x ∈ { toSubmodule := p, lie_mem := h } ↔ x ∈ p

@[simp]

theorem LieSubmodule.mem_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} : x ∈ ↑N ↔ x ∈ N

theorem LieSubmodule.mem_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} : x ∈ ↑N ↔ x ∈ N

@[simp]

theorem LieSubmodule.zero_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : 0 ∈ N

theorem LieSubmodule.mk_eq_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} (h : x ∈ N) : ⟨x, h⟩ = 0 ↔ x = 0

@[simp]

theorem LieSubmodule.coe_toSet_mk {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : M}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x : L} {m : M}, m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { 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 LieSubmodule.coe_toSubmodule_mk {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (p : Submodule R M) (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier) : ↑{ toSubmodule := p, lie_mem := h } = p

theorem LieSubmodule.coeSubmodule_injective {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Function.Injective LieSubmodule.toSubmodule

theorem LieSubmodule.ext {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (h : ∀ (m : M), m ∈ N ↔ m ∈ N') : N = N'

@[simp]

theorem LieSubmodule.coe_toSubmodule_eq_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : ↑N = ↑N' ↔ N = N'

def LieSubmodule.copy {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (s : Set M) (hs : s = ↑N) : LieSubmodule R L M

Copy of a LieSubmodule with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• N.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

@[simp]

theorem LieSubmodule.coe_copy {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : LieSubmodule R L M) (s : Set M) (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem LieSubmodule.copy_eq {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : LieSubmodule R L M) (s : Set M) (hs : s = ↑S) : S.copy s hs = S

instance LieSubmodule.instLieRingModuleSubtypeMemSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : LieRingModule L ↥↑N

Equations

• N.instLieRingModuleSubtypeMemSubmodule = LieRingModule.mk ⋯ ⋯ ⋯

instance LieSubmodule.module' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {S : Type u_1} [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Module S ↥↑N

Equations

• N.module' = (↑N).module'

instance LieSubmodule.instModuleSubtypeMemSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : Module R ↥↑N

Equations

• N.instModuleSubtypeMemSubmodule = (↑N).module

instance LieSubmodule.instIsCentralScalarSubtypeMemSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {S : Type u_1} [Semiring S] [SMul S R] [SMul Sᵐᵒᵖ R] [Module S M] [Module Sᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S ↥↑N

Equations

• ⋯ = ⋯

instance LieSubmodule.instLieModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) : LieModule R L ↥↑N

Equations

• ⋯ = ⋯

@[simp]

theorem LieSubmodule.coe_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : ↑0 = 0

@[simp]

theorem LieSubmodule.coe_add {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) (m' : ↥N) : ↑(m + m') = ↑m + ↑m'

@[simp]

theorem LieSubmodule.coe_neg {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) : ↑(-m) = -↑m

@[simp]

theorem LieSubmodule.coe_sub {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) (m' : ↥N) : ↑(m - m') = ↑m - ↑m'

@[simp]

theorem LieSubmodule.coe_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (t : R) (m : ↥N) : ↑(t • m) = t • ↑m

@[simp]

theorem LieSubmodule.coe_bracket {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (x : L) (m : ↥N) : ↑⁅x, m⁆ = ⁅x, ↑m⁆

instance LieSubmodule.instUniqueOfSubsingleton {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [Subsingleton M] : Unique (LieSubmodule R L M)

Equations

• LieSubmodule.instUniqueOfSubsingleton = { default := 0, uniq := ⋯ }

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

Equations

• LieIdeal R L = LieSubmodule R L L

theorem lie_mem_right (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : L) (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 : L) (y : L) (h : x ∈ I) : ⁅x, y⁆ ∈ I

def lieIdealSubalgebra (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.

Equations

• lieIdealSubalgebra R L I = let __src := ↑I; { toSubmodule := __src, lie_mem' := ⋯ }

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

Equations

• instCoeLieIdealLieSubalgebra R L = { coe := lieIdealSubalgebra R L }

@[simp]

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

@[simp]

theorem LieIdeal.coe_to_lieSubalgebra_to_submodule (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : (lieIdealSubalgebra 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.

Equations

• LieIdeal.lieRing R L I = LieSubalgebra.lieRing R L (lieIdealSubalgebra R L I)

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.

Equations

• LieIdeal.lieAlgebra R L I = LieSubalgebra.lieAlgebra R L (lieIdealSubalgebra R L I)

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.

Equations

• LieIdeal.lieRingModule M I = (lieIdealSubalgebra R L I).lieRingModule

@[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] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) : LieModule R (↥↑I) M

Transfer the LieModule instance from the coercion LieIdeal → LieSubalgebra.

Equations

• ⋯ = ⋯

theorem Submodule.exists_lieSubmodule_coe_eq_iff {R : Type u} (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (p : Submodule R M) : (∃ (N : LieSubmodule R L M), ↑N = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

def LieSubalgebra.toLieSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : LieSubmodule R (↥K) L

Given a Lie subalgebra K ⊆ L, if we view L as a K-module by restriction, it contains a distinguished Lie submodule for the action of K, namely K itself.

Equations

• K.toLieSubmodule = let __src := K.toSubmodule; { toSubmodule := __src, lie_mem := ⋯ }

@[simp]

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

@[simp]

theorem LieSubalgebra.mem_toLieSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} (x : L) : x ∈ K.toLieSubmodule ↔ x ∈ K

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), lieIdealSubalgebra 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'), lieIdealSubalgebra R (↥K') I = LieSubalgebra.ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

theorem LieSubmodule.coe_injective {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Function.Injective SetLike.coe

@[simp]

theorem LieSubmodule.coeSubmodule_le_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : ↑N ≤ ↑N' ↔ N ≤ N'

instance LieSubmodule.instBot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Bot (LieSubmodule R L M)

Equations

• LieSubmodule.instBot = { bot := 0 }

@[simp]

theorem LieSubmodule.bot_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : ↑⊥ = {0}

@[simp]

theorem LieSubmodule.bot_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : ↑⊥ = ⊥

@[simp]

theorem LieSubmodule.coeSubmodule_eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : ↑N = ⊥ ↔ N = ⊥

@[simp]

theorem LieSubmodule.mk_eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : Submodule R M} {h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier} : { toSubmodule := N, lie_mem := h } = ⊥ ↔ N = ⊥

@[simp]

theorem LieSubmodule.mem_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (x : M) : x ∈ ⊥ ↔ x = 0

instance LieSubmodule.instTop {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Top (LieSubmodule R L M)

Equations

• LieSubmodule.instTop = { top := let __src := ⊤; { toSubmodule := __src, lie_mem := ⋯ } }

@[simp]

theorem LieSubmodule.top_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : ↑⊤ = Set.univ

@[simp]

theorem LieSubmodule.top_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : ↑⊤ = ⊤

@[simp]

theorem LieSubmodule.coeSubmodule_eq_top_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : ↑N = ⊤ ↔ N = ⊤

@[simp]

theorem LieSubmodule.mk_eq_top_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : Submodule R M} {h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier} : { toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤

@[simp]

theorem LieSubmodule.mem_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (x : M) : x ∈ ⊤

instance LieSubmodule.instInf {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Inf (LieSubmodule R L M)

Equations

• LieSubmodule.instInf = { inf := fun (N N' : LieSubmodule R L M) => let __src := ↑N ⊓ ↑N'; { toSubmodule := __src, lie_mem := ⋯ } }

instance LieSubmodule.instInfSet {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : InfSet (LieSubmodule R L M)

Equations

• LieSubmodule.instInfSet = { sInf := fun (S : Set (LieSubmodule R L M)) => { toSubmodule := sInf {x : Submodule R M | ∃ s ∈ S, ↑s = x}, lie_mem := ⋯ } }

@[simp]

theorem LieSubmodule.inf_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : ↑(N ⊓ N') = ↑N ∩ ↑N'

@[simp]

theorem LieSubmodule.inf_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : ↑(N ⊓ N') = ↑N ⊓ ↑N'

@[simp]

theorem LieSubmodule.sInf_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) : ↑(sInf S) = sInf {x : Submodule R M | ∃ s ∈ S, ↑s = x}

theorem LieSubmodule.sInf_coe_toSubmodule' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) : ↑(sInf S) = ⨅ N ∈ S, ↑N

@[simp]

theorem LieSubmodule.iInf_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) : ↑(⨅ (i : ι), p i) = ⨅ (i : ι), ↑(p i)

@[simp]

theorem LieSubmodule.sInf_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem LieSubmodule.iInf_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) : ↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)

@[simp]

theorem LieSubmodule.mem_iInf {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) {x : M} : x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i

instance LieSubmodule.instSup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Sup (LieSubmodule R L M)

Equations

• LieSubmodule.instSup = { sup := fun (N N' : LieSubmodule R L M) => { toSubmodule := ↑N ⊔ ↑N', lie_mem := ⋯ } }

instance LieSubmodule.instSupSet {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : SupSet (LieSubmodule R L M)

Equations

• LieSubmodule.instSupSet = { sSup := fun (S : Set (LieSubmodule R L M)) => { toSubmodule := sSup {x : Submodule R M | ∃ p ∈ S, ↑p = x}, lie_mem := ⋯ } }

@[simp]

theorem LieSubmodule.sup_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : ↑(N ⊔ N') = ↑N ⊔ ↑N'

@[simp]

theorem LieSubmodule.sSup_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) : ↑(sSup S) = sSup {x : Submodule R M | ∃ s ∈ S, ↑s = x}

theorem LieSubmodule.sSup_coe_toSubmodule' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) : ↑(sSup S) = ⨆ N ∈ S, ↑N

@[simp]

theorem LieSubmodule.iSup_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) : ↑(⨆ (i : ι), p i) = ⨆ (i : ι), ↑(p i)

instance LieSubmodule.instCompleteLattice {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : CompleteLattice (LieSubmodule R L M)

The set of Lie submodules of a Lie module form a complete lattice.

Equations

• LieSubmodule.instCompleteLattice = let __src := Function.Injective.completeLattice LieSubmodule.toSubmodule ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem LieSubmodule.mem_iSup_of_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} {b : M} {N : ι → LieSubmodule R L M} (i : ι) (h : b ∈ N i) : b ∈ ⨆ (i : ι), N i

theorem LieSubmodule.iSup_induction {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (N : ι → LieSubmodule R L M) {C : M → Prop} {x : M} (hx : x ∈ ⨆ (i : ι), N i) (hN : ∀ (i : ι), ∀ y ∈ N i, C y) (h0 : C 0) (hadd : ∀ (y z : M), C y → C z → C (y + z)) : C x

theorem LieSubmodule.iSup_induction' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (N : ι → LieSubmodule R L M) {C : (x : M) → x ∈ ⨆ (i : ι), N i → Prop} (hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯) (h0 : C 0 ⋯) (hadd : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), N i) (hy : y ∈ ⨆ (i : ι), N i), C x hx → C y hy → C (x + y) ⋯) {x : M} (hx : x ∈ ⨆ (i : ι), N i) : C x hx

theorem LieSubmodule.disjoint_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : Disjoint N N' ↔ Disjoint ↑N ↑N'

theorem LieSubmodule.codisjoint_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : Codisjoint N N' ↔ Codisjoint ↑N ↑N'

theorem LieSubmodule.isCompl_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : IsCompl N N' ↔ IsCompl ↑N ↑N'

theorem LieSubmodule.independent_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Type u_1} {N : ι → LieSubmodule R L M} : CompleteLattice.Independent N ↔ CompleteLattice.Independent fun (i : ι) => ↑(N i)

theorem LieSubmodule.iSup_eq_top_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} {N : ι → LieSubmodule R L M} : ⨆ (i : ι), N i = ⊤ ↔ ⨆ (i : ι), ↑(N i) = ⊤

instance LieSubmodule.instAdd {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Add (LieSubmodule R L M)

Equations

• LieSubmodule.instAdd = { add := Sup.sup }

instance LieSubmodule.instZero_1 {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Zero (LieSubmodule R L M)

Equations

• LieSubmodule.instZero_1 = { zero := ⊥ }

instance LieSubmodule.instAddCommMonoid {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : AddCommMonoid (LieSubmodule R L M)

Equations

• LieSubmodule.instAddCommMonoid = AddCommMonoid.mk ⋯

@[simp]

theorem LieSubmodule.add_eq_sup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) : N + N' = N ⊔ N'

@[simp]

theorem LieSubmodule.mem_inf {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (x : M) : x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'

theorem LieSubmodule.mem_sup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (x : M) : x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

theorem LieSubmodule.eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : N = ⊥ ↔ ∀ m ∈ N, m = 0

instance LieSubmodule.subsingleton_of_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Subsingleton (LieSubmodule R L ↥↑⊥)

Equations

• ⋯ = ⋯

instance LieSubmodule.instIsModularLattice {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : IsModularLattice (LieSubmodule R L M)

Equations

• ⋯ = ⋯

@[simp]

theorem LieSubmodule.toSubmodule_orderEmbedding_apply (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (self : LieSubmodule R L M) : (LieSubmodule.toSubmodule_orderEmbedding R L M) self = ↑self

def LieSubmodule.toSubmodule_orderEmbedding (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : LieSubmodule R L M ↪o Submodule R M

The natural functor that forgets the action of L as an order embedding.

Equations

• LieSubmodule.toSubmodule_orderEmbedding R L M = { toFun := LieSubmodule.toSubmodule, inj' := ⋯, map_rel_iff' := ⋯ }

theorem LieSubmodule.wellFounded_of_noetherian (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsNoetherian R M] : WellFounded fun (x x_1 : LieSubmodule R L M) => x > x_1

theorem LieSubmodule.wellFounded_of_isArtinian (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsArtinian R M] : WellFounded fun (x x_1 : LieSubmodule R L M) => x < x_1

instance LieSubmodule.instIsAtomicOfIsArtinian (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsArtinian R M] : IsAtomic (LieSubmodule R L M)

Equations

• ⋯ = ⋯

@[simp]

theorem LieSubmodule.subsingleton_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Subsingleton (LieSubmodule R L M) ↔ Subsingleton M

@[simp]

theorem LieSubmodule.nontrivial_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Nontrivial (LieSubmodule R L M) ↔ Nontrivial M

instance LieSubmodule.instNontrivial (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [Nontrivial M] : Nontrivial (LieSubmodule R L M)

Equations

• ⋯ = ⋯

theorem LieSubmodule.nontrivial_iff_ne_bot (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} : Nontrivial ↥↑N ↔ N ≠ ⊥

def LieSubmodule.incl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : ↥↑N →ₗ⁅R,L⁆ M

The inclusion of a Lie submodule into its ambient space is a morphism of Lie modules.

Equations

• N.incl = let __src := (↑N).subtype; { toLinearMap := __src, map_lie' := ⋯ }

@[simp]

theorem LieSubmodule.incl_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : ↑N.incl = (↑N).subtype

@[simp]

theorem LieSubmodule.incl_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) : N.incl m = ↑m

theorem LieSubmodule.incl_eq_val {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : ⇑N.incl = Subtype.val

theorem LieSubmodule.injective_incl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : Function.Injective ⇑N.incl

def LieSubmodule.inclusion {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') : ↥↑N →ₗ⁅R,L⁆ ↥↑N'

Given two nested Lie submodules N ⊆ N', the inclusion N ↪ N' is a morphism of Lie modules.

Equations

• LieSubmodule.inclusion h = let __spread.0 := Submodule.inclusion ⋯; { toLinearMap := __spread.0, map_lie' := ⋯ }

@[simp]

theorem LieSubmodule.coe_inclusion {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N) : ↑((LieSubmodule.inclusion h) m) = ↑m

theorem LieSubmodule.inclusion_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N) : (LieSubmodule.inclusion h) m = ⟨↑m, ⋯⟩

theorem LieSubmodule.inclusion_injective {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') : Function.Injective ⇑(LieSubmodule.inclusion h)

def LieSubmodule.lieSpan (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (s : Set M) : LieSubmodule R L M

The lieSpan of a set s ⊆ M is the smallest Lie submodule of M that contains s.

Equations

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

theorem LieSubmodule.mem_lieSpan {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} {x : M} : x ∈ LieSubmodule.lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

theorem LieSubmodule.subset_lieSpan {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} : s ⊆ ↑(LieSubmodule.lieSpan R L s)

theorem LieSubmodule.submodule_span_le_lieSpan {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} : Submodule.span R s ≤ ↑(LieSubmodule.lieSpan R L s)

@[simp]

theorem LieSubmodule.lieSpan_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} {N : LieSubmodule R L M} : LieSubmodule.lieSpan R L s ≤ N ↔ s ⊆ ↑N

theorem LieSubmodule.lieSpan_mono {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} {t : Set M} (h : s ⊆ t) : LieSubmodule.lieSpan R L s ≤ LieSubmodule.lieSpan R L t

theorem LieSubmodule.lieSpan_eq {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : LieSubmodule.lieSpan R L ↑N = N

theorem LieSubmodule.coe_lieSpan_submodule_eq_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {p : Submodule R M} : ↑(LieSubmodule.lieSpan R L ↑p) = p ↔ ∃ (N : LieSubmodule R L M), ↑N = p

def LieSubmodule.gi (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : GaloisInsertion (LieSubmodule.lieSpan R L) SetLike.coe

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

Equations

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

@[simp]

theorem LieSubmodule.span_empty (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : LieSubmodule.lieSpan R L ∅ = ⊥

@[simp]

theorem LieSubmodule.span_univ (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : LieSubmodule.lieSpan R L Set.univ = ⊤

theorem LieSubmodule.lieSpan_eq_bot_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} : LieSubmodule.lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0

theorem LieSubmodule.span_union (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (s : Set M) (t : Set M) : LieSubmodule.lieSpan R L (s ∪ t) = LieSubmodule.lieSpan R L s ⊔ LieSubmodule.lieSpan R L t

theorem LieSubmodule.span_iUnion (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (s : ι → Set M) : LieSubmodule.lieSpan R L (⋃ (i : ι), s i) = ⨆ (i : ι), LieSubmodule.lieSpan R L (s i)

theorem LieSubmodule.isCompactElement_lieSpan_singleton (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) : CompleteLattice.IsCompactElement (LieSubmodule.lieSpan R L {m})

@[simp]

theorem LieSubmodule.sSup_image_lieSpan_singleton (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : sSup ((fun (x : M) => LieSubmodule.lieSpan R L {x}) '' ↑N) = N

instance LieSubmodule.instIsCompactlyGenerated (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : IsCompactlyGenerated (LieSubmodule R L M)

Equations

• ⋯ = ⋯

def LieSubmodule.map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) : LieSubmodule R L M'

A morphism of Lie modules f : M → M' pushes forward Lie submodules of M to Lie submodules of M'.

Equations

• LieSubmodule.map f N = let __src := Submodule.map ↑f ↑N; { toSubmodule := __src, lie_mem := ⋯ }

@[simp]

theorem LieSubmodule.coe_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) : ↑(LieSubmodule.map f N) = ⇑f '' ↑N

@[simp]

theorem LieSubmodule.coeSubmodule_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) : ↑(LieSubmodule.map f N) = Submodule.map ↑f ↑N

def LieSubmodule.comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M') : LieSubmodule R L M

A morphism of Lie modules f : M → M' pulls back Lie submodules of M' to Lie submodules of M.

Equations

• LieSubmodule.comap f N' = let __src := Submodule.comap ↑f ↑N'; { toSubmodule := __src, lie_mem := ⋯ }

@[simp]

theorem LieSubmodule.coeSubmodule_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M') : ↑(LieSubmodule.comap f N') = Submodule.comap ↑f ↑N'

theorem LieSubmodule.map_le_iff_le_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N' : LieSubmodule R L M'} : LieSubmodule.map f N ≤ N' ↔ N ≤ LieSubmodule.comap f N'

theorem LieSubmodule.gc_map_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') : GaloisConnection (LieSubmodule.map f) (LieSubmodule.comap f)

theorem LieSubmodule.map_inf_le {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} : LieSubmodule.map f (N ⊓ N₂) ≤ LieSubmodule.map f N ⊓ LieSubmodule.map f N₂

theorem LieSubmodule.map_inf {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (hf : Function.Injective ⇑f) : LieSubmodule.map f (N ⊓ N₂) = LieSubmodule.map f N ⊓ LieSubmodule.map f N₂

@[simp]

theorem LieSubmodule.map_sup {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} : LieSubmodule.map f (N ⊔ N₂) = LieSubmodule.map f N ⊔ LieSubmodule.map f N₂

@[simp]

theorem LieSubmodule.comap_inf {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N' : LieSubmodule R L M'} {N₂' : LieSubmodule R L M'} : LieSubmodule.comap f (N' ⊓ N₂') = LieSubmodule.comap f N' ⊓ LieSubmodule.comap f N₂'

@[simp]

theorem LieSubmodule.map_iSup {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {ι : Sort u_1} (N : ι → LieSubmodule R L M) : LieSubmodule.map f (⨆ (i : ι), N i) = ⨆ (i : ι), LieSubmodule.map f (N i)

@[simp]

theorem LieSubmodule.mem_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} (m' : M') : m' ∈ LieSubmodule.map f N ↔ ∃ m ∈ N, f m = m'

theorem LieSubmodule.mem_map_of_mem {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {m : M} (h : m ∈ N) : f m ∈ LieSubmodule.map f N

@[simp]

theorem LieSubmodule.mem_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N' : LieSubmodule R L M'} {m : M} : m ∈ LieSubmodule.comap f N' ↔ f m ∈ N'

theorem LieSubmodule.comap_incl_eq_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} : LieSubmodule.comap N.incl N₂ = ⊤ ↔ N ≤ N₂

theorem LieSubmodule.comap_incl_eq_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} : LieSubmodule.comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥

theorem LieSubmodule.map_mono {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : N ≤ N₂) : LieSubmodule.map f N ≤ LieSubmodule.map f N₂

theorem LieSubmodule.map_comp {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {M'' : Type u_1} [AddCommGroup M''] [Module R M''] [LieRingModule L M''] {g : M' →ₗ⁅R,L⁆ M''} : LieSubmodule.map (g.comp f) N = LieSubmodule.map g (LieSubmodule.map f N)

@[simp]

theorem LieSubmodule.map_id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} : LieSubmodule.map LieModuleHom.id N = N

@[simp]

theorem LieSubmodule.map_bot {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} : LieSubmodule.map f ⊥ = ⊥

theorem LieSubmodule.map_le_map_iff {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (hf : Function.Injective ⇑f) : LieSubmodule.map f N ≤ LieSubmodule.map f N₂ ↔ N ≤ N₂

theorem LieSubmodule.map_injective_of_injective {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective ⇑f) : Function.Injective (LieSubmodule.map f)

@[simp]

theorem LieSubmodule.mapOrderEmbedding_apply {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective ⇑f) (N : LieSubmodule R L M) : (LieSubmodule.mapOrderEmbedding hf) N = LieSubmodule.map f N

def LieSubmodule.mapOrderEmbedding {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective ⇑f) : LieSubmodule R L M ↪o LieSubmodule R L M'

An injective morphism of Lie modules embeds the lattice of submodules of the domain into that of the target.

Equations

• LieSubmodule.mapOrderEmbedding hf = { toFun := LieSubmodule.map f, inj' := ⋯, map_rel_iff' := ⋯ }

noncomputable def LieSubmodule.equivMapOfInjective {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (N : LieSubmodule R L M) (hf : Function.Injective ⇑f) : ↥↑N ≃ₗ⁅R,L⁆ ↥↑(LieSubmodule.map f N)

For an injective morphism of Lie modules, any Lie submodule is equivalent to its image.

Equations

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

@[simp]

theorem LieSubmodule.orderIsoMapComap_symm_apply {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M') : (RelIso.symm (LieSubmodule.orderIsoMapComap e)) N' = LieSubmodule.comap e.toLieModuleHom N'

@[simp]

theorem LieSubmodule.orderIsoMapComap_apply {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) : (LieSubmodule.orderIsoMapComap e) N = LieSubmodule.map e.toLieModuleHom N

def LieSubmodule.orderIsoMapComap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') : LieSubmodule R L M ≃o LieSubmodule R L M'

An equivalence of Lie modules yields an order-preserving equivalence of their lattices of Lie Submodules.

Equations

• LieSubmodule.orderIsoMapComap e = { toFun := LieSubmodule.map e.toLieModuleHom, invFun := LieSubmodule.comap e.toLieModuleHom, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

def LieIdeal.map {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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'.

Equations

• LieIdeal.map f I = LieSubmodule.lieSpan R L' ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)

def LieIdeal.comap {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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.

Equations

• LieIdeal.comap f J = let __src := Submodule.comap (↑f) (lieIdealSubalgebra R L' J).toSubmodule; { toSubmodule := __src, lie_mem := ⋯ }

@[simp]

theorem LieIdeal.map_coeSubmodule {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (h : ↑(LieIdeal.map f I) = ⇑f '' ↑I) : ↑(LieIdeal.map f I) = Submodule.map ↑f ↑I

@[simp]

theorem LieIdeal.comap_coeSubmodule {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') : ↑(LieIdeal.comap f J) = Submodule.comap ↑f ↑J

theorem LieIdeal.map_le {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (J : LieIdeal R L') : LieIdeal.map f I ≤ J ↔ ⇑f '' ↑I ⊆ ↑J

theorem LieIdeal.mem_map {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {x : L} (hx : x ∈ I) : f x ∈ LieIdeal.map f I

@[simp]

theorem LieIdeal.mem_comap {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} {x : L} : x ∈ LieIdeal.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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'} : LieIdeal.map f I ≤ J ↔ I ≤ LieIdeal.comap f J

theorem LieIdeal.gc_map_comap {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') : GaloisConnection (LieIdeal.map f) (LieIdeal.comap f)

@[simp]

theorem LieIdeal.map_sup {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {I₂ : LieIdeal R L} : LieIdeal.map f (I ⊔ I₂) = LieIdeal.map f I ⊔ LieIdeal.map f I₂

theorem LieIdeal.map_comap_le {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} : LieIdeal.map f (LieIdeal.comap f J) ≤ J

theorem LieIdeal.comap_map_le {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : I ≤ LieIdeal.comap f (LieIdeal.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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} : Monotone (LieIdeal.map f)

theorem LieIdeal.comap_mono {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} : Monotone (LieIdeal.comap f)

theorem LieIdeal.map_of_image {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'} (h : ⇑f '' ↑I = ↑J) : LieIdeal.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.

Equations

• ⋯ = ⋯

def LieHom.ker {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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.

Equations

• f.ker = LieIdeal.comap f ⊥

def LieHom.idealRange {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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.

Equations

• f.idealRange = LieSubmodule.lieSpan R L' ↑f.range

theorem LieHom.idealRange_eq_lieSpan_range {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') : Prop

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

Equations

• f.IsIdealMorphism = (lieIdealSubalgebra R L' f.idealRange = f.range)

@[simp]

theorem LieHom.isIdealMorphism_def {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') : f.IsIdealMorphism ↔ lieIdealSubalgebra R L' f.idealRange = f.range

theorem LieHom.IsIdealMorphism.eq {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} (hf : f.IsIdealMorphism) : lieIdealSubalgebra R L' f.idealRange = f.range

theorem LieHom.isIdealMorphism_iff {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') : f.ker ≤ LieIdeal.comap f J

@[simp]

theorem LieHom.ker_coeSubmodule {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') : f.ker = ⊥ ↔ Function.Injective ⇑f

@[simp]

theorem LieHom.range_coeSubmodule {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing 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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : LieIdeal.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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} (h : Function.Surjective ⇑f) : ↑(LieIdeal.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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {y : L'} (h₁ : Function.Surjective ⇑f) (h₂ : y ∈ LieIdeal.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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} (h₁ : Function.Injective ⇑f) (h₂ : LieIdeal.map f I = ⊥) : I = ⊥

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

Equations

• LieIdeal.inclusion h = let __spread.0 := Submodule.inclusion ⋯; { toLinearMap := __spread.0, map_lie' := ⋯ }

@[simp]

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

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

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

theorem LieIdeal.map_sup_ker_eq_map {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : LieIdeal.map f (I ⊔ f.ker) = LieIdeal.map f I

@[simp]

theorem LieIdeal.map_sup_ker_eq_map' {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} : LieIdeal.map f I ⊔ LieIdeal.map f f.ker = LieIdeal.map f I

@[simp]

theorem LieIdeal.map_comap_eq {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} (h : f.IsIdealMorphism) : LieIdeal.map f (LieIdeal.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] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} (h : ↑(LieIdeal.map f I) = ⇑f '' ↑I) : LieIdeal.comap f (LieIdeal.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.

Equations

• I.incl = (lieIdealSubalgebra R L I).incl

@[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 = lieIdealSubalgebra 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 = (lieIdealSubalgebra 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) : LieIdeal.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

def LieModuleHom.ker {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : LieSubmodule R L M

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

Equations

• f.ker = LieSubmodule.comap f ⊥

@[simp]

theorem LieModuleHom.ker_coeSubmodule {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : ↑f.ker = LinearMap.ker ↑f

theorem LieModuleHom.ker_eq_bot {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : f.ker = ⊥ ↔ Function.Injective ⇑f

@[simp]

theorem LieModuleHom.mem_ker {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} (m : M) : m ∈ f.ker ↔ f m = 0

@[simp]

theorem LieModuleHom.ker_id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : LieModuleHom.id.ker = ⊥

@[simp]

theorem LieModuleHom.comp_ker_incl {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} : f.comp f.ker.incl = 0

theorem LieModuleHom.le_ker_iff_map {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} (M' : LieSubmodule R L M) : M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥

def LieModuleHom.range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : LieSubmodule R L N

The range of a morphism of Lie modules f : M → N is a Lie submodule of N. See Note [range copy pattern].

Equations

• f.range = (LieSubmodule.map f ⊤).copy (Set.range ⇑f) ⋯

@[simp]

theorem LieModuleHom.coe_range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : ↑f.range = Set.range ⇑f

@[simp]

theorem LieModuleHom.coeSubmodule_range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : ↑f.range = LinearMap.range ↑f

@[simp]

theorem LieModuleHom.mem_range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (n : N) : n ∈ f.range ↔ ∃ (m : M), f m = n

@[simp]

theorem LieModuleHom.map_top {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : LieSubmodule.map f ⊤ = f.range

theorem LieModuleHom.range_eq_top {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : f.range = ⊤ ↔ Function.Surjective ⇑f

def LieModuleHom.codRestrict {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (P : LieSubmodule R L N) (f : M →ₗ⁅R,L⁆ N) (h : ∀ (m : M), f m ∈ P) : M →ₗ⁅R,L⁆ ↥↑P

A morphism of Lie modules f : M → N whose values lie in a Lie submodule P ⊆ N can be restricted to a morphism of Lie modules M → P.

Equations

• LieModuleHom.codRestrict P f h = let __spread.0 := LinearMap.codRestrict (↑P) (↑f) h; { toFun := ⇑(LinearMap.codRestrict (↑P) (↑f) h), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem LieModuleHom.codRestrict_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (P : LieSubmodule R L N) (f : M →ₗ⁅R,L⁆ N) (h : ∀ (m : M), f m ∈ P) (m : M) : ↑((LieModuleHom.codRestrict P f h) m) = f m

@[simp]

theorem LieSubmodule.ker_incl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : N.incl.ker = ⊥

@[simp]

theorem LieSubmodule.range_incl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : N.incl.range = N

@[simp]

theorem LieSubmodule.comap_incl_self {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : LieSubmodule.comap N.incl N = ⊤

theorem LieSubmodule.map_incl_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : LieSubmodule.map N.incl ⊤ = N

@[simp]

theorem LieSubmodule.map_le_range {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {M' : Type u_1} [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') : LieSubmodule.map f N ≤ f.range

@[simp]

theorem LieSubmodule.map_incl_lt_iff_lt_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L ↥↑N} : LieSubmodule.map N.incl N' < N ↔ N' < ⊤

@[simp]

theorem LieSubmodule.map_incl_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L ↥↑N} : LieSubmodule.map N.incl N' ≤ N

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

The natural equivalence between the 'top' Lie subalgebra and the enclosing Lie algebra.

This is the Lie subalgebra version of Submodule.topEquiv.

Equations

• LieSubalgebra.topEquiv = let __src := ⊤.incl; { toLieHom := __src, invFun := fun (x : L) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

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.

Equations

• LieIdeal.topEquiv = LieSubalgebra.topEquiv

@[simp]

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

def LieModuleEquiv.ofTop (R : Type u) (L : Type v) [CommRing R] [LieRing L] (M : Type u_1) [AddCommGroup M] [Module R M] [LieRingModule L M] : ↥↑⊤ ≃ₗ⁅R,L⁆ M

The natural equivalence between the 'top' Lie submodule and the enclosing Lie module.

Equations

• LieModuleEquiv.ofTop R L M = let __src := LinearEquiv.ofTop ⊤ ⋯; { toLinearMap := ↑__src, map_lie' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LieModuleEquiv.ofTop_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] (M : Type u_1) [AddCommGroup M] [Module R M] [LieRingModule L M] (x : ↥⊤) : (LieModuleEquiv.ofTop R L M) x = ↑x

@[simp]

theorem LieModuleEquiv.range_coe (R : Type u) (L : Type v) [CommRing R] [LieRing L] (M : Type u_1) [AddCommGroup M] [Module R M] [LieRingModule L M] {M' : Type u_2} [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') : e.range = ⊤