# Lie subalgebras #

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

## Main definitions #

• LieSubalgebra
• LieSubalgebra.incl
• LieSubalgebra.map
• LieHom.range
• LieEquiv.ofInjective
• LieEquiv.ofEq
• LieEquiv.ofSubalgebras

## Tags #

lie algebra, lie subalgebra

structure LieSubalgebra (R : Type u) (L : Type v) [] [] [] extends :

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.

• carrier : Set L
• add_mem' : ∀ {a b : L}, a self.carrierb self.carriera + b self.carrier
• zero_mem' : 0 self.carrier
• smul_mem' : ∀ (c : R) {x : L}, x self.carrierc x self.carrier
• lie_mem' : ∀ {x y : L}, x self.carriery self.carrierx, y self.carrier

A Lie subalgebra is closed under Lie bracket.

Instances For
instance instZeroLieSubalgebra (R : Type u) (L : Type v) [] [] [] :
Zero ()

The zero algebra is a subalgebra of any Lie algebra.

Equations
• = { zero := { toSubmodule := 0, lie_mem' := } }
instance instInhabitedLieSubalgebra (R : Type u) (L : Type v) [] [] [] :
Equations
• = { default := 0 }
Equations
• = { coe := LieSubalgebra.toSubmodule }
instance LieSubalgebra.instSetLikeLieSubalgebra (R : Type u) (L : Type v) [] [] [] :
SetLike () L
Equations
• = { coe := fun (L' : ) => L'.carrier, coe_injective' := }
instance LieSubalgebra.lieRing (R : Type u) (L : Type v) [] [] [] (L' : ) :
LieRing L'

A Lie subalgebra forms a new Lie ring.

Equations

A Lie subalgebra inherits module structures from L.

Equations
• One or more equations did not get rendered due to their size.
Equations
• =
instance LieSubalgebra.lieAlgebra (R : Type u) (L : Type v) [] [] [] (L' : ) :
LieAlgebra R L'

A Lie subalgebra forms a new Lie algebra.

Equations
@[simp]
theorem LieSubalgebra.zero_mem {R : Type u} {L : Type v} [] [] [] (L' : ) :
0 L'
theorem LieSubalgebra.add_mem {R : Type u} {L : Type v} [] [] [] (L' : ) {x : L} {y : L} :
x L'y L'x + y L'
theorem LieSubalgebra.sub_mem {R : Type u} {L : Type v} [] [] [] (L' : ) {x : L} {y : L} :
x L'y L'x - y L'
theorem LieSubalgebra.smul_mem {R : Type u} {L : Type v} [] [] [] (L' : ) (t : R) {x : L} (h : x L') :
t x L'
theorem LieSubalgebra.lie_mem {R : Type u} {L : Type v} [] [] [] (L' : ) {x : L} {y : L} (hx : x L') (hy : y L') :
x, y L'
theorem LieSubalgebra.mem_carrier {R : Type u} {L : Type v} [] [] [] (L' : ) {x : L} :
x L'.carrier x L'
@[simp]
x { toSubmodule := { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }, lie_mem' := h₄ } x S
@[simp]
theorem LieSubalgebra.mem_coe_submodule {R : Type u} {L : Type v} [] [] [] (L' : ) {x : L} :
x L'.toSubmodule x L'
theorem LieSubalgebra.mem_coe {R : Type u} {L : Type v} [] [] [] (L' : ) {x : L} :
x L' x L'
@[simp]
theorem LieSubalgebra.coe_bracket {R : Type u} {L : Type v} [] [] [] (L' : ) (x : L') (y : L') :
x, y = x, y
theorem LieSubalgebra.ext_iff {R : Type u} {L : Type v} [] [] [] (L' : ) (x : L') (y : L') :
x = y x = y
theorem LieSubalgebra.coe_zero_iff_zero {R : Type u} {L : Type v} [] [] [] (L' : ) (x : L') :
x = 0 x = 0
theorem LieSubalgebra.ext {R : Type u} {L : Type v} [] [] [] (L₁' : ) (L₂' : ) (h : ∀ (x : L), x L₁' x L₂') :
L₁' = L₂'
theorem LieSubalgebra.ext_iff' {R : Type u} {L : Type v} [] [] [] (L₁' : ) (L₂' : ) :
L₁' = L₂' ∀ (x : L), x L₁' x L₂'
@[simp]
{ toSubmodule := { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }, lie_mem' := h₄ } = S
theorem LieSubalgebra.coe_to_submodule_mk {R : Type u} {L : Type v} [] [] [] (p : ) (h : ∀ {x y : L}, x p.carriery p.carrierx, y p.carrier) :
{ toSubmodule := p, lie_mem' := h }.toSubmodule = p
theorem LieSubalgebra.coe_injective {R : Type u} {L : Type v} [] [] [] :
Function.Injective SetLike.coe
theorem LieSubalgebra.coe_set_eq {R : Type u} {L : Type v} [] [] [] (L₁' : ) (L₂' : ) :
L₁' = L₂' L₁' = L₂'
theorem LieSubalgebra.to_submodule_injective {R : Type u} {L : Type v} [] [] [] :
Function.Injective LieSubalgebra.toSubmodule
@[simp]
theorem LieSubalgebra.coe_to_submodule_eq_iff {R : Type u} {L : Type v} [] [] [] (L₁' : ) (L₂' : ) :
L₁'.toSubmodule = L₂'.toSubmodule L₁' = L₂'
theorem LieSubalgebra.coe_to_submodule {R : Type u} {L : Type v} [] [] [] (L' : ) :
L'.toSubmodule = L'
instance LieSubalgebra.lieRingModule {R : Type u} {L : Type v} [] [] [] (L' : ) {M : Type w} [] [] :
LieRingModule (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 LieSubalgebra.coe_bracket_of_module {R : Type u} {L : Type v} [] [] [] (L' : ) {M : Type w} [] [] (x : L') (m : M) :
x, m = x, m
instance LieSubalgebra.lieModule {R : Type u} {L : Type v} [] [] [] (L' : ) {M : Type w} [] [] [Module R M] [LieModule R L M] :
LieModule 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 LieModuleHom.restrictLie {R : Type u} {L : Type v} [] [] [] {M : Type w} [] [] {N : Type w₁} [] [] [Module R N] [Module R M] (f : M →ₗ⁅R,L N) (L' : ) :
M →ₗ⁅R,L' N

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

Equations
• = let __src := f; { toLinearMap := __src, map_lie' := }
Instances For
@[simp]
theorem LieModuleHom.coe_restrictLie {R : Type u} {L : Type v} [] [] [] (L' : ) {M : Type w} [] [] {N : Type w₁} [] [] [Module R N] [Module R M] (f : M →ₗ⁅R,L N) :
() = f
def LieSubalgebra.incl {R : Type u} {L : Type v} [] [] [] (L' : ) :
L' →ₗ⁅R L

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

Equations
• = let __src := Submodule.subtype L'.toSubmodule; { toLinearMap := __src, map_lie' := }
Instances For
@[simp]
theorem LieSubalgebra.coe_incl {R : Type u} {L : Type v} [] [] [] (L' : ) :
() = Subtype.val
def LieSubalgebra.incl' {R : Type u} {L : Type v} [] [] [] (L' : ) :
L' →ₗ⁅R,L' L

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

Equations
• = let __src := Submodule.subtype L'.toSubmodule; { toLinearMap := __src, map_lie' := }
Instances For
@[simp]
theorem LieSubalgebra.coe_incl' {R : Type u} {L : Type v} [] [] [] (L' : ) :
() = Subtype.val
def LieHom.range {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :

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

Equations
• = let __src := ; { toSubmodule := __src, lie_mem' := }
Instances For
@[simp]
theorem LieHom.range_coe {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
() =
@[simp]
theorem LieHom.mem_range {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (x : L₂) :
∃ (y : L), f y = x
theorem LieHom.mem_range_self {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (x : L) :
f x
def LieHom.rangeRestrict {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
L →ₗ⁅R ()

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

Equations
• = let __src := ; { toLinearMap := __src, map_lie' := }
Instances For
@[simp]
theorem LieHom.rangeRestrict_apply {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (x : L) :
x = { val := f x, property := }
theorem LieHom.surjective_rangeRestrict {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
noncomputable def LieHom.equivRangeOfInjective {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (h : ) :
L ≃ₗ⁅R ()

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

Equations
Instances For
@[simp]
theorem LieHom.equivRangeOfInjective_apply {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (h : ) (x : L) :
x = { val := f x, property := }
theorem Submodule.exists_lieSubalgebra_coe_eq_iff {R : Type u} {L : Type v} [] [] [] (p : ) :
(∃ (K : ), K.toSubmodule = p) ∀ (x y : L), x py px, y p
@[simp]
theorem LieSubalgebra.incl_range {R : Type u} {L : Type v} [] [] [] (K : ) :
def LieSubalgebra.map {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (K : ) :

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

Equations
• = let __src := Submodule.map (f) K.toSubmodule; { toSubmodule := __src, lie_mem' := }
Instances For
@[simp]
theorem LieSubalgebra.mem_map {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (K : ) (x : L₂) :
x ∃ y ∈ K, f y = x
theorem LieSubalgebra.mem_map_submodule {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (K : ) (e : L ≃ₗ⁅R L₂) (x : L₂) :
x LieSubalgebra.map e.toLieHom K x Submodule.map () K.toSubmodule
def LieSubalgebra.comap {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) (K₂ : ) :

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

Equations
• = let __src := Submodule.comap (f) K₂.toSubmodule; { toSubmodule := __src, lie_mem' := }
Instances For
instance LieSubalgebra.instPartialOrderLieSubalgebra {R : Type u} {L : Type v} [] [] [] :
Equations
• LieSubalgebra.instPartialOrderLieSubalgebra = let __src := PartialOrder.lift SetLike.coe ;
theorem LieSubalgebra.le_def {R : Type u} {L : Type v} [] [] [] (K : ) (K' : ) :
K K' K K'
@[simp]
theorem LieSubalgebra.coe_submodule_le_coe_submodule {R : Type u} {L : Type v} [] [] [] (K : ) (K' : ) :
K.toSubmodule K'.toSubmodule K K'
instance LieSubalgebra.instBotLieSubalgebra {R : Type u} {L : Type v} [] [] [] :
Bot ()
Equations
• LieSubalgebra.instBotLieSubalgebra = { bot := 0 }
@[simp]
theorem LieSubalgebra.bot_coe {R : Type u} {L : Type v} [] [] [] :
= {0}
@[simp]
theorem LieSubalgebra.bot_coe_submodule {R : Type u} {L : Type v} [] [] [] :
.toSubmodule =
@[simp]
theorem LieSubalgebra.mem_bot {R : Type u} {L : Type v} [] [] [] (x : L) :
x x = 0
instance LieSubalgebra.instTopLieSubalgebra {R : Type u} {L : Type v} [] [] [] :
Top ()
Equations
• LieSubalgebra.instTopLieSubalgebra = { top := let __src := ; { toSubmodule := __src, lie_mem' := } }
@[simp]
theorem LieSubalgebra.top_coe {R : Type u} {L : Type v} [] [] [] :
= Set.univ
@[simp]
theorem LieSubalgebra.top_coe_submodule {R : Type u} {L : Type v} [] [] [] :
.toSubmodule =
@[simp]
theorem LieSubalgebra.mem_top {R : Type u} {L : Type v} [] [] [] (x : L) :
theorem LieHom.range_eq_map {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R L₂) :
instance LieSubalgebra.instInfLieSubalgebra {R : Type u} {L : Type v} [] [] [] :
Inf ()
Equations
• LieSubalgebra.instInfLieSubalgebra = { inf := fun (K K' : ) => let __src := K.toSubmodule K'.toSubmodule; { toSubmodule := __src, lie_mem' := } }
instance LieSubalgebra.instInfSetLieSubalgebra {R : Type u} {L : Type v} [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LieSubalgebra.inf_coe {R : Type u} {L : Type v} [] [] [] (K : ) (K' : ) :
(K K') = K K'
@[simp]
theorem LieSubalgebra.sInf_coe_to_submodule {R : Type u} {L : Type v} [] [] [] (S : Set ()) :
(sInf S).toSubmodule = sInf {x : | ∃ s ∈ S, s.toSubmodule = x}
@[simp]
theorem LieSubalgebra.sInf_coe {R : Type u} {L : Type v} [] [] [] (S : Set ()) :
(sInf S) = ⋂ s ∈ S, s
theorem LieSubalgebra.sInf_glb {R : Type u} {L : Type v} [] [] [] (S : Set ()) :
IsGLB S (sInf S)
instance LieSubalgebra.completeLattice {R : Type u} {L : Type v} [] [] [] :

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 completeLatticeOfInf.

Equations
instance LieSubalgebra.instAddLieSubalgebra {R : Type u} {L : Type v} [] [] [] :
Equations
instance LieSubalgebra.instZeroLieSubalgebra {R : Type u} {L : Type v} [] [] [] :
Zero ()
Equations
• LieSubalgebra.instZeroLieSubalgebra = { zero := }
instance LieSubalgebra.addCommMonoid {R : Type u} {L : Type v} [] [] [] :
Equations
Equations
@[simp]
theorem LieSubalgebra.add_eq_sup {R : Type u} {L : Type v} [] [] [] (K : ) (K' : ) :
K + K' = K K'
@[simp]
theorem LieSubalgebra.inf_coe_to_submodule {R : Type u} {L : Type v} [] [] [] (K : ) (K' : ) :
(K K').toSubmodule = K.toSubmodule K'.toSubmodule
@[simp]
theorem LieSubalgebra.mem_inf {R : Type u} {L : Type v} [] [] [] (K : ) (K' : ) (x : L) :
x K K' x K x K'
theorem LieSubalgebra.eq_bot_iff {R : Type u} {L : Type v} [] [] [] (K : ) :
K = xK, x = 0
instance LieSubalgebra.subsingleton_of_bot {R : Type u} {L : Type v} [] [] [] :
Equations
• =
theorem LieSubalgebra.subsingleton_bot {R : Type u} {L : Type v} [] [] [] :
theorem LieSubalgebra.wellFounded_of_noetherian (R : Type u) (L : Type v) [] [] [] [] :
WellFounded fun (x x_1 : ) => x > x_1
def LieSubalgebra.inclusion {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') :
K →ₗ⁅R K'

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

Equations
• = let __src := ; { toLinearMap := __src, map_lie' := }
Instances For
@[simp]
theorem LieSubalgebra.coe_inclusion {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') (x : K) :
() = x
theorem LieSubalgebra.inclusion_apply {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') (x : K) :
= { val := x, property := }
theorem LieSubalgebra.inclusion_injective {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') :
def LieSubalgebra.ofLe {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (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
Instances For
@[simp]
theorem LieSubalgebra.mem_ofLe {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') (x : K') :
x K
theorem LieSubalgebra.ofLe_eq_comap_incl {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') :
@[simp]
theorem LieSubalgebra.coe_ofLe {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') :
.toSubmodule =
noncomputable def LieSubalgebra.equivOfLe {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') :
K ≃ₗ⁅R

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

Equations
Instances For
@[simp]
theorem LieSubalgebra.equivOfLe_apply {R : Type u} {L : Type v} [] [] [] {K : } {K' : } (h : K K') (x : K) :
= { val := , property := }
theorem LieSubalgebra.map_le_iff_le_comap {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] {f : L →ₗ⁅R L₂} {K : } {K' : } :
K' K
theorem LieSubalgebra.gc_map_comap {R : Type u} {L : Type v} [] [] [] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] {f : L →ₗ⁅R L₂} :
def LieSubalgebra.lieSpan (R : Type u) (L : Type v) [] [] [] (s : Set L) :

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

Equations
Instances For
theorem LieSubalgebra.mem_lieSpan {R : Type u} {L : Type v} [] [] [] {s : Set L} {x : L} :
x ∀ (K : ), s Kx K
theorem LieSubalgebra.subset_lieSpan {R : Type u} {L : Type v} [] [] [] {s : Set L} :
s ()
theorem LieSubalgebra.submodule_span_le_lieSpan {R : Type u} {L : Type v} [] [] [] {s : Set L} :
().toSubmodule
theorem LieSubalgebra.lieSpan_le {R : Type u} {L : Type v} [] [] [] {s : Set L} {K : } :
K s K
theorem LieSubalgebra.lieSpan_mono {R : Type u} {L : Type v} [] [] [] {s : Set L} {t : Set L} (h : s t) :
theorem LieSubalgebra.lieSpan_eq {R : Type u} {L : Type v} [] [] [] (K : ) :
= K
theorem LieSubalgebra.coe_lieSpan_submodule_eq_iff {R : Type u} {L : Type v} [] [] [] {p : } :
().toSubmodule = p ∃ (K : ), K.toSubmodule = p
def LieSubalgebra.gi (R : Type u) (L : Type v) [] [] [] :
GaloisInsertion () SetLike.coe

lieSpan forms a Galois insertion with the coercion from LieSubalgebra to Set.

Equations
• = { choice := fun (s : Set L) (x : () s) => , gc := , le_l_u := , choice_eq := }
Instances For
@[simp]
theorem LieSubalgebra.span_empty (R : Type u) (L : Type v) [] [] [] :
@[simp]
theorem LieSubalgebra.span_univ (R : Type u) (L : Type v) [] [] [] :
theorem LieSubalgebra.span_union (R : Type u) {L : Type v} [] [] [] (s : Set L) (t : Set L) :
theorem LieSubalgebra.span_iUnion (R : Type u) {L : Type v} [] [] [] {ι : Sort u_1} (s : ιSet L) :
LieSubalgebra.lieSpan R L (⋃ (i : ι), s i) = ⨆ (i : ι), LieSubalgebra.lieSpan R L (s i)
theorem LieSubalgebra.lieSpan_induction (R : Type u) {L : Type v} [] [] [] {s : Set L} {p : LProp} {x : L} (h : x ) (mem : xs, p x) (zero : p 0) (smul : ∀ (r : R) {x : L}, p xp (r x)) (add : ∀ (x y : L), p xp yp (x + y)) (lie : ∀ (x y : L), p xp yp x, y) :
p x

If a predicate p is true on some set s ⊆ L, true for 0, stable by scalar multiplication, by addition and by Lie bracket, then the predicate is true on the Lie span of s. (Since s can be empty, and the Lie span always contains 0, the assumption that p 0 holds cannot be removed.)

noncomputable def LieEquiv.ofInjective {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : ) :
L₁ ≃ₗ⁅R ()

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

Equations
• = let __src := ; { toLieHom := { toLinearMap := __src, map_lie' := }, invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LieEquiv.ofInjective_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (h : ) (x : L₁) :
(() x) = f x
def LieEquiv.ofEq {R : Type u} {L₁ : Type v} [] [LieRing L₁] [LieAlgebra R L₁] (L₁' : ) (L₁'' : ) (h : L₁' = L₁'') :
L₁' ≃ₗ⁅R L₁''

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LieEquiv.ofEq_apply {R : Type u} {L₁ : Type v} [] [LieRing L₁] [LieAlgebra R L₁] (L : ) (L' : ) (h : L = L') (x : L) :
((LieEquiv.ofEq L L' h) x) = x
def LieEquiv.lieSubalgebraMap {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁'' : ) (e : L₁ ≃ₗ⁅R L₂) :
L₁'' ≃ₗ⁅R (LieSubalgebra.map e.toLieHom L₁'')

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LieEquiv.lieSubalgebraMap_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁'' : ) (e : L₁ ≃ₗ⁅R L₂) (x : L₁'') :
(() x) = e x
def LieEquiv.ofSubalgebras {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : ) (L₂' : ) (e : L₁ ≃ₗ⁅R L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') :
L₁' ≃ₗ⁅R L₂'

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LieEquiv.ofSubalgebras_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : ) (L₂' : ) (e : L₁ ≃ₗ⁅R L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : L₁') :
((LieEquiv.ofSubalgebras L₁' L₂' e h) x) = e x
@[simp]
theorem LieEquiv.ofSubalgebras_symm_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (L₁' : ) (L₂' : ) (e : L₁ ≃ₗ⁅R L₂) (h : LieSubalgebra.map e.toLieHom L₁' = L₂') (x : L₂') :
((LieEquiv.symm (LieEquiv.ofSubalgebras L₁' L₂' e h)) x) = () x