The relative spectrum of a quasi-coherent commutative algebra

Let X be a scheme. A commutative 𝒪ₓ-algebra is a commutative monoid object A in the symmetric monoidal category X.Modules, and it is quasi-coherent when its underlying module A.X is. This file constructs the relative spectrum Spec_X(A) ⟶ X of a quasi-coherent commutative 𝒪ₓ-algebra by gluing the affine schemes Spec Γ(A.X, U) over the affine opens U of X.

The sections Γ(A.X, U) of a commutative 𝒪ₓ-algebra form a commutative Γ(X, U)-algebra: the sections functor Scheme.Modules.sectionsFunctor U is lax braided monoidal, so it carries A to a commutative monoid in Γ(X, U)-modules. Restriction of sections is a ring homomorphism, which gives a presheaf of commutative rings A.sectionsPresheaf on X under the structure presheaf. When A is quasi-coherent, the sections over a basic open X.basicOpen f of an affine open U are the localization of the sections over U at f (CategoryTheory.CommMon.isLocalization_basicOpen). This is exactly the input of Mathlib's relative gluing on the small affine Zariski site (AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData).

Main declarations

• CategoryTheory.CommMon.sectionsAlgHom and CategoryTheory.CommMon.sectionsPresheafMap: algebra morphisms on sections and their compatibility with restriction and structure maps;
• CategoryTheory.CommMon.isLocalization_basicOpen: for quasi-coherent A, an affine open U and f ∈ Γ(X, U), Γ(A.X, X.basicOpen f) is the localization of Γ(A.X, U) away from f;
• CategoryTheory.CommMon.relativeSpec A: the relative spectrum of a quasi-coherent commutative 𝒪ₓ-algebra, with structure morphism CategoryTheory.CommMon.relativeSpecToBase A, which is affine;
• CategoryTheory.CommMon.isPullback_relativeSpecCover: over an affine open U of X, the relative spectrum is Spec Γ(A.X, U).

References

• The Stacks Project, Tag 01LL (relative spectrum via gluing).
• A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique II, §1.3.

noncomputable def CategoryTheory.CommMon.sectionsAlgHom {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f : A ⟶ B) (U : X.Opens) : ↑(A.X.presheaf.obj (Opposite.op U)) →ₐ[↑(X.presheaf.obj (Opposite.op U))] ↑(B.X.presheaf.obj (Opposite.op U))

The algebra map on sections induced by a morphism of commutative 𝒪ₓ-algebras. It sends each section to its image under the morphism and preserves the structure map from Γ(X, U).

Equations

• CategoryTheory.CommMon.sectionsAlgHom f U = AlgCat.Hom.hom (ModuleCat.MonModuleEquivalenceAlgebra.functor.map ((AlgebraicGeometry.Scheme.Modules.sectionsFunctor U).mapCommMon.map f).hom)

@[simp]

theorem CategoryTheory.CommMon.sectionsAlgHom_apply {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f : A ⟶ B) (U : X.Opens) (x : ↑(A.X.presheaf.obj (Opposite.op U))) : (sectionsAlgHom f U) x = (ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app f.hom.hom U)) x

theorem CategoryTheory.CommMon.hom_ext_of_sectionsAlgHom {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} {f g : A ⟶ B} (h : ∀ (U : X.Opens), sectionsAlgHom f U = sectionsAlgHom g U) : f = g

A morphism of commutative 𝒪ₓ-algebras is determined by the algebra maps it induces on sections.

@[simp]

theorem CategoryTheory.CommMon.sectionsAlgHom_id {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) (U : X.Opens) : sectionsAlgHom (CategoryStruct.id A) U = AlgHom.id ↑(X.presheaf.obj (Opposite.op U)) ↑(A.X.presheaf.obj (Opposite.op U))

@[simp]

theorem CategoryTheory.CommMon.sectionsAlgHom_comp {X : AlgebraicGeometry.Scheme} {A B C : CommMon X.Modules} (f : A ⟶ B) (g : B ⟶ C) (U : X.Opens) : sectionsAlgHom (CategoryStruct.comp f g) U = (sectionsAlgHom g U).comp (sectionsAlgHom f U)

noncomputable def CategoryTheory.CommMon.sectionsPresheafMap {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f : A ⟶ B) : A.sectionsPresheaf ⟶ B.sectionsPresheaf

A morphism of commutative sheaf algebras induces a morphism of their presheaves of rings.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.CommMon.sectionsPresheafMap_app {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f : A ⟶ B) (U : X.Opensᵒᵖ) : (sectionsPresheafMap f).app U = CommRingCat.ofHom (sectionsAlgHom f (Opposite.unop U)).toRingHom

@[simp]

theorem CategoryTheory.CommMon.sectionsPresheafMap_id {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) : sectionsPresheafMap (CategoryStruct.id A) = CategoryStruct.id A.sectionsPresheaf

@[simp]

theorem CategoryTheory.CommMon.sectionsPresheafMap_comp {X : AlgebraicGeometry.Scheme} {A B C : CommMon X.Modules} (f : A ⟶ B) (g : B ⟶ C) : sectionsPresheafMap (CategoryStruct.comp f g) = CategoryStruct.comp (sectionsPresheafMap f) (sectionsPresheafMap g)

@[simp]

theorem CategoryTheory.CommMon.toSectionsPresheaf_comp_sectionsPresheafMap {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f : A ⟶ B) : CategoryStruct.comp A.toSectionsPresheaf (sectionsPresheafMap f) = B.toSectionsPresheaf

