# mathlibdocumentation

algebra.lie.submodule

# Lie submodules of a Lie algebra #

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

## Main definitions #

• `lie_submodule`
• `lie_submodule.well_founded_of_noetherian`
• `lie_submodule.lie_span`
• `lie_submodule.map`
• `lie_submodule.comap`
• `lie_ideal`
• `lie_ideal.map`
• `lie_ideal.comap`

## 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] [ L] [ M] [ M] [ L 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.

@[nolint]
def lie_submodule.to_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (self : M) :
M
@[protected, instance]
def lie_submodule.set_like {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
set_like L M) M
Equations
@[protected, instance]
def lie_submodule.has_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] :
has_coe L M) M)
Equations
@[norm_cast]
theorem lie_submodule.coe_to_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
@[simp]
theorem lie_submodule.mem_carrier {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (S : set M) (h₁ : 0 S) (h₂ : ∀ {a b : M}, a Sb Sa + b S) (h₃ : ∀ (c : R) {x : M}, x Sc x S) (h₄ : ∀ {x : L} {m : M}, m Sx,m S) {x : M} :
x {carrier := S, zero_mem' := h₁, add_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] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (N : M) {x : M} :
x N x N
@[simp]
theorem lie_submodule.zero_mem {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
0 N
@[simp]
theorem lie_submodule.coe_to_set_mk {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (S : set M) (h₁ : 0 S) (h₂ : ∀ {a b : M}, a Sb Sa + b S) (h₃ : ∀ (c : R) {x : M}, x Sc x S) (h₄ : ∀ {x : L} {m : M}, m Sx,m S) :
{carrier := S, zero_mem' := h₁, add_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] [ L] [ M] [ M] [ L M] (p : M) (h : ∀ {x : L} {m : M}, m p.carrierx,m p.carrier) :
{carrier := p.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _, lie_mem := h} = p
theorem lie_submodule.coe_submodule_injective {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[ext]
theorem lie_submodule.ext {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (N : M) (s : set M) (hs : s = N) :
M

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] [ L] [ M] [ M] [ L M] (S : 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] [ L] [ M] [ M] [ L M] (S : 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] [ L] [ M] [ M] [ L M] (N : M) :
Equations
@[protected, instance]
def lie_submodule.module' {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) {S : Type u_1} [semiring S] [ R] [ M] [ M] :
N
Equations
@[protected, instance]
def lie_submodule.module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
N
Equations
@[protected, instance]
def lie_submodule.is_central_scalar {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) {S : Type u_1} [semiring S] [ R] [ R] [ M] [ M] [ M] [ M] [ M] :
@[protected, instance]
def lie_submodule.lie_module {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
L N
Equations
@[simp, norm_cast]
theorem lie_submodule.coe_zero {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (N : M) (x : L) (m : N) :
def lie_ideal (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] :
Type v

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

theorem lie_mem_right (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) (x y : L) (h : y I) :
theorem lie_mem_left (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) (x y : L) (h : x I) :
def lie_ideal_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : 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] [ L] :
has_coe L) L)
Equations
• = {coe := λ (I : L), I}
@[norm_cast]
theorem lie_ideal.coe_to_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) :
@[norm_cast]
theorem lie_ideal.coe_to_lie_subalgebra_to_submodule (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (I : L) :
theorem submodule.exists_lie_submodule_coe_eq_iff {R : Type u} (L : Type v) {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (p : M) :
(∃ (N : M), N = p) ∀ (x : L) (m : M), m px,m p
def lie_subalgebra.to_lie_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (K : L) :
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
@[simp]
theorem lie_subalgebra.coe_to_lie_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (K : L) :
@[simp]
theorem lie_subalgebra.mem_to_lie_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {K : L} (x : L) :
x K
theorem lie_subalgebra.exists_lie_ideal_coe_eq_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {K : L} :
(∃ (I : L), I = K) ∀ (x y : L), y Kx,y K
theorem lie_subalgebra.exists_nested_lie_ideal_coe_eq_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {K K' : L} (h : K K') :
(∃ (I : K'), ∀ (x y : L), x K'y Kx,y K
theorem lie_submodule.coe_injective {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[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] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] :
has_bot L M)
Equations
@[simp]
theorem lie_submodule.bot_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_submodule.mem_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] :
has_top L M)
Equations
@[simp]
theorem lie_submodule.top_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_submodule.top_coe_submodule {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_submodule.mem_top {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] :
has_inf 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] [ L] [ M] [ M] [ L M] :
has_Inf L M)
Equations
@[simp]
theorem lie_submodule.inf_coe {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (S : set L M)) :
(Inf S) = Inf {_x : M | ∃ (s : 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] [ L] [ M] [ M] [ L M] (S : set L M)) :
(Inf S) = ⋂ (s : 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] [ L] [ M] [ M] [ L M] (S : set L M)) :
(Inf S)
@[protected, instance]
def lie_submodule.complete_lattice {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :

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]
def lie_submodule.add_comm_monoid {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
Equations
@[simp]
theorem lie_submodule.add_eq_sup {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (N N' : 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] [ L] [ M] [ M] [ L M] (N : M) :
N = ∀ (m : M), m Nm = 0
theorem lie_submodule.subsingleton_of_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[protected, instance]
def lie_submodule.is_modular_lattice {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
theorem lie_submodule.well_founded_of_noetherian (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ M] :
@[simp]
theorem lie_submodule.subsingleton_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_submodule.nontrivial_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
@[protected, instance]
def lie_submodule.nontrivial (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [nontrivial M] :
theorem lie_submodule.nontrivial_iff_ne_bot (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N : M} :
def lie_submodule.incl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :

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

Equations
@[simp]
theorem lie_submodule.incl_apply {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : 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] [ L] [ M] [ M] [ L M] (N : M) :
def lie_submodule.hom_of_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N N' : 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] [ L] [ M] [ M] [ L M] {N N' : M} (h : N N') (m : N) :
m) = m
theorem lie_submodule.hom_of_le_apply {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N N' : M} (h : N N') (m : N) :
= m.val, _⟩
theorem lie_submodule.hom_of_le_injective {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {N N' : M} (h : N N') :
def lie_submodule.lie_span (R : Type u) (L : Type v) {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (s : set M) :
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] [ L] [ M] [ M] [ L M] {s : set M} {x : M} :
x ∀ (N : M), s Nx N
theorem lie_submodule.subset_lie_span {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {s : set M} :
s s)
theorem lie_submodule.submodule_span_le_lie_span {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {s : set M} :
s)
theorem lie_submodule.lie_span_le {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {s : set M} {N : M} :
N s N
theorem lie_submodule.lie_span_mono {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] (N : M) :
= N
theorem lie_submodule.coe_lie_span_submodule_eq_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {p : M} :
p) = p ∃ (N : M), N = p
@[protected]
def lie_submodule.gi (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :

`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] [ L] [ M] [ M] [ L M] :
@[simp]
theorem lie_submodule.span_univ (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
theorem lie_submodule.lie_span_eq_bot_iff (R : Type u) (L : Type v) (M : Type w) [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {s : set M} :
= ∀ (m : M), m sm = 0
theorem lie_submodule.span_union (R : Type u) (L : Type v) {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (s t : set M) :
(s t) =
theorem lie_submodule.span_Union (R : Type u) (L : Type v) {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] {ι : Sort u_1} (s : ι → set M) :
(⋃ (i : ι), s i) = ⨆ (i : ι), (s i)
def lie_submodule.map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] (f : M →ₗ⁅R,L M') (N : M) :
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] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] (f : M →ₗ⁅R,L M') (N : M) :
N) =
def lie_submodule.comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] (f : M →ₗ⁅R,L M') (N' : M') :
M

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

Equations
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] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] {f : M →ₗ⁅R,L M'} {N : M} {N' : M'} :
N' N
theorem lie_submodule.gc_map_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ 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] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] {f : M →ₗ⁅R,L M'} {N N₂ : M} :
(N N₂) =
theorem lie_submodule.mem_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] {f : M →ₗ⁅R,L M'} {N : M} (m' : M') :
m' ∃ (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] [ L] [ M] [ M] [ L M] [add_comm_group M'] [ M'] [ M'] [ L M'] {f : M →ₗ⁅R,L M'} {N' : M'} {m : M} :
m f m N'
@[simp]
theorem lie_ideal.top_coe_lie_subalgebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] :
def lie_ideal.map {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (I : L) :
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] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (J : L') :
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] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (I : L) (h : I) = f '' I) :
I) =
@[simp]
theorem lie_ideal.comap_coe_submodule {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (J : L') :
J) =
theorem lie_ideal.map_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (I : L) (J : L') :
theorem lie_ideal.mem_map {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} {x : L} (hx : x I) :
f x
@[simp]
theorem lie_ideal.mem_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {J : L'} {x : L} :
x f x J
theorem lie_ideal.map_le_iff_le_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} {J : L'} :
J I
theorem lie_ideal.gc_map_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I I₂ : L} :
(I I₂) = I₂
theorem lie_ideal.map_comap_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {J : L'} :
J) J
theorem lie_ideal.comap_map_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} :
I I)

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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} {J : L'} (h : f '' I = J) :
= J
theorem lie_ideal.subsingleton_of_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] :

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] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') :
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] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') :
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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (I : L) :
theorem lie_hom.ker_le_comap {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (J : L') :
f.ker
@[simp]
theorem lie_hom.ker_coe_submodule {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (I : L) :
I f.ker ∀ (x : L), x If x = 0
theorem lie_hom.ker_eq_bot {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') (h : function.surjective f) :
theorem lie_hom.is_ideal_morphism_of_surjective {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ 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] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} :
= I f.ker
theorem lie_ideal.coe_map_of_surjective {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} (h : function.surjective f) :
I) =
theorem lie_ideal.mem_map_of_surjective {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} {y : L'} (h₁ : function.surjective f) (h₂ : y ) :
∃ (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] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} (h₁ : function.injective f) (h₂ : = ) :
I =
def lie_ideal.hom_of_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I₁ I₂ : 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] [ L] {I₁ I₂ : L} (h : I₁ I₂) (x : I₁) :
( x) = x
theorem lie_ideal.hom_of_le_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I₁ I₂ : L} (h : I₁ I₂) (x : I₁) :
x = x.val, _⟩
theorem lie_ideal.hom_of_le_injective {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I₁ I₂ : 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] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} :
(I f.ker) =
@[simp]
theorem lie_ideal.map_comap_eq {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {J : L'} (h : f.is_ideal_morphism) :
J) = f.ideal_range J
@[simp]
theorem lie_ideal.comap_map_eq {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {I : L} (h : I) = f '' I) :
I) = I f.ker
def lie_ideal.incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : 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] [ L] (I : L) :
@[simp]
theorem lie_ideal.incl_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : 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] [ L] (I : L) :
@[simp]
theorem lie_ideal.comap_incl_self {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :
@[simp]
theorem lie_ideal.ker_incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :
@[simp]
theorem lie_ideal.incl_ideal_range {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :
theorem lie_ideal.incl_is_ideal_morphism {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) :
def lie_module_hom.ker {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) :
M

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

Equations
@[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] [ L] [ M] [ M] [ L M] [ N] [ N] [ 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] [ L] [ M] [ M] [ 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] [ L] [ M] [ M] [ L M] [ N] [ N] [ 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] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] {f : M →ₗ⁅R,L N} (M' : M) :
M' f.ker =
def lie_module_hom.range {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) :
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] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) :
(f.range) =
@[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] [ L] [ M] [ M] [ L M] [ N] [ N] [ 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] [ L] [ M] [ M] [ L M] [ N] [ N] [ 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] [ L] [ M] [ M] [ L M] [ N] [ N] [ L N] (f : M →ₗ⁅R,L N) :
def lie_subalgebra.top_equiv_self {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] :

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

Equations
@[simp]
theorem lie_subalgebra.top_equiv_self_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (x : ) :
def lie_ideal.top_equiv_self {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] :

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

Equations
@[simp]
theorem lie_ideal.top_equiv_self_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (x : ) :