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.instLieRingModule {ι : Type v} {L : Type w₁} {M : ι → Type w} [LieRing L] [(i : ι) → AddCommGroup (M i)] [(i : ι) → LieRingModule L (M i)] : LieRingModule L (DirectSum ι fun (i : ι) => M i)

Equations

• DirectSum.instLieRingModule = LieRingModule.mk ⋯ ⋯ ⋯

@[simp]

theorem DirectSum.lie_module_bracket_apply {ι : Type v} {L : Type w₁} {M : ι → Type w} [LieRing L] [(i : ι) → AddCommGroup (M i)] [(i : ι) → LieRingModule L (M i)] (x : L) (m : DirectSum ι fun (i : ι) => M i) (i : ι) : ⁅x, m⁆ i = ⁅x, m i⁆

instance DirectSum.instLieModule {R : Type u} {ι : Type v} [CommRing R] {L : Type w₁} {M : ι → Type w} [LieRing L] [LieAlgebra R L] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [(i : ι) → LieRingModule L (M i)] [∀ (i : ι), LieModule R L (M i)] : LieModule R L (DirectSum ι fun (i : ι) => M i)

def DirectSum.lieModuleOf (R : Type u) (ι : Type v) [CommRing R] (L : Type w₁) (M : ι → Type w) [LieRing L] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [(i : ι) → LieRingModule L (M i)] [DecidableEq ι] (j : ι) : M j →ₗ⁅R,L⁆ DirectSum ι fun (i : ι) => M i

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

Equations

• DirectSum.lieModuleOf R ι L M j = { toLinearMap := DirectSum.lof R ι M j, map_lie' := ⋯ }

def DirectSum.lieModuleComponent (R : Type u) (ι : Type v) [CommRing R] (L : Type w₁) (M : ι → Type w) [LieRing L] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [(i : ι) → LieRingModule L (M i)] (j : ι) : (DirectSum ι fun (i : ι) => M i) →ₗ⁅R,L⁆ M j

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

Equations

• DirectSum.lieModuleComponent R ι L M j = { toLinearMap := DirectSum.component R ι M j, map_lie' := ⋯ }

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 (DirectSum ι fun (i : ι) => L i)

Equations

• DirectSum.lieRing L = LieRing.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DirectSum.bracket_apply {ι : Type v} (L : ι → Type w) [(i : ι) → LieRing (L i)] (x y : DirectSum ι fun (i : ι) => L i) (i : ι) : ⁅x, y⁆ i = ⁅x i, y i⁆

theorem DirectSum.lie_of_same {ι : Type v} (L : ι → Type w) [(i : ι) → LieRing (L i)] [DecidableEq ι] {i : ι} (x y : L i) : ⁅(DirectSum.of L i) x, (DirectSum.of L i) y⁆ = (DirectSum.of L i) ⁅x, y⁆

theorem DirectSum.lie_of_of_ne {ι : Type v} (L : ι → Type w) [(i : ι) → LieRing (L i)] [DecidableEq ι] {i j : ι} (hij : i ≠ j) (x : L i) (y : L j) : ⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = 0

@[simp]

theorem DirectSum.lie_of {ι : Type v} (L : ι → Type w) [(i : ι) → LieRing (L i)] [DecidableEq ι] {i j : ι} (x : L i) (y : L j) : ⁅(DirectSum.of L i) x, (DirectSum.of L j) y⁆ = if hij : i = j then (DirectSum.of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

instance DirectSum.lieAlgebra {R : Type u} {ι : Type v} [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] : LieAlgebra R (DirectSum ι fun (i : ι) => L i)

Equations

• DirectSum.lieAlgebra L = LieAlgebra.mk ⋯

def DirectSum.lieAlgebraOf (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ DirectSum ι fun (i : ι) => L i

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

Equations

• DirectSum.lieAlgebraOf R ι L j = { toFun := ⇑(DirectSum.of L j), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem DirectSum.lieAlgebraOf_apply (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (j : ι) (a : L j) : (DirectSum.lieAlgebraOf R ι L j) a = (DirectSum.of L j) a

def DirectSum.lieAlgebraComponent (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] (j : ι) : (DirectSum ι fun (i : ι) => L i) →ₗ⁅R⁆ L j

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

Equations

• DirectSum.lieAlgebraComponent R ι L j = { toFun := ⇑(DirectSum.component R ι L j), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem DirectSum.lieAlgebraComponent_apply (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] (j : ι) (a : DirectSum ι fun (i : ι) => L i) : (DirectSum.lieAlgebraComponent R ι L j) a = (DirectSum.component R ι L j) a

theorem DirectSum.lieAlgebra_ext (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] {x y : DirectSum ι fun (i : ι) => L i} (h : ∀ (i : ι), (DirectSum.lieAlgebraComponent R ι L i) x = (DirectSum.lieAlgebraComponent R ι L i) y) : x = y

def DirectSum.toLieAlgebra {R : Type u} {ι : Type v} [CommRing R] {L : ι → Type w} [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (L' : Type w₁) [LieRing L'] [LieAlgebra R L'] (f : (i : ι) → L i →ₗ⁅R⁆ L') (hf : Pairwise fun (i j : ι) => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0) : (DirectSum ι fun (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.

Equations

• DirectSum.toLieAlgebra L' f hf = { toFun := ⇑(DirectSum.toModule R ι L' fun (i : ι) => ↑(f i)), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem DirectSum.toLieAlgebra_apply {R : Type u} {ι : Type v} [CommRing R] {L : ι → Type w} [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (L' : Type w₁) [LieRing L'] [LieAlgebra R L'] (f : (i : ι) → L i →ₗ⁅R⁆ L') (hf : Pairwise fun (i j : ι) => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0) (a : DirectSum ι fun (i : ι) => L i) : (DirectSum.toLieAlgebra L' f hf) a = (DirectSum.toModule R ι L' fun (i : ι) => ↑(f i)) a

instance DirectSum.lieRingOfIdeals {R : Type u} {ι : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (I : ι → LieIdeal R L) : LieRing (DirectSum ι fun (i : ι) => ↥(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).

Equations

• DirectSum.lieRingOfIdeals I = DirectSum.lieRing fun (i : ι) => ↥(I i)

instance DirectSum.lieAlgebraOfIdeals {R : Type u} {ι : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (I : ι → LieIdeal R L) : LieAlgebra R (DirectSum ι fun (i : ι) => ↥(I i))

See DirectSum.lieRingOfIdeals comment.

Equations

• DirectSum.lieAlgebraOfIdeals I = DirectSum.lieAlgebra fun (i : ι) => ↥(I i)