Invariant functions of a descent datum

Let p : S' ⟶ S be a morphism of schemes and D a descent datum relative to p on a scheme X ⟶ S', with action D.act : S' ×_S X ⟶ X. A global function b on X is invariant under D when its pullbacks along the action and along the second projection S' ×_S X ⟶ X agree: b (s · x) = b x. The invariant functions form a subring D.invariants of Γ(X, ⊤), which contains the functions pulled back from S.

For affine schemes this is the descended algebra of the dictionary TauCeti.Algebra.DescentDatum.specEquiv between descent data on Spec B and coactions on B (TauCeti.Algebra.DescentDatum.ΓSpecIso_inv_mem_invariants_spec_iff). Hence effective descent for algebras along a flat map gives the following form of effective descent for affine schemes: if S, S' and X are affine and p is flat, then Γ(S, ⊤) ⟶ Γ(S', ⊤), Γ(S, ⊤) ⟶ D.invariants, D.invariants ⟶ Γ(X, ⊤) and Γ(S', ⊤) ⟶ Γ(X, ⊤) form a pushout square of rings (TauCeti.DescentDatum.isPushout_invariants): Γ(X, ⊤) = Γ(S', ⊤) ⊗[Γ(S, ⊤)] D.invariants. Unlike TauCeti.DescentDatum.exists_isAffine_baseChange_hom_isIso, this names the descended ring intrinsically in terms of D, so that it can be compared with the descended scheme TauCeti.DescentDatum.descended of a descent datum on an affine morphism.

Main declarations

• TauCeti.DescentDatum.invariants D: the ring of global functions on X invariant under D;
• TauCeti.DescentDatum.mem_invariants_iff_of_isIso: invariance tested on an isomorphic copy of the action space;
• TauCeti.DescentDatum.Hom.appTop_mem_invariants_iff and TauCeti.DescentDatum.mem_invariants_transportArrow_iff: invariance of D.invariants under isomorphisms of descent data and under transport along isomorphisms of arrows;
• TauCeti.Algebra.DescentDatum.ΓSpecIso_inv_mem_invariants_spec_iff: the invariant functions of the descent datum on Spec B defined by a coaction on B form the descended algebra;
• TauCeti.DescentDatum.toInvariants D: the functions on S, as invariant functions on X;
• TauCeti.DescentDatum.isPushout_invariants: effective descent for affine schemes, in terms of invariant functions.

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.

noncomputable def TauCeti.DescentDatum.invariants {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} (D : DescentDatum p X) : Subring ↑(X.left.presheaf.obj (Opposite.op ⊤))

The global functions on X invariant under a descent datum D: those whose pullbacks along the action S' ×_S X ⟶ X and along the second projection S' ×_S X ⟶ X agree.

@[simp]

theorem TauCeti.DescentDatum.mem_invariants_iff {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} {D : DescentDatum p X} {b : ↑(X.left.presheaf.obj (Opposite.op ⊤))} : b ∈ D.invariants ↔ (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop D.act)) b = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Limits.pullback.snd p (CategoryTheory.CategoryStruct.comp X.hom p)))) b

theorem TauCeti.DescentDatum.mem_invariants_iff_of_isIso {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} {D : DescentDatum p X} {b : ↑(X.left.presheaf.obj (Opposite.op ⊤))} {Z : AlgebraicGeometry.Scheme} (g : Z ⟶ CategoryTheory.Limits.pullback p (CategoryTheory.CategoryStruct.comp X.hom p)) [CategoryTheory.IsIso g] : b ∈ D.invariants ↔ (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp g D.act))) b = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.pullback.snd p (CategoryTheory.CategoryStruct.comp X.hom p))))) b

Invariance can be tested after precomposing the action and the projection with an isomorphism onto the action space S' ×_S X.

theorem TauCeti.DescentDatum.hom_comp_appTop_mem_invariants {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} (D : DescentDatum p X) (r : ↑(S.presheaf.obj (Opposite.op ⊤))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp X.hom p))) r ∈ D.invariants

A function on X pulled back from S is invariant.

noncomputable def TauCeti.DescentDatum.toInvariants {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} (D : DescentDatum p X) : ↑(S.presheaf.obj (Opposite.op ⊤)) →+* ↥D.invariants

The functions on S, as invariant functions on X.

@[simp]

theorem TauCeti.DescentDatum.coe_toInvariants {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} (D : DescentDatum p X) (r : ↑(S.presheaf.obj (Opposite.op ⊤))) : ↑(D.toInvariants r) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp X.hom p))) r

theorem TauCeti.DescentDatum.Hom.appTop_mem_invariants {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X Y : CategoryTheory.Over S'} {D : DescentDatum p X} {E : DescentDatum p Y} (f : D.Hom E) {b : ↑(Y.left.presheaf.obj (Opposite.op ⊤))} (hb : b ∈ E.invariants) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Over.Hom.left f.hom))) b ∈ D.invariants

A morphism of descent data pulls back invariant functions to invariant functions.

theorem TauCeti.DescentDatum.Hom.appTop_mem_invariants_iff {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X Y : CategoryTheory.Over S'} {D : DescentDatum p X} {E : DescentDatum p Y} (f : D.Hom E) [CategoryTheory.IsIso f.hom] {b : ↑(Y.left.presheaf.obj (Opposite.op ⊤))} : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Over.Hom.left f.hom))) b ∈ D.invariants ↔ b ∈ E.invariants

An isomorphism of descent data identifies the invariant functions.

theorem TauCeti.DescentDatum.mem_invariants_transportArrow_iff {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} {T T' : AlgebraicGeometry.Scheme} {q : T' ⟶ T} (e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk q) (D : DescentDatum p X) {b : ↑(X.left.presheaf.obj (Opposite.op ⊤))} : b ∈ (transportArrow e D).invariants ↔ b ∈ D.invariants

Transport along an isomorphism of arrows does not change the invariant functions.

theorem TauCeti.Algebra.DescentDatum.ΓSpecIso_inv_mem_invariants_spec_iff {R S B : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (E : DescentDatum R S B) {b : B} : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧B).inv) b ∈ E.spec.invariants ↔ b ∈ E.descended

The invariant functions of the descent datum E.spec on Spec B defined by a descent datum E on the algebra B are the elements of the descended algebra E.descended.

theorem TauCeti.DescentDatum.isPushout_invariants {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S} {X : CategoryTheory.Over S'} [AlgebraicGeometry.IsAffine S] [AlgebraicGeometry.IsAffine S'] [AlgebraicGeometry.Flat p] [AlgebraicGeometry.IsAffine X.left] (D : DescentDatum p X) : CategoryTheory.IsPushout (CommRingCat.ofHom D.toInvariants) (AlgebraicGeometry.Scheme.Hom.appTop p) (CommRingCat.ofHom D.invariants.subtype) (AlgebraicGeometry.Scheme.Hom.appTop X.hom)

Effective descent for affine schemes, in terms of invariant functions. Let p : S' ⟶ S be a flat morphism of affine schemes and D a descent datum relative to p on an affine scheme X over S'. Then Γ(X, ⊤) is the base change Γ(S', ⊤) ⊗[Γ(S, ⊤)] D.invariants of the ring of invariant functions: the square formed by D.toInvariants, p.appTop, the inclusion of the invariant functions and X.hom.appTop is a pushout square of rings.