Base change of group-scheme isogenies

Isogenies of group schemes remain isogenies after arbitrary base change: finiteness, flatness and surjectivity of the underlying scheme morphism are each stable under base change. The group-scheme base change is the pullback functor on the over category, lifted to group objects.

Main declarations

• TauCeti.GroupScheme.IsIsogeny.baseChange: isogenies remain isogenies after arbitrary base change.

References

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

theorem TauCeti.GroupScheme.IsIsogeny.baseChange {X Y : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over X)} (s : Y ⟶ X) {f : G ⟶ H} (hf : IsIsogeny f) : IsIsogeny ((CategoryTheory.Over.pullback s).mapGrp.map f)

Arbitrary base change preserves group-scheme isogenies.