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 := _, nsmul := add_comm_group.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg infer_instance, sub := add_comm_group.sub infer_instance, sub_eq_add_neg := _, gsmul := add_comm_group.gsmul infer_instance, gsmul_zero' := _, gsmul_succ' := _, gsmul_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_12}, 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_module := {to_distrib_mul_action := module.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' := _}