Lie submodules of a Lie algebra

In this file we define Lie submodules, 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

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 R M : 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

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

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

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 10000]

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

Equations

• LieSubmodule.coeSort = { coe := fun (N : LieSubmodule R L M) => ↥N }

@[instance 500]

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.instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket {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

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

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_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) {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

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

@[simp]

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.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.toSubmodule_injective {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Function.Injective 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 N' : LieSubmodule R L M) (h : ∀ (m : M), m ∈ N ↔ m ∈ N') : N = N'

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

@[simp]

theorem LieSubmodule.toSubmodule_inj {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N 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.instLieRingModuleSubtypeMem {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.instLieRingModuleSubtypeMem = { bracket := fun (x : L) (m : ↥N) => ⟨⁅x, ↑m⁆, ⋯⟩, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

@[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 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 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.instIsNoetherianSubtypeMem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsNoetherian R M] (N : LieSubmodule R L M) : IsNoetherian R ↥N

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

instance LieSubmodule.instNoZeroSMulDivisorsSubtypeMem {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) [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R ↥N

instance LieSubmodule.instLieModule {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) [LieAlgebra R L] [LieModule R L M] : LieModule R L ↥N

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 := ⋯ }

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 = { toSubmodule := K.toSubmodule, 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 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.toSubmodule_le_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N 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 }

instance LieSubmodule.instUniqueBot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Unique ↥⊥

Equations

• LieSubmodule.instUniqueBot = inferInstanceAs (Unique ↥⊥)

@[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_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : ↑⊥ = ⊥

@[simp]

theorem LieSubmodule.toSubmodule_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 = ⊥ ↔ 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_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : ↑⊤ = ⊤

@[simp]

theorem LieSubmodule.toSubmodule_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 = ⊤ ↔ 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.instMin {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Min (LieSubmodule R L M)

Equations

• LieSubmodule.instMin = { min := 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

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

@[simp]

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

@[deprecated LieSubmodule.coe_inf (since := "2025-08-31")]

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 N' : LieSubmodule R L M) : ↑(N ⊓ N') = ↑N ∩ ↑N'

Alias of LieSubmodule.coe_inf.

@[simp]

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

@[simp]

theorem LieSubmodule.sInf_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_toSubmodule_eq_iInf {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_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.coe_sInf {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

@[deprecated LieSubmodule.coe_sInf (since := "2025-08-31")]

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

Alias of LieSubmodule.coe_sInf.

@[simp]

theorem LieSubmodule.coe_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) : ↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)

@[deprecated LieSubmodule.coe_iInf (since := "2025-08-31")]

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)

Alias of LieSubmodule.coe_iInf.

@[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.instMax {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Max (LieSubmodule R L M)

Equations

• LieSubmodule.instMax = { max := fun (N N' : LieSubmodule R L M) => let __Submodule := ↑N ⊔ ↑N'; { toSubmodule := __Submodule, 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

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

@[simp]

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

@[simp]

theorem LieSubmodule.sSup_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_toSubmodule_eq_iSup {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_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 Lie submodules of a Lie module form a complete lattice.

Equations

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

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) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ (i : ι), N i) (mem : ∀ (i : ι), ∀ y ∈ N i, motive y) (zero : motive 0) (add : ∀ (y z : M), motive y → motive z → motive (y + z)) : motive 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) {motive : (x : M) → x ∈ ⨆ (i : ι), N i → Prop} (mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), N i) (hy : y ∈ ⨆ (i : ι), N i), motive x hx → motive y hy → motive (x + y) ⋯) {x : M} (hx : x ∈ ⨆ (i : ι), N i) : motive x hx

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LieSubmodule.iSupIndep_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} : (iSupIndep fun (i : ι) => ↑(N i)) ↔ iSupIndep N

@[simp]

theorem LieSubmodule.iSup_toSubmodule_eq_top {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 := max }

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

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

@[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 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 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 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 ↥⊥)

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)

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' := ⋯ }

@[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) : (toSubmodule_orderEmbedding R L M) self = ↑self

instance LieSubmodule.wellFoundedGT_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] : WellFoundedGT (LieSubmodule R L M)

theorem LieSubmodule.wellFoundedLT_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] : WellFoundedLT (LieSubmodule R L M)

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)

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

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 = { toLinearMap := (↑N).subtype, 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 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 = { toLinearMap := Submodule.inclusion ⋯, 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 N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N) : ↑((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 N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N) : (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 N' : LieSubmodule R L M} (h : N ≤ N') : Function.Injective ⇑(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 ∈ 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 ⊆ ↑(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 ≤ ↑(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} : 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 t : Set M} (h : s ⊆ t) : lieSpan R L s ≤ 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) : 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} : ↑(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 (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] : 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] : 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} : 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 t : Set M) : lieSpan R L (s ∪ t) = lieSpan R L s ⊔ 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) : lieSpan R L (⋃ (i : ι), s i) = ⨆ (i : ι), lieSpan R L (s i)

theorem LieSubmodule.lieSpan_induction (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} {p : (x : M) → x ∈ lieSpan R L s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : M) (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 : M) (hx : x ∈ lieSpan R L s), p x hx → p (a • x) ⋯) {x : M} (lie : ∀ (x : L) (y : M) (hy : y ∈ lieSpan R L s), 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 submodule spanned by s.

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 (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) => 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)

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 = { toSubmodule := Submodule.map ↑f ↑N, 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) : ↑(map f N) = ⇑f '' ↑N

@[simp]

theorem LieSubmodule.toSubmodule_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) : ↑(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' = { toSubmodule := Submodule.comap ↑f ↑N', lie_mem := ⋯ }

@[simp]

theorem LieSubmodule.toSubmodule_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') : ↑(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'} : map f N ≤ N' ↔ N ≤ 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 (map f) (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 N₂ : LieSubmodule R L M} : map f (N ⊓ N₂) ≤ map f N ⊓ 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 N₂ : LieSubmodule R L M} (hf : Function.Injective ⇑f) : map f (N ⊓ N₂) = map f N ⊓ 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 N₂ : LieSubmodule R L M} : map f (N ⊔ N₂) = map f N ⊔ 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' N₂' : LieSubmodule R L M'} : comap f (N' ⊓ N₂') = comap f N' ⊓ 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) : map f (⨆ (i : ι), N i) = ⨆ (i : ι), 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' ∈ 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 ∈ 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 ∈ 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 N₂ : LieSubmodule R L M} : 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 N₂ : LieSubmodule R L M} : 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 N₂ : LieSubmodule R L M} (h : N ≤ N₂) : map f N ≤ 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''} : map (g.comp f) N = map g (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} : 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'} : 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 N₂ : LieSubmodule R L M} (hf : Function.Injective ⇑f) : map f N ≤ 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 (map f)

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' := ⋯ }

@[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) : (mapOrderEmbedding hf) N = map f N

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⁆ ↥(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.

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 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) : (orderIsoMapComap e) N = map e.toLieModuleHom N

@[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 (orderIsoMapComap e)) N' = comap e.toLieModuleHom N'

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_toSubmodule {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] : 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.toSubmodule_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 = { 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) : ↑((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) : 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) : 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') : 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} : 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} : map N.incl N' ≤ N

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 = { toLinearMap := ↑(LinearEquiv.ofTop ⊤ ⋯), map_lie' := ⋯, invFun := (LinearEquiv.ofTop ⊤ ⋯).invFun, left_inv := ⋯, right_inv := ⋯ }

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 : ↥⊤) : (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 = ⊤

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 = { toLieHom := ⊤.incl, 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 : ↥⊤) : topEquiv x = ↑x