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.

source
instance DirectSum.instLieRingModuleDirectSumToAddCommMonoidInstAddCommGroupDirectSumToAddCommMonoid {ι : Type v} {L : Type w₁} {M : ι → Type w} [LieRing L] [(i : ι) → AddCommGroup (M i)] [(i : ι) → LieRingModule L (M i)] :
LieRingModule L (⨁ (i : ι), M i)
source
@[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 : ⨁ (i : ι), M i) (i : ι) :
↑⁅x, m⁆ i = ⁅x, ↑m i⁆
source
instance DirectSum.instLieModuleDirectSumToAddCommMonoidInstAddCommGroupDirectSumToAddCommMonoidInstModuleDirectSumInstAddCommMonoidDirectSumToSemiringToCommSemiringInstLieRingModuleDirectSumToAddCommMonoidInstAddCommGroupDirectSumToAddCommMonoid {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 (⨁ (i : ι), M i)
source
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⁆ ⨁ (i : ι), M i

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

Instances For
    source
    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 : ι) :
    (⨁ (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.

      source
      instance DirectSum.lieRing {ι : Type v} (L : ι → Type w) [(i : ι) → LieRing (L i)] :
      LieRing (⨁ (i : ι), L i)
      source
      @[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⁆
      source
      instance DirectSum.lieAlgebra {R : Type u} {ι : Type v} [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] :
      LieAlgebra R (⨁ (i : ι), L i)
      source
      @[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
      source
      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⁆ ⨁ (i : ι), L i

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

      Instances For
        source
        @[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 : ⨁ (i : ι), L i) :
        ↑(DirectSum.lieAlgebraComponent R ι L j) a = ↑(DirectSum.component R ι L j) a
        source
        def DirectSum.lieAlgebraComponent (R : Type u) (ι : Type v) [CommRing R] (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
          source
          theorem DirectSum.lieAlgebra_ext (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] {x : ⨁ (i : ι), L i} {y : ⨁ (i : ι), L i} (h : ∀ (i : ι), ↑(DirectSum.lieAlgebraComponent R ι L i) x = ↑(DirectSum.lieAlgebraComponent R ι L i) y) :
          x = y
          source
          theorem DirectSum.lie_of_of_ne (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] {i : ι} {j : ι} (hij : j ≠ i) (x : L i) (y : L j) :
          ⁅↑(DirectSum.of L i) x, ↑(DirectSum.of L j) y⁆ = 0
          source
          theorem DirectSum.lie_of_of_eq (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] {i : ι} {j : ι} (hij : j = i) (x : L i) (y : L j) :
          ⁅↑(DirectSum.of L i) x, ↑(DirectSum.of L j) y⁆ = ↑(DirectSum.of L i) ⁅x, Eq.recOn hij y⁆
          source
          @[simp]
          theorem DirectSum.lie_of (R : Type u) (ι : Type v) [CommRing R] (L : ι → Type w) [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] {i : ι} {j : ι} (x : L i) (y : L j) :
          ⁅↑(DirectSum.of L i) x, ↑(DirectSum.of L j) y⁆ = if hij : j = i then ↑(DirectSum.lieAlgebraOf R ι L i) ⁅x, Eq.recOn hij y⁆ else 0
          source
          @[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 : ∀ (i j : ι), i ≠ j → ∀ (x : L i) (y : L j), ⁅↑(f i) x, ↑(f j) y⁆ = 0) (a : ⨁ (i : ι), L i) :
          ↑(DirectSum.toLieAlgebra L' f hf) a = ↑(DirectSum.toModule R ι L' fun i => ↑(f i)) a
          source
          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 : ∀ (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
            source
            instance DirectSum.lieRingOfIdeals {R : Type u} {ι : Type v} [CommRing R] {L : Type w} [LieRing L] [LieAlgebra R L] (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).

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

            See DirectSum.lieRingOfIdeals comment.