Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.HopfAlgebra

The Hopf algebra structure on a universal enveloping algebra #

The standard bialgebra structure on a universal enveloping algebra is a Hopf algebra. Its antipode reverses products and negates the canonical Lie generators. This file joins the independently useful bialgebra and antipode constructions: the antipode is a two-sided convolution inverse of the identity.

The Hopf instance uses Mathlib's HopfAlgebra.ofConvInverse; multiplication of coalgebra representations is handled by Mathlib's Coalgebra.Repr.mul.

Main declarations #

Roadmap #

This is a prerequisite for the Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap. The Kostant integral form must be stable under comultiplication, counit, and antipode before it can supply the integral Hopf data used in that construction; the ambient Hopf structure is what those operations restrict from.

References #

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

A universal enveloping algebra with its standard bialgebra structure is a Hopf algebra.

The antipode is TauCeti.UniversalEnvelopingAlgebra.antipode, the linear endomorphism underlying the anti-automorphism antipodeEquiv: it reverses products and negates every canonical Lie generator.

Equations
source
theorem TauCeti.UniversalEnvelopingAlgebra.hopfAlgebraStructAntipode_eq_antipode (R : Type u) [CommRing R] (L : Type v) [LieRing L] [LieAlgebra R L] :
HopfAlgebraStruct.antipode R = antipode R

The antipode supplied by the Hopf algebra instance is the canonical universal-enveloping antipode constructed independently of the bialgebra structure.