The quotient by the augmentation ideal

A Hopf ideal in the coordinate Hopf algebra of an affine group cuts out a closed subgroup, and the augmentation ideal cuts out the identity subgroup. This file records the corresponding identification of coordinate rings: the quotient of a finite-type commutative Hopf algebra by its augmentation ideal is the base field, which is the coordinate ring of the trivial affine group.

The identification is the first isomorphism theorem for Hopf ideals. The augmentation ideal is by definition the kernel Hopf ideal of the counit, and the counit is surjective because the unit splits it, so the kernel quotient equivalence applies verbatim.

Main declaration

• TauCeti.HopfIdeal.quotientAugmentationIso: the quotient by the augmentation ideal is the trivial finite-type Hopf algebra.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §2.1.
• J. S. Milne, Algebraic Groups (2017), around Proposition 4.1.

noncomputable def TauCeti.HopfIdeal.quotientAugmentationIso {k : Type u} [CommRing k] (H : FiniteTypeCommHopfAlgCat k) : H.quotient (augmentation k ↑H.obj) ≅ FiniteTypeCommHopfAlgCat.of k k

The quotient by the augmentation ideal is the trivial finite-type Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.HopfIdeal.mkQuotient_comp_quotientAugmentationIso_hom {k : Type u} [CommRing k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.CategoryStruct.comp (H.mkQuotient (augmentation k ↑H.obj)) (quotientAugmentationIso H).hom = FiniteTypeCommHopfAlgCat.ofHom (Bialgebra.counitBialgHom k ↑H.obj)

The quotient map followed by the quotient-augmentation isomorphism is the counit.