Closed immersions between finite flat schemes of equal rank #
A closed immersion between schemes finite and flat over the same base is an isomorphism if their rank functions agree. This works over arbitrary schemes, including nonreduced bases, and does not require local finite presentation. It detects when an inclusion of finite flat closed subschemes is equality.
The algebraic input is Mathlib's
Module.bijective_of_surjective_of_rankAtStalk_eq.
theorem
AlgebraicGeometry.Scheme.Hom.isIso_iff_finrank_comp_eq
{X Y S : Scheme}
(i : X ⟶ Y)
(g : Y ⟶ S)
[IsClosedImmersion i]
[IsFinite g]
[Flat g]
[Flat (CategoryTheory.CategoryStruct.comp i g)]
:
A closed immersion between schemes finite and flat over the same base is an isomorphism exactly when their rank functions over the base agree.