Flat monomorphisms of finite presentation are open immersions #
We show the titular result AlgebraicGeometry.IsOpenImmersion.of_flat_of_mono by fpqc descent.
theorem
AlgebraicGeometry.Flat.isIso_of_surjective_of_mono
{X Y : Scheme}
(f : X ⟶ Y)
[Flat f]
[QuasiCompact f]
[Surjective f]
[CategoryTheory.Mono f]
:
theorem
AlgebraicGeometry.IsOpenImmersion.of_flat_of_mono
{X Y : Scheme}
(f : X ⟶ Y)
[Flat f]
[LocallyOfFinitePresentation f]
[CategoryTheory.Mono f]
:
Flat monomorphisms that are locally of finite presentation are open immersions. In particular,
every smooth monomorphism is an open immersion.
The converse holds by inferInstance.