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

source
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] :
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.

Instances for lie_submodule
source
@[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) :
submodule R M
source
@[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] :
set_like (lie_submodule R L M) M
Equations
source
@[protected, instance]
def lie_submodule.add_subgroup_class {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] :
add_subgroup_class (lie_submodule R L M) M
source
@[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] :
has_zero (lie_submodule R L M)

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

Equations
source
@[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] :
inhabited (lie_submodule R L M)
Equations
source
@[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] :
has_coe (lie_submodule R L M) (submodule R M)
Equations
source
@[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) :
N.to_submodule = ↑N
source
@[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) :
↑↑N = ↑N
source
@[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} :
x ∈ N.carrier ↔ x ∈ ↑N
source
@[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
source
@[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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem lie_submodule.coe_submodule_injective {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] :
function.injective lie_submodule.to_submodule
source
@[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'
source
@[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'
source
@[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) :
lie_submodule R L M

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

Equations
source
@[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
source
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
source
@[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) :
lie_ring_module L ↥N
Equations
source
@[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] :
module S ↥N
Equations
source
@[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) :
module R ↥N
Equations
source
@[protected, instance]
def lie_submodule.is_central_scalar {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] [has_smul Sᵐᵒᵖ R] [module S M] [module Sᵐᵒᵖ M] [is_scalar_tower S R M] [is_scalar_tower Sᵐᵒᵖ R M] [is_central_scalar S M] :
is_central_scalar S ↥N
source
@[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) :
lie_module R L ↥N
Equations
source
@[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
source
@[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'
source
@[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) :
↑-m = -↑m
source
@[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'
source
@[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
source
@[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) :
↑⁅x, m⁆ = ⁅x, ↑m⁆
source
@[reducible]
def lie_ideal (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Type v

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

source
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) :
⁅x, y⁆ ∈ I
source
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) :
⁅x, y⁆ ∈ I
source
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) :
lie_subalgebra R L

An ideal of a Lie algebra is a Lie subalgebra.

Equations
source
@[protected, instance]
def lie_subalgebra.has_coe (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
has_coe (lie_ideal R L) (lie_subalgebra R L)
Equations
source
@[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) :
↑↑I = ↑I
source
@[norm_cast]
theorem lie_ideal.coe_to_lie_subalgebra_to_submodule (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
↑↑I = ↑I
source
@[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) :
lie_ring ↥I

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

Equations
source
@[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) :
lie_algebra R ↥I

Transfer the lie_algebra instance from the coercion lie_ideal → lie_subalgebra.

Equations
source
@[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] :
lie_ring_module ↥I M

Transfer the lie_module instance from the coercion lie_ideal → lie_subalgebra.

Equations
source
@[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) :
⁅x, m⁆ = ⁅↑x, m⁆
source
@[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) :
lie_module R ↥I M

Transfer the lie_module instance from the coercion lie_ideal → lie_subalgebra.

Equations
source
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
source
def lie_subalgebra.to_lie_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K : lie_subalgebra R L) :
lie_submodule 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
source
@[simp]
theorem lie_subalgebra.coe_to_lie_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K : lie_subalgebra R L) :
↑(K.to_lie_submodule) = ↑K
source
@[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) :
x ∈ K.to_lie_submodule ↔ x ∈ K
source
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
source
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
source
theorem lie_submodule.coe_injective {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] :
function.injective coe
source
@[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'
source
@[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] :
has_bot (lie_submodule R L M)
Equations
source
@[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}
source
@[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] :
↑⊥ = ⊥
source
@[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
source
@[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] :
has_top (lie_submodule R L M)
Equations
source
@[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] :
↑⊤ = set.univ
source
@[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] :
↑⊤ = ⊤
source
@[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) :
x ∈ ⊤
source
@[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] :
has_inf (lie_submodule R L M)
Equations
source
@[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] :
has_Inf (lie_submodule R L M)
Equations
source
@[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'
source
@[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}
source
@[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
source
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)) :
is_glb S (has_Inf.Inf S)
source
@[protected, instance]
def lie_submodule.complete_lattice {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] :
complete_lattice (lie_submodule R 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
source
@[protected, instance]
def lie_submodule.add_comm_monoid {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] :
add_comm_monoid (lie_submodule R L M)
Equations
source
@[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'
source
@[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'
source
@[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'
source
@[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'
source
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
source
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
source
@[protected, instance]
def lie_submodule.subsingleton_of_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] :
subsingleton (lie_submodule R L ↥⊥)
source
@[protected, instance]
def lie_submodule.is_modular_lattice {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] :
is_modular_lattice (lie_submodule R L M)
source
theorem lie_submodule.well_founded_of_noetherian (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] [is_noetherian R M] :
well_founded gt
source
@[simp]
theorem lie_submodule.subsingleton_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] :
subsingleton (lie_submodule R L M) ↔ subsingleton M
source
@[simp]
theorem lie_submodule.nontrivial_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] :
nontrivial (lie_submodule R L M) ↔ nontrivial M
source
@[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] :
nontrivial (lie_submodule R L M)
source
theorem lie_submodule.nontrivial_iff_ne_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 : lie_submodule R L M} :
nontrivial ↥N ↔ N ≠ ⊥
source
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) :
↥N →ₗ⁅R,L⁆ M

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

Equations
source
@[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) :
↑(N.incl) = ↑N.subtype
source
@[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
source
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) :
⇑(N.incl) = subtype.val
source
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') :
↥N →ₗ⁅R,L⁆ ↥N'

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

Equations
source
@[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) :
↑(⇑(lie_submodule.hom_of_le h) m) = ↑m
source
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) :
⇑(lie_submodule.hom_of_le h) m = ⟨m.val, _⟩
source
theorem lie_submodule.hom_of_le_injective {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') :
function.injective ⇑(lie_submodule.hom_of_le h)
source
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) :
lie_submodule R L M

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

Equations
source
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} :
x ∈ lie_submodule.lie_span R L s ↔ ∀ (N : lie_submodule R L M), s ⊆ ↑N → x ∈ N
source
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} :
s ⊆ ↑(lie_submodule.lie_span R L s)
source
theorem lie_submodule.submodule_span_le_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} :
submodule.span R s ≤ ↑(lie_submodule.lie_span R L s)
source
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} :
lie_submodule.lie_span R L s ≤ N ↔ s ⊆ ↑N
source
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) :
lie_submodule.lie_span R L s ≤ lie_submodule.lie_span R L t
source
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) :
lie_submodule.lie_span R L ↑N = N
source
theorem lie_submodule.coe_lie_span_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] {p : submodule R M} :
↑(lie_submodule.lie_span R L ↑p) = p ↔ ∃ (N : lie_submodule R L M), ↑N = p
source
@[protected]
def lie_submodule.gi (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] :
galois_insertion (lie_submodule.lie_span R L) coe

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

Equations
source
@[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] :
lie_submodule.lie_span R L ∅ = ⊥
source
@[simp]
theorem lie_submodule.span_univ (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] :
lie_submodule.lie_span R L set.univ = ⊤
source
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
source
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] (s t : set M) :
lie_submodule.lie_span R L (s ∪ t) = lie_submodule.lie_span R L s ⊔ lie_submodule.lie_span R L t
source
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)
source
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) :
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
source
@[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) :
↑(lie_submodule.map f N) = submodule.map ↑f ↑N
source
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') :
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
source
@[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') :
↑(lie_submodule.comap f N') = submodule.comap ↑f ↑N'
source
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'} :
lie_submodule.map f N ≤ N' ↔ N ≤ lie_submodule.comap f N'
source
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') :
galois_connection (lie_submodule.map f) (lie_submodule.comap f)
source
@[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} :
lie_submodule.map f (N ⊔ N₂) = lie_submodule.map f N ⊔ lie_submodule.map f N₂
source
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'
source
@[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} :
m ∈ lie_submodule.comap f N' ↔ ⇑f m ∈ N'
source
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} :
lie_submodule.comap N.incl N₂ = ⊤ ↔ N ≤ N₂
source
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} :
lie_submodule.comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥
source
@[simp]
theorem lie_ideal.top_coe_lie_subalgebra {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
↑⊤ = ⊤
source
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) :
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
source
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') :
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
source
@[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) :
↑(lie_ideal.map f I) = submodule.map ↑f ↑I
source
@[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') :
↑(lie_ideal.comap f J) = submodule.comap ↑f ↑J
source
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') :
lie_ideal.map f I ≤ J ↔ ⇑f '' ↑I ⊆ ↑J
source
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) :
⇑f x ∈ lie_ideal.map f I
source
@[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} :
x ∈ lie_ideal.comap f J ↔ ⇑f x ∈ J
source
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'} :
lie_ideal.map f I ≤ J ↔ I ≤ lie_ideal.comap f J
source
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') :
galois_connection (lie_ideal.map f) (lie_ideal.comap f)
source
@[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} :
lie_ideal.map f (I ⊔ I₂) = lie_ideal.map f I ⊔ lie_ideal.map f I₂
source
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'} :
lie_ideal.map f (lie_ideal.comap f J) ≤ J
source
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} :
I ≤ lie_ideal.comap f (lie_ideal.map f I)

