# Documentation

Mathlib.Algebra.Lie.DirectSum

# Direct sums of Lie algebras and Lie modules #

Direct sums of Lie algebras and Lie modules carry natural algebra 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 DirectSum.instLieRingModuleDirectSumToAddCommMonoidInstAddCommGroupDirectSumToAddCommMonoid {ι : Type v} {L : Type w₁} {M : ιType w} [] [(i : ι) → AddCommGroup (M i)] [(i : ι) → LieRingModule L (M i)] :
LieRingModule L (⨁ (i : ι), M i)
@[simp]
theorem DirectSum.lie_module_bracket_apply {ι : Type v} {L : Type w₁} {M : ιType w} [] [(i : ι) → AddCommGroup (M i)] [(i : ι) → LieRingModule L (M i)] (x : L) (m : ⨁ (i : ι), M i) (i : ι) :
x, m i = x, m i
def DirectSum.lieModuleOf (R : Type u) (ι : Type v) [] (L : Type w₁) (M : ιType w) [] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [(i : ι) → LieRingModule L (M i)] [] (j : ι) :
M j →ₗ⁅R,L ⨁ (i : ι), M i

The inclusion of each component into a direct sum as a morphism of Lie modules.

Instances For
def DirectSum.lieModuleComponent (R : Type u) (ι : Type v) [] (L : Type w₁) (M : ιType w) [] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [(i : ι) → LieRingModule L (M i)] (j : ι) :
(⨁ (i : ι), M i) →ₗ⁅R,L M j

The projection map onto one component, as a morphism of Lie modules.

Instances For

The direct sum of Lie algebras carries a natural Lie algebra structure.

instance DirectSum.lieRing {ι : Type v} (L : ιType w) [(i : ι) → LieRing (L i)] :
LieRing (⨁ (i : ι), L i)
@[simp]
theorem DirectSum.bracket_apply {ι : Type v} (L : ιType w) [(i : ι) → LieRing (L i)] (x : ⨁ (i : ι), L i) (y : ⨁ (i : ι), L i) (i : ι) :
x, y i = x i, y i
instance DirectSum.lieAlgebra {R : Type u} {ι : Type v} [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] :
LieAlgebra R (⨁ (i : ι), L i)
@[simp]
theorem DirectSum.lieAlgebraOf_apply (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [] (j : ι) (a : L j) :
↑() a = ↑() a
def DirectSum.lieAlgebraOf (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [] (j : ι) :
L j →ₗ⁅R ⨁ (i : ι), L i

The inclusion of each component into the direct sum as morphism of Lie algebras.

Instances For
@[simp]
theorem DirectSum.lieAlgebraComponent_apply (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] (j : ι) (a : ⨁ (i : ι), L i) :
↑() a = ↑() a
def DirectSum.lieAlgebraComponent (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] (j : ι) :
(⨁ (i : ι), L i) →ₗ⁅R L j

The projection map onto one component, as a morphism of Lie algebras.

Instances For
theorem DirectSum.lieAlgebra_ext (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] {x : ⨁ (i : ι), L i} {y : ⨁ (i : ι), L i} (h : ∀ (i : ι), ↑() x = ↑() y) :
x = y
theorem DirectSum.lie_of_of_ne (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [] {i : ι} {j : ι} (hij : j i) (x : L i) (y : L j) :
↑() x, ↑() y = 0
theorem DirectSum.lie_of_of_eq (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [] {i : ι} {j : ι} (hij : j = i) (x : L i) (y : L j) :
↑() x, ↑() y = ↑() x, Eq.recOn hij y
@[simp]
theorem DirectSum.lie_of (R : Type u) (ι : Type v) [] (L : ιType w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [] {i : ι} {j : ι} (x : L i) (y : L j) :
↑() x, ↑() y = if hij : j = i then ↑() x, Eq.recOn hij y else 0
@[simp]
theorem DirectSum.toLieAlgebra_apply {R : Type u} {ι : Type v} [] {L : ιType w} [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [] (L' : Type w₁) [LieRing L'] [LieAlgebra R L'] (f : (i : ι) → L i →ₗ⁅R L') (hf : ∀ (i j : ι), i j∀ (x : L i) (y : L j), ↑(f i) x, ↑(f j) y = 0) (a : ⨁ (i : ι), L i) :
↑() a = ↑(DirectSum.toModule R ι L' fun i => ↑(f i)) a
def DirectSum.toLieAlgebra {R : Type u} {ι : Type v} [] {L : ιType w} [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [] (L' : Type w₁) [LieRing L'] [LieAlgebra R L'] (f : (i : ι) → L i →ₗ⁅R L') (hf : ∀ (i j : ι), i j∀ (x : L i) (y : L j), ↑(f i) x, ↑(f j) y = 0) :
(⨁ (i : ι), L i) →ₗ⁅R L'

Given a family of Lie algebras L i, together with a family of morphisms of Lie algebras f i : L i →ₗ⁅R⁆ L' into a fixed Lie algebra L', we have a natural linear map: (⨁ i, L i) →ₗ[R] L'. If in addition ⁅f i x, f j y⁆ = 0 for any x ∈ L i and y ∈ L j (i ≠ j) then this map is a morphism of Lie algebras.

Instances For
instance DirectSum.lieRingOfIdeals {R : Type u} {ι : Type v} [] {L : Type w} [] [] (I : ιLieIdeal R L) :
LieRing (⨁ (i : ι), { x // x ↑(I i) })

The fact that this instance is necessary seems to be a bug in typeclass inference. See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ Typeclass.20resolution.20under.20binders/near/245151099).

instance DirectSum.lieAlgebraOfIdeals {R : Type u} {ι : Type v} [] {L : Type w} [] [] (I : ιLieIdeal R L) :
LieAlgebra R (⨁ (i : ι), { x // x ↑(I i) })

See DirectSum.lieRingOfIdeals comment.