The relative spectrum of an equalizer of quasi-coherent algebras

Let f g : A ⟶ B be morphisms of quasi-coherent commutative 𝒪ₓ-algebras on a scheme X. Over each open U of X, the sections of A on which f and g agree form a Γ(X, U)-subalgebra CommMon.equalizerSections f g U of Γ(A.X, U), stable under restriction: a presheaf of subalgebras CommMon.equalizerSubalgebraPresheaf f g. Over a basic open X.basicOpen r of an affine open U, these sections are the localization away from r of the sections over U. Hence, exactly as for the relative spectrum CommMon.relativeSpec of a quasi-coherent algebra, the affine schemes Spec of these subalgebras glue to the relative spectrum (CommMon.equalizerSubalgebraPresheaf f g).relativeSpec of the equalizer, affine over X (CommMon.SubalgebraPresheaf.relativeSpec). The inclusions of the subalgebras glue to a morphism (CommMon.equalizerSubalgebraPresheaf f g).relativeSpecπ from A.relativeSpec over X, which coequalizes CommMon.relativeSpecMap f and CommMon.relativeSpecMap g.

This is the quotient construction of faithfully flat descent: for a descent datum on a scheme affine over the cover, the candidate descended scheme is the relative spectrum of the functions on which the two pullbacks to the double overlap agree (TauCeti.DescentDatum.descended).

Main declarations

• CommMon.equalizerSubalgebraPresheaf f g: the presheaf of subalgebras U ↦ CommMon.equalizerSections f g U of the sections of A;
• CommMon.isLocalization_equalizerSections_basicOpen: over basic opens of affine opens its sections are localizations, so that it is coequifibered over the structure presheaf (CommMon.isCoequifibered_equalizerSubalgebraPresheaf);
• CommMon.relativeSpecMap_equalizerSubalgebraPresheaf_relativeSpecπ: the projection to the relative spectrum of the equalizer coequalizes CommMon.relativeSpecMap f and CommMon.relativeSpecMap g.

References

• The Stacks Project, Tag 01LL (relative spectrum via gluing).
• A. Grothendieck, Revêtements étales et groupe fondamental (SGA 1), Exposé VIII, §1.

noncomputable def CategoryTheory.CommMon.equalizerSections {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) (U : X.Opens) : Subalgebra ↑(X.presheaf.obj (Opposite.op U)) ↑(A.X.presheaf.obj (Opposite.op U))

The Γ(X, U)-subalgebra of sections of A over U on which the algebra morphisms f and g agree.

@[simp]

theorem CategoryTheory.CommMon.mem_equalizerSections {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} {f g : A ⟶ B} {U : X.Opens} {x : ↑(A.X.presheaf.obj (Opposite.op U))} : x ∈ equalizerSections f g U ↔ (sectionsAlgHom f U) x = (sectionsAlgHom g U) x

theorem CategoryTheory.CommMon.restrictSections_mem_equalizerSections {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) {U V : X.Opens} (i : V ⟶ U) {x : ↑(A.X.presheaf.obj (Opposite.op U))} (hx : x ∈ equalizerSections f g U) : (A.restrictSections i) x ∈ equalizerSections f g V

Restriction of sections preserves the sections on which f and g agree.

noncomputable def CategoryTheory.CommMon.equalizerSubalgebraPresheaf {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) : A.SubalgebraPresheaf

The presheaf of subalgebras of sections of A on which f and g agree.

@[simp]

theorem CategoryTheory.CommMon.equalizerSubalgebraPresheaf_sections {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) (U : X.Opens) : (equalizerSubalgebraPresheaf f g).sections U = equalizerSections f g U

theorem CategoryTheory.CommMon.isLocalization_equalizerSections_basicOpen {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (r : ↑(X.presheaf.obj (Opposite.op U))) : IsLocalization.Away ((algebraMap ↑(X.presheaf.obj (Opposite.op U)) ↥(equalizerSections f g U)) r) ↥(equalizerSections f g (X.basicOpen r))

Over the basic open X.basicOpen r of an affine open U, the sections of A on which f and g agree are the localization away from r of those over U. This is the counterpart of CommMon.isLocalization_basicOpen for the equalizer: localization is exact.

instance CategoryTheory.CommMon.isCoequifibered_equalizerSubalgebraPresheaf {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] : (equalizerSubalgebraPresheaf f g).IsCoequifibered

On the affine opens of X, the presheaf of sections on which f and g agree is coequifibered over the structure presheaf: its sections over basic opens are localizations.

theorem CategoryTheory.CommMon.relativeSpecMap_equalizerSubalgebraPresheaf_relativeSpecπ {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] : CategoryStruct.comp (relativeSpecMap f) (equalizerSubalgebraPresheaf f g).relativeSpecπ = CategoryStruct.comp (relativeSpecMap g) (equalizerSubalgebraPresheaf f g).relativeSpecπ

The morphism Spec_X(A) ⟶ Spec_X(equalizer of f and g) coequalizes the morphisms of relative spectra induced by f and g.

theorem CategoryTheory.CommMon.relativeSpecMap_equalizerSubalgebraPresheaf_relativeSpecπ_assoc {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f g : A ⟶ B) [SheafOfModules.IsQuasicoherent A.X] [SheafOfModules.IsQuasicoherent B.X] {Z : AlgebraicGeometry.Scheme} (h : (equalizerSubalgebraPresheaf f g).relativeSpec ⟶ Z) : CategoryStruct.comp (relativeSpecMap f) (CategoryStruct.comp (equalizerSubalgebraPresheaf f g).relativeSpecπ h) = CategoryStruct.comp (relativeSpecMap g) (CategoryStruct.comp (equalizerSubalgebraPresheaf f g).relativeSpecπ h)

The morphism Spec_X(A) ⟶ Spec_X(equalizer of f and g) coequalizes the morphisms of relative spectra induced by f and g.