The Zariski cotangent space at the augmentation point

For a commutative bialgebra, specializing the generic augmented-algebra comparison from TauCeti.AlgebraicGeometry.TangentSpace.Affine to the counit identifies the cotangent space at the identity of the represented affine monoid with the corresponding Zariski cotangent space. With an additional Hopf-algebra structure, its k-dual is the Hopf-algebra model of Lie(G) for the represented affine group.

Main declarations

• Bialgebra.cotangentLinearEquivZariski: the augmentation cotangent space is the Zariski cotangent space at the augmentation point.
• Bialgebra.finrank_cotangentSpace_eq_finrank_zariskiCotangentSpace: equality of their dimensions over the ground field.

References

• J. S. Milne, Algebraic Groups (2017), §10.a.

noncomputable def TauCeti.Bialgebra.cotangentLinearEquivZariski (k : Type u) [Field k] (H : Type v) [CommRing H] [Bialgebra k H] : CotangentSpace k H ≃ₗ[k] AlgebraicGeometry.ZariskiCotangentSpace (AlgebraicGeometry.Spec ↧H) (augmentationPoint k H)

The augmentation cotangent space of a commutative bialgebra is canonically the Zariski cotangent space of its affine spectrum at the augmentation point.

Equations

• TauCeti.Bialgebra.cotangentLinearEquivZariski k H = (Bialgebra.counitAlgHom k H).kernelCotangentLinearEquivZariski

@[simp]

theorem TauCeti.Bialgebra.cotangentLinearEquivZariski_toCotangent (k : Type u) [Field k] (H : Type v) [CommRing H] [Bialgebra k H] (a : ↥(AugmentationIdeal k H)) : (cotangentLinearEquivZariski k H) ((AugmentationIdeal k H).toCotangent a) = (IsLocalRing.maximalIdeal ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (augmentationPoint k H))).toCotangent ⟨(algebraMap H ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (augmentationPoint k H))) ↑a, ⋯⟩

On an element of the augmentation ideal, the cotangent comparison is induced by the map from the coordinate ring to its stalk at the augmentation point.

theorem TauCeti.Bialgebra.finrank_cotangentSpace_eq_finrank_zariskiCotangentSpace (k : Type u) [Field k] (H : Type v) [CommRing H] [Bialgebra k H] : Module.finrank k (CotangentSpace k H) = Module.finrank k (AlgebraicGeometry.ZariskiCotangentSpace (AlgebraicGeometry.Spec ↧H) (augmentationPoint k H))

The augmentation cotangent space and the Zariski cotangent space at the augmentation point have the same dimension over the ground field.