mathlib documentation

algebra.lie.subalgebra

Lie subalgebras #

This file defines Lie subalgebras of a Lie algebra and provides basic related definitions and results.

Main definitions #

Tags #

lie algebra, lie subalgebra

structure lie_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Type v

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

Instances for lie_subalgebra
@[protected, instance]
def lie_subalgebra.has_zero (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

The zero algebra is a subalgebra of any Lie algebra.

Equations
@[protected, instance]
def lie_subalgebra.inhabited (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[protected, instance]
def submodule.has_coe (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[protected, instance]
def lie_subalgebra.set_like (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[protected, instance]
def lie_subalgebra.add_subgroup_class (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[protected, instance]
def lie_subalgebra.lie_ring (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :

A Lie subalgebra forms a new Lie ring.

Equations
@[protected, instance]
def lie_subalgebra.module (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] {R₁ : Type u_1} [semiring R₁] [has_smul R₁ R] [module R₁ L] [is_scalar_tower R₁ R L] (L' : lie_subalgebra R L) :
module R₁ L'

A Lie subalgebra inherits module structures from L.

Equations
@[protected, instance]
def lie_subalgebra.is_central_scalar (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] {R₁ : Type u_1} [semiring R₁] [has_smul R₁ R] [has_smul R₁ᵐᵒᵖ R] [module R₁ L] [module R₁ᵐᵒᵖ L] [is_scalar_tower R₁ R L] [is_scalar_tower R₁ᵐᵒᵖ R L] [is_central_scalar R₁ L] (L' : lie_subalgebra R L) :
@[protected, instance]
def lie_subalgebra.is_scalar_tower (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] {R₁ : Type u_1} [semiring R₁] [has_smul R₁ R] [module R₁ L] [is_scalar_tower R₁ R L] (L' : lie_subalgebra R L) :
@[protected, instance]
def lie_subalgebra.is_noetherian (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) [is_noetherian R L] :
@[protected, instance]
def lie_subalgebra.lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :

A Lie subalgebra forms a new Lie algebra.

Equations
@[protected, simp]
theorem lie_subalgebra.zero_mem {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :
0 L'
@[protected]
theorem lie_subalgebra.add_mem {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) {x y : L} :
x L'y L'x + y L'
@[protected]
theorem lie_subalgebra.sub_mem {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) {x y : L} :
x L'y L'x - y L'
theorem lie_subalgebra.smul_mem {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) (t : R) {x : L} (h : x L') :
t x L'
theorem lie_subalgebra.lie_mem {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) {x y : L} (hx : x L') (hy : y L') :
@[simp]
theorem lie_subalgebra.mem_carrier {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) {x : L} :
@[simp]
theorem lie_subalgebra.mem_mk_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (S : set L) (h₁ : ∀ {a b : L}, a Sb Sa + b S) (h₂ : 0 S) (h₃ : ∀ (c : R) {x : L}, x Sc x S) (h₄ : ∀ {x y : L}, x {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carriery {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrierx,y {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier) {x : L} :
x {to_submodule := {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}, lie_mem' := h₄} x S
@[simp]
theorem lie_subalgebra.mem_coe_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) {x : L} :
x L' x L'
theorem lie_subalgebra.mem_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) {x : L} :
x L' x L'
@[simp, norm_cast]
theorem lie_subalgebra.coe_bracket {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) (x y : L') :
theorem lie_subalgebra.ext_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) (x y : L') :
x = y x = y
theorem lie_subalgebra.coe_zero_iff_zero {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) (x : L') :
x = 0 x = 0
@[ext]
theorem lie_subalgebra.ext {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L₁' L₂' : lie_subalgebra R L) (h : ∀ (x : L), x L₁' x L₂') :
L₁' = L₂'
theorem lie_subalgebra.ext_iff' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L₁' L₂' : lie_subalgebra R L) :
L₁' = L₂' ∀ (x : L), x L₁' x L₂'
@[simp]
theorem lie_subalgebra.mk_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (S : set L) (h₁ : ∀ {a b : L}, a Sb Sa + b S) (h₂ : 0 S) (h₃ : ∀ (c : R) {x : L}, x Sc x S) (h₄ : ∀ {x y : L}, x {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carriery {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrierx,y {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier) :
{to_submodule := {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}, lie_mem' := h₄} = S
@[simp]
theorem lie_subalgebra.coe_to_submodule_mk {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (p : submodule R L) (h : ∀ {x y : L}, x {carrier := p.carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}.carriery {carrier := p.carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}.carrierx,y {carrier := p.carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}.carrier) :
theorem lie_subalgebra.coe_injective {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
@[norm_cast]
theorem lie_subalgebra.coe_set_eq {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L₁' L₂' : lie_subalgebra R L) :
L₁' = L₂' L₁' = L₂'
@[simp]
theorem lie_subalgebra.coe_to_submodule_eq_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L₁' L₂' : lie_subalgebra R L) :
L₁' = L₂' L₁' = L₂'
@[norm_cast]
theorem lie_subalgebra.coe_to_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :
@[protected, instance]
def lie_subalgebra.lie_ring_module {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) {M : Type w} [add_comm_group M] [lie_ring_module L M] :

Given a Lie algebra L containing a Lie subalgebra L' ⊆ L, together with a Lie ring module M of L, we may regard M as a Lie ring module of L' by restriction.

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

Given a Lie algebra L containing a Lie subalgebra L' ⊆ L, together with a Lie module M of L, we may regard M as a Lie module of L' by restriction.

Equations
def lie_module_hom.restrict_lie {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type w} [add_comm_group M] [lie_ring_module L M] {N : Type w₁} [add_comm_group N] [lie_ring_module L N] [module R N] [lie_module R L N] [module R M] [lie_module R L M] (f : M →ₗ⁅R,L N) (L' : lie_subalgebra R L) :

An L-equivariant map of Lie modules M → N is L'-equivariant for any Lie subalgebra L' ⊆ L.

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

The embedding of a Lie subalgebra into the ambient space as a morphism of Lie algebras.

Equations
@[simp]
theorem lie_subalgebra.coe_incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :
def lie_subalgebra.incl' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :

The embedding of a Lie subalgebra into the ambient space as a morphism of Lie modules.

Equations
@[simp]
theorem lie_subalgebra.coe_incl' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (L' : lie_subalgebra R L) :
def lie_hom.range {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) :

The range of a morphism of Lie algebras is a Lie subalgebra.

Equations
@[simp]
theorem lie_hom.range_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) :
@[simp]
theorem lie_hom.mem_range {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (x : L₂) :
x f.range ∃ (y : L), f y = x
theorem lie_hom.mem_range_self {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (x : L) :
def lie_hom.range_restrict {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) :

We can restrict a morphism to a (surjective) map to its range.

Equations
@[simp]
theorem lie_hom.range_restrict_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (x : L) :
(f.range_restrict) x = f x, _⟩
theorem lie_hom.surjective_range_restrict {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) :
noncomputable def lie_hom.equiv_range_of_injective {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (h : function.injective f) :

A Lie algebra is equivalent to its range under an injective Lie algebra morphism.

Equations
@[simp]
theorem lie_hom.equiv_range_of_injective_apply {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (h : function.injective f) (x : L) :
theorem submodule.exists_lie_subalgebra_coe_eq_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (p : submodule R L) :
(∃ (K : lie_subalgebra R L), K = p) ∀ (x y : L), x py px,y p
@[simp]
theorem lie_subalgebra.incl_range {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K : lie_subalgebra R L) :
def lie_subalgebra.map {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (K : lie_subalgebra R L) :

The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the codomain.

Equations
@[simp]
theorem lie_subalgebra.mem_map {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (K : lie_subalgebra R L) (x : L₂) :
x lie_subalgebra.map f K ∃ (y : L), y K f y = x
@[simp]
theorem lie_subalgebra.mem_map_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (K : lie_subalgebra R L) (e : L ≃ₗ⁅R L₂) (x : L₂) :
def lie_subalgebra.comap {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) (K₂ : lie_subalgebra R L₂) :

The preimage of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the domain.

Equations
@[protected, instance]
def lie_subalgebra.partial_order {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
theorem lie_subalgebra.le_def {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K K' : lie_subalgebra R L) :
K K' K K'
@[simp, norm_cast]
theorem lie_subalgebra.coe_submodule_le_coe_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K K' : lie_subalgebra R L) :
K K' K K'
@[protected, instance]
def lie_subalgebra.has_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[simp]
theorem lie_subalgebra.bot_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
= {0}
@[simp]
theorem lie_subalgebra.bot_coe_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
@[simp]
theorem lie_subalgebra.mem_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (x : L) :
x x = 0
@[protected, instance]
def lie_subalgebra.has_top {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[simp]
theorem lie_subalgebra.top_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
@[simp]
theorem lie_subalgebra.top_coe_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
@[simp]
theorem lie_subalgebra.mem_top {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (x : L) :
theorem lie_hom.range_eq_map {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] (f : L →ₗ⁅R L₂) :
@[protected, instance]
def lie_subalgebra.has_inf {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[protected, instance]
def lie_subalgebra.has_Inf {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[simp]
theorem lie_subalgebra.inf_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K K' : lie_subalgebra R L) :
(K K') = K K'
@[simp]
theorem lie_subalgebra.Inf_coe_to_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (S : set (lie_subalgebra R L)) :
(has_Inf.Inf S) = has_Inf.Inf {_x : submodule R L | ∃ (s : lie_subalgebra R L) (H : s S), s = _x}
@[simp]
theorem lie_subalgebra.Inf_coe {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (S : set (lie_subalgebra R L)) :
(has_Inf.Inf S) = ⋂ (s : lie_subalgebra R L) (H : s S), s
theorem lie_subalgebra.Inf_glb {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (S : set (lie_subalgebra R L)) :
@[protected, instance]
def lie_subalgebra.complete_lattice {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :

The set of Lie subalgebras of a Lie algebra 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_subalgebra.add_comm_monoid {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
Equations
@[simp]
theorem lie_subalgebra.add_eq_sup {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K K' : lie_subalgebra R L) :
K + K' = K K'
@[simp, norm_cast]
theorem lie_subalgebra.inf_coe_to_submodule {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K K' : lie_subalgebra R L) :
(K K') = K K'
@[simp]
theorem lie_subalgebra.mem_inf {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K K' : lie_subalgebra R L) (x : L) :
x K K' x K x K'
theorem lie_subalgebra.eq_bot_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K : lie_subalgebra R L) :
K = ∀ (x : L), x Kx = 0
@[protected, instance]
theorem lie_subalgebra.subsingleton_bot {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] :
def lie_subalgebra.hom_of_le {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') :

Given two nested Lie subalgebras K ⊆ K', the inclusion K ↪ K' is a morphism of Lie algebras.

Equations
@[simp]
theorem lie_subalgebra.coe_hom_of_le {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') (x : K) :
theorem lie_subalgebra.hom_of_le_apply {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') (x : K) :
theorem lie_subalgebra.hom_of_le_injective {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') :
def lie_subalgebra.of_le {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') :

Given two nested Lie subalgebras K ⊆ K', we can view K as a Lie subalgebra of K', regarded as Lie algebra in its own right.

Equations
@[simp]
theorem lie_subalgebra.mem_of_le {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') (x : K') :
theorem lie_subalgebra.of_le_eq_comap_incl {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') :
@[simp]
theorem lie_subalgebra.coe_of_le {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') :
noncomputable def lie_subalgebra.equiv_of_le {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') :

Given nested Lie subalgebras K ⊆ K', there is a natural equivalence from K to its image in K'.

Equations
@[simp]
theorem lie_subalgebra.equiv_of_le_apply {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') (x : K) :
theorem lie_subalgebra.map_le_iff_le_comap {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] {f : L →ₗ⁅R L₂} {K : lie_subalgebra R L} {K' : lie_subalgebra R L₂} :
theorem lie_subalgebra.gc_map_comap {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂] {f : L →ₗ⁅R L₂} :
def lie_subalgebra.lie_span (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (s : set L) :

The Lie subalgebra of a Lie algebra L generated by a subset s ⊆ L.

Equations
theorem lie_subalgebra.mem_lie_span {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {s : set L} {x : L} :
x lie_subalgebra.lie_span R L s ∀ (K : lie_subalgebra R L), s Kx K
theorem lie_subalgebra.subset_lie_span {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {s : set L} :
theorem lie_subalgebra.submodule_span_le_lie_span {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {s : set L} :
theorem lie_subalgebra.lie_span_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {s : set L} {K : lie_subalgebra R L} :
theorem lie_subalgebra.lie_span_mono {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {s t : set L} (h : s t) :
theorem lie_subalgebra.lie_span_eq {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (K : lie_subalgebra R L) :
theorem lie_subalgebra.coe_lie_span_submodule_eq_iff {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {p : submodule R L} :
@[protected]
def lie_subalgebra.gi (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :

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

Equations
@[simp]
theorem lie_subalgebra.span_empty (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
@[simp]
theorem lie_subalgebra.span_univ (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] :
theorem lie_subalgebra.span_union (R : Type u) {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (s t : set L) :
theorem lie_subalgebra.span_Union (R : Type u) {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {ι : Sort u_1} (s : ι → set L) :
lie_subalgebra.lie_span R L (⋃ (i : ι), s i) = ⨆ (i : ι), lie_subalgebra.lie_span R L (s i)
noncomputable def lie_equiv.of_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : function.injective f) :

An injective Lie algebra morphism is an equivalence onto its range.

Equations
@[simp]
theorem lie_equiv.of_injective_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : function.injective f) (x : L₁) :
def lie_equiv.of_eq {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (L₁' L₁'' : lie_subalgebra R L₁) (h : L₁' = L₁'') :
L₁' ≃ₗ⁅R L₁''

Lie subalgebras that are equal as sets are equivalent as Lie algebras.

Equations
@[simp]
theorem lie_equiv.of_eq_apply {R : Type u} {L₁ : Type v} [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] (L L' : lie_subalgebra R L₁) (h : L = L') (x : L) :
def lie_equiv.lie_subalgebra_map {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁'' : lie_subalgebra R L₁) (e : L₁ ≃ₗ⁅R L₂) :

An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image.

Equations
@[simp]
theorem lie_equiv.lie_subalgebra_map_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁'' : lie_subalgebra R L₁) (e : L₁ ≃ₗ⁅R L₂) (x : L₁'') :
def lie_equiv.of_subalgebras {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : lie_subalgebra.map e L₁' = L₂') :
L₁' ≃ₗ⁅R L₂'

An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image.

Equations
@[simp]
theorem lie_equiv.of_subalgebras_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : lie_subalgebra.map e L₁' = L₂') (x : L₁') :
((lie_equiv.of_subalgebras L₁' L₂' e h) x) = e x
@[simp]
theorem lie_equiv.of_subalgebras_symm_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂] (L₁' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂) (e : L₁ ≃ₗ⁅R L₂) (h : lie_subalgebra.map e L₁' = L₂') (x : L₂') :
(((lie_equiv.of_subalgebras L₁' L₂' e h).symm) x) = (e.symm) x