The presentation limit is the limit over rational subsets #
Wedhorn §8.1 assigns A⟨T/s⟩ to the rational subset R(T/s) and sets
𝒪_X(V) = lim_U 𝒪_X(U), the limit over the rational subsets U contained in the open V.
TauCeti.ValuationSpectrum.presentationLimit takes the same limit over presentations (T, s).
This file builds the diagram of coordinate rings on TauCeti.ValuationSpectrum.RationalSubsetIndex
— the rational subsets of V — identifies the two limits, and assembles the limits over rational
subsets into a presheaf isomorphic to TauCeti.ValuationSpectrum.presentationLimitPresheaf.
The diagram, and why the choice of presentation is invisible #
A rational subset carries no presentation, while A⟨T/s⟩ is built from the data (T, s). So the
diagram sends a rational subset to the coordinate ring of a presentation chosen for it, which
TauCeti.ValuationSpectrum.exists_presentationToRationalSubsetIndex_obj_eq supplies. The limit
does not see the choice: two presentations of one rational subset have canonically isomorphic
coordinate rings (TauCeti.ValuationSpectrum.completionLocObjIsoOfRationalSubsetEq), and a
containment of rational subsets acts by the comparison morphism of Wedhorn's Proposition 8.2(1),
which depends on the two subsets alone.
The identification of the limits then has two inputs. The diagram of presentations is isomorphic
to this diagram restricted along TauCeti.ValuationSpectrum.presentationToRationalSubsetIndex,
by presentation independence again; and that functor is initial, so restricting along it leaves
the limit unchanged. That isomorphism of diagrams is stated on its own, as
TauCeti.ValuationSpectrum.presentationIndexDiagramIso, so that it is available apart from the
identification of the limits it is used for here.
The presheaf #
For W ≤ V every rational subset of W is one of V, and restriction from V to W is the map
of limits along that inclusion of index categories. The two diagrams may choose different
presentations of the same rational subset, so the restriction map also applies the comparison
morphisms of Proposition 8.2(1) between them. The value-wise identification of the two limits
commutes with these restriction maps, which makes it an isomorphism of presheaves and lets
sheafhood pass between them.
All coordinate rings here are those of presentations over one pair of definition P, so both
presheaves are built from P; this file does not compare the presheaves of two pairs of
definition.
Main definitions #
TauCeti.ValuationSpectrum.RationalSubsetIndex.presentationIndex: the admissible presentation chosen for a rational subset.TauCeti.ValuationSpectrum.rationalSubsetIndexDiagram: the diagram of coordinate rings on the rational subsets ofV, with the comparison morphisms of Proposition 8.2(1) as its action on containments.TauCeti.ValuationSpectrum.presentationIndexDiagramIso: the two diagrams agree — the diagram of presentations is the diagram above, restricted alongTauCeti.ValuationSpectrum.presentationToRationalSubsetIndex.TauCeti.ValuationSpectrum.presentationLimitToRationalSubsetLimit: the comparison map from the presentation-indexed limit to the subset-indexed one.TauCeti.ValuationSpectrum.presentationLimitIsoRationalSubsetLimit: that comparison map as an isomorphism.TauCeti.ValuationSpectrum.rationalSubsetIndexRestrict: the inclusion of the rational subsets ofWamong those ofV, forW ≤ V.TauCeti.ValuationSpectrum.rationalSubsetLimitMap: the restriction map of the limits over rational subsets.TauCeti.ValuationSpectrum.rationalSubsetLimitPresheaf: the presheafV ↦ lim_{U ⊆ V} A⟨U⟩.TauCeti.ValuationSpectrum.presentationLimitPresheafIsoRationalSubsetLimitPresheaf: the presentation-indexed presheaf is the presheaf of limits over rational subsets.
Main results #
TauCeti.ValuationSpectrum.rationalSubset_presentationIndex_eq: the presentation chosen for a rational subset has the same rational subset as any other presentation of it.TauCeti.ValuationSpectrum.presentationLimitToRationalSubsetLimit_comp_π: the comparison map projects at a rational subset to the projection at the presentation chosen for it.TauCeti.ValuationSpectrum.isIso_presentationLimitToRationalSubsetLimit: the two limits agree, whenA⁺consists of power-bounded elements.TauCeti.ValuationSpectrum.presentationLimitToRationalSubsetLimit_naturality: the comparison map commutes with restriction.isSheaf_presentationLimitPresheaf_iff_isSheaf_rationalSubsetLimitPresheaf: the presentation-indexed presheaf is a sheaf exactly when the presheaf of limits over rational subsets is.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1 and Proposition 8.2(1).
The presentation chosen for a rational subset #
A chosen admissible presentation of a rational subset of V. Every object of
RationalSubsetIndex has one, by
TauCeti.ValuationSpectrum.exists_presentationToRationalSubsetIndex_obj_eq. Two presentations of
one rational subset have canonically isomorphic coordinate rings
(TauCeti.ValuationSpectrum.completionLocObjIsoOfRationalSubsetEq), and the diagram below has the
comparison morphisms of Wedhorn's Proposition 8.2(1) for its arrows, so its limit does not see the
choice.
Equations
- U.presentationIndex = ⋯.choose
Instances For
The choice is a section of presentationToRationalSubsetIndex: forgetting the chosen
presentation returns the rational subset it was chosen for. This is the equation the choice was
made by, so it, and not the open-level equation below, is what pins the choice down.
The chosen presentation presents the rational subset it was chosen for.
A containment of rational subsets is a containment of the chosen presentations' rational subsets, so the comparison morphism of Wedhorn's Proposition 8.2(1) is available along it.
The choice of presentation does not change the rational subset: a presentation i of the
rational subset U and the presentation chosen for U have the same rational subset, so the
comparison morphisms of Wedhorn's Proposition 8.2(1) run between their coordinate rings in both
directions.
The diagram of coordinate rings on rational subsets #
The diagram the subset-indexed limit is taken over: each rational subset of V
contributes the coordinate ring of its chosen presentation, and a containment contributes the
comparison morphism of Wedhorn's Proposition 8.2(1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The diagram sends a rational subset to the coordinate ring of its chosen presentation.
The diagram sends a containment to the comparison morphism of Proposition 8.2(1), between the coordinate rings of the two chosen presentations.
The universal property of presentationLimit, recovered #
The comparison of the two diagrams #
The diagram of presentations is the rational-subset diagram, restricted along
presentationToRationalSubsetIndex. This is the compatibility of the new diagram with the
existing one: the coordinate ring of a presentation and the coordinate ring of the presentation
chosen for the rational subset it presents are canonically isomorphic, naturally in the
presentation.
Identifying the two limits is one use of it; as an isomorphism of the diagrams themselves it also
transports cones, restrictions along a functor, and whatever else is built from a diagram. The
body is not exposed; presentationIndexDiagramIso_hom_app and
presentationIndexDiagramIso_inv_app give its components in both directions.
Equations
- TauCeti.ValuationSpectrum.presentationIndexDiagramIso Aplus hAplus V = CategoryTheory.NatIso.ofComponents (TauCeti.ValuationSpectrum.presentationIndexDiagramIsoApp✝ Aplus hAplus V) ⋯
Instances For
The comparison at a presentation is a comparison morphism of Proposition 8.2(1): at a
presentation i the isomorphism of the two diagrams is the comparison morphism of the containment
supplied by rationalSubset_presentationIndex_eq, from the coordinate ring of i to that of the
presentation chosen for the rational subset i presents, transported to the two diagrams'
objects.
The inverse comparison at a presentation is the comparison morphism of the reverse
containment: the two rational subsets are equal, so Wedhorn's Proposition 8.2(1) supplies a
morphism each way, and the inverse of the isomorphism of the two diagrams is the one running from
the coordinate ring of the presentation chosen for the rational subset i presents back to that
of i, transported to the two diagrams' objects.
The comparison map of the two limits #
The comparison map of the two limits: the map to the limit over the rational subsets of
V whose component at a rational subset is the projection of presentationLimit at the
presentation chosen for that subset. It is an isomorphism
(isIso_presentationLimitToRationalSubsetLimit).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The comparison map projects to the chosen presentations: its component at a rational
subset of V is the projection of presentationLimit at the presentation chosen for that
subset, transported to the diagram object.
The two limits agree. The comparison map from the presentation-indexed limit to the limit
over the rational subsets of V is an isomorphism, when A⁺ consists of power-bounded elements:
the presentations are cofinal among the rational subsets, and the two diagrams agree up to
canonical isomorphism.
The presentation-indexed limit is the limit over rational subsets, as an isomorphism of
complete separated topological rings. Its forward map is
presentationLimitToRationalSubsetLimit.
Equations
Instances For
The isomorphism of the two limits is the comparison map.
The presheaf of limits over rational subsets #
The inclusion of the rational subsets of W among those of V, for W ≤ V, as a functor
of index categories: precomposing with it restricts a diagram on the rational subsets of V to
those of W.
Instances For
Including a rational subset of W among those of V keeps its underlying open.
Including a rational subset of U among those of W, and then among those of V, is including
it among those of V directly.
For W ≤ V, the presentations chosen for a rational subset U of W in W and in V both
present U, so the comparison morphism of Proposition 8.2(1) runs from the second to the first.
The comparison of the two diagrams on the rational subsets of W, for W ≤ V: from the
diagram of V, restricted to the rational subsets of W, to the diagram of W. The body is not
exposed; rationalSubsetIndexDiagramRestrictComparison_app gives the components.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At a rational subset U of W, the comparison of the two diagrams is the comparison morphism
of Proposition 8.2(1) from the coordinate ring of the presentation chosen for U in V to that of
the one chosen in W, transported to the diagram objects.
The restriction map of the limit over rational subsets, for W ≤ V: the map
lim_{U ⊆ V} A⟨U⟩ ⟶ lim_{U ⊆ W} A⟨U⟩ of Wedhorn §8.1, reindexing along
rationalSubsetIndexRestrict h followed by rationalSubsetIndexDiagramRestrictComparison. The
body is not exposed; rationalSubsetLimitMap_comp_π gives its projections.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restriction then projection: projecting the restriction at a rational subset U of W is
projecting at U as a rational subset of V, then comparing the two diagrams at U.
The comparison of the two limits commutes with restriction: for W ≤ V, restricting the
presentation-indexed limit from V to W and then comparing agrees with comparing at V and then
restricting the limit over rational subsets.
Restricting along le_refl is the identity.
Successive restrictions compose to the restriction along the transitive containment.
The presheaf V ↦ lim_{U ⊆ V} A⟨U⟩ on Spa(A,A⁺) of Wedhorn §8.1, valued in
CompleteSeparatedTopCommRingCat, with the coordinate rings of presentations over P and
restriction maps rationalSubsetLimitMap. The body is not exposed;
rationalSubsetLimitPresheaf_obj and rationalSubsetLimitPresheaf_map give its values and
restriction maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluating the presheaf on an open is the limit over the rational subsets it contains.
The presheaf's action on a containment is rationalSubsetLimitMap, transported along
rationalSubsetLimitPresheaf_obj.
The presentation-indexed presheaf is the presheaf of limits over rational subsets, when
A⁺ consists of power-bounded elements; at an open V it is
presentationLimitIsoRationalSubsetLimit. Both presheaves are built from the pair of definition
P. The body is not exposed; presentationLimitPresheafIsoRationalSubsetLimitPresheaf_hom_app
gives its components.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At an open V, the forward map of the isomorphism of the two presheaves is the comparison map
presentationLimitToRationalSubsetLimit of the two limits at V, transported along
presentationLimitPresheaf_obj and rationalSubsetLimitPresheaf_obj.
Sheafhood transfers between the two presheaves: when A⁺ consists of power-bounded
elements, presentationLimitPresheaf P Aplus is a sheaf exactly when
rationalSubsetLimitPresheaf P Aplus hAplus is.