See also lie_ideal.map_comap_eq.

source
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'} :
monotone (lie_ideal.map f)
source
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'} :
monotone (lie_ideal.comap f)
source
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) :
lie_ideal.map f I = J
source
@[protected, instance]
def lie_ideal.subsingleton_of_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
subsingleton (lie_ideal R ↥⊥)

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.

source
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') :
lie_ideal R L

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

Equations
source
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') :
lie_ideal R L'

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

Equations
source
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') :
f.ideal_range = lie_submodule.lie_span R L' ↑(f.range)
source
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') :
f.ideal_range = lie_ideal.map f ⊤
source
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
source
@[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') :
f.is_ideal_morphism ↔ ↑(f.ideal_range) = f.range
source
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
source
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') :
↑(f.range) ⊆ ↑(f.ideal_range)
source
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) :
lie_ideal.map f I ≤ f.ideal_range
source
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') :
f.ker ≤ lie_ideal.comap f J
source
@[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') :
↑(f.ker) = linear_map.ker ↑f
source
@[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
source
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} :
⇑f x ∈ f.ideal_range
source
@[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
source
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
source
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') :
f.ker = ⊥ ↔ function.injective ⇑f
source
@[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') :
↑(f.range) = linear_map.range ↑f
source
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') :
f.range = ⊤ ↔ function.surjective ⇑f
source
@[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) :
f.ideal_range = ⊤
source
theorem lie_hom.is_ideal_morphism_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) :
f.is_ideal_morphism
source
@[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} :
lie_ideal.map f I = ⊥ ↔ I ≤ f.ker
source
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) :
↑(lie_ideal.map f I) = submodule.map ↑f ↑I
source
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
source
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 = ⊥
source
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₂) :
↥I₁ →ₗ⁅R⁆ ↥I₂

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

