Effective epimorphisms in the category of schemes

We collect results about effective epimorphisms in the category of schemes.

Main results

For a surjective and flat morphism π : X ⟶ Y between affine schemes, we prove the following.

• exists_comp_eq_of_flat_of_isAffine: Any morphism f : X ⟶ S of schemes whose two pullbacks to X ×[Y] X agree descends to a morphism u : Y ⟶ S with π ≫ u = f.
• isRegularEpi_of_flat_of_surjective_of_isAffine: The map π : X ⟶ Y is a regular epimorphism in the category of schemes. This implies EffectiveEpi π by inferInstance.

For the general result that a quasi-compact, surjective and flat morphism is an effective epimorphism, see the file Mathlib.AlgebraicGeometry.Sites.Fpqc.

Reference

• https://stacks.math.columbia.edu/tag/023Q

instance AlgebraicGeometry.effectiveEpi_base_of_flat {X Y : Scheme} {f : X ⟶ Y} [Flat f] [Surjective f] [QuasiCompact f] : CategoryTheory.EffectiveEpi f.base

The underlying continuous map of a flat, surjective and quasi-compact morphism of schemes is an effective epimorphism in the category of topological spaces.

theorem AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine {X Y : Scheme} [IsAffine X] [IsAffine Y] (π : X ⟶ Y) [Surjective π] [Flat π] : CategoryTheory.IsRegularEpi π

If π : X ⟶ Y is a flat and surjective morphism between affine schemes, then π is a regular epimorphism in the category of schemes.