The presentation-indexed limit behind the structure presheaf

Wedhorn §8.1 assigns A⟨T/s⟩ to the rational subset R(T/s) and extends the assignment to an arbitrary open V ⊆ Spa(A,A⁺) by the limit over the rational subsets contained in V. This file constructs that limit indexed by presentations rather than by rational subsets, and makes it a presheaf. It is named for its index rather than for 𝒪_X: see Relation to Wedhorn's 𝒪_X below.

The index is PresentationIndex: a presentation together with a proof that the rational subset it presents lies in V, ordered by refinement. RefinementCategory already makes the assignment p ↦ A⟨p.num / p.den⟩ functorial on presentations, so the diagram is obtained by restricting that functor along the forgetful map, and the value is its limit — which exists because CompleteSeparatedTopCommRingCat has all small limits.

Main definitions

• TauCeti.ValuationSpectrum.PresentationIndex : the index category for an open — presentations whose numerator ideal is open, so that the basic open they present really is a rational subset.
• TauCeti.ValuationSpectrum.PresentationIndex.commonRefinement : the common refinement of two indices.
• TauCeti.ValuationSpectrum.presentationIndexDiagram : the diagram it indexes.
• TauCeti.ValuationSpectrum.presentationLimit : the limit itself.
• TauCeti.ValuationSpectrum.presentationLimitMap : the restriction morphism of a containment.
• TauCeti.ValuationSpectrum.presentationLimitPresheaf : the presheaf they assemble into.

Main results

• IsDirected (TauCeti.ValuationSpectrum.PresentationIndex Aplus V) (· ≤ ·) : the index is directed — two admissible presentations refining V have an admissible common refinement. Presentation.commonRefinement leaves both index fields to its consumers, because Presentation carries no openness field.
• TauCeti.ValuationSpectrum.presentationLimit_hom_ext : two morphisms into the limit agree as soon as their projections do.
• TauCeti.ValuationSpectrum.presentationLimitMap_comp_π : restriction is reindexing — restricting and then projecting is projecting at the same presentation.
• TauCeti.ValuationSpectrum.presentationLimitMap_refl and TauCeti.ValuationSpectrum.presentationLimitMap_comp : the two functor laws, as normal forms for a restriction map along le_refl and for a composite of two restriction maps.

Why the index is presentations and not subsets

A⟨T/s⟩ is built from the data (T, s), and two presentations of the same rational subset give canonically isomorphic but not equal rings. Indexing the limit by presentations rather than by subsets avoids having to choose one.

Relation to Wedhorn's 𝒪_X

Wedhorn indexes the limit by rational subsets U ⊆ V; here the index is presentations, so the presheaf is built from presentation data, and it is named for that. When A⁺ consists of power-bounded elements the two indexings give isomorphic presheaves:

• refinement maps between two presentations of the same rational subset are isomorphisms, so that p ↦ A⟨p.num / p.den⟩ descends to a function of the subset. This is TauCeti.ValuationSpectrum.isIso_restrictionHom_of_rationalSubset_eq; and
• the presentation index is cofinal in the subset index. This is expressed by TauCeti.ValuationSpectrum.presentationToRationalSubsetIndex in TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.Cofinality; its Initial instance is the categorical comparison needed for limits.

TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.SubsetLimit puts these together, on each open into TauCeti.ValuationSpectrum.presentationLimitIsoRationalSubsetLimit and as presheaves into TauCeti.ValuationSpectrum.presentationLimitPresheafIsoRationalSubsetLimitPresheaf. Both presheaves are built from the same pair of definition P.

Nothing in this file computes 𝒪_X(V). What it establishes is self-contained: the limit exists, restriction along a containment is reindexing, and the two functor laws hold. On a rational open U the value is identified with A_U in TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.Rational.Basic, when A⁺ consists of power-bounded elements.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1.

Provenance

The idea of indexing the limit by presentations, and the refinement relation ordering them, were adapted from AINTLIB (Apache-2.0), commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, projects/AdicSpaces/Adic spaces/StructurePresheafLimit.lean. The Lean here is written against this repository's own RefinementCategory and PairOfDefinition.Presentation API; no code was copied.

