Finiteness of the tangent space of a finite-type affine monoid

The counit of a finite-type commutative bialgebra has finite cotangent space at the identity over any commutative base ring. Over a field it is consequently finite-dimensional and projective. This is the finiteness input for the scalar-extension description of the tangent space and the adjoint representation.

Main declarations

• TauCeti.Bialgebra.instModuleFiniteCotangentSpace: the specialization to the counit of a finite-type commutative bialgebra.

References

• J. S. Milne, Algebraic Groups (2017), §§12 and 14.
• Mathlib's Algebra.FinitePresentation.ker_fG_of_surjective supplies finite generation of the augmentation kernel in a polynomial presentation.

instance TauCeti.Bialgebra.instModuleFiniteCotangentSpace (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Bialgebra R A] [Algebra.FiniteType R A] : Module.Finite R (CotangentSpace R A)

The cotangent space at the identity of a finite-type commutative bialgebra is finite over any commutative base ring.