Base change of isogenies in Hopf coordinates

Let f : H ⟶ K be a morphism of commutative Hopf algebras over a commutative ring k. Scalar extension along k → L gives a coordinate morphism L ⊗[k] H ⟶ L ⊗[k] K. This file proves that isogenies and central isogenies remain so after this scalar extension.

The proof keeps the coordinate and scheme models synchronized. Hopf spectrum turns f contravariantly into a morphism of affine group schemes; scheme-theoretic pullback preserves (central) isogenies, and the natural Hopf-spectrum base-change comparison identifies that pullback with the spectrum of the scalar-extended coordinate morphism.

Main declarations

• TauCeti.CommHopfAlgCat.IsIsogeny.baseChange: scalar extension preserves isogenies.
• TauCeti.CommHopfAlgCat.IsCentralIsogeny.baseChange: scalar extension preserves central isogenies.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Sections 4 and 16.
• J. S. Milne, Algebraic Groups (2017), Sections 1.f and 18.a.
• The coordinate proof structure, including its use of MorphismProperty.overPullbackMap, is adapted from TauCeti.AlgebraicGeometry.GroupScheme.CentralIsogeny.BaseChange.

This supplies scalar-extension stability for the central-isogeny interface in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. It is used when comparing simply connected and adjoint forms after passage to an algebraic closure.

theorem TauCeti.CommHopfAlgCat.IsIsogeny.baseChange {k L : Type u} [CommRing k] [CommRing L] [Algebra k L] {H K : CommHopfAlgCat k} {f : H ⟶ K} (hf : IsIsogeny f) : IsIsogeny (baseChangeMap f)

Scalar extension of a coordinate morphism preserves isogenies of affine group schemes.

theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.baseChange {k L : Type u} [CommRing k] [CommRing L] [Algebra k L] {H K : CommHopfAlgCat k} {f : H ⟶ K} (hf : IsCentralIsogeny f) : IsCentralIsogeny (baseChangeMap f)

Scalar extension of a coordinate morphism preserves central isogenies of affine group schemes.