Descent of morphisms along contractions

Let c : X ⟶ Y be a morphism of locally ringed spaces, for instance of schemes, which is a topological quotient map and for which 𝒪_Y → c_* 𝒪_X is an isomorphism, that is, every Γ(Y, U) ⟶ Γ(X, c⁻¹ U) is an isomorphism. A proper surjective morphism of schemes with c_* 𝒪_X = 𝒪_Y, such as the contraction of rational tails and bridges of a nodal curve, or the contraction of an exceptional curve on a surface, is of this kind: a closed surjective continuous map is a quotient map.

This file shows that such a c is a categorical quotient for maps which are constant on its fibres: a morphism h : X ⟶ Z to an arbitrary scheme Z whose underlying map is constant on the fibres of c factors uniquely through c. The construction uses nothing about schemes, so it is carried out for locally ringed spaces in TauCeti.Geometry.RingedSpace.LocallyRingedSpace (AlgebraicGeometry.LocallyRingedSpace.Hom.descOfIsQuotientMap), and the scheme versions here are deduced from it; in particular no separatedness of Z is needed. A morphism X ⟶ Z over a base S which is constant on every geometric fibre of c is constant on its set-theoretic fibres, since each geometric fibre surjects onto the corresponding fibre, so it descends to a morphism Y ⟶ Z over S.

The construction is compatible with any commutative square, in particular with base change: if c' : X' ⟶ Y' has the same two properties and u ≫ c = c' ≫ v, then the descent of u ≫ h along c' is v followed by the descent of h along c.

Main definitions

• AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap: the morphism Y ⟶ Z of schemes induced by a morphism X ⟶ Z which is constant on the fibres of c.

Main results

• AlgebraicGeometry.Scheme.Hom.comp_descOfIsQuotientMap: the descended morphism factors h.
• AlgebraicGeometry.Scheme.Hom.eq_descOfIsQuotientMap: it is the only such factorization.
• AlgebraicGeometry.Scheme.Hom.existsUnique_comp_eq_of_isQuotientMap: the universal property.
• AlgebraicGeometry.Scheme.Hom.existsUnique_comp_eq_of_universallyClosed: the universal property for a universally closed surjective c, for instance a proper surjective one.
• AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap_comp_eq: descent preserves morphisms over a base S.
• AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap_of_commSq: compatibility with commutative squares, and so with base change.

References

• The Stacks Project, Tag 0E7B (contractions of nodal curves) and Tag 0E8A (the stabilization of a family of nodal curves, where morphisms are descended along such contractions).

noncomputable def AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) : Y ⟶ Z

Descent along a contraction. Let c : X ⟶ Y be a topological quotient map for which 𝒪_Y → c_* 𝒪_X is an isomorphism. A morphism h : X ⟶ Z whose underlying map is constant on the fibres of c induces the morphism Y ⟶ Z through which it factors (AlgebraicGeometry.Scheme.Hom.comp_descOfIsQuotientMap). This is the descent of h as a morphism of locally ringed spaces (AlgebraicGeometry.LocallyRingedSpace.Hom.descOfIsQuotientMap).

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_descOfIsQuotientMap {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) : CategoryTheory.CategoryStruct.comp c (descOfIsQuotientMap c hq hc h hh) = h

