Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Bialgebra

The bialgebra structure on a universal enveloping algebra #

This file equips the universal enveloping algebra of a Lie algebra with its standard cocommutative bialgebra structure. Every element of the original Lie algebra is primitive: its comultiplication is x ⊗ 1 + 1 ⊗ x, and its counit is zero.

The construction is needed for the Kostant integral form in the Chevalley--Demazure construction. The integral form is generated inside a universal enveloping algebra by divided powers of root vectors and binomial coefficients in coroots; its stability under this comultiplication is what eventually makes the corresponding distribution algebra a Hopf algebra over ℤ.

Main definitions #

Main results #

References #

The construction follows J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26, and J. C. Jantzen, Representations of Algebraic Groups, II.1. It supplies a prerequisite for the Kostant ℤ-form in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

The formal development is modelled on the closest Mathlib analogue, Mathlib/RingTheory/Bialgebra/SymmetricAlgebra.lean by Robert Hawkins, which makes the generators of a symmetric algebra primitive: the declaration order (structure, generator equations, cocommutativity), the use of Bialgebra.ofAlgHom on maps produced by a universal property, and the identification of the instance projections with those maps are all adapted from that file.

source
@[instance_reducible]
instance TauCeti.UniversalEnvelopingAlgebra.instBialgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
Bialgebra R (UniversalEnvelopingAlgebra R L)

The standard cocommutative bialgebra structure on a universal enveloping algebra: the unique one for which every Lie generator is primitive.

The comultiplication and the counit are supplied inline, as the algebra homomorphisms the universal property produces from x ↦ x ⊗ 1 + 1 ⊗ x and from 0, so that Bialgebra.comulAlgHom and Bialgebra.counitAlgHom remain the names for them. How they act on Lie generators is recorded by comulAlgHom_ι and counitAlgHom_ι below.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem TauCeti.UniversalEnvelopingAlgebra.comul_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
CoalgebraStruct.comul ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) x ⊗ₜ[R] 1 + 1 ⊗ₜ[R] (UniversalEnvelopingAlgebra.ι R) x

Lie generators are primitive for the bialgebra comultiplication.

source
@[simp]
theorem TauCeti.UniversalEnvelopingAlgebra.comul_ι' (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
CoalgebraStruct.comul ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x) ⊗ₜ[R] 1 + 1 ⊗ₜ[R] (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)

The simp-normal form of comul_ι, stated for the canonical generators as simp writes them: ι R x unfolds to mkAlgHom R L (TensorAlgebra.ι R x).

source
theorem TauCeti.UniversalEnvelopingAlgebra.counit_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
CoalgebraStruct.counit ((UniversalEnvelopingAlgebra.ι R) x) = 0

The bialgebra counit vanishes on Lie generators.

source
@[simp]
theorem TauCeti.UniversalEnvelopingAlgebra.counit_ι' (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :
CoalgebraStruct.counit ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = 0

The simp-normal form of counit_ι, stated for the canonical generators as simp writes them: ι R x unfolds to mkAlgHom R L (TensorAlgebra.ι R x).

source
theorem TauCeti.UniversalEnvelopingAlgebra.comul_ι_pow (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (n : ℕ) :
CoalgebraStruct.comul ((UniversalEnvelopingAlgebra.ι R) x ^ n) = ∑ mn ∈ Finset.antidiagonal n, n.choose mn.1 • ((UniversalEnvelopingAlgebra.ι R) x ^ mn.1) ⊗ₜ[R] ((UniversalEnvelopingAlgebra.ι R) x ^ mn.2)

The comultiplication of a power of a Lie generator is its binomial expansion.

This integral-coefficient formula is the input for proving that divided powers of Chevalley root vectors are stable under comultiplication in the Kostant form. The two tensor factors commute even though the universal enveloping algebra itself need not be commutative.

source
theorem TauCeti.UniversalEnvelopingAlgebra.comul_ι_dividedPower (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.comul (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) x)) = ∑ ij ∈ Finset.antidiagonal n, Associative.dividedPower ij.1 ((UniversalEnvelopingAlgebra.ι ℚ) x) ⊗ₜ[ℚ] Associative.dividedPower ij.2 ((UniversalEnvelopingAlgebra.ι ℚ) x)

The comultiplication of a divided power of a canonical Lie generator is the antidiagonal sum of the corresponding divided powers in the two tensor factors.

source
@[simp]
theorem TauCeti.UniversalEnvelopingAlgebra.comul_ι_dividedPower' (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.comul (Associative.dividedPower n ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x))) = ∑ ij ∈ Finset.antidiagonal n, Associative.dividedPower ij.1 ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x)) ⊗ₜ[ℚ] Associative.dividedPower ij.2 ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x))

