Descent data on objects over a base, relative to a morphism #

Let p : S' ⟶ S be a morphism in a category with pullbacks. A descent datum on an object π : X ⟶ S' over S' relative to p identifies the fibres of X over any two points of S' with the same image in S, compatibly with composition. This file records it in action form: a morphism

act : S' ×_S X ⟶ X, written (s, x) ↦ s · x,

lying over the first projection (π (s · x) = s), with π x · x = x and the cocycle condition s₁ · (s₂ · x) = s₁ · x. In other words, act is an action of the groupoid S' ×_S S' ⇉ S' on X.

Mathematically this is the classical notion of a descent datum, an isomorphism φ : pr₁^* X ≅ pr₂^* X over S' ×_S S' satisfying φ₁₃ = φ₂₃ ∘ φ₁₂: on points, φ sends x in the fibre over s₁ to s₂ · x in the fibre over s₂, and the normalisation and the cocycle condition make s₁ · inverse to s₂ · on these fibres. The action form involves only the pullbacks S' ×_S X and S' ×_S (S' ×_S X), so the cocycle condition is a single equation between two morphisms S' ×_S (S' ×_S X) ⟶ X, with no reassociation of iterated pullbacks. It is the geometric counterpart of the coaction form TauCeti.Algebra.DescentDatum of a descent datum on an algebra: for affine schemes, act is Spec of the coaction (TauCeti.Algebra.DescentDatum.specEquiv).

Mathlib's CategoryTheory.Pseudofunctor.DescentData describes descent data for a pseudofunctor to Cat, relative to a family of morphisms. The structure here is the concrete special case of the pullback pseudofunctor X ↦ Over X and a single morphism p, which Mathlib does not construct.

Main definitions #

TauCeti.DescentDatum p X: a descent datum on X : Over S' relative to p : S' ⟶ S.
TauCeti.DescentDatum.Hom: a morphism over S' intertwining the actions, with Hom.id, Hom.comp, and the inverse Hom.inv of a morphism which is an isomorphism over S'.
TauCeti.DescentDatum.transport e E: the descent datum transported from E along an isomorphism e : X ≅ Y over S', with the isomorphism transportHom e E to E.
TauCeti.DescentDatum.pullbackAlong D q: the descent datum obtained from D after an arbitrary base change q : T ⟶ S, functorial on morphisms of descent data. Its carrier and its action space are the base changes along q of X and of the action space S' ×_S X (isPullback_pullbackAlongObj, isPullback_pullbackAlongActionComparison).
TauCeti.DescentDatum.baseChange p X: the canonical descent datum on the base change X ×_S S' of an object X over S, acting by s · (x, s₀) = (x, s), with the morphism baseChangeHom p f : Hom (baseChange p X) (baseChange p Y) induced by f : X ⟶ Y over S, a pullback of f (isPullback_baseChangeHom).
TauCeti.DescentDatum.transportArrow e D: the descent datum relative to q obtained from a descent datum D relative to p along an isomorphism of arrows e : Arrow.mk p ≅ Arrow.mk q, functorial on morphisms, inverse to transport along e.symm (transportArrowSymmHom), and compatible with canonical descent data (baseChangeTransportArrowHom).
TauCeti.DescentDatum.overBaseChange f: for a morphism f : Hom D (baseChange p X₀) to a canonical descent datum, the descent datum on Z ⟶ X₀ ×_S S' relative to the base change X₀ ×_S S' ⟶ X₀ of p, with TauCeti.DescentDatum.Hom.ofOverBaseChange translating effectivity of it back to effectivity of D, compatibly with f (Hom.comp_ofOverBaseChange).

A descent datum D is effective when there are an object X over S and a morphism baseChange p X ⟶ D of descent data which is an isomorphism over S'. Effectivity is invariant under isomorphisms of arrows (TauCeti.DescentDatum.exists_baseChange_hom_isIso_of_transportArrow), so an effectivity theorem proved for a normal form of p, such as Spec of a ring map, applies to every arrow isomorphic to it.

References #

A. Grothendieck, Revêtements étales et groupe fondamental (SGA 1), Exposé VIII, §1.
The Stacks Project, Chapter Descent, Section Descent data for schemes over schemes.