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} [LieRing L] [(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} [LieRing L] [(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) [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
    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.

      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} [CommRing R] (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) [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 ⨁ (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) [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
        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
          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
          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
          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
          @[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
          @[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
          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
            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).

            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.