The descended scheme of a descent datum on an affine morphism #

Let p : S' ⟶ S be an affine morphism of schemes and D a descent datum relative to p, in the sense of TauCeti.DescentDatum p X, on a scheme X ⟶ S' affine over S'. Write π = X.hom ≫ p : X ⟶ S, an affine morphism. The datum gives two morphisms over S from S' ×_S X to X: the action (s, x) ↦ s · x and the second projection (s, x) ↦ x. On functions, these are two morphisms of quasi-coherent 𝒪_S-algebras π_* 𝒪_X ⟶ (π')_* 𝒪_{S' ×_S X}, and this file defines the descended scheme D.descended as the relative spectrum over S of their equalizer (CommMon.equalizerSubalgebraPresheaf). Over an affine open U of S it is the spectrum of the functions on π⁻¹ U which are invariant under the descent datum (CommMon.SubalgebraPresheaf.isPullback_relativeSpecCover); this is the global form of the invariant subalgebra TauCeti.Algebra.DescentDatum.descended used over an affine base.

The quotient map D.toDescended : X ⟶ D.descended lies over S and is invariant under the action (DescentDatum.act_toDescended). Consequently it induces a morphism of descent data D.toBaseChangeDescended : Hom D (baseChange p D.descended) from D to the canonical descent datum on D.descended ×_S S'. Faithfully flat descent for affine morphisms asserts that this comparison is an isomorphism when p is flat, so that D is then effective with descended scheme D.descended.

This file constructs the comparison and proves that it is an isomorphism whenever p is flat (DescentDatum.isIso_toBaseChangeDescended_hom), over an arbitrary base S. Being an isomorphism is local on S, so it suffices to work over an affine open U of S. There the descent datum restricts to the descent datum D.pullbackAlong U.ι relative to U ×_S S' ⟶ U, on X ×_{S'} (U ×_S S'), the part of X over U. Its invariant functions are the equalizer sections over U, by which the chart of D.descended over U is defined. Effective descent for affine schemes in terms of invariant functions (DescentDatum.isPushout_invariants) then shows that the part of X over U is the base change of this chart.

Main declarations #

TauCeti.DescentDatum.actAlgebraMap D and TauCeti.DescentDatum.sndAlgebraMap p X: pullback of functions along the action and along the second projection;
TauCeti.DescentDatum.descended D: the descended scheme, affine over S, identified with the relative spectrum of the equalizer by TauCeti.DescentDatum.descended_left and TauCeti.DescentDatum.descended_hom;
TauCeti.DescentDatum.toDescended D: the quotient map X ⟶ D.descended over S, with TauCeti.DescentDatum.relativeSpecFunctionsToScheme_toDescended and TauCeti.DescentDatum.act_toDescended;
TauCeti.DescentDatum.toBaseChangeDescended D: the comparison morphism of descent data from D to the canonical descent datum on the base change of D.descended;
TauCeti.DescentDatum.isIso_toBaseChangeDescended_hom: for p flat, the comparison is an isomorphism, so that D is effective with descended scheme D.descended;
TauCeti.DescentDatum.isPullback_toDescended: for p flat, X is the base change of D.descended along p, through the quotient map.

References #

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