The simp-normal form of comul_ι_dividedPower, stated for canonical generators as simp writes them.

source
theorem TauCeti.UniversalEnvelopingAlgebra.counit_ι_dividedPower (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.counit (Associative.dividedPower (n + 1) ((UniversalEnvelopingAlgebra.ι ℚ) x)) = 0

Every positive divided power of a canonical Lie generator has counit zero.

source
@[simp]
theorem TauCeti.UniversalEnvelopingAlgebra.counit_ι_dividedPower' (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.counit (Associative.dividedPower (n + 1) ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x))) = 0

The simp-normal form of counit_ι_dividedPower, stated for canonical generators as simp writes them.

source
theorem TauCeti.UniversalEnvelopingAlgebra.comul_ι_choose (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.comul (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) x) n) = ∑ ij ∈ Finset.antidiagonal n, Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) x) ij.1 ⊗ₜ[ℚ] Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) x) ij.2

The comultiplication of a binomial coefficient in a canonical Lie generator is the antidiagonal sum of the corresponding binomial coefficients in the two tensor factors.

source
@[simp]
theorem TauCeti.UniversalEnvelopingAlgebra.comul_ι_choose' (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.comul (Ring.choose ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x)) n) = ∑ ij ∈ Finset.antidiagonal n, Ring.choose ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x)) ij.1 ⊗ₜ[ℚ] Ring.choose ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x)) ij.2

The simp-normal form of comul_ι_choose, stated for canonical generators as simp writes them.

source
theorem TauCeti.UniversalEnvelopingAlgebra.counit_ι_choose (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.counit (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) x) (n + 1)) = 0

Every positive binomial coefficient in a canonical Lie generator has counit zero.

source
@[simp]
theorem TauCeti.UniversalEnvelopingAlgebra.counit_ι_choose' (L : Type v) [LieRing L] [LieAlgebra ℚ L] (x : L) (n : ℕ) :
CoalgebraStruct.counit (Ring.choose ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) x)) (n + 1)) = 0

The simp-normal form of counit_ι_choose, stated for canonical generators as simp writes them.

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.mapBialgHom (R : Type u) [CommRing R] {L₁ : Type v} {L₂ : Type w} [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) :
UniversalEnvelopingAlgebra R L₁ →ₐc[R] UniversalEnvelopingAlgebra R L₂

A Lie algebra homomorphism induces a bialgebra homomorphism of universal enveloping algebras.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.mapBialgHom_toAlgHom (R : Type u) [CommRing R] {L₁ : Type v} {L₂ : Type w} [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) :
    ↑(mapBialgHom R f) = map R f

    The algebra homomorphism underlying mapBialgHom is the induced map map.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.mapBialgHom_ι (R : Type u) [CommRing R] {L₁ : Type v} {L₂ : Type w} [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) :
    (mapBialgHom R f) ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) (f x)

    The bialgebra homomorphism induced by a Lie homomorphism agrees with it on Lie generators.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.mapBialgHom_ι' (R : Type u) [CommRing R] {L₁ : Type v} {L₂ : Type w} [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) :
    (mapBialgHom R f) ((UniversalEnvelopingAlgebra.mkAlgHom R L₁) ((TensorAlgebra.ι R) x)) = (UniversalEnvelopingAlgebra.mkAlgHom R L₂) ((TensorAlgebra.ι R) (f x))

    The simp-normal form of mapBialgHom_ι, stated for the canonical generators as simp writes them: ι R x unfolds to mkAlgHom R L (TensorAlgebra.ι R x).

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.mapBialgHom_id (R : Type u) [CommRing R] {L₁ : Type v} [LieRing L₁] [LieAlgebra R L₁] :
    mapBialgHom R LieHom.id = BialgHom.id R (UniversalEnvelopingAlgebra R L₁)

    The identity Lie homomorphism induces the identity bialgebra homomorphism.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.mapBialgHom_comp (R : Type u) [CommRing R] {L₁ : Type v} {L₂ : Type w} {L₃ : Type x} [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ →ₗ⁅R⁆ L₃) :
    mapBialgHom R (g.comp f) = (mapBialgHom R g).comp (mapBialgHom R f)

    Composition of Lie homomorphisms becomes composition of the induced bialgebra homomorphisms.

    source
    instance TauCeti.UniversalEnvelopingAlgebra.instIsCocomm (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :
    Coalgebra.IsCocomm R (UniversalEnvelopingAlgebra R L)

    The standard bialgebra structure on a universal enveloping algebra is cocommutative.