Epimorphisms of schemes with injective stalk or section maps

A surjective morphism of schemes f : X ⟶ Y whose stalk maps 𝒪_{Y, f x} → 𝒪_{X, x} are all injective is an epimorphism in the category of schemes: two morphisms out of Y which agree after composing with f agree on points because f is surjective, and on stalks because the stalk maps of f are injective. This is the criterion behind Mathlib's AlgebraicGeometry.Flat.epi_of_flat_of_surjective, where faithful flatness of the stalk maps supplies their injectivity; here injectivity is assumed directly. It applies, for instance, to the quotient of an affine scheme by a finite group, whose stalk maps are injective but need not be flat.

The same argument works with the maps on sections Γ(Y, U) → Γ(X, f⁻¹ U) in place of the stalk maps. Their injectivity holds when 𝒪_Y → f_* 𝒪_X is an isomorphism, a condition on sections rather than on stalks, which is how contraction morphisms of curves are controlled. This version uses nothing about schemes and is deduced from its locally-ringed-space form AlgebraicGeometry.LocallyRingedSpace.epi_of_base_surjective_of_c_app_mono.

Both hypotheses survive base change along an open immersion U ⟶ Y: surjectivity is stable under base change, and the stalk maps of X ×_Y U ⟶ U are those of f, up to the stalk isomorphisms of the two open immersions X ×_Y U ⟶ X and U ⟶ Y. So such an f remains an epimorphism over every open subscheme of Y, which is what gluing arguments over an open cover of Y need: a morphism out of X which factors locally over an open cover of Y then factors through f. This gluing step follows the proof of Mathlib's AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine.

The flat criterion itself applies to the spectrum of a homomorphism of fields, which is flat and surjective, so it is an epimorphism of schemes (RingHom.epi_SpecMap_ofHom).

Main results

• AlgebraicGeometry.Scheme.Hom.epi_of_surjective_of_stalkMap_injective: a surjective morphism with injective stalk maps is an epimorphism.
• AlgebraicGeometry.Scheme.Hom.epi_of_surjective_of_app_injective: a surjective morphism which is injective on sections over every open is an epimorphism.
• AlgebraicGeometry.Scheme.Hom.stalkMap_pullback_snd_injective: the stalk maps of a base change along an open immersion are injective when those of f are.
• AlgebraicGeometry.Scheme.Hom.epi_pullback_snd_of_isOpenImmersion: the base change of such an f along an open immersion is again an epimorphism.
• AlgebraicGeometry.Scheme.Hom.exists_comp_eq_of_openCover: if every base change of π along an open immersion is an epimorphism, local factorizations through π over an open cover glue.
• RingHom.epi_SpecMap_ofHom: the spectrum of a homomorphism of fields is an epimorphism of schemes.

References

• The Stacks Project, Tag 02VW, for the flat case.

theorem AlgebraicGeometry.Scheme.Hom.epi_of_surjective_of_stalkMap_injective {X Y : Scheme} (f : X ⟶ Y) [Surjective f] (h : ∀ (x : ↥X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (stalkMap f x))) : CategoryTheory.Epi f

A surjective morphism of schemes with injective stalk maps is an epimorphism.

theorem AlgebraicGeometry.Scheme.Hom.epi_of_surjective_of_app_injective {X Y : Scheme} (f : X ⟶ Y) [Surjective f] (h : ∀ (U : Y.Opens), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (app f U))) : CategoryTheory.Epi f

A surjective morphism of schemes injective on sections is an epimorphism. If f : X ⟶ Y is surjective and every Γ(Y, U) ⟶ Γ(X, f⁻¹ U) is injective, as when 𝒪_Y ⟶ f_* 𝒪_X is an isomorphism, then two morphisms out of Y which agree after composing with f agree on points because f is surjective, and on sections because f is injective on sections.

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_pullback_snd_injective {X Y Z : Scheme} (f : X ⟶ Y) (g : Z ⟶ Y) [IsOpenImmersion g] (h : ∀ (x : ↥X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (stalkMap f x))) (z : ↥(CategoryTheory.Limits.pullback f g)) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (stalkMap (CategoryTheory.Limits.pullback.snd f g) z))

The stalk maps of the base change of f along an open immersion are injective when those of f are.

theorem AlgebraicGeometry.Scheme.Hom.epi_pullback_snd_of_isOpenImmersion {X Y Z : Scheme} (f : X ⟶ Y) [Surjective f] (g : Z ⟶ Y) [IsOpenImmersion g] (h : ∀ (x : ↥X), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (stalkMap f x))) : CategoryTheory.Epi (CategoryTheory.Limits.pullback.snd f g)

The base change of a surjective morphism with injective stalk maps along an open immersion is an epimorphism.

theorem AlgebraicGeometry.Scheme.Hom.exists_comp_eq_of_openCover {X Y Z : Scheme} (π : X ⟶ Y) (hπ : ∀ ⦃U : Scheme⦄ (g : U ⟶ Y), IsOpenImmersion g → CategoryTheory.Epi (CategoryTheory.Limits.pullback.snd π g)) (𝒰 : Y.OpenCover) (f : X ⟶ Z) (u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z) (hu : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (𝒰.f i)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (𝒰.f i)) (u i)) : ∃ (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp π h = f

Descent along a morphism which stays an epimorphism over open subschemes. Let π : X ⟶ Y be a morphism whose base change along every open immersion is an epimorphism, and let f : X ⟶ Z. If over each member U_i of an open cover of Y the base change of f factors through X ×_Y U_i ⟶ U_i, then f factors through π. The local factorizations agree on overlaps because the base change of π to an overlap is an epimorphism, so they glue.

instance RingHom.epi_SpecMap_ofHom {F L : Type u} [Field F] [Field L] (ι : F →+* L) : CategoryTheory.Epi (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ι))

The spectrum of a homomorphism of fields is an epimorphism of schemes: it is flat and surjective.