The morphism descended along c factors the original morphism.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_descOfIsQuotientMap_assoc {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) {Z✝ : Scheme} (h✝ : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp c (CategoryTheory.CategoryStruct.comp (descOfIsQuotientMap c hq hc h hh) h✝) = CategoryTheory.CategoryStruct.comp h h✝

The morphism descended along c factors the original morphism.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap_apply {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) (x : ↥X) : (descOfIsQuotientMap c hq hc h hh) (c x) = h x

On points, the morphism descended along c sends c x to h x.

theorem AlgebraicGeometry.Scheme.Hom.eq_descOfIsQuotientMap {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) {g : Y ⟶ Z} (hg : CategoryTheory.CategoryStruct.comp c g = h) : g = descOfIsQuotientMap c hq hc h hh

The morphism descended along c is the only morphism through which h factors.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap_comp {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (g : Y ⟶ Z) (hh' : Function.FactorsThrough ⇑(CategoryTheory.CategoryStruct.comp c g) ⇑c) : descOfIsQuotientMap c hq hc (CategoryTheory.CategoryStruct.comp c g) hh' = g

Descending a morphism already expressed as a composite through c recovers that morphism.

theorem AlgebraicGeometry.Scheme.Hom.existsUnique_comp_eq_of_isQuotientMap {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) : ∃! g : Y ⟶ Z, CategoryTheory.CategoryStruct.comp c g = h

The universal property of a contraction. If c : X ⟶ Y is a topological quotient map for which 𝒪_Y → c_* 𝒪_X is an isomorphism, then every morphism of schemes h : X ⟶ Z whose underlying map is constant on the fibres of c factors uniquely through c.

theorem AlgebraicGeometry.Scheme.Hom.existsUnique_comp_eq_of_universallyClosed {X Y Z : Scheme} (c : X ⟶ Y) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) [UniversallyClosed c] [Surjective c] : ∃! g : Y ⟶ Z, CategoryTheory.CategoryStruct.comp c g = h

The universal property of a contraction, for a universally closed surjective morphism, such as a proper surjective one, for which 𝒪_Y → c_* 𝒪_X is an isomorphism.

theorem AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap_comp_eq {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) {S : Scheme} {p : Y ⟶ S} {q : Z ⟶ S} (e : CategoryTheory.CategoryStruct.comp h q = CategoryTheory.CategoryStruct.comp c p) : CategoryTheory.CategoryStruct.comp (descOfIsQuotientMap c hq hc h hh) q = p

Descent along c preserves morphisms over a base: if h lies over S through Z ⟶ S and c lies over S through Y ⟶ S, then so does the descended morphism.

theorem AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap_comp_eq_assoc {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) {S : Scheme} {p : Y ⟶ S} {q : Z ⟶ S} (e : CategoryTheory.CategoryStruct.comp h q = CategoryTheory.CategoryStruct.comp c p) {Z✝ : Scheme} (h✝ : S ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (descOfIsQuotientMap c hq hc h hh) (CategoryTheory.CategoryStruct.comp q h✝) = CategoryTheory.CategoryStruct.comp p h✝

Descent along c preserves morphisms over a base: if h lies over S through Z ⟶ S and c lies over S through Y ⟶ S, then so does the descended morphism.

theorem AlgebraicGeometry.Scheme.Hom.factorsThrough_comp_of_commSq {X Y Z : Scheme} (c : X ⟶ Y) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) {X' Y' : Scheme} {c' : X' ⟶ Y'} {u : X' ⟶ X} {v : Y' ⟶ Y} (sq : CategoryTheory.CommSq u c' c v) : Function.FactorsThrough ⇑(CategoryTheory.CategoryStruct.comp u h) ⇑c'

Given a commutative square u ≫ c = c' ≫ v, if h is constant on the fibres of c, then u ≫ h is constant on the fibres of c'.

theorem AlgebraicGeometry.Scheme.Hom.descOfIsQuotientMap_of_commSq {X Y Z : Scheme} (c : X ⟶ Y) (hq : Topology.IsQuotientMap ⇑c) (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (app c U)) (h : X ⟶ Z) (hh : Function.FactorsThrough ⇑h ⇑c) {X' Y' : Scheme} {c' : X' ⟶ Y'} {u : X' ⟶ X} {v : Y' ⟶ Y} (sq : CategoryTheory.CommSq u c' c v) (hq' : Topology.IsQuotientMap ⇑c') (hc' : ∀ (U : Y'.Opens), CategoryTheory.IsIso (app c' U)) : descOfIsQuotientMap c' hq' hc' (CategoryTheory.CategoryStruct.comp u h) ⋯ = CategoryTheory.CategoryStruct.comp v (descOfIsQuotientMap c hq hc h hh)

Descent commutes with base change. Given a commutative square u ≫ c = c' ≫ v in which c' is also a topological quotient map that is an isomorphism on sections, for instance the base change of c along v when these properties hold universally, the descent of u ≫ h along c' is v followed by the descent of h along c.