Documentation

TauCeti.Algebra.Lie.Pi

Products of families of Lie algebras #

A dependent product of Lie algebras carries the pointwise bracket. The coordinate projections and single-coordinate inclusions are Lie homomorphisms, and distinct factors commute. These maps allow invariant forms on finite products to be restricted to their factors. The API follows the binary-product constructions in Mathlib.Algebra.Lie.Prod.

source
@[instance_reducible]
instance LieAlgebra.Pi.instLieRing {ι : Type u_1} {L : ι → Type u_3} [(i : ι) → LieRing (L i)] :
LieRing ((i : ι) → L i)
source
@[simp]
theorem LieAlgebra.Pi.bracket_apply {ι : Type u_1} {L : ι → Type u_3} [(i : ι) → LieRing (L i)] (x y : (i : ι) → L i) (i : ι) :
⁅x, y⁆ i = ⁅x i, y i⁆
source
@[instance_reducible]
instance LieAlgebra.Pi.instLieAlgebra {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] :
LieAlgebra R ((i : ι) → L i)
source
theorem LieAlgebra.Pi.lie_single_single_of_ne {ι : Type u_1} {L : ι → Type u_3} [(i : ι) → LieRing (L i)] [DecidableEq ι] {i j : ι} (hij : i ≠ j) (x : L i) (y : L j) :
⁅Pi.single i x, Pi.single j y⁆ = 0

Single-coordinate elements from distinct factors commute.

source
def LieHom.proj {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] (i : ι) :
((i : ι) → L i) →ₗ⁅R⁆ L i

Projection from a product of Lie algebras to one factor.

Instances For
    source
    @[simp]
    theorem LieHom.proj_apply {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] (i : ι) (x : (i : ι) → L i) :
    (proj i) x = x i
    source
    def LieHom.single {ι : Type u_1} (R : Type u_2) (L : ι → Type u_3) [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (i : ι) :
    L i →ₗ⁅R⁆ (i : ι) → L i

    Inclusion of a factor into a product of Lie algebras.

    Instances For
      source
      @[simp]
      theorem LieHom.single_apply {ι : Type u_1} {R : Type u_2} {L : ι → Type u_3} [CommRing R] [(i : ι) → LieRing (L i)] [(i : ι) → LieAlgebra R (L i)] [DecidableEq ι] (i : ι) (x : L i) :
      (single R L i) x = Pi.single i x