Descent of sections and morphisms along effective epimorphisms #
Let p : S' ⟶ S be a morphism in a category with pullbacks, and let S'' = S' ×_S S', with
projections pr₁ pr₂ : S'' ⟶ S'. For an object X over S write X' = X ×_S S' and
X'' = X ×_S S''; the projections induce pr₁^*, pr₂^* : X'' ⟶ X', the base changes of the
second factor along pr₁ and pr₂ (pullback.mapSnd).
This file proves effective descent, with uniqueness, of sections and of morphisms.
- A section
s'ofY' ⟶ S'whose two pullbacks toS''agree is the base change of a unique section ofY ⟶ S, provided thatpis an effective epimorphism. A section ofY ×_S S'' ⟶ S''is determined by itsS''-point ofY, so the condition sayspr₁ ≫ s' ≫ fst = pr₂ ≫ s' ≫ fst. - A morphism
φ : X' ⟶ Y'overS'whose two pullbacks toS''agree is the base change of a unique morphismX ⟶ YoverS, provided that the base changeX' ⟶ Xofpis an effective epimorphism. A morphismX'' ⟶ Y ×_S S''overS''is determined by its composite toY, so the condition sayspr₁^* ≫ φ ≫ fst = pr₂^* ≫ φ ≫ fst.
In both cases base change is a bijection onto the sections, respectively morphisms, satisfying
the descent condition (sectionDescentEquiv, homDescentEquiv). The proof of the second case
uses that pr₁^*, pr₂^* form the kernel pair of X' ⟶ X (pullback.isKernelPair_mapSnd), so
that X' ⟶ X is their coequalizer.
Uniqueness on its own only needs base change of p to be an epimorphism, and is Mathlib's
CategoryTheory.Over.faithful_pullback.
In the language of descent data (TauCeti.DescentDatum), a morphism
baseChange p X ⟶ baseChange p Y of canonical descent data is a morphism over S' satisfying the
descent condition. So base change from objects over S to descent data relative to p is fully
faithful (DescentDatum.baseChangeHomEquiv). This is the uniqueness half of effective descent of
objects: an object X over S with an isomorphism of descent data baseChange p X ≅ D is unique
up to a unique isomorphism compatible with the descent data (DescentDatum.Hom.descendIso).
In particular, if every base change of p is an effective epimorphism, then base change along p
reflects isomorphisms (TauCeti.reflectsIsomorphisms_pullback).
For schemes, Mathlib shows that a flat surjective morphism which is quasi-compact, or locally of
finite presentation, is an effective epimorphism, and these properties are stable under base
change (Mathlib.AlgebraicGeometry.Sites.Fpqc). Instance search therefore discharges the
hypotheses here for any fpqc or fppf morphism p : S' ⟶ S of schemes, and the results are
effective fpqc (and fppf) descent of sections and morphisms of schemes.
Main definitions #
TauCeti.descendSection: the section ofY ⟶ Sdescended from a section ofY ×_S S' ⟶ S'satisfying the descent condition.TauCeti.descendHom: the morphismX ⟶ YoverSdescended from a morphismX ×_S S' ⟶ Y ×_S S'overS'satisfying the descent condition.TauCeti.sectionDescentEquiv,TauCeti.homDescentEquiv: base change as a bijection onto the sections, respectively morphisms, satisfying the descent condition.TauCeti.DescentDatum.baseChangeHomEquiv: base change as a bijection from morphisms overSto morphisms of canonical descent data.TauCeti.DescentDatum.Hom.descendIso: the isomorphism between two objects overSwhose canonical descent data are isomorphic to the same descent datum, unique byDescentDatum.Hom.eq_descendIso.TauCeti.reflectsIsomorphisms_pullback: base change alongpreflects isomorphisms.
References #
- [A. Vistoli, Notes on Grothendieck topologies, fibered categories and descent theory], Theorem 2.55 (representable functors are fpqc sheaves).
Descent of a section. Let p : S' ⟶ S be an effective epimorphism and g : Y ⟶ S. A
morphism s' : S' ⟶ Y ×_S S' whose two pullbacks to S' ×_S S' agree as S' ×_S S'-points of
Y descends to a morphism S ⟶ Y (comp_descendSection). If s' is a section of
Y ×_S S' ⟶ S', its descent is a section of g (descendSection_comp) whose base change is s'
(pullbackSection_descendSection).
Instances For
The descended section, pulled back to S', is the S'-point of Y given by s'.
The descended section, pulled back to S', is the S'-point of Y given by s'.
The descent of a section of Y ×_S S' ⟶ S' is a section of g.
The descent of a section of Y ×_S S' ⟶ S' is a section of g.
Uniqueness of descended sections. A morphism S ⟶ Y whose pullback to S' is the
S'-point of Y given by s' is the descended section.
Effectiveness of descent of sections. The base change of the descended section is s'.
Descent of sections. Base change along an effective epimorphism p : S' ⟶ S is a
bijection from the sections of g : Y ⟶ S to the sections of Y ×_S S' ⟶ S' whose two pullbacks
to S' ×_S S' agree.
Instances For
sectionDescentEquiv sends a section s of g to its base change.
The inverse of sectionDescentEquiv is descent of sections.
Descent of a morphism. A morphism φ : X ×_S S' ⟶ Y ×_S S' over S', whose two pullbacks
to S' ×_S S' agree, descends to a morphism X ⟶ Y over S, provided that the base change
X ×_S S' ⟶ X of p is an effective epimorphism. Its base change is φ
(pullback_map_descendHom).
Instances For
The descended morphism, composed with the projection X ×_S S' ⟶ X, is φ followed by
the projection Y ×_S S' ⟶ Y.
The descended morphism, composed with the projection X ×_S S' ⟶ X, is φ followed by
the projection Y ×_S S' ⟶ Y.
Uniqueness of descended morphisms. A morphism X ⟶ Y over S whose composite with the
projection X ×_S S' ⟶ X is φ followed by the projection Y ×_S S' ⟶ Y is the descended
morphism.
Effectiveness of descent of morphisms. The base change of the descended morphism is
φ.
Descent of morphisms. If the base change X ×_S S' ⟶ X of p : S' ⟶ S is an effective
epimorphism, then base change along p is a bijection from the morphisms X ⟶ Y over S to the
morphisms X ×_S S' ⟶ Y ×_S S' over S' whose two pullbacks to S' ×_S S' agree.
Instances For
homDescentEquiv sends a morphism over S to its base change.
The inverse of homDescentEquiv is descent of morphisms.
Descent of morphisms of canonical descent data. A morphism
baseChange p X ⟶ baseChange p Y of descent data descends to a morphism X ⟶ Y over S,
provided that the base change X ×_S S' ⟶ X of p is an effective epimorphism. Its base change
is φ (baseChangeHom_descend).
Instances For
The descended morphism, composed with the projection X ×_S S' ⟶ X, is φ followed by the
projection Y ×_S S' ⟶ Y.
The descended morphism, composed with the projection X ×_S S' ⟶ X, is φ followed by the
projection Y ×_S S' ⟶ Y.
Effectiveness. The base change of the descended morphism is φ.
Uniqueness. Descending the base change of a morphism u : X ⟶ Y over S recovers
u.
Full faithfulness of base change into descent data. If the base change X ×_S S' ⟶ X
of p : S' ⟶ S is an effective epimorphism, then base change along p is a bijection from the
morphisms X ⟶ Y over S to the morphisms of canonical descent data
baseChange p X ⟶ baseChange p Y.
Instances For
baseChangeHomEquiv sends a morphism over S to its base change.
The inverse of baseChangeHomEquiv is descent of morphisms of canonical descent data.
Uniqueness of effective descent. Two objects X and Y over S whose canonical
descent data are both isomorphic to the same descent datum D, through f and g, are
isomorphic over S; the isomorphism is compatible with f and g
(Hom.comp_baseChangeHom_descendIso), and it is the only such isomorphism
(Hom.eq_descendIso).
Instances For
The forward map of Hom.descendIso f g descends g⁻¹ ∘ f.
The inverse map of Hom.descendIso f g descends f⁻¹ ∘ g.
The isomorphism Hom.descendIso f g : X ≅ Y carries f to g.
Hom.descendIso f g is the only isomorphism X ≅ Y carrying f to g.
Descent of isomorphisms. If every base change of p : S' ⟶ S is an effective
epimorphism, then base change along p reflects isomorphisms: a morphism u : X ⟶ Y over S
whose base change X ×_S S' ⟶ Y ×_S S' is an isomorphism is itself an isomorphism.