Lie subalgebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines Lie subalgebras of a Lie algebra and provides basic related definitions and results.
Main definitions #
lie_subalgebralie_subalgebra.incllie_subalgebra.maplie_hom.rangelie_equiv.of_injectivelie_equiv.of_eqlie_equiv.of_subalgebralie_equiv.of_subalgebras
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
- to_submodule : submodule R L
- lie_mem' : ∀ {x y : L}, x ∈ self.to_submodule.carrier → y ∈ self.to_submodule.carrier → ⁅x, y⁆ ∈ self.to_submodule.carrier
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
- lie_subalgebra.has_sizeof_inst
- lie_subalgebra.has_zero
- lie_subalgebra.inhabited
- submodule.has_coe
- lie_subalgebra.set_like
- lie_subalgebra.add_subgroup_class
- lie_subalgebra.partial_order
- lie_subalgebra.has_bot
- lie_subalgebra.has_top
- lie_subalgebra.has_inf
- lie_subalgebra.has_Inf
- lie_subalgebra.complete_lattice
- lie_subalgebra.add_comm_monoid
- lie_subalgebra.canonically_ordered_add_monoid
- lie_subalgebra.subsingleton_of_bot
- lie_subalgebra.has_coe
@[protected, instance]
def
lie_subalgebra.has_zero
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
has_zero (lie_subalgebra R L)
The zero algebra is a subalgebra of any Lie algebra.
@[protected, instance]
def
lie_subalgebra.inhabited
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
inhabited (lie_subalgebra R L)
Equations
- lie_subalgebra.inhabited R L = {default := 0}
@[protected, instance]
def
submodule.has_coe
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
has_coe (lie_subalgebra R L) (submodule R L)
Equations
- submodule.has_coe R L = {coe := lie_subalgebra.to_submodule _inst_3}
@[protected, instance]
def
lie_subalgebra.set_like
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
set_like (lie_subalgebra R L) L
Equations
- lie_subalgebra.set_like R L = {coe := λ (L' : lie_subalgebra R L), ↑L', coe_injective' := _}
@[protected, instance]
def
lie_subalgebra.add_subgroup_class
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
add_subgroup_class (lie_subalgebra R L) L
@[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
- lie_subalgebra.lie_ring R L L' = {to_add_comm_group := add_subgroup_class.to_add_comm_group L' _, to_has_bracket := {bracket := λ (x y : ↥L'), ⟨⁅x.val, y.val⁆, _⟩}, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}
@[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) :
A Lie subalgebra inherits module structures from L.
Equations
- lie_subalgebra.module R L L' = L'.to_submodule.module'
@[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) :
is_central_scalar 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) :
is_scalar_tower R₁ 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] :
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) :
lie_algebra R ↥L'
A Lie subalgebra forms a new Lie algebra.
Equations
- lie_subalgebra.lie_algebra R L L' = {to_module := lie_subalgebra.module R L L', lie_smul := _}
@[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} :
@[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} :
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') :
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 ∈ S → b ∈ S → a + b ∈ S)
(h₂ : 0 ∈ S)
(h₃ : ∀ (c : R) {x : L}, x ∈ S → c • x ∈ S)
(h₄ : ∀ {x y : L}, x ∈ {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier → y ∈ {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier → ⁅x, y⁆ ∈ {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier)
{x : L} :
@[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} :
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} :
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') :
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') :
@[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) :
@[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 ∈ S → b ∈ S → a + b ∈ S)
(h₂ : 0 ∈ S)
(h₃ : ∀ (c : R) {x : L}, x ∈ S → c • x ∈ S)
(h₄ : ∀ {x y : L}, x ∈ {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier → y ∈ {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier → ⁅x, y⁆ ∈ {carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃}.carrier) :
@[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' := _}.carrier → y ∈ {carrier := p.carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}.carrier → ⁅x, 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) :
theorem
lie_subalgebra.to_submodule_injective
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R 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) :
@[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] :
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
- L'.lie_ring_module = {to_has_bracket := {bracket := λ (x : ↥L') (m : M), ⁅↑x, m⁆}, add_lie := _, lie_add := _, leibniz_lie := _}
@[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] :
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
- L'.lie_module = {smul_lie := _, lie_smul := _}
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.
@[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) :
⇑(f.restrict_lie L') = ⇑f
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.
@[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.
@[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₂) :
lie_subalgebra R L₂
The range of a morphism of Lie algebras is a Lie subalgebra.
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
- f.range_restrict = {to_linear_map := {to_fun := ↑f.range_restrict.to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
@[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) :
⇑(f.equiv_range_of_injective h) x = ⟨⇑f x, _⟩
@[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) :
lie_subalgebra R L₂
The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the codomain.
Equations
- lie_subalgebra.map f K = {to_submodule := {carrier := (submodule.map ↑f ↑K).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}, lie_mem' := _}
@[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₂) :
@[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₂) :
x ∈ lie_subalgebra.map ↑e K ↔ x ∈ submodule.map ↑e ↑K
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₂) :
lie_subalgebra R L
The preimage of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the domain.
Equations
- lie_subalgebra.comap f K₂ = {to_submodule := {carrier := (submodule.comap ↑f ↑K₂).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}, lie_mem' := _}
@[protected, instance]
def
lie_subalgebra.partial_order
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
partial_order (lie_subalgebra R L)
Equations
- lie_subalgebra.partial_order = {le := λ (N N' : lie_subalgebra R L), ∀ ⦃x : L⦄, x ∈ N → x ∈ N', lt := partial_order.lt (partial_order.lift coe lie_subalgebra.coe_injective), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
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) :
@[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) :
@[protected, instance]
def
lie_subalgebra.has_bot
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
has_bot (lie_subalgebra R L)
Equations
- lie_subalgebra.has_bot = {bot := 0}
@[simp]
theorem
lie_subalgebra.bot_coe
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
@[protected, instance]
def
lie_subalgebra.has_top
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
has_top (lie_subalgebra 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₂) :
f.range = lie_subalgebra.map f ⊤
@[protected, instance]
def
lie_subalgebra.has_inf
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
has_inf (lie_subalgebra 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] :
has_Inf (lie_subalgebra R L)
Equations
- lie_subalgebra.has_Inf = {Inf := λ (S : set (lie_subalgebra R L)), {to_submodule := {carrier := (has_Inf.Inf {_x : submodule R L | ∃ (s : lie_subalgebra R L) (H : s ∈ S), ↑s = _x}).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}, lie_mem' := _}}
@[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) :
@[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)) :
is_glb S (has_Inf.Inf S)
@[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
- lie_subalgebra.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (lie_subalgebra R L) lie_subalgebra.Inf_glb), le := complete_lattice.le (complete_lattice_of_Inf (lie_subalgebra R L) lie_subalgebra.Inf_glb), lt := complete_lattice.lt (complete_lattice_of_Inf (lie_subalgebra R L) lie_subalgebra.Inf_glb), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf lie_subalgebra.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (lie_subalgebra R L) lie_subalgebra.Inf_glb), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (lie_subalgebra R L) lie_subalgebra.Inf_glb), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
@[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
- lie_subalgebra.add_comm_monoid = {add := has_sup.sup (semilattice_sup.to_has_sup (lie_subalgebra R L)), add_assoc := _, zero := ⊥, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default ⊥ has_sup.sup lie_subalgebra.add_comm_monoid._proof_4 lie_subalgebra.add_comm_monoid._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
def
lie_subalgebra.canonically_ordered_add_monoid
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
Equations
- lie_subalgebra.canonically_ordered_add_monoid = {add := add_comm_monoid.add lie_subalgebra.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero lie_subalgebra.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul lie_subalgebra.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := complete_lattice.le lie_subalgebra.complete_lattice, lt := complete_lattice.lt lie_subalgebra.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := complete_lattice.bot lie_subalgebra.complete_lattice, bot_le := _, exists_add_of_le := _, le_self_add := _}
@[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) :
@[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) :
@[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) :
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) :
@[protected, instance]
def
lie_subalgebra.subsingleton_of_bot
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
theorem
lie_subalgebra.subsingleton_bot
{R : Type u}
{L : Type v}
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
theorem
lie_subalgebra.well_founded_of_noetherian
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L]
[is_noetherian 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
- lie_subalgebra.hom_of_le h = {to_linear_map := {to_fun := (submodule.of_le h).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
@[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) :
↑(⇑(lie_subalgebra.hom_of_le h) x) = ↑x
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) :
⇑(lie_subalgebra.hom_of_le h) x = ⟨x.val, _⟩
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') :
lie_subalgebra R ↥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') :
x ∈ lie_subalgebra.of_le h ↔ ↑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') :
↥K ≃ₗ⁅R⁆ ↥(lie_subalgebra.of_le h)
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) :
⇑(lie_subalgebra.equiv_of_le h) x = ⟨⇑(lie_subalgebra.hom_of_le h) x, _⟩
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₂} :
lie_subalgebra.map f K ≤ K' ↔ K ≤ lie_subalgebra.comap f K'
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) :
lie_subalgebra R L
The Lie subalgebra of a Lie algebra L generated by a subset s ⊆ L.
Equations
- lie_subalgebra.lie_span R L s = has_Inf.Inf {N : lie_subalgebra R L | s ⊆ ↑N}
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 ⊆ ↑K → x ∈ 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} :
s ⊆ ↑(lie_subalgebra.lie_span R L s)
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} :
submodule.span R s ≤ ↑(lie_subalgebra.lie_span R L s)
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} :
lie_subalgebra.lie_span R L s ≤ K ↔ s ⊆ ↑K
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) :
lie_subalgebra.lie_span R L s ≤ lie_subalgebra.lie_span R L 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) :
lie_subalgebra.lie_span R L ↑K = K
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} :
↑(lie_subalgebra.lie_span R L ↑p) = p ↔ ∃ (K : lie_subalgebra R L), ↑K = p
@[protected]
lie_span forms a Galois insertion with the coercion from lie_subalgebra to set.
Equations
- lie_subalgebra.gi R L = {choice := λ (s : set L) (_x : ↑(lie_subalgebra.lie_span R L s) ≤ s), lie_subalgebra.lie_span R L s, gc := _, le_l_u := _, choice_eq := _}
@[simp]
theorem
lie_subalgebra.span_empty
(R : Type u)
(L : Type v)
[comm_ring R]
[lie_ring L]
[lie_algebra R L] :
lie_subalgebra.lie_span 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) :
lie_subalgebra.lie_span R L (s ∪ t) = lie_subalgebra.lie_span R L s ⊔ lie_subalgebra.lie_span R L t
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
- lie_equiv.of_injective f h = {to_lie_hom := {to_linear_map := {to_fun := (linear_equiv.of_injective ↑f _).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := (linear_equiv.of_injective ↑f _).inv_fun, left_inv := _, right_inv := _}
@[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₁) :
↑(⇑(lie_equiv.of_injective f h) x) = ⇑f x
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₁'') :
Lie subalgebras that are equal as sets are equivalent as Lie algebras.
Equations
- lie_equiv.of_eq L₁' L₁'' h = {to_lie_hom := {to_linear_map := {to_fun := (linear_equiv.of_eq ↑L₁' ↑L₁'' _).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := (linear_equiv.of_eq ↑L₁' ↑L₁'' _).inv_fun, left_inv := _, right_inv := _}
@[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) :
↑(⇑(lie_equiv.of_eq L L' h) x) = ↑x
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
- lie_equiv.lie_subalgebra_map L₁'' e = {to_lie_hom := {to_linear_map := {to_fun := (↑e.submodule_map ↑L₁'').to_fun, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := (↑e.submodule_map ↑L₁'').inv_fun, left_inv := _, right_inv := _}
@[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₂') :
An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its image.
Equations
- lie_equiv.of_subalgebras L₁' L₂' e h = {to_lie_hom := {to_linear_map := {to_fun := (↑e.of_submodules ↑L₁' ↑L₂' _).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := (↑e.of_submodules ↑L₁' ↑L₂' _).inv_fun, left_inv := _, right_inv := _}
@[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₁') :
@[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₂') :