Documentation

TauCeti.Algebra.AlgebraicGroup.Isogeny.Descent

Descent of isogenies #

A coordinate morphism is an isogeny if and only if it becomes one after faithfully flat extension of the base ring. Over fields, the same holds for central isogenies. Consequently, central isogenies can be detected after passage to an algebraic closure, where character lattices can be used for groups of multiplicative type.

Finiteness and faithful flatness descend as properties of ring homomorphisms. Centrality descends because formation of the center and of the kernel Hopf ideal commutes with field extension, and faithfully flat extension reflects containment of ideals.

The descent equivalences use a common universe for the base ring, extension ring, and coordinate Hopf algebras, as required by IsIsogeny.baseChange and IsCentralIsogeny.baseChange. The center base-change identity also requires the extension ring and coordinate algebra to share a universe. On the reflection side, RingHom.CodescendsAlong quantifies its entire pushout square in one universe, as does RingHom.CodescendsAlong.of_tensorProduct_map. Algebraic closure stays in the universe of the field, so these restrictions still allow descent from an algebraic closure when the coordinate algebras lie in that universe.

References #

@[simp]

Faithfully flat scalar extension preserves and reflects isogenies.

@[simp]

Field extension preserves and reflects central isogenies, including those with non-reduced kernels.