Presentations are cofinal among rational subsets #
Wedhorn defines the structure presheaf on Spa(A,A⁺) at an open V as the limit of the
coordinate rings of the rational subsets contained in V. The existing construction
TauCeti.ValuationSpectrum.presentationLimit instead indexes the limit by admissible
presentations (T,s) of those subsets. This file supplies the categorical comparison of the
two indices needed once the coordinate rings are assembled into a diagram on rational subsets.
RationalSubsetIndex Aplus V is the partial order of rational subsets contained in V, ordered by
reverse inclusion, so a morphism points in the direction of restriction. The functor
presentationToRationalSubsetIndex forgets a presentation and remembers its subset. Every
rational subset has a presentation in this functor's image: openness of its numerator ideal gives
the standing denominator-power condition by
TauCeti.Huber.PairOfDefinition.hasDenominatorPower_of_isOpen_span.
The forgetful functor is both final and initial. Finality records the usual meaning of cofinality for a basis ordered by refinement. Initiality is the form needed for limits: the costructured arrow category over a rational subset is connected because two presentations containing it have a common refinement which still contains it. Consequently, once a compatible coordinate-ring diagram on rational subsets is constructed, its limit can be computed over presentations without choosing a preferred presentation.
Main definitions #
TauCeti.ValuationSpectrum.RationalSubsetIndex: rational subsets contained in an open, ordered by reverse inclusion.TauCeti.ValuationSpectrum.presentationToRationalSubsetIndex: the functor forgetting presentation data.
Main results #
TauCeti.ValuationSpectrum.exists_presentationIndex_mem: the rational opens presented by the indices of an open cover it.TauCeti.ValuationSpectrum.exists_presentationToRationalSubsetIndex_obj_eq: every rational subset index is exactly represented by an admissible presentation.CategoryTheory.Functor.Final (TauCeti.ValuationSpectrum.presentationToRationalSubsetIndex Aplus V): presentations are cofinal among rational subsets.CategoryTheory.Functor.Initial (TauCeti.ValuationSpectrum.presentationToRationalSubsetIndex Aplus V): the cofinality condition that will preserve the rational-subset-indexed limit once its diagram is constructed.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1.
A rational open contained in an open V, ordered by reverse inclusion so that arrows point
from a rational open to a smaller one, in the direction of restriction maps.
Equations
- TauCeti.ValuationSpectrum.RationalSubsetIndex Aplus V = { U : TopologicalSpace.Opens ↑(TauCeti.ValuationSpectrum.spa Aplus) // U ∈ TauCeti.ValuationSpectrum.spaRationalOpens Aplus ∧ U ≤ V }ᵒᵈ
Instances For
The order on rational-subset indices is reverse inclusion of their underlying opens.
Forget an admissible presentation and retain the rational subset it presents. Refinement
becomes reverse inclusion by rationalSubset_subset_rationalSubset_of_le.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The open underlying the image of a presentation is the rational open it presents.
Every rational subset index has an admissible presentation. The open numerator ideal in
the definition of spaRationalFamily supplies HasDenominatorPower, so the chosen presentation
is an object of PresentationIndex, and forgetting it recovers the original subset exactly.
Every point of an open lies in the rational open of one of its indices: the rational opens
R(i), for i ranging over the indices of V, cover V.
The functor from presentations to rational subsets is final: every rational subset is in its image, and the presentation index is filtered by common refinement. This is the categorical cofinality assertion for the two index preorders.
The functor from presentations to rational subsets is initial. Thus limits indexed by rational subsets are unchanged after restricting to presentations.