Direct sums of Lie algebras and Lie modules
Direct sums of Lie algebras and Lie modules carry natural algbebra and module structures.
Tags
lie algebra, lie module, direct sum
The direct sum of Lie modules over a fixed Lie algebra carries a natural Lie module structure.
@[instance]
def
direct_sum.lie_ring_module
{ι : Type v}
{L : Type w₁}
{M : ι → Type w}
[lie_ring L]
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), lie_ring_module L (M i)] :
lie_ring_module L (⨁ (i : ι), M i)
Equations
- direct_sum.lie_ring_module = {to_has_bracket := {bracket := λ (x : L) (m : ⨁ (i : ι), M i), dfinsupp.map_range (λ (i : ι) (m' : (λ (i : ι), M i) i), ⁅x,m'⁆) _ m}, add_lie := _, lie_add := _, leibniz_lie := _}
@[simp]
theorem
direct_sum.lie_module_bracket_apply
{ι : Type v}
{L : Type w₁}
{M : ι → Type w}
[lie_ring L]
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), lie_ring_module L (M i)]
(x : L)
(m : ⨁ (i : ι), M i)
(i : ι) :
@[instance]
def
direct_sum.lie_module
{R : Type u}
{ι : Type v}
[comm_ring R]
{L : Type w₁}
{M : ι → Type w}
[lie_ring L]
[lie_algebra R L]
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), module R (M i)]
[Π (i : ι), lie_ring_module L (M i)]
[Π (i : ι), lie_module R L (M i)] :
lie_module R L (⨁ (i : ι), M i)
Equations
- direct_sum.lie_module = {smul_lie := _, lie_smul := _}
def
direct_sum.lie_module_of
(R : Type u)
(ι : Type v)
[comm_ring R]
(L : Type w₁)
(M : ι → Type w)
[lie_ring L]
[lie_algebra R L]
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), module R (M i)]
[Π (i : ι), lie_ring_module L (M i)]
[Π (i : ι), lie_module R L (M i)]
[decidable_eq ι]
(j : ι) :
The inclusion of each component into a direct sum as a morphism of Lie modules.
Equations
- direct_sum.lie_module_of R ι L M j = {to_fun := (direct_sum.lof R ι M j).to_fun, map_add' := _, map_smul' := _, map_lie := _}
def
direct_sum.lie_module_component
(R : Type u)
(ι : Type v)
[comm_ring R]
(L : Type w₁)
(M : ι → Type w)
[lie_ring L]
[lie_algebra R L]
[Π (i : ι), add_comm_group (M i)]
[Π (i : ι), module R (M i)]
[Π (i : ι), lie_ring_module L (M i)]
[Π (i : ι), lie_module R L (M i)]
(j : ι) :
The projection map onto one component, as a morphism of Lie modules.
Equations
- direct_sum.lie_module_component R ι L M j = {to_fun := (direct_sum.component R ι M j).to_fun, map_add' := _, map_smul' := _, map_lie := _}
The direct sum of Lie algebras carries a natural Lie algebra structure.
@[instance]
def
direct_sum.lie_ring
{ι : Type v}
{L : ι → Type w}
[Π (i : ι), lie_ring (L i)] :
lie_ring (⨁ (i : ι), L i)
Equations
- direct_sum.lie_ring = {to_add_comm_group := {add := add_comm_group.add infer_instance, add_assoc := _, zero := add_comm_group.zero infer_instance, zero_add := _, add_zero := _, neg := add_comm_group.neg infer_instance, sub := add_comm_group.sub infer_instance, sub_eq_add_neg := _, add_left_neg := _, add_comm := _}, to_has_bracket := {bracket := dfinsupp.zip_with (λ (i : ι) (x y : (λ (i : ι), L i) i), ⁅x,y⁆) direct_sum.lie_ring._proof_7}, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}
@[instance]
def
direct_sum.lie_algebra
{R : Type u}
{ι : Type v}
[comm_ring R]
{L : ι → Type w}
[Π (i : ι), lie_ring (L i)]
[Π (i : ι), lie_algebra R (L i)] :
lie_algebra R (⨁ (i : ι), L i)
Equations
- direct_sum.lie_algebra = {to_semimodule := {to_distrib_mul_action := semimodule.to_distrib_mul_action infer_instance, add_smul := _, zero_smul := _}, lie_smul := _}
def
direct_sum.lie_algebra_of
(R : Type u)
(ι : Type v)
[comm_ring R]
(L : ι → Type w)
[Π (i : ι), lie_ring (L i)]
[Π (i : ι), lie_algebra R (L i)]
[decidable_eq ι]
(j : ι) :
The inclusion of each component into the direct sum as morphism of Lie algebras.
Equations
- direct_sum.lie_algebra_of R ι L j = {to_fun := (direct_sum.lof R ι L j).to_fun, map_add' := _, map_smul' := _, map_lie := _}
def
direct_sum.lie_algebra_component
(R : Type u)
(ι : Type v)
[comm_ring R]
(L : ι → Type w)
[Π (i : ι), lie_ring (L i)]
[Π (i : ι), lie_algebra R (L i)]
(j : ι) :
The projection map onto one component, as a morphism of Lie algebras.
Equations
- direct_sum.lie_algebra_component R ι L j = {to_fun := (direct_sum.component R ι L j).to_fun, map_add' := _, map_smul' := _, map_lie := _}