Algebra morphisms commute with the structure map from the structure presheaf.

@[simp]

theorem CategoryTheory.CommMon.toSectionsPresheaf_comp_sectionsPresheafMap_assoc {X : AlgebraicGeometry.Scheme} {A B : CommMon X.Modules} (f : A ⟶ B) {Z : TopCat.Presheaf CommRingCat ↑X.toPresheafedSpace} (h : B.sectionsPresheaf ⟶ Z) : CategoryStruct.comp A.toSectionsPresheaf (CategoryStruct.comp (sectionsPresheafMap f) h) = CategoryStruct.comp B.toSectionsPresheaf h

Algebra morphisms commute with the structure map from the structure presheaf.

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

The sections of a quasi-coherent commutative 𝒪ₓ-algebra over the basic open X.basicOpen f of an affine open U are the localization of its sections over U away from f. This is the algebra counterpart of AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen.

theorem CategoryTheory.CommMon.coequifibered_toSectionsPresheaf {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : NatTrans.Coequifibered ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.whiskerLeft A.toSectionsPresheaf)

On the affine opens of X, the presheaf of sections of a quasi-coherent commutative 𝒪ₓ-algebra is coequifibered over the structure presheaf: its sections over basic opens are localizations. This is the condition under which Mathlib glues the spectra of its sections (AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData).

noncomputable def CategoryTheory.CommMon.relativeSpecGluingData {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : AlgebraicGeometry.Scheme.Cover.RelativeGluingData (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X)

The relative gluing datum of a quasi-coherent commutative 𝒪ₓ-algebra: the affine schemes Spec Γ(A.X, U) over the affine opens U of X.

Equations

• A.relativeSpecGluingData = AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData ⋯

instance CategoryTheory.CommMon.isLocallyDirected_relativeSpecGluingData {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : (A.relativeSpecGluingData.functor.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected

The gluing diagram of the relative spectrum is locally directed.

noncomputable def CategoryTheory.CommMon.relativeSpec {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : AlgebraicGeometry.Scheme

The relative spectrum Spec_X(A) of a quasi-coherent commutative 𝒪ₓ-algebra A, glued from the affine schemes Spec Γ(A.X, U) over the affine opens U of X.

Equations

• A.relativeSpec = A.relativeSpecGluingData.glued

noncomputable def CategoryTheory.CommMon.relativeSpecToBase {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : A.relativeSpec ⟶ X

The structure morphism Spec_X(A) ⟶ X of the relative spectrum.

Equations

• A.relativeSpecToBase = A.relativeSpecGluingData.toBase

noncomputable def CategoryTheory.CommMon.relativeSpecCover {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : A.relativeSpec.OpenCover

The open cover of the relative spectrum by the spectra Spec Γ(A.X, U) of the sections over the affine opens U of X.

Equations

• A.relativeSpecCover = A.relativeSpecGluingData.cover

instance CategoryTheory.CommMon.isOpenImmersion_relativeSpecCover_f {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : AlgebraicGeometry.IsOpenImmersion (A.relativeSpecCover.f U)

theorem CategoryTheory.CommMon.relativeSpecCover_X {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : A.relativeSpecCover.X U = AlgebraicGeometry.Spec ↧↑(A.X.presheaf.obj (Opposite.op ↑U))

theorem CategoryTheory.CommMon.relativeSpecCover_f_relativeSpecToBase {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : CategoryStruct.comp (A.relativeSpecCover.f U) A.relativeSpecToBase = CategoryStruct.comp (AlgebraicGeometry.Spec.map (A.toSectionsPresheaf.app (Opposite.op ↑U))) ⋯.fromSpec

Over an affine open U, the structure morphism of the relative spectrum is Spec of the structure map Γ(X, U) ⟶ Γ(A.X, U).

theorem CategoryTheory.CommMon.relativeSpecCover_f_relativeSpecToBase_assoc {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryStruct.comp (A.relativeSpecCover.f U) (CategoryStruct.comp A.relativeSpecToBase h) = CategoryStruct.comp (CategoryStruct.comp (AlgebraicGeometry.Spec.map (A.toSectionsPresheaf.app (Opposite.op ↑U))) ⋯.fromSpec) h

Over an affine open U, the structure morphism of the relative spectrum is Spec of the structure map Γ(X, U) ⟶ Γ(A.X, U).

theorem CategoryTheory.CommMon.relativeSpecToBase_preimage {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : (TopologicalSpace.Opens.map A.relativeSpecToBase.base).obj ↑U = AlgebraicGeometry.Scheme.Hom.opensRange (A.relativeSpecCover.f U)

The preimage of an affine open U under the structure morphism of the relative spectrum is the image of the chart Spec Γ(A.X, U).

theorem CategoryTheory.CommMon.isPullback_relativeSpecCover {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : IsPullback (CategoryStruct.comp (AlgebraicGeometry.Spec.map (A.toSectionsPresheaf.app (Opposite.op ↑U))) ⋯.isoSpec.inv) (A.relativeSpecCover.f U) (↑U).ι A.relativeSpecToBase

Over an affine open U of X, the relative spectrum is Spec Γ(A.X, U): the chart of the relative spectrum over U is the base change of the structure morphism along U ⟶ X.

instance CategoryTheory.CommMon.isAffineHom_relativeSpecToBase {X : AlgebraicGeometry.Scheme} (A : CommMon X.Modules) [SheafOfModules.IsQuasicoherent A.X] : AlgebraicGeometry.IsAffineHom A.relativeSpecToBase

The structure morphism of the relative spectrum is affine.