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 := _}

source

@[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 : ι) :

⇑⁅x,m⁆ i = ⁅x,⇑m i⁆

source

@[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 := _}

source

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 : ι) :

M j →ₗ⁅R,L⁆ ⨁ (i : ι), M i

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 := _}

source

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 : ι) :

(⨁ (i : ι), M i) →ₗ⁅R,L⁆ M 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.

source

@[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 := _}

source

@[simp]

theorem direct_sum.bracket_apply {ι : Type v} {L : ι → Type w} [Π (i : ι), lie_ring (L i)] (x y : ⨁ (i : ι), L i) (i : ι) :

⇑⁅x,y⁆ i = ⁅⇑x i,⇑y i⁆

source

@[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 := _}

source

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 : ι) :

L j →ₗ⁅R⁆ ⨁ (i : ι), L i

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 := _}

source

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 : ι) :

(⨁ (i : ι), L i) →ₗ⁅R⁆ L 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 := _}