Equations
source
@[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₁) :
↑(⇑(lie_ideal.hom_of_le h) x) = ↑x
source
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₁) :
⇑(lie_ideal.hom_of_le h) x = ⟨x.val, _⟩
source
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₂) :
function.injective ⇑(lie_ideal.hom_of_le h)
source
@[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} :
lie_ideal.map f (I ⊔ f.ker) = lie_ideal.map f I
source
@[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) :
lie_ideal.map f (lie_ideal.comap f J) = f.ideal_range ⊓ J
source
@[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) :
lie_ideal.comap f (lie_ideal.map f I) = I ⊔ f.ker
source
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) :
↥I →ₗ⁅R⁆ L

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

Equations
source
@[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) :
I.incl.range = ↑I
source
@[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
source
@[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) :
↑(I.incl) = ↑I.subtype
source
@[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) :
lie_ideal.comap I.incl I = ⊤
source
@[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) :
I.incl.ker = ⊥
source
@[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) :
I.incl.ideal_range = I
source
theorem lie_ideal.incl_is_ideal_morphism {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) :
I.incl.is_ideal_morphism
source
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) :
lie_submodule R L M

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

Equations
source
@[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) :
↑(f.ker) = linear_map.ker ↑f
source
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) :
f.ker = ⊥ ↔ function.injective ⇑f
source
@[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
source
@[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] :
lie_module_hom.id.ker = ⊥
source
@[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
source
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) :
M' ≤ f.ker ↔ lie_submodule.map f M' = ⊥
source
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) :
lie_submodule 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
source
@[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) :
↑(f.range) = set.range ⇑f
source
@[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) :
↑(f.range) = linear_map.range ↑f
source
@[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
source
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) :
lie_submodule.map f ⊤ = f.range
source
@[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) :
N.incl.ker = ⊥
source
@[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) :
N.incl.range = N
source
@[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) :
lie_submodule.comap N.incl N = ⊤
source
def lie_subalgebra.top_equiv {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra 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.top_equiv.

Equations
source
@[simp]
theorem lie_subalgebra.top_equiv_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (x : ↥⊤) :
⇑lie_subalgebra.top_equiv x = ↑x
source
def lie_ideal.top_equiv {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
↥⊤ ≃ₗ⁅R⁆ L

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

This is the Lie ideal version of submodule.top_equiv.

Equations
source
@[simp]
theorem lie_ideal.top_equiv_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (x : ↥⊤) :
⇑lie_ideal.top_equiv x = ↑x