mathlib documentation

algebra.lie.direct_sum

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
@[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
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
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

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
@[simp]
theorem direct_sum.bracket_apply {ι : Type v} {L : ι → Type w} [Π (i : ι), lie_ring (L i)] (x y : ⨁ (i : ι), L i) (i : ι) :

@[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
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
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