Geometric reducedness under base change

Geometric reducedness of a commutative Hopf algebra is preserved by and descends along extension of the base field. In particular, H is geometrically reduced over k if and only if the scalar extension K ⊗[k] H is geometrically reduced over any field extension K / k.

Main declarations

• TauCeti.geometricallyReducedCommHopfAlgProperty.baseChange: geometric reducedness is preserved by extension of the base field.
• TauCeti.geometricallyReducedCommHopfAlgProperty.of_baseChange: geometric reducedness descends from an extension of the base field.
• TauCeti.geometricallyReducedCommHopfAlgProperty.baseChange_iff: geometric reducedness is equivalent before and after extension of the base field.

References

• J. S. Milne, Algebraic Groups (2017), for the geometric-reducedness terminology.

For preservation, reducedness is transported along the equivalence cancelling successive scalar extensions. For descent, the two scalar extensions are compared in a common overfield, then reducedness descends along the resulting injective map.

This advances Layer 2, "Smoothness and dimension tools via Lie(G)", of the ReductiveGroups roadmap.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty.baseChange {k : Type u} (K : Type (max u v)) [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} (hH : geometricallyReducedCommHopfAlgProperty k H) : geometricallyReducedCommHopfAlgProperty K (CommHopfAlgCat.baseChange H)

Geometric reducedness is preserved by extension of the base field.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty.of_baseChange {k : Type u} (K : Type (max u v)) [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) (hH : geometricallyReducedCommHopfAlgProperty K (CommHopfAlgCat.baseChange H)) : geometricallyReducedCommHopfAlgProperty k H

Geometric reducedness descends from an extension of the base field.

If K ⊗[k] H is geometrically reduced over a field extension K / k, then H is geometrically reduced over k.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty.baseChange_iff {k : Type u} (K : Type (max u v)) [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : geometricallyReducedCommHopfAlgProperty K (CommHopfAlgCat.baseChange H) ↔ geometricallyReducedCommHopfAlgProperty k H

Geometric reducedness is equivalent before and after extension of the base field.