structure TauCeti.ValuationSpectrum.PresentationIndex {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) : Type v

The index of the limit: presentations whose numerator ideal is open and whose rational subset lies in V.

The openness of Ideal.span pres.num is what makes R(pres.num / pres.den) a rational subset in Wedhorn's sense rather than a general basic open — it is the defining condition of TauCeti.ValuationSpectrum.spaRationalFamily. Carrying it as a field of the index restricts the diagram to admissible presentations; because it is a field, every object supplies its own proof and the refinement morphisms carry no preservation obligation.

• pres : P.Presentation

  The presentation.

• isOpen_span : IsOpen ↑(Ideal.span ↑self.pres.num)

  Its numerator ideal is open, so the subset it presents is rational.

• le_open : spaBasicOpen Aplus self.pres.num self.pres.den ≤ V

  Its rational subset is contained in V.

@[instance_reducible]

instance TauCeti.ValuationSpectrum.instPreorderPresentationIndex {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} : Preorder (PresentationIndex Aplus V)

Refinement of the underlying presentations orders the index.

Equations

• TauCeti.ValuationSpectrum.instPreorderPresentationIndex = Preorder.lift TauCeti.ValuationSpectrum.PresentationIndex.pres

theorem TauCeti.ValuationSpectrum.PresentationIndex.ext {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {i j : PresentationIndex Aplus V} (h : i.pres = j.pres) : i = j

An index is its presentation. The other two fields are propositions, so they are proof-irrelevant and carry no information: equality of indices reduces to equality of the underlying presentations.

theorem TauCeti.ValuationSpectrum.PresentationIndex.ext_iff {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {i j : PresentationIndex Aplus V} : i = j ↔ i.pres = j.pres

theorem TauCeti.ValuationSpectrum.rationalSubset_commonRefinement {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (p q : P.Presentation) : rationalSubset Aplus (p.commonRefinement q).num (p.commonRefinement q).den = rationalSubset Aplus p.num p.den ∩ rationalSubset Aplus q.num q.den

The common refinement presents the intersection: R(p · q) = R(p) ∩ R(q) for the common refinement of two presentations. This is TauCeti.ValuationSpectrum.rationalSubset_inter, whose presentation of an intersection the common refinement follows.

theorem TauCeti.ValuationSpectrum.PresentationIndex.rationalSubset_subset {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} (i : PresentationIndex Aplus V) {T : Finset A} {s : A} (hV : V ≤ spaBasicOpen Aplus T s) : rationalSubset Aplus i.pres.num i.pres.den ⊆ rationalSubset Aplus T s

The rational subset of an index of V lies in every rational subset containing V.

noncomputable def TauCeti.ValuationSpectrum.PresentationIndex.commonRefinement {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} (i j : PresentationIndex Aplus V) : PresentationIndex Aplus V

The common refinement of two indices: Presentation.commonRefinement of the underlying presentations, which is again admissible and presents the intersection of the two rational subsets, so it again lies in V.

Both of the index's own fields have to be re-established, which is what TauCeti.Huber.PairOfDefinition.Presentation.commonRefinement deliberately does not do — it carries no openness field. The containment in V is rationalSubset_commonRefinement, and openness of the numerator span is TauCeti.Huber.PairOfDefinition.isOpen_span_insert_mul_insert, the admissibility half of Wedhorn Remark 7.30(5), which TauCeti.ValuationSpectrum.inter_mem_spaRationalFamily_of_pairOfDefinition also uses.

Equations

• i.commonRefinement j = { pres := i.pres.commonRefinement j.pres, isOpen_span := ⋯, le_open := ⋯ }

@[simp]

theorem TauCeti.ValuationSpectrum.PresentationIndex.commonRefinement_pres {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} (i j : PresentationIndex Aplus V) : (i.commonRefinement j).pres = i.pres.commonRefinement j.pres

The presentation of the common refinement of two indices is the common refinement of their presentations.

theorem TauCeti.ValuationSpectrum.PresentationIndex.le_commonRefinement_left {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} (i j : PresentationIndex Aplus V) : i ≤ i.commonRefinement j

The common refinement of two indices refines the left one.

theorem TauCeti.ValuationSpectrum.PresentationIndex.le_commonRefinement_right {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} (i j : PresentationIndex Aplus V) : j ≤ i.commonRefinement j

The common refinement of two indices refines the right one.

instance TauCeti.ValuationSpectrum.instIsDirectedPresentationIndexLe {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} : IsDirected (PresentationIndex Aplus V) fun (x1 x2 : PresentationIndex Aplus V) => x1 ≤ x2

The index is directed: two admissible presentations refining V are both refined by their common refinement PresentationIndex.commonRefinement.

noncomputable def TauCeti.ValuationSpectrum.presentationIndexDiagram {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) : CategoryTheory.Functor (PresentationIndex Aplus V) CompleteSeparatedTopCommRingCat

The diagram the limit is taken over: each admissible presentation refining V contributes A⟨T/s⟩, and a refinement contributes its restriction morphism.

Equations

• TauCeti.ValuationSpectrum.presentationIndexDiagram Aplus V = (TauCeti.ValuationSpectrum.presentationIndexInclusion✝ Aplus V).comp P.presentationFunctor

theorem TauCeti.ValuationSpectrum.presentationIndexDiagram_obj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (i : PresentationIndex Aplus V) : (presentationIndexDiagram Aplus V).obj i = i.pres.completionLocObj

The diagram sends an index to the completed localization of its presentation.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationIndexDiagram_map {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) {i j : PresentationIndex Aplus V} (f : i ⟶ j) : (presentationIndexDiagram Aplus V).map f ≍ Huber.PairOfDefinition.Presentation.restrictionHom ⋯

The diagram takes a refinement of indices to the restriction morphism of the underlying refinement of presentations.

noncomputable def TauCeti.ValuationSpectrum.presentationIndexCone {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (W : CompleteSeparatedTopCommRingCat) (app : (i : PresentationIndex Aplus V) → W ⟶ i.pres.completionLocObj) (naturality : ∀ {i j : PresentationIndex Aplus V} (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (app i) (Huber.PairOfDefinition.Presentation.restrictionHom ⋯) = app j) : CategoryTheory.Limits.Cone (presentationIndexDiagram Aplus V)

Build a cone over the presentation diagram from maps to the completed localization at each index that commute with restriction morphisms.

Equations

• TauCeti.ValuationSpectrum.presentationIndexCone Aplus V W app naturality = ⋯.mpr { pt := W, π := { app := app, naturality := ⋯ } }

theorem TauCeti.ValuationSpectrum.presentationIndexCone_pt {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (W : CompleteSeparatedTopCommRingCat) (app : (i : PresentationIndex Aplus V) → W ⟶ i.pres.completionLocObj) (naturality : ∀ {i j : PresentationIndex Aplus V} (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (app i) (Huber.PairOfDefinition.Presentation.restrictionHom ⋯) = app j) : (presentationIndexCone Aplus V W app ⋯).pt = W

The vertex of a cone built with presentationIndexCone is the specified object.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationIndexCone_π_app {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (W : CompleteSeparatedTopCommRingCat) (app : (i : PresentationIndex Aplus V) → W ⟶ i.pres.completionLocObj) (naturality : ∀ {i j : PresentationIndex Aplus V} (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (app i) (Huber.PairOfDefinition.Presentation.restrictionHom ⋯) = app j) (i : PresentationIndex Aplus V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((presentationIndexCone Aplus V W app ⋯).π.app i) (CategoryTheory.eqToHom ⋯)) = app i

A cone built with presentationIndexCone has the specified leg after transporting the diagram object to the completed localization of its presentation.

noncomputable def TauCeti.ValuationSpectrum.presentationLimit {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) : CompleteSeparatedTopCommRingCat

The limit over the presentations refining V, lim_{R(T/s) ⊆ V} A⟨T/s⟩ — Wedhorn §8.1's formula for 𝒪_X(V), but indexed by presentations rather than by rational subsets. The limit exists because CompleteSeparatedTopCommRingCat has all small limits. This is not shown to be 𝒪_X(V); see the module docstring.

Equations

• TauCeti.ValuationSpectrum.presentationLimit Aplus V = CategoryTheory.Limits.limit (TauCeti.ValuationSpectrum.presentationIndexDiagram Aplus V)

def TauCeti.ValuationSpectrum.presentationIndexRestrict {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (h : W ≤ V) : CategoryTheory.Functor (PresentationIndex Aplus W) (PresentationIndex Aplus V)

Restricting the containment reindexes the diagram: a presentation refining W refines V whenever W ≤ V.

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.presentationIndexRestrict_obj_pres {A : Type v} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (h : W ≤ V) (i : PresentationIndex Aplus W) : ((presentationIndexRestrict h).obj i).pres = i.pres

Restricting an index keeps its presentation.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitMap {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (h : W ≤ V) : presentationLimit Aplus V ⟶ presentationLimit Aplus W

The restriction morphism of a containment W ≤ V: the limit over the presentations refining V maps to the limit over the smaller index, by reindexing.

Equations

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

The projection, and the restriction normal forms

presentationLimit is a limit, so Mathlib's limit.w, limit.lift and limit.lift_π are its interface and are not restated here. Two names do have to exist. presentationLimitπ is load-bearing rather than cosmetic: presentationLimitMap's codomain is presentationLimit W, and because that definition is sealed the elaborator will not identify it with limit (diagram W), so limit.π cannot be written at the use site — it reports "definitions were not unfolded because their definition is not exposed". presentationLimit_hom_ext follows it: limit.hom_ext leaves goals spelled with limit.π, which the restriction lemmas below then fail to rewrite.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitπ {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (i : PresentationIndex Aplus V) : presentationLimit Aplus V ⟶ (presentationIndexDiagram Aplus V).obj i

The projection of presentationLimit at an index.

Equations

• TauCeti.ValuationSpectrum.presentationLimitπ Aplus V i = CategoryTheory.Limits.limit.π (TauCeti.ValuationSpectrum.presentationIndexDiagram Aplus V) i

noncomputable def TauCeti.ValuationSpectrum.presentationLimitπToPresentation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (i : PresentationIndex Aplus V) : presentationLimit Aplus V ⟶ i.pres.completionLocObj

The projection at an index, with its codomain transported to the completed localization of the underlying presentation.

Equations

• TauCeti.ValuationSpectrum.presentationLimitπToPresentation Aplus V i = CategoryTheory.CategoryStruct.comp (TauCeti.ValuationSpectrum.presentationLimitπ Aplus V i) (CategoryTheory.eqToHom ⋯)

theorem TauCeti.ValuationSpectrum.presentationLimitπToPresentation_eq {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (i : PresentationIndex Aplus V) : presentationLimitπToPresentation Aplus V i = CategoryTheory.CategoryStruct.comp (presentationLimitπ Aplus V i) (CategoryTheory.eqToHom ⋯)

The transported projection is the projection followed by the transport.

theorem TauCeti.ValuationSpectrum.presentationLimitπToPresentation_comp_eqToHom_congr {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {i j : PresentationIndex Aplus V} (h : i = j) {X : CompleteSeparatedTopCommRingCat} (e : i.pres.completionLocObj = X) (e' : j.pres.completionLocObj = X) : CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus V i) (CategoryTheory.eqToHom e) = CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus V j) (CategoryTheory.eqToHom e')

Projections at equal indices agree, after transporting their codomains to a common object.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitπ_comp_map {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {i j : PresentationIndex Aplus V} (h : i ⟶ j) : CategoryTheory.CategoryStruct.comp (presentationLimitπ Aplus V i) ((presentationIndexDiagram Aplus V).map h) = presentationLimitπ Aplus V j

Projections are compatible with refinement: projecting then restricting along a refinement is projecting at the finer index.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitπ_comp_restriction {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {i j : PresentationIndex Aplus V} (h : i ≤ j) : CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus V i) (Huber.PairOfDefinition.Presentation.restrictionHom h) = presentationLimitπToPresentation Aplus V j

Projecting at a presentation and then restricting is projection at the refined presentation, after transporting the diagram objects to their completed-localization descriptions.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitLift {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (s : CategoryTheory.Limits.Cone (presentationIndexDiagram Aplus V)) : s.pt ⟶ presentationLimit Aplus V

The universal property: a cone over the diagram factors through the limit.

Equations

• TauCeti.ValuationSpectrum.presentationLimitLift Aplus V s = CategoryTheory.Limits.limit.lift (TauCeti.ValuationSpectrum.presentationIndexDiagram Aplus V) s

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitLift_comp_π {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (s : CategoryTheory.Limits.Cone (presentationIndexDiagram Aplus V)) (i : PresentationIndex Aplus V) : CategoryTheory.CategoryStruct.comp (presentationLimitLift Aplus V s) (presentationLimitπ Aplus V i) = s.π.app i

The lift is a factorisation: composing it with a projection recovers the cone leg.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitLift_comp_πToPresentation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (s : CategoryTheory.Limits.Cone (presentationIndexDiagram Aplus V)) (i : PresentationIndex Aplus V) : CategoryTheory.CategoryStruct.comp (presentationLimitLift Aplus V s) (presentationLimitπToPresentation Aplus V i) = CategoryTheory.CategoryStruct.comp (s.π.app i) (CategoryTheory.eqToHom ⋯)

The lift followed by the projection transported to the presentation object is the transported cone leg.

theorem TauCeti.ValuationSpectrum.presentationIndexCone_lift_comp_πToPresentation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) (W : CompleteSeparatedTopCommRingCat) (app : (i : PresentationIndex Aplus V) → W ⟶ i.pres.completionLocObj) (naturality : ∀ {i j : PresentationIndex Aplus V} (f : i ⟶ j), CategoryTheory.CategoryStruct.comp (app i) (Huber.PairOfDefinition.Presentation.restrictionHom ⋯) = app j) (i : PresentationIndex Aplus V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (presentationLimitLift Aplus V (presentationIndexCone Aplus V W app ⋯)) (presentationLimitπToPresentation Aplus V i)) = app i

The lift of a cone built from presentationwise maps has those maps as its transported projections.

theorem TauCeti.ValuationSpectrum.presentationLimit_hom_ext {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {W : CompleteSeparatedTopCommRingCat} {f g : W ⟶ presentationLimit Aplus V} (h : ∀ (i : PresentationIndex Aplus V), CategoryTheory.CategoryStruct.comp f (presentationLimitπ Aplus V i) = CategoryTheory.CategoryStruct.comp g (presentationLimitπ Aplus V i)) : f = g

Extensionality: maps into the limit agree when their projections do.

theorem TauCeti.ValuationSpectrum.presentationLimit_hom_ext_iff {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {W : CompleteSeparatedTopCommRingCat} {f g : W ⟶ presentationLimit Aplus V} : f = g ↔ ∀ (i : PresentationIndex Aplus V), CategoryTheory.CategoryStruct.comp f (presentationLimitπ Aplus V i) = CategoryTheory.CategoryStruct.comp g (presentationLimitπ Aplus V i)

theorem TauCeti.ValuationSpectrum.presentationLimit_hom_ext_toPresentation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V : TopologicalSpace.Opens ↑(spa Aplus)} {W : CompleteSeparatedTopCommRingCat} {f g : W ⟶ presentationLimit Aplus V} (h : ∀ (i : PresentationIndex Aplus V), CategoryTheory.CategoryStruct.comp f (presentationLimitπToPresentation Aplus V i) = CategoryTheory.CategoryStruct.comp g (presentationLimitπToPresentation Aplus V i)) : f = g

Extensionality using the projections transported to their presentation objects.

theorem TauCeti.ValuationSpectrum.presentationIndexDiagram_obj_restrict {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (h : W ≤ V) (i : PresentationIndex Aplus W) : (presentationIndexDiagram Aplus V).obj ((presentationIndexRestrict h).obj i) = (presentationIndexDiagram Aplus W).obj i

Restricting an index does not change what the diagram sends it to.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitMap_comp_π {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (h : W ≤ V) (i : PresentationIndex Aplus W) : CategoryTheory.CategoryStruct.comp (presentationLimitMap h) (presentationLimitπ Aplus W i) = CategoryTheory.CategoryStruct.comp (presentationLimitπ Aplus V ((presentationIndexRestrict h).obj i)) (CategoryTheory.eqToHom ⋯)

Restriction is reindexing: restricting to W and then projecting at an index of W is projecting at the same presentation viewed as an index of V, transported along presentationIndexDiagram_obj_restrict.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitMap_comp_πToPresentation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (h : W ≤ V) (i : PresentationIndex Aplus W) : CategoryTheory.CategoryStruct.comp (presentationLimitMap h) (presentationLimitπToPresentation Aplus W i) = CategoryTheory.CategoryStruct.comp (presentationLimitπToPresentation Aplus V ((presentationIndexRestrict h).obj i)) (CategoryTheory.eqToHom ⋯)

Restriction followed by a projection transported to its presentation object is the corresponding transported projection before restriction.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitMap_refl {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (V : TopologicalSpace.Opens ↑(spa Aplus)) : presentationLimitMap ⋯ = CategoryTheory.CategoryStruct.id (presentationLimit Aplus V)

Restricting along le_refl is the identity.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitMap_comp {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {U V W : TopologicalSpace.Opens ↑(spa Aplus)} (h₁ : W ≤ V) (h₂ : U ≤ W) : CategoryTheory.CategoryStruct.comp (presentationLimitMap h₁) (presentationLimitMap h₂) = presentationLimitMap ⋯

Successive restrictions compose to the restriction along the transitive containment.

theorem TauCeti.ValuationSpectrum.presentationLimitMap_apply_presentationLimitMap_apply {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {U V W : TopologicalSpace.Opens ↑(spa Aplus)} (h₁ : W ≤ V) (h₂ : U ≤ W) (z : (presentationLimit Aplus V).obj.α) : ↑(presentationLimitMap h₂).hom (↑(presentationLimitMap h₁).hom z) = ↑(presentationLimitMap ⋯).hom z

Successive restrictions compose, on sections: presentationLimitMap_comp evaluated at a section z over V.

theorem TauCeti.ValuationSpectrum.eqToHom_presentationLimit {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : Huber.PairOfDefinition A} {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (e : V = W) (e' : presentationLimit Aplus V = presentationLimit Aplus W) : CategoryTheory.eqToHom e' = presentationLimitMap ⋯

A transport between presentation limits along an equality of opens is a restriction map: the eqToHom of presentationLimit V = presentationLimit W induced by V = W is the restriction map along W ≤ V.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitPresheaf {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : CategoryTheory.Functor (TopologicalSpace.Opens ↑(spa Aplus))ᵒᵖ CompleteSeparatedTopCommRingCat

The presheaf V ↦ presentationLimit V on Spa(A,A⁺), valued in CompleteSeparatedTopCommRingCat. Both functor laws are reindexing identities for the limit: restricting along le_refl is the identity on the index, and restricting twice is restricting once. When A⁺ consists of power-bounded elements it is isomorphic to Wedhorn §8.1's 𝒪_X, the presheaf of limits over rational subsets built from the same pair of definition P (TauCeti.ValuationSpectrum.presentationLimitPresheafIsoRationalSubsetLimitPresheaf).

Equations

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

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPresheaf_obj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (V : (TopologicalSpace.Opens ↑(spa Aplus))ᵒᵖ) : (presentationLimitPresheaf P Aplus).obj V = presentationLimit Aplus (Opposite.unop V)

Evaluating the presheaf on an open is the limit over that open.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitPresheaf_map {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) {V W : (TopologicalSpace.Opens ↑(spa Aplus))ᵒᵖ} (h : V ⟶ W) : (presentationLimitPresheaf P Aplus).map h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (presentationLimitMap ⋯) (CategoryTheory.eqToHom ⋯))

The presheaf's action on a containment is the reindexing map.