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)

Equations

• ⋯ = ⋯

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 = let __src := DirectSum.lof R ι M j; { toLinearMap := __src, 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 = let __src := DirectSum.component R ι M j; { toLinearMap := __src, 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 = let __src := inferInstance; LieRing.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DirectSum.bracket_apply {ι : Type v} (L : ι → Type w) [(i : ι) → LieRing (L i)] (x : DirectSum ι fun (i : ι) => L i) (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 : L i) (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 = let __src := inferInstance; LieAlgebra.mk ⋯

@[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.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 = let __src := DirectSum.lof R ι L j; { toFun := ⇑(DirectSum.of 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

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 = let __src := DirectSum.component R ι L j; { toFun := ⇑(DirectSum.component R ι L j), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

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

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

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

• One or more equations did not get rendered due to their size.

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)