English
A surjective, quasi-compact, flat morphism is a quotient map on topological spaces.
Русский
Сюръективный, квази-компактный, плоский морфизм является факторизацией по топологическому отображению.
LaTeX
$$$\\text{Surjective}(f) \\land \\text{QuasiCompact}(f) \\land \\text{Flat}(f) \\Rightarrow \\text{Topology.IsQuotientMap}(f.base)$$$
Lean4
/-- A flat surjective morphism of schemes is an epimorphism in the category of schemes. -/
@[stacks 02VW]
theorem epi_of_flat_of_surjective {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [Surjective f] : Epi f :=
by
apply CategoryTheory.Functor.epi_of_epi_map (Scheme.forgetToLocallyRingedSpace)
apply CategoryTheory.Functor.epi_of_epi_map (LocallyRingedSpace.forgetToSheafedSpace)
apply SheafedSpace.epi_of_base_surjective_of_stalk_mono _ ‹Surjective f›.surj
intro x
apply ConcreteCategory.mono_of_injective
algebraize [(f.stalkMap x).hom]
have : Module.FaithfullyFlat (Y.presheaf.stalk (f.base.hom x)) (X.presheaf.stalk x) :=
@Module.FaithfullyFlat.of_flat_of_isLocalHom _ _ _ _ _ _ _ (Flat.stalkMap f x) (f.toLRSHom.prop x)
exact ‹RingHom.FaithfullyFlat _›.injective
