mathlib3 documentation

algebra.lie.submodule

Lie submodules of a Lie algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Tags #

lie algebra, lie submodule, lie ideal, lattice structure

structure lie_submodule (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

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.

Instances for lie_submodule
@[nolint]
def lie_submodule.to_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (self : lie_submodule R L M) :
@[protected, instance]
def lie_submodule.set_like {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[protected, instance]
@[protected, instance]
def lie_submodule.has_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :

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

Equations
@[protected, instance]
def lie_submodule.inhabited {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[protected, instance]
def lie_submodule.coe_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[simp]
theorem lie_submodule.to_submodule_eq_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
@[norm_cast]
theorem lie_submodule.coe_to_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
@[simp]
theorem lie_submodule.mem_carrier {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) {x : M} :
@[simp]
theorem lie_submodule.mem_mk_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (S : set M) (h₁ : {a b : M}, a S b S a + b S) (h₂ : 0 S) (h₃ : (c : R) {x : M}, x S c x S) (h₄ : {x : L} {m : M}, m S x, m S) {x : M} :
x {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄} x S
@[simp]
theorem lie_submodule.mem_coe_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) {x : M} :
x N x N
theorem lie_submodule.mem_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) {x : M} :
x N x N
@[protected, simp]
theorem lie_submodule.zero_mem {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
0 N
@[simp]
theorem lie_submodule.mk_eq_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) {x : M} (h : x N) :
x, h⟩ = 0 x = 0
@[simp]
theorem lie_submodule.coe_to_set_mk {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (S : set M) (h₁ : {a b : M}, a S b S a + b S) (h₂ : 0 S) (h₃ : (c : R) {x : M}, x S c x S) (h₄ : {x : L} {m : M}, m S x, m S) :
{carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄} = S
@[simp]
theorem lie_submodule.coe_to_submodule_mk {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (p : submodule R M) (h : {x : L} {m : M}, m p.carrier x, m p.carrier) :
{carrier := p.carrier, add_mem' := _, zero_mem' := _, smul_mem' := _, lie_mem := h} = p
@[ext]
theorem lie_submodule.ext {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (h : (m : M), m N m N') :
N = N'
@[simp]
theorem lie_submodule.coe_to_submodule_eq_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
N = N' N = N'
@[protected]
def lie_submodule.copy {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (s : set M) (hs : s = N) :

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

Equations
@[simp]
theorem lie_submodule.coe_copy {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (S : lie_submodule R L M) (s : set M) (hs : s = S) :
(S.copy s hs) = s
theorem lie_submodule.copy_eq {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (S : lie_submodule R L M) (s : set M) (hs : s = S) :
S.copy s hs = S
@[protected, instance]
def lie_submodule.lie_ring_module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
Equations
@[protected, instance]
def lie_submodule.module' {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) {S : Type u_1} [semiring S] [has_smul S R] [module S M] [is_scalar_tower S R M] :
Equations
@[protected, instance]
def lie_submodule.module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
Equations
@[protected, instance]
@[protected, instance]
def lie_submodule.lie_module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
Equations
@[simp, norm_cast]
theorem lie_submodule.coe_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
0 = 0
@[simp, norm_cast]
theorem lie_submodule.coe_add {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (m m' : N) :
(m + m') = m + m'
@[simp, norm_cast]
theorem lie_submodule.coe_neg {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (m : N) :
@[simp, norm_cast]
theorem lie_submodule.coe_sub {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (m m' : N) :
(m - m') = m - m'
@[simp, norm_cast]
theorem lie_submodule.coe_smul {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (t : R) (m : N) :
(t m) = t m
@[simp, norm_cast]
theorem lie_submodule.coe_bracket {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (x : L) (m : N) :
@[reducible]
def lie_ideal (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

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

theorem lie_mem_right (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) (x y : L) (h : y I) :
theorem lie_mem_left (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) (x y : L) (h : x I) :
def lie_ideal_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :

An ideal of a Lie algebra is a Lie subalgebra.

Equations
@[protected, instance]
def lie_subalgebra.has_coe (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[norm_cast]
theorem lie_ideal.coe_to_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
@[norm_cast]
@[protected, instance]
def lie_ideal.lie_ring (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :

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

Equations
@[protected, instance]
def lie_ideal.lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :

Transfer the lie_algebra instance from the coercion lie_ideallie_subalgebra.

Equations
@[protected, instance]
def lie_ideal.lie_ring_module (M : Type w) [add_comm_group M] {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) [lie_ring_module L M] :

Transfer the lie_module instance from the coercion lie_ideallie_subalgebra.

Equations
@[simp]
theorem lie_ideal.coe_bracket_of_module (M : Type w) [add_comm_group M] {R : Type u_1} {L : Type u_2} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) [lie_ring_module L M] (x : I) (m : M) :
@[protected, instance]
def lie_ideal.lie_module (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (I : lie_ideal R L) :

Transfer the lie_module instance from the coercion lie_ideallie_subalgebra.

Equations
theorem submodule.exists_lie_submodule_coe_eq_iff {R : Type u} (L : Type v) {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (p : submodule R M) :
( (N : lie_submodule R L M), N = p) (x : L) (m : M), m p x, m p

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
@[simp]
@[simp]
theorem lie_subalgebra.mem_to_lie_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {K : lie_subalgebra R L} (x : L) :
theorem lie_subalgebra.exists_lie_ideal_coe_eq_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {K : lie_subalgebra R L} :
( (I : lie_ideal R L), I = K) (x y : L), y K x, y K
theorem lie_subalgebra.exists_nested_lie_ideal_coe_eq_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {K K' : lie_subalgebra R L} (h : K K') :
( (I : lie_ideal R K'), I = lie_subalgebra.of_le h) (x y : L), x K' y K x, y K
@[simp, norm_cast]
theorem lie_submodule.coe_submodule_le_coe_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
N N' N N'
@[protected, instance]
def lie_submodule.has_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[simp]
theorem lie_submodule.bot_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
= {0}
@[simp]
theorem lie_submodule.bot_coe_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
@[simp]
theorem lie_submodule.mem_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (x : M) :
x x = 0
@[protected, instance]
def lie_submodule.has_top {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[simp]
theorem lie_submodule.top_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
@[simp]
theorem lie_submodule.top_coe_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
@[simp]
theorem lie_submodule.mem_top {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (x : M) :
@[protected, instance]
def lie_submodule.has_inf {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[protected, instance]
def lie_submodule.has_Inf {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
Equations
@[simp]
theorem lie_submodule.inf_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
(N N') = N N'
@[simp]
theorem lie_submodule.Inf_coe_to_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (S : set (lie_submodule R L M)) :
(has_Inf.Inf S) = has_Inf.Inf {_x : submodule R M | (s : lie_submodule R L M) (H : s S), s = _x}
@[simp]
theorem lie_submodule.Inf_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (S : set (lie_submodule R L M)) :
(has_Inf.Inf S) = (s : lie_submodule R L M) (H : s S), s
theorem lie_submodule.Inf_glb {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (S : set (lie_submodule R L M)) :
@[protected, instance]

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

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

Equations
@[protected, instance]
Equations
@[simp]
theorem lie_submodule.add_eq_sup {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
N + N' = N N'
@[simp, norm_cast]
theorem lie_submodule.sup_coe_to_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
(N N') = N N'
@[simp, norm_cast]
theorem lie_submodule.inf_coe_to_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
(N N') = N N'
@[simp]
theorem lie_submodule.mem_inf {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (x : M) :
x N N' x N x N'
theorem lie_submodule.mem_sup {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (x : M) :
x N N' (y : M) (H : y N) (z : M) (H : z N'), y + z = x
theorem lie_submodule.eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
N = (m : M), m N m = 0
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[protected, instance]
def lie_submodule.nontrivial (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [nontrivial M] :
def lie_submodule.incl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :

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

Equations
@[simp]
theorem lie_submodule.incl_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
@[simp]
theorem lie_submodule.incl_apply {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (m : N) :
(N.incl) m = m
theorem lie_submodule.incl_eq_val {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
def lie_submodule.hom_of_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N N' : lie_submodule R L M} (h : N N') :

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

Equations
@[simp]
theorem lie_submodule.coe_hom_of_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N N' : lie_submodule R L M} (h : N N') (m : N) :
theorem lie_submodule.hom_of_le_apply {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N N' : lie_submodule R L M} (h : N N') (m : N) :
def lie_submodule.lie_span (R : Type u) (L : Type v) {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (s : set M) :

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

Equations
theorem lie_submodule.mem_lie_span {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {s : set M} {x : M} :
theorem lie_submodule.subset_lie_span {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {s : set M} :
theorem lie_submodule.lie_span_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {s : set M} {N : lie_submodule R L M} :
theorem lie_submodule.lie_span_mono {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {s t : set M} (h : s t) :
theorem lie_submodule.lie_span_eq {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
@[protected]

lie_span forms a Galois insertion with the coercion from lie_submodule to set.

Equations
@[simp]
theorem lie_submodule.span_empty (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
@[simp]
theorem lie_submodule.lie_span_eq_bot_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {s : set M} :
lie_submodule.lie_span R L s = (m : M), m s m = 0
theorem lie_submodule.span_Union (R : Type u) (L : Type v) {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {ι : Sort u_1} (s : ι set M) :
lie_submodule.lie_span R L ( (i : ι), s i) = (i : ι), lie_submodule.lie_span R L (s i)
def lie_submodule.map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] (f : M →ₗ⁅R,L M') (N : lie_submodule R L M) :

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

Equations
@[simp]
theorem lie_submodule.coe_submodule_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] (f : M →ₗ⁅R,L M') (N : lie_submodule R L M) :
def lie_submodule.comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] (f : M →ₗ⁅R,L M') (N' : lie_submodule R L M') :

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

Equations
@[simp]
theorem lie_submodule.coe_submodule_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] (f : M →ₗ⁅R,L M') (N' : lie_submodule R L M') :
theorem lie_submodule.map_le_iff_le_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] {f : M →ₗ⁅R,L M'} {N : lie_submodule R L M} {N' : lie_submodule R L M'} :
theorem lie_submodule.gc_map_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] (f : M →ₗ⁅R,L M') :
@[simp]
theorem lie_submodule.map_sup {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] {f : M →ₗ⁅R,L M'} {N N₂ : lie_submodule R L M} :
theorem lie_submodule.mem_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] {f : M →ₗ⁅R,L M'} {N : lie_submodule R L M} (m' : M') :
m' lie_submodule.map f N (m : M), m N f m = m'
@[simp]
theorem lie_submodule.mem_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M'] [module R M'] [lie_ring_module L M'] [lie_module R L M'] {f : M →ₗ⁅R,L M'} {N' : lie_submodule R L M'} {m : M} :
theorem lie_submodule.comap_incl_eq_top {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N N₂ : lie_submodule R L M} :
theorem lie_submodule.comap_incl_eq_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {N N₂ : lie_submodule R L M} :
@[simp]
def lie_ideal.map {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (I : lie_ideal R L) :

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

Note that unlike lie_submodule.map, we must take the lie_span 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
def lie_ideal.comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (J : lie_ideal 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 lie_submodule.comap but we do not exploit this fact.

Equations
@[simp]
theorem lie_ideal.map_coe_submodule {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (I : lie_ideal R L) (h : (lie_ideal.map f I) = f '' I) :
@[simp]
theorem lie_ideal.comap_coe_submodule {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (J : lie_ideal R L') :
theorem lie_ideal.map_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (I : lie_ideal R L) (J : lie_ideal R L') :
theorem lie_ideal.mem_map {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} {x : L} (hx : x I) :
@[simp]
theorem lie_ideal.mem_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {J : lie_ideal R L'} {x : L} :
theorem lie_ideal.map_le_iff_le_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} {J : lie_ideal R L'} :
theorem lie_ideal.gc_map_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
@[simp]
theorem lie_ideal.map_sup {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I I₂ : lie_ideal R L} :
theorem lie_ideal.map_comap_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {J : lie_ideal R L'} :
theorem lie_ideal.comap_map_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} :

See also lie_ideal.map_comap_eq.

theorem lie_ideal.map_mono {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} :
theorem lie_ideal.comap_mono {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} :
theorem lie_ideal.map_of_image {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} {J : lie_ideal R L'} (h : f '' I = J) :
@[protected, instance]

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

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

def lie_hom.ker {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :

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

Equations
def lie_hom.ideal_range {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :

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

Equations
theorem lie_hom.ideal_range_eq_lie_span_range {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
theorem lie_hom.ideal_range_eq_map {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
def lie_hom.is_ideal_morphism {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
Prop

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

Equations
@[simp]
theorem lie_hom.is_ideal_morphism_def {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
theorem lie_hom.is_ideal_morphism_iff {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
f.is_ideal_morphism (x : L') (y : L), (z : L), x, f y = f z
theorem lie_hom.range_subset_ideal_range {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
theorem lie_hom.map_le_ideal_range {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (I : lie_ideal R L) :
theorem lie_hom.ker_le_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (J : lie_ideal R L') :
@[simp]
theorem lie_hom.ker_coe_submodule {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
@[simp]
theorem lie_hom.mem_ker {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') {x : L} :
x f.ker f x = 0
theorem lie_hom.mem_ideal_range {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') {x : L} :
@[simp]
theorem lie_hom.mem_ideal_range_iff {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (h : f.is_ideal_morphism) {y : L'} :
y f.ideal_range (x : L), f x = y
theorem lie_hom.le_ker_iff {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (I : lie_ideal R L) :
I f.ker (x : L), x I f x = 0
theorem lie_hom.ker_eq_bot {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
@[simp]
theorem lie_hom.range_coe_submodule {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
theorem lie_hom.range_eq_top {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') :
@[simp]
theorem lie_hom.ideal_range_eq_top_of_surjective {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') (h : function.surjective f) :
@[simp]
theorem lie_ideal.map_eq_bot_iff {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} :
theorem lie_ideal.coe_map_of_surjective {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} (h : function.surjective f) :
theorem lie_ideal.mem_map_of_surjective {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} {y : L'} (h₁ : function.surjective f) (h₂ : y lie_ideal.map f I) :
(x : I), f x = y
theorem lie_ideal.bot_of_map_eq_bot {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} (h₁ : function.injective f) (h₂ : lie_ideal.map f I = ) :
I =
def lie_ideal.hom_of_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I₁ I₂ : lie_ideal R L} (h : I₁ I₂) :

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

Equations
@[simp]
theorem lie_ideal.coe_hom_of_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I₁ I₂ : lie_ideal R L} (h : I₁ I₂) (x : I₁) :
theorem lie_ideal.hom_of_le_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I₁ I₂ : lie_ideal R L} (h : I₁ I₂) (x : I₁) :
theorem lie_ideal.hom_of_le_injective {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {I₁ I₂ : lie_ideal R L} (h : I₁ I₂) :
@[simp]
theorem lie_ideal.map_sup_ker_eq_map {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} :
@[simp]
theorem lie_ideal.map_comap_eq {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {J : lie_ideal R L'} (h : f.is_ideal_morphism) :
@[simp]
theorem lie_ideal.comap_map_eq {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] {f : L →ₗ⁅R L'} {I : lie_ideal R L} (h : (lie_ideal.map f I) = f '' I) :
def lie_ideal.incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :

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

Equations
@[simp]
theorem lie_ideal.incl_range {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
@[simp]
theorem lie_ideal.incl_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) (x : I) :
(I.incl) x = x
@[simp]
theorem lie_ideal.incl_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
@[simp]
theorem lie_ideal.comap_incl_self {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
@[simp]
theorem lie_ideal.ker_incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
@[simp]
theorem lie_ideal.incl_ideal_range {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
def lie_module_hom.ker {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅R,L N) :

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

Equations
@[simp]
theorem lie_module_hom.ker_coe_submodule {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅R,L N) :
theorem lie_module_hom.ker_eq_bot {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅R,L N) :
@[simp]
theorem lie_module_hom.mem_ker {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] {f : M →ₗ⁅R,L N} (m : M) :
m f.ker f m = 0
@[simp]
theorem lie_module_hom.ker_id {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] :
@[simp]
theorem lie_module_hom.comp_ker_incl {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] {f : M →ₗ⁅R,L N} :
f.comp f.ker.incl = 0
theorem lie_module_hom.le_ker_iff_map {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] {f : M →ₗ⁅R,L N} (M' : lie_submodule R L M) :
def lie_module_hom.range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅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
@[simp]
theorem lie_module_hom.coe_range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅R,L N) :
@[simp]
theorem lie_module_hom.coe_submodule_range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅R,L N) :
@[simp]
theorem lie_module_hom.mem_range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅R,L N) (n : N) :
n f.range (m : M), f m = n
theorem lie_module_hom.map_top {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N] (f : M →ₗ⁅R,L N) :
@[simp]
theorem lie_submodule.ker_incl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
@[simp]
theorem lie_submodule.range_incl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
@[simp]
theorem lie_submodule.comap_incl_self {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :

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

This is the Lie subalgebra version of submodule.top_equiv.

Equations
def lie_ideal.top_equiv {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :

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

This is the Lie ideal version of submodule.top_equiv.

Equations
@[simp]