The refinement category of presentations, and its functor to complete separated rings

The refinement preorder on Presentation (LocalizationTopology/Presentation.lean) has an associated category; this file makes the assignment p ↦ A⟨p.num / p.den⟩ a functor from it into CompleteSeparatedTopCommRingCat, with the restriction morphisms of CompleteSeparated/Restriction.lean as its action on arrows.

This preorder is intended to index the adic structure presheaf — 𝒪_X(V) as a limit of this functor over the presentations whose rational subset lies in V — but no presheaf exists in this file's imports, and refinement is the cofactor relation on presentation data: sufficient for containment of the rational subsets, and not proved equivalent to it. TauCeti.ValuationSpectrum.existsUnique_continuous_ringHom_of_rationalSubset_subset produces the comparison map from a containment alone, when A⁺ consists of power-bounded elements; refinement needs no such hypothesis.

Main definitions

• TauCeti.Huber.PairOfDefinition.Presentation.completionLocObj : the object A⟨T/s⟩ of a presentation.
• TauCeti.Huber.PairOfDefinition.Presentation.completionLocObjCommRingCatIso : identifies its underlying ring with the completed localization.
• TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom : the restriction morphism of a refinement, from an arbitrary choice of cofactor.
• TauCeti.Huber.PairOfDefinition.presentationFunctor : the functor into CompleteSeparatedTopCommRingCat.

Main results

• TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom_eq : cofactor-independence — the morphism is computed by any cofactor witnessing the refinement.
• TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom_refl and …restrictionHom_comp : the identity and composition laws, stated on restrictionHom itself so that simp-normalised goals can still reach them.

Why the cofactor must be quantified away

A category whose arrows carried the cofactor would not be a preorder category, and the intended index has to be one: a limit over the presentations inside V is indexed by a condition on presentations, not by extra data. Quantifying the cofactor away is only legitimate because the restriction morphism does not depend on it — restrictionObjHom_congr — which is what lets the functor's action be defined by an arbitrary choice and still be functorial.

For the same reason the cofactor accessor and its two spec lemmas are private here rather than public in LocalizationTopology/Presentation.lean: they name a choose witness with no mathematical content, so exporting them would let a consumer depend on the choice. The public route from p ≤ q to a cofactor is Presentation.le_def, and the public statement about the morphism is Presentation.restrictionHom_eq, which holds for every cofactor.

Provenance

Adapted from AINTLIB's StructurePresheafLimit.lean (see References): the idea of indexing the structure presheaf by presentation data rather than by rational subsets, and the refinement relation between presentations, are that file's. The bundling differs deliberately: AINTLIB threads RationalLocData records through explicit hypotheses, while here Presentation packs the data so that refinement is a Preorder and this assignment is a functor — the shape a categorical limit needs.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1–§8.2.
• C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit 37bbdaeb, projects/AdicSpaces/Adic spaces/StructurePresheafLimit.lean.

@[reducible, inline]

noncomputable abbrev TauCeti.Huber.PairOfDefinition.Presentation.completionLocObj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) : CompleteSeparatedTopCommRingCat

The completed rational localization A⟨T/s⟩ attached to a presentation, as an object.

Equations

• p.completionLocObj = P.completionLocObj p.num p.den (Localization.Away p.den) ⋯

noncomputable def TauCeti.Huber.PairOfDefinition.Presentation.completionLocObjCommRingCatIso {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) : (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget₂ TopCommRingCat CommRingCat)).obj p.completionLocObj ≅ ↧(UniformSpace.Completion (Localization.Away p.den))

The underlying commutative ring of p.completionLocObj is the completed rational localisation A⟨p⟩ = UniformSpace.Completion (Localization.Away p.den): the transport along completionLocObj_obj, with its target stated as CommRingCat.of of the completion so that maps out of A⟨p⟩ compose with it on the nose.

Equations

• p.completionLocObjCommRingCatIso = (CategoryTheory.forget₂ TopCommRingCat CommRingCat).mapIso (CategoryTheory.eqToIso ⋯)

