Effective faithfully flat descent for algebras #

Let S be an R-algebra. A descent datum on an S-algebra B relative to R → S is recorded as an S-algebra map θ : B → S ⊗[R] B (the coaction) which is a section of the multiplication map S ⊗[R] B → B and satisfies the coassociativity condition (id ⊗ θ) ∘ θ = (id ⊗ (1 ⊗ ·)) ∘ θ in S ⊗[R] (S ⊗[R] B).

The definitions of descent data and their morphisms, and the equivalence with classical gluing data below, allow commutative semirings R and S and a possibly noncommutative semiring B. The flatness and effectivity results assume rings.

The coaction formulation is equivalent to the classical isomorphism-plus-cocycle formulation TauCeti.Algebra.IsoDescentDatum: an isomorphism of S ⊗[R] S-algebras φ : B ⊗[R] S ≅ S ⊗[R] B with φ₁₃ = φ₂₃ ∘ φ₁₂ on B ⊗[R] S ⊗[R] S. The equivalence TauCeti.Algebra.DescentDatum.equivIsoDescentDatum is given by θ b = φ (b ⊗ 1) and φ (b ⊗ t) = θ b * (1 ⊗ t). The cocycle condition corresponds to coassociativity, while the counit equation (the normalisation of φ along the diagonal) is not imposed on φ: it follows from the cocycle condition and the invertibility of φ. For commutative B, B ⊗[R] S and S ⊗[R] B are the coordinate rings of the two pullbacks of Spec B along the projections Spec (S ⊗[R] S) → Spec S, so IsoDescentDatum is the usual scheme-theoretic descent datum on an affine scheme over Spec S, and the equivalence makes the results below available for it.

Forgetting the multiplication, a descent datum is in particular a coalgebra for the comonad S ⊗[R] - on S-modules (the module form of descent, behind Mathlib's comonadicExtendScalars); the algebra structure adds the requirement that the coaction be an S-algebra map.

Since Spec is an anti-equivalence between commutative R-algebras and affine schemes over Spec R, the results below are effective descent for affine schemes along a faithfully flat morphism Spec S → Spec R of affine schemes (the scheme-theoretic statements are in TauCeti.AlgebraicGeometry.Descent.Affine):

TauCeti.Algebra.DescentDatum.baseChangeEquiv (effectivity): if S is flat over R, the descended algebra D.descended = {b | θ b = 1 ⊗ b} satisfies S ⊗[R] D.descended ≃ B, and coaction_baseChangeEquiv identifies θ with the canonical datum on S ⊗[R] D.descended.
TauCeti.Algebra.DescentDatum.toBaseChangeDescended: the inverse of baseChangeEquiv as a morphism from D to the canonical descent datum on S ⊗[R] D.descended.
TauCeti.Algebra.DescentDatum.descended_baseChange: if S is faithfully flat over R, the canonical datum on S ⊗[R] A descends to (the image of) A.
TauCeti.Algebra.DescentDatum.equivDescended (uniqueness): if S is faithfully flat over R, every R-algebra A with S ⊗[R] A ≃ B compatibly with the descent data is isomorphic to D.descended.

Morphisms of descent data (TauCeti.Algebra.DescentDatum.Hom, S-algebra maps intertwining the coactions) descend as well. Together with effectivity, this says that A ↦ baseChange R S A from R-algebras to algebras with descent data is fully faithful and essentially surjective when S is faithfully flat over R:

TauCeti.Algebra.DescentDatum.homEquiv (descent of morphisms): if S is flat over R, morphisms of descent data D → D' correspond to R-algebra maps D.descended → D'.descended, compatibly with identities and composition (Hom.descend_id, Hom.descend_comp) and with baseChangeEquiv (Hom.toAlgHom_baseChangeEquiv).
TauCeti.Algebra.DescentDatum.baseChangeHomEquiv (full faithfulness): if S is faithfully flat over R, the R-algebra maps A → A' are exactly the morphisms between the canonical descent data on S ⊗[R] A and S ⊗[R] A'.

Forming the descended algebra commutes with arbitrary base change R → R':

TauCeti.Algebra.DescentDatum.exact_lTensor_descended_val and lTensor_descended_val_injective: if S is faithfully flat over R, then M ⊗[R] D.descended → M ⊗[R] B ⇉ M ⊗[R] (S ⊗[R] B) is an equalizer for every R-module M.
TauCeti.Algebra.DescentDatum.tensorDescendedEquiv: if S is faithfully flat over R and a descent datum D' on B' relative to R' → S' is the base change of D along R → R' (that is, S' = R' ⊗[R] S and B' = R' ⊗[R] B compatibly with the coactions), then R' ⊗[R] D.descended ≃ D'.descended. This is the compatibility on overlaps needed to glue the descents over the affine opens of a non-affine base.

The faithfully flat input is the exactness of the Amitsur sequence M → S ⊗[R] M ⇉ S ⊗[R] (S ⊗[R] M) for an arbitrary R-module M (Module.FaithfullyFlat.exact_mk_one_lTensor_sub_mk_one), which generalises Mathlib's Algebra.IsEffective.of_faithfullyFlat (the case M = R, after identifying S ⊗[R] R with S).

References #

A. Grothendieck, Revêtements étales et groupe fondamental (SGA 1), Exposé VIII, Théorème 2.1 (effective descent for affine morphisms along faithfully flat quasi-compact morphisms).
The Stacks Project, Chapter Descent, Section Descent for modules (the Amitsur complex argument used here, and the isomorphism-plus-cocycle definition of a descent datum).

Effective faithfully flat descent for algebras #

References #

Morphisms of descent data #

Change of the base ring #

Comparison along a base change of descent data #

The classical form of a descent datum #