Rank transport over a fixed base #
The rank function of a finite flat morphism is invariant under isomorphisms over its base.
This packages Mathlib's Scheme.Hom.finrank_comp_left_of_isIso for objects of Over S.
TauCeti.finrank_eq_of_nonempty_iso_over requires only the existence of an isomorphism over the
base, incorporating its commuting triangle. It compares an affine group scheme with the Hopf
spectrum of its coordinate algebra, and also transports rank through isomorphisms with Cartier
duals.
For e : X ≅ Y in Over S, use TauCeti.finrank_eq_of_nonempty_iso_over ⟨e⟩ to obtain
X.hom.finrank = Y.hom.finrank when Y.hom is finite and flat.
theorem
TauCeti.finrank_eq_of_nonempty_iso_over
{S : AlgebraicGeometry.Scheme}
{X Y : CategoryTheory.Over S}
(h : Nonempty (X ≅ Y))
[AlgebraicGeometry.Flat Y.hom]
[AlgebraicGeometry.IsFinite Y.hom]
:
Isomorphic schemes over a fixed base have the same rank function when the target structural morphism is finite and flat.