@[simp]

theorem TauCeti.Huber.PairOfDefinition.Presentation.completionLocObjCommRingCatIso_hom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) : p.completionLocObjCommRingCatIso.hom = (CategoryTheory.forget₂ TopCommRingCat CommRingCat).map (CategoryTheory.eqToHom ⋯)

The forward map identifying the underlying ring of a completed localization.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.Presentation.completionLocObjCommRingCatIso_inv {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) : p.completionLocObjCommRingCatIso.inv = (CategoryTheory.forget₂ TopCommRingCat CommRingCat).map (CategoryTheory.eqToHom ⋯)

The inverse map identifying the underlying ring of a completed localization.

noncomputable def TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q : P.Presentation} (h : p ≤ q) : p.completionLocObj ⟶ q.completionLocObj

The restriction morphism attached to a refinement, taking the chosen cofactor. It does not depend on that choice — Presentation.restrictionHom_eq — and it is the preorder-category counterpart of restrictionObjHom, not Mathlib's arrow LE.le.hom.

Equations

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

theorem TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom_eq {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q : P.Presentation} (h : p ≤ q) (r : A) (hr : q.den = p.den * r) (hT : ∀ t ∈ p.num, t * r ∈ q.num) : restrictionHom h = P.restrictionObjHom p.num p.den (Localization.Away p.den) ⋯ q.num q.den (Localization.Away q.den) ⋯ r hr hT

Presentation.restrictionHom is computed by any cofactor witnessing the refinement, not only the chosen one. This is restrictionObjHom_congr transported to the preorder.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom_refl {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (p : P.Presentation) : restrictionHom ⋯ = CategoryTheory.CategoryStruct.id p.completionLocObj

The restriction morphism of the trivial refinement is the identity.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom_comp {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q w : P.Presentation} (h₁ : p ≤ q) (h₂ : q ≤ w) : CategoryTheory.CategoryStruct.comp (restrictionHom h₁) (restrictionHom h₂) = restrictionHom ⋯

Restriction morphisms compose along composite refinements.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.Presentation.restrictionHom_comp_assoc {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} {p q w : P.Presentation} (h₁ : p ≤ q) (h₂ : q ≤ w) {Z : CompleteSeparatedTopCommRingCat} (h : w.completionLocObj ⟶ Z) : CategoryTheory.CategoryStruct.comp (restrictionHom h₁) (CategoryTheory.CategoryStruct.comp (restrictionHom h₂) h) = CategoryTheory.CategoryStruct.comp (restrictionHom ⋯) h

Restriction morphisms compose along composite refinements.

noncomputable def TauCeti.Huber.PairOfDefinition.presentationFunctor {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) : CategoryTheory.Functor P.Presentation CompleteSeparatedTopCommRingCat

The functor p ↦ A⟨p.num / p.den⟩ from the refinement category into CompleteSeparatedTopCommRingCat, with the restriction morphisms as its action on arrows. Functoriality is restrictionHom_refl and restrictionHom_comp.

@[expose] is load-bearing, for a narrower reason than exposure usually carries: with the body sealed, presentationFunctor_map below does not typecheck as a statement. Its two sides live in (presentationFunctor P).obj p ⟶ (presentationFunctor P).obj q and in p.completionLocObj ⟶ q.completionLocObj, and only unfolding the functor identifies those types. presentationFunctor_obj is statable either way; it is the map equation, and the definitional reindexing a limit over this category needs, that the exposure provides.

Equations

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

@[simp]

theorem TauCeti.Huber.PairOfDefinition.presentationFunctor_obj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (p : P.Presentation) : P.presentationFunctor.obj p = p.completionLocObj

The functor takes a presentation to its own object.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.presentationFunctor_map {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) {p q : P.Presentation} (h : p ⟶ q) : P.presentationFunctor.map h = Presentation.restrictionHom ⋯

The functor takes a refinement to its restriction morphism.