Reduction of commutative Hopf algebras

Let H be a commutative Hopf algebra over a reduced commutative ring. Its nilradical is automatically stable under the counit and antipode. It is stable under comultiplication provided the tensor square of the reduced algebra is reduced: the image of a nilpotent element under comultiplication is nilpotent, hence vanishes in that tensor square. Thus reducedness of this tensor square is a sufficient hypothesis for packaging the nilradical as a Hopf ideal.

The tensor-square hypothesis ensures that reduction commutes with the product used by the comultiplication. It holds, in particular, for finite-type algebras over a perfect field by geometric reducedness. Keeping it explicit here separates the Hopf-algebra argument from that commutative-algebra input.

Main declarations

• TauCeti.HopfIdeal.reduction: the nilradical, packaged as a Hopf ideal.
• TauCeti.HopfIdeal.reduction_toIdeal: its underlying ideal is the nilradical.
• TauCeti.HopfIdeal.mem_reduction: membership is nilpotence.
• TauCeti.HopfIdeal.isReduced_quotient_reduction: the quotient is reduced.
• TauCeti.HopfIdeal.reduction_le_of_isReduced_quotient: its minimality among Hopf ideals with reduced quotient.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §11.4.
• J. S. Milne, Algebraic Groups (2017), §1.f.

noncomputable def TauCeti.HopfIdeal.reduction (R : Type u) [CommRing R] [IsReduced R] (H : Type v) [CommRing H] [HopfAlgebra R H] [IsReduced (TensorProduct R (H ⧸ nilradical H) (H ⧸ nilradical H))] : HopfIdeal R H

The nilradical of a commutative Hopf algebra, as a Hopf ideal.

Assuming the tensor square of the reduced algebra is reduced, the comultiplication descends: a nilpotent element maps to a nilpotent element of that tensor square and therefore to zero.

Equations

• TauCeti.HopfIdeal.reduction R H = TauCeti.HopfIdeal.ofIdeal (nilradical H) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.HopfIdeal.reduction_toIdeal (R : Type u) [CommRing R] [IsReduced R] (H : Type v) [CommRing H] [HopfAlgebra R H] [IsReduced (TensorProduct R (H ⧸ nilradical H) (H ⧸ nilradical H))] : (reduction R H).toIdeal = nilradical H

The underlying ideal of the reduction Hopf ideal is the nilradical.

@[simp]

theorem TauCeti.HopfIdeal.mem_reduction (R : Type u) [CommRing R] [IsReduced R] (H : Type v) [CommRing H] [HopfAlgebra R H] [IsReduced (TensorProduct R (H ⧸ nilradical H) (H ⧸ nilradical H))] {x : H} : x ∈ reduction R H ↔ IsNilpotent x

Membership in the reduction Hopf ideal is nilpotence.

instance TauCeti.HopfIdeal.isReduced_quotient_reduction (R : Type u) [CommRing R] [IsReduced R] (H : Type v) [CommRing H] [HopfAlgebra R H] [IsReduced (TensorProduct R (H ⧸ nilradical H) (H ⧸ nilradical H))] : IsReduced (H ⧸ (reduction R H).toIdeal)

The quotient by the reduction Hopf ideal is reduced.

theorem TauCeti.HopfIdeal.reduction_le_of_isReduced_quotient (R : Type u) [CommRing R] [IsReduced R] (H : Type v) [CommRing H] [HopfAlgebra R H] [IsReduced (TensorProduct R (H ⧸ nilradical H) (H ⧸ nilradical H))] (I : HopfIdeal R H) [IsReduced (H ⧸ I.toIdeal)] : reduction R H ≤ I

The reduction is contained in every Hopf ideal whose quotient is reduced.