The relative spectrum of a presheaf of subalgebras of sections #
Let A be a commutative 𝒪ₓ-algebra on a scheme X. A CommMon.SubalgebraPresheaf A is a
family of Γ(X, U)-subalgebras S.sections U of the sections Γ(A.X, U), stable under
restriction. Such a family is a presheaf of rings S.sectionsPresheaf on X, under the structure
presheaf and inside the sections of A. When it is coequifibered over the structure presheaf on
the affine opens (CommMon.SubalgebraPresheaf.IsCoequifibered), that is, when its sections over a
basic open of an affine open are localizations, the affine schemes Spec (S.sections U) glue, with
Mathlib's relative gluing on the small affine Zariski site, to a scheme S.relativeSpec affine over
X. For quasi-coherent A, the inclusions of the subalgebras glue to a morphism
S.relativeSpecπ : A.relativeSpec ⟶ S.relativeSpec over X, which over every affine open of X
is Spec of the inclusion.
This is the common construction behind the relative spectrum of an equalizer of quasi-coherent
algebras (CommMon.equalizerSubalgebraPresheaf) and the quotient of a scheme affine over X by a
finite group (CommMon.invariantSubalgebraPresheaf).
Main declarations #
CommMon.SubalgebraPresheaf A: families of subalgebras of the sections ofAstable under restriction, with the presheaf of ringsS.sectionsPresheaf, its structure mapS.toSectionsPresheafand its inclusionS.sectionsPresheafιinto the sections ofA;CommMon.SubalgebraPresheaf.IsCoequifibered: the localization condition under which the spectra glue, with the criterionCommMon.SubalgebraPresheaf.IsCoequifibered.of_isLocalizationAway;CommMon.SubalgebraPresheaf.relativeSpec, with the affine structure morphismCommMon.SubalgebraPresheaf.relativeSpecToBase, the chart descriptionCommMon.SubalgebraPresheaf.isPullback_relativeSpecCoverand the chartwise criterionCommMon.SubalgebraPresheaf.relativeSpecToBase_ifffor its local properties;CommMon.SubalgebraPresheaf.relativeSpecπ, withCommMon.SubalgebraPresheaf.isPullback_relativeSpecπandCommMon.SubalgebraPresheaf.relativeSpecMap_relativeSpecπ.
References #
- The Stacks Project, Tag 01LL (relative spectrum via gluing).
A family of Γ(X, U)-subalgebras of the sections of a commutative 𝒪ₓ-algebra A over the
opens U of X, stable under restriction: a sub-presheaf of rings of the sections of A under
the structure presheaf.
- sections (U : X.Opens) : Subalgebra ↑(X.presheaf.obj (Opposite.op U)) ↑(A.X.presheaf.obj (Opposite.op U))
The subalgebra of sections over
U. - restrictSections_mem {U V : X.Opens} (i : V ⟶ U) {x : ↑(A.X.presheaf.obj (Opposite.op U))} : x ∈ self.sections U → (A.restrictSections i) x ∈ self.sections V
Restriction of sections preserves the subalgebras.
Instances For
Two presheaves of subalgebras are equal when they have the same sections over every open.
The presheaf of rings U ↦ S.sections U.
Instances For
The structure morphism from the structure presheaf of X: regular functions act on A
through the algebra map, whose image lies in every subalgebra.
Instances For
The inclusion of the subalgebras into all sections of A.
Instances For
The inclusion of the subalgebras is the algebra map of the subalgebra.
The inclusion of the subalgebras is compatible with the structure maps from the structure presheaf.
The inclusion of the subalgebras is compatible with the structure maps from the structure presheaf.
If the algebra morphisms f and g agree on the subalgebras, the inclusion of the
subalgebras equalizes the morphisms of section rings they induce.
On the affine opens of X, the presheaf of rings S.sectionsPresheaf 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).
- coequifibered_toSectionsPresheaf : NatTrans.Coequifibered ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.whiskerLeft S.toSectionsPresheaf)
The structure map of
S, restricted to the affine opens, is coequifibered.
Instances
S is coequifibered when, over the basic open X.basicOpen r of every affine open U, its
subalgebra is the localization away from r of its subalgebra over U.
The relative gluing datum of S: the affine schemes Spec (S.sections U) over the affine
opens U of X.
Instances For
The gluing diagram of the relative spectrum of S is locally directed.
The relative spectrum of a coequifibered presheaf of subalgebras of the sections of A, glued
from the affine schemes Spec (S.sections U) over the affine opens U of X.
Instances For
The structure morphism of the relative spectrum of S.
Instances For
The open cover of the relative spectrum of S by the spectra of its subalgebras over the
affine opens of X.
Instances For
Over an affine open U, the structure morphism of the relative spectrum of S is Spec of
the structure map Γ(X, U) ⟶ S.sections U.
Over an affine open U, the structure morphism of the relative spectrum of S is Spec of
the structure map Γ(X, U) ⟶ S.sections U.
The preimage of an affine open U under the structure morphism of the relative spectrum of
S is the image of its chart over U.
Over an affine open U of X, the relative spectrum of S is Spec (S.sections U).
The structure morphism of the relative spectrum of S is affine.
A morphism property which is local on the target holds for the structure morphism of the
relative spectrum of S exactly when it holds for Spec of the structure maps
Γ(X, U) ⟶ S.sections U over the affine opens U of X.
Maps out of the relative spectrum of S are determined on its affine charts.
The morphism Spec_X(A) ⟶ S.relativeSpec over X, given on each affine chart by Spec of
the inclusion S.sections U ⟶ Γ(A.X, U).
Instances For
On an affine chart, S.relativeSpecπ is Spec of the inclusion of the subalgebra.
On an affine chart, S.relativeSpecπ is Spec of the inclusion of the subalgebra.
S.relativeSpecπ is a morphism over X.
S.relativeSpecπ is a morphism over X.
If the algebra morphisms f and g agree on the subalgebras, then S.relativeSpecπ
coequalizes the morphisms of relative spectra they induce.
Over an affine open U of X, S.relativeSpecπ is Spec of the inclusion
S.sections U ⟶ Γ(A.X, U): the square formed with the two charts over U is a pullback
square.
A morphism property which is local on the target holds for S.relativeSpecπ exactly when it
holds for Spec of the inclusions S.sections U ⟶ Γ(A.X, U) over the affine opens U of
X.