The Kostant form as a Hopf algebra over the integers

The comultiplication, counit, and antipode of a rational universal enveloping algebra preserve its Kostant integral form. This file assembles those three restrictions into a genuine HopfAlgebra ℤ instance on the form. In particular, all coalgebra and antipode identities hold integrally; they are not merely identities after extending scalars to ℚ.

The proof reflects each identity into the rational universal enveloping algebra, where it is one of the standard Hopf algebra laws. For coassociativity this requires an injective map from the integral triple tensor product into the rational triple tensor product. Its injectivity follows from flatness over ℤ: the Kostant form is torsion-free because it is a subring of a rational algebra, and tensor products of flat modules are flat.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.instHopfAlgebraKostantForm: the Kostant form is a Hopf algebra over ℤ.
• TauCeti.UniversalEnvelopingAlgebra.kostantForm_comul and TauCeti.UniversalEnvelopingAlgebra.kostantForm_counit: the bundled coalgebra maps are the previously constructed integral restrictions.
• TauCeti.UniversalEnvelopingAlgebra.kostantForm_antipode: the bundled antipode is the restriction of the rational universal-enveloping antipode.

References

The Hopf order on the Kostant form is standard; see J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26, and J. C. Jantzen, Representations of Algebraic Groups, II.1. This completes the Hopf-algebra packaging of the Kostant-form prerequisite for the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of the CFSGStatement roadmap.

@[instance_reducible]

def TauCeti.UniversalEnvelopingAlgebra.kostantTensorModule {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : Module ℤ (TensorProduct ℤ ↥(kostantForm e h) ↥(kostantForm e h))

The module structure on the tensor square of the Kostant form definitionally aligned with its algebra structure; both canonical instances have the same action, but iterated tensor maps must use one consistently.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTensorModule e h = Algebra.toModule

Faithful scalar extension for three tensor factors

The bialgebra structure

@[instance_reducible]

noncomputable instance TauCeti.UniversalEnvelopingAlgebra.instBialgebraKostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : Bialgebra ℤ ↥(kostantForm e h)

The Kostant integral form is a bialgebra over ℤ. Its comultiplication and counit are the canonical restrictions of those on the rational universal enveloping algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_comul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : CoalgebraStruct.comul = (kostantFormComul e h).toLinearMap

The bialgebra comultiplication on the Kostant form is its canonical integral comultiplication.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_counit {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : CoalgebraStruct.counit = (kostantFormCounit e h).toLinearMap

The bialgebra counit on the Kostant form is its canonical integral counit.

instance TauCeti.UniversalEnvelopingAlgebra.instIsCocommKostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : Coalgebra.IsCocomm ℤ ↥(kostantForm e h)

The standard coalgebra structure on the Kostant form is cocommutative.

The antipode and Hopf algebra structure

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantFormAntipodeLinearMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : ↥(kostantForm e h) →ₗ[ℤ] ↥(kostantForm e h)

The restricted Kostant-form antipode, regarded as a ℤ-linear endomorphism rather than an equivalence with the opposite ring.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantFormAntipodeLinearMap e h = ↑((↑(TauCeti.UniversalEnvelopingAlgebra.kostantFormAntipode e h).toIntAlgEquiv).trans (MulOpposite.opLinearEquiv ℤ).symm)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormAntipodeLinearMap_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) (a : ↥(kostantForm e h)) : ↑((kostantFormAntipodeLinearMap e h) a) = (HopfAlgebraStruct.antipode ℚ) ↑a

The integral linear antipode agrees with the rational universal-enveloping antipode after including the Kostant form in its ambient algebra.

@[instance_reducible]

noncomputable instance TauCeti.UniversalEnvelopingAlgebra.instHopfAlgebraKostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : HopfAlgebra ℤ ↥(kostantForm e h)

The Kostant integral form, with its restricted standard operations, is a Hopf algebra over the integers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_antipode {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type v} {J : Type w} (e : I → L) (h : J → L) : HopfAlgebraStruct.antipode ℤ = kostantFormAntipodeLinearMap e h

The Hopf algebra antipode on the Kostant form is the restriction of the rational universal-enveloping antipode.