Effective faithfully flat descent for affine schemes

Let R → S be a map of commutative rings and p = Spec.map (algebraMap R S) : Spec S ⟶ Spec R. This file identifies descent data, in the sense of TauCeti.DescentDatum p, on an affine scheme Spec B ⟶ Spec S with descent data on the S-algebra B relative to R → S in the sense of TauCeti.Algebra.DescentDatum R S B: the action Spec S ×_{Spec R} Spec B ⟶ Spec B is Spec of the coaction B → S ⊗[R] B. Through this dictionary, effective descent for algebras gives effective descent for affine schemes.

Main declarations

• TauCeti.Algebra.DescentDatum.spec: the descent datum on Spec B with action Spec (S ⊗[R] B) ⟶ Spec B given by Spec of the coaction.
• TauCeti.Algebra.DescentDatum.specEquiv: every descent datum on Spec B relative to p arises in this way from a unique descent datum on B.
• TauCeti.Algebra.DescentDatum.Hom.spec: a morphism of descent data on algebras gives a morphism, in the opposite direction, of the descent data on their spectra; it preserves identities and reverses composition (Hom.id_spec, Hom.comp_spec).
• TauCeti.Algebra.DescentDatum.specBaseChangeHom: for an R-algebra A, the canonical descent datum on Spec A ×_{Spec R} Spec S is isomorphic to the descent datum on Spec (S ⊗[R] A) given by Spec of the canonical coaction.
• TauCeti.Algebra.DescentDatum.specDescendedHom: if S is flat over R (for instance if p is faithfully flat), every descent datum on Spec B relative to p is isomorphic to the canonical descent datum on the base change of the affine scheme Spec D.descended over Spec R.
• TauCeti.DescentDatum.exists_isAffine_baseChange_hom_isIso: effective descent for affine schemes. For a flat morphism p : S' ⟶ S of affine schemes, every descent datum on an affine scheme over S' relative to p is isomorphic to the canonical descent datum on the base change of an affine scheme over S.
• TauCeti.DescentDatum.exists_isAffine_baseChange_hom_isIso_pullbackAlong: for an affine flat morphism p : S' ⟶ S over an arbitrary base and a descent datum on an affine morphism X ⟶ S', the base change of the datum to any affine scheme over S, for instance an affine open of S, is effective. This is the local input for effectivity over a non-affine base.
• TauCeti.effectiveEpi_pullback_fst_specAlgebraMap: if S is faithfully flat over R, every base change of Spec S ⟶ Spec R is an effective epimorphism. Hence descent of morphisms applies to Spec S ⟶ Spec R, and in particular the uniqueness half of effective descent: base change is fully faithful into descent data (TauCeti.DescentDatum.baseChangeHomEquiv), so for p = Spec S ⟶ Spec R the scheme X₀ over Spec R produced by exists_isAffine_baseChange_hom_isIso is unique up to a unique isomorphism compatible with the descent data (TauCeti.DescentDatum.Hom.descendIso, TauCeti.DescentDatum.Hom.eq_descendIso).

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.

theorem TauCeti.Algebra.DescentDatum.isPullback_spec_tensorProduct (R S B : Type u) [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] : CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)) (AlgebraicGeometry.Spec.algebraMap R S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap S B)).hom (AlgebraicGeometry.Spec.algebraMap R S))

Spec (S ⊗[R] B) is the fibre product of Spec S ⟶ Spec R and Spec B ⟶ Spec S ⟶ Spec R.

noncomputable def TauCeti.Algebra.DescentDatum.spec {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (D : DescentDatum R S B) : TauCeti.DescentDatum (AlgebraicGeometry.Spec.algebraMap R S) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap S B))

The descent datum on Spec B ⟶ Spec S relative to Spec S ⟶ Spec R defined by a descent datum D on B: the action Spec S ×_{Spec R} Spec B = Spec (S ⊗[R] B) ⟶ Spec B is Spec of the coaction of D.

@[simp]

theorem TauCeti.Algebra.DescentDatum.lift_spec_act {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (D : DescentDatum R S B) (h : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) (AlgebraicGeometry.Spec.algebraMap R S) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.algebraMap S B) (AlgebraicGeometry.Spec.algebraMap R S))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h) D.spec.act = AlgebraicGeometry.Spec.map (CommRingCat.ofHom D.coaction.toRingHom)

The action of D.spec is Spec of the coaction of D, through the canonical map Spec (S ⊗[R] B) ⟶ Spec S ×_{Spec R} Spec B.

@[simp]

theorem TauCeti.Algebra.DescentDatum.lift_spec_act_assoc {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (D : DescentDatum R S B) (h : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) (AlgebraicGeometry.Spec.algebraMap R S) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.algebraMap S B) (AlgebraicGeometry.Spec.algebraMap R S))) {Z : AlgebraicGeometry.Scheme} (h✝ : (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap S B)).left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h) (CategoryTheory.CategoryStruct.comp D.spec.act h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom D.coaction.toRingHom)) h✝

The action of D.spec is Spec of the coaction of D, through the canonical map Spec (S ⊗[R] B) ⟶ Spec S ×_{Spec R} Spec B.

noncomputable def TauCeti.Algebra.DescentDatum.specEquiv (R S B : Type u) [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] : DescentDatum R S B ≃ TauCeti.DescentDatum (AlgebraicGeometry.Spec.algebraMap R S) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap S B))

Descent data on Spec B ⟶ Spec S relative to Spec S ⟶ Spec R are the same as descent data on the S-algebra B relative to R → S: the action is Spec of the coaction.

@[simp]

theorem TauCeti.Algebra.DescentDatum.specEquiv_apply {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (D : DescentDatum R S B) : (specEquiv R S B) D = D.spec

@[simp]

theorem TauCeti.Algebra.DescentDatum.spec_specEquiv_symm {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (D : TauCeti.DescentDatum (AlgebraicGeometry.Spec.algebraMap R S) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap S B))) : ((specEquiv R S B).symm D).spec = D

noncomputable def TauCeti.Algebra.DescentDatum.Hom.spec {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {B' : Type u} [CommRing B'] [Algebra R B'] [Algebra S B'] [IsScalarTower R S B'] {D : DescentDatum R S B} {D' : DescentDatum R S B'} (f : D.Hom D') : D'.spec.Hom D.spec

A morphism of descent data on algebras induces a morphism, in the opposite direction, of the descent data on their spectra.

@[simp]

theorem TauCeti.Algebra.DescentDatum.Hom.spec_hom_left {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {B' : Type u} [CommRing B'] [Algebra R B'] [Algebra S B'] [IsScalarTower R S B'] {D : DescentDatum R S B} {D' : DescentDatum R S B'} (f : D.Hom D') : CategoryTheory.Over.Hom.left f.spec.hom = AlgebraicGeometry.Spec.map (CommRingCat.ofHom f.toAlgHom.toRingHom)

@[simp]

theorem TauCeti.Algebra.DescentDatum.Hom.id_spec {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (D : DescentDatum R S B) : (id D).spec = TauCeti.DescentDatum.Hom.id D.spec

Hom.spec preserves identities.

@[simp]

theorem TauCeti.Algebra.DescentDatum.Hom.comp_spec {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {B' B'' : Type u} [CommRing B'] [Algebra R B'] [Algebra S B'] [IsScalarTower R S B'] [CommRing B''] [Algebra R B''] [Algebra S B''] [IsScalarTower R S B''] {D : DescentDatum R S B} {D' : DescentDatum R S B'} {D'' : DescentDatum R S B''} (g : D'.Hom D'') (f : D.Hom D') : (g.comp f).spec = f.spec.comp g.spec

Hom.spec reverses composition.

noncomputable def TauCeti.Algebra.DescentDatum.specBaseChangeHom {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (A : Type u) [CommRing A] [Algebra R A] : (TauCeti.DescentDatum.baseChange (AlgebraicGeometry.Spec.algebraMap R S) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap R A))).Hom (baseChange R S A).spec

The canonical descent datum on the base change Spec A ×_{Spec R} Spec S of an affine scheme Spec A over Spec R is Spec of the canonical descent datum on S ⊗[R] A: the identification Spec A ×_{Spec R} Spec S ≅ Spec (S ⊗[R] A) is an isomorphism of descent data.

@[simp]

theorem TauCeti.Algebra.DescentDatum.specBaseChangeHom_hom_left {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (A : Type u) [CommRing A] [Algebra R A] : CategoryTheory.Over.Hom.left (specBaseChangeHom A).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R A))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))).hom (AlgebraicGeometry.pullbackSpecIso R S A).hom

instance TauCeti.Algebra.DescentDatum.instIsIsoOverSchemeSpecOfHomSpecBaseChangeHom {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (A : Type u) [CommRing A] [Algebra R A] : CategoryTheory.IsIso (specBaseChangeHom A).hom

noncomputable def TauCeti.Algebra.DescentDatum.specDescendedHom {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Module.Flat R S] (D : DescentDatum R S B) : (TauCeti.DescentDatum.baseChange (AlgebraicGeometry.Spec.algebraMap R S) (CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap R ↥D.descended))).Hom D.spec

Effective descent for affine schemes. If S is flat over R, the descent datum D.spec on Spec B is isomorphic (isIso_specDescendedHom_hom) to the canonical descent datum on the base change of the affine scheme Spec D.descended over Spec R.

@[simp]

theorem TauCeti.Algebra.DescentDatum.specDescendedHom_hom {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Module.Flat R S] (D : DescentDatum R S B) : D.specDescendedHom.hom = CategoryTheory.CategoryStruct.comp (specBaseChangeHom ↥D.descended).hom D.toBaseChangeDescended.spec.hom

instance TauCeti.Algebra.DescentDatum.isIso_specDescendedHom_hom {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Module.Flat R S] (D : DescentDatum R S B) : CategoryTheory.IsIso D.specDescendedHom.hom

theorem TauCeti.DescentDatum.exists_isAffine_baseChange_hom_isIso {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} [AlgebraicGeometry.IsAffine S] [AlgebraicGeometry.IsAffine S'] [AlgebraicGeometry.Flat p] {X : CategoryTheory.Over S'} [AlgebraicGeometry.IsAffine X.left] (D : DescentDatum p X) : ∃ (X₀ : CategoryTheory.Over S), AlgebraicGeometry.IsAffine X₀.left ∧ ∃ (f : (baseChange p X₀).Hom D), CategoryTheory.IsIso f.hom

Effective descent for affine schemes. Let p : S' ⟶ S be a flat morphism of affine schemes (for instance a faithfully flat one). Every descent datum on an affine scheme X ⟶ S' relative to p is effective: it is isomorphic to the canonical descent datum on the base change of an affine scheme over S.

theorem TauCeti.DescentDatum.exists_isAffine_baseChange_hom_isIso_pullbackAlong {S S' T : AlgebraicGeometry.Scheme} {p : S' ⟶ S} [AlgebraicGeometry.IsAffineHom p] [AlgebraicGeometry.Flat p] {X : CategoryTheory.Over S'} [AlgebraicGeometry.IsAffineHom X.hom] (D : DescentDatum p X) (q : T ⟶ S) [AlgebraicGeometry.IsAffine T] : ∃ (X₀ : CategoryTheory.Over T), AlgebraicGeometry.IsAffine X₀.left ∧ ∃ (f : (baseChange (CategoryTheory.Limits.pullback.fst q p) X₀).Hom (pullbackAlong q D)), CategoryTheory.IsIso f.hom

Effective descent for affine morphisms, after base change to an affine scheme. Let p : S' ⟶ S be an affine flat morphism, and D a descent datum relative to p on X ⟶ S' affine. For every morphism q : T ⟶ S from an affine scheme, for instance the inclusion of an affine open of S, the base change D.pullbackAlong q of D to T is effective.

instance TauCeti.effectiveEpi_pullback_fst_specAlgebraMap {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) : CategoryTheory.EffectiveEpi (CategoryTheory.Limits.pullback.fst f (AlgebraicGeometry.Spec.algebraMap R S))

If S is faithfully flat over R, then the base change X ×_{Spec R} Spec S ⟶ X of Spec S ⟶ Spec R along any f : X ⟶ Spec R is an effective epimorphism, being flat, surjective and quasi-compact. This is the hypothesis of descent of morphisms (TauCeti.homDescentEquiv, TauCeti.DescentDatum.baseChangeHomEquiv) along Spec S ⟶ Spec R.