Comparing two presentations of a rational localisation

A rational subset U = R(T/s) of Spa(A,A⁺) has many presentations (T,s), so the completed localisations they give must be compared by canonical isomorphisms, compatible for three presentations. This file supplies the conditional half: given comparison maps compatible with the structure maps from A, they are mutually inverse and compose correctly.

The other half is the passage from an equality of two rational subsets to the existence of those maps — the step Mathlib-side rationalSubset_subset_rationalSubset_iff stops short of, in its own words "leaving the passage from those facts to invertibility of s and power-boundedness of t/s in the coordinate ring as a separate, genuinely algebraic step" (Wedhorn §8.2). That passage is TauCeti.ValuationSpectrum.presentationRingEquivOfEq, which instantiates the comparison theory here through Wedhorn's Proposition 8.2(1).

The file has two halves. The first bundles a presentation as Presentation and orders those bundles by refinement — the Preorder and IsDirected instances, Presentation.commonRefinement as the common refinement, and le_def as the route from p ≤ q to a cofactor.

The second is the comparison theory, and there everything is uniqueness: no comparison map is constructed. Given maps in both directions that commute with the structure maps, they are mutually inverse, and given three presentations the comparison through the middle one is the direct comparison. That is exactly what TauCeti.Huber.PairOfDefinition.eq_id_of_comp_toCompletionLoc_eq_self and …eq_comp_of_comp_toCompletionLoc_eq say about maps out of A⟨T/s⟩, so each proof in that half is a single application of one of them.

Main definitions

• TauCeti.Huber.PairOfDefinition.Presentation: the bundle (num, den, hasDenominatorPower) of a presentation, with the refinement preorder Presentation.RefinedBy and the common refinement Presentation.commonRefinement making refinement directed. Presentation.commonRefinement_num and Presentation.commonRefinement_den are its projection equations, since the body is not exported.
• TauCeti.Huber.PairOfDefinition.presentationRingEquiv: the canonical isomorphism A⟨T/s⟩ ≃+* A⟨T'/s'⟩ assembled from compatible comparison maps in both directions.

Main results

• TauCeti.Huber.PairOfDefinition.comp_eq_id_of_comp_toCompletionLoc_eq: compatible comparison maps in both directions compose to the identity.
• TauCeti.Huber.PairOfDefinition.eq_comp_of_comp_toCompletionLoc_eq_three: compatibility for three presentations — the comparison from the first to the third is the composite through the second.
• TauCeti.Huber.PairOfDefinition.presentationRingEquiv_coe and …_symm_coe: the characteristic equations — the isomorphism is the forward map it was built from, and its inverse is the backward one, so it introduces nothing new.
• TauCeti.Huber.PairOfDefinition.continuous_presentationRingEquiv, its …_symm counterpart, and …_coe_comp_toCompletionLoc: it is an isomorphism of topological rings, and compatible with the structure maps from A — the property that determines it.

Provenance

The bundle-and-refinement section is adapted from AINTLIB (see References): the idea of indexing the structure presheaf by presentation data rather than by rational subsets, and the refinement relation between presentations, are StructurePresheafLimit.lean's. The bundling differs deliberately — AINTLIB threads RationalLocData records through explicit hypotheses, while here Presentation packs (num, den, hasDenominatorPower) so that refinement is a Preorder and downstream constructions can be functorial. The comparison theory in the rest of this file is original to this repository.

References

• C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit 37bbdaeb, projects/AdicSpaces/Adic spaces/StructurePresheafLimit.lean, Apache-2.0.
• T. Wedhorn, Adic Spaces, §8.1–8.2.

The bundle of presentations, and refinement

The comparison theory below works with two presentations given separately; consumers indexing a construction by all presentations — the intended structure presheaf — need them bundled and ordered. Refinement here is a cofactor condition on the presentation data. It is sufficient for containment of the rational subsets. The converse is not claimed, and the gap is not the comparison-map step described above: exists_refinement_of_subset already produces numerator and denominator data from a containment. What it does not supply is the standing HasDenominatorPower hypothesis for the re-presented pair, which is what Presentation requires.

structure TauCeti.Huber.PairOfDefinition.Presentation {A : Type u_1} [CommRing A] [TopologicalSpace A] (P : PairOfDefinition A) : Type u_1

A presentation of a rational localization: a numerator finset, a denominator, and the standing HasDenominatorPower hypothesis for the localization away from the denominator.

• num : Finset A

  The numerators.

• den : A

  The denominator.

• hasDenominatorPower : P.HasDenominatorPower self.num self.den (Localization.Away self.den)

  The denominator-power hypothesis for Localization.Away den.

theorem TauCeti.Huber.PairOfDefinition.Presentation.ext_iff {A : Type u_1} {inst✝ : CommRing A} {inst✝¹ : TopologicalSpace A} {P : PairOfDefinition A} {x y : P.Presentation} : x = y ↔ x.num = y.num ∧ x.den = y.den

theorem TauCeti.Huber.PairOfDefinition.Presentation.ext {A : Type u_1} {inst✝ : CommRing A} {inst✝¹ : TopologicalSpace A} {P : PairOfDefinition A} {x y : P.Presentation} (num : x.num = y.num) (den : x.den = y.den) : x = y

def TauCeti.Huber.PairOfDefinition.Presentation.RefinedBy {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p q : P.Presentation) : Prop

The refinement relation: q refines p when some cofactor r has q.den = p.den * r and carries every numerator of p into a numerator of q.

Equations

• p.RefinedBy q = ∃ (r : A), q.den = p.den * r ∧ ∀ t ∈ p.num, t * r ∈ q.num

theorem TauCeti.Huber.PairOfDefinition.Presentation.refinedBy_witness_one {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p : P.Presentation) : p.den = p.den * 1 ∧ ∀ t ∈ p.num, t * 1 ∈ p.num

The witness facts for the trivial refinement, with cofactor 1.

theorem TauCeti.Huber.PairOfDefinition.Presentation.refinedBy_witness_mul {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} {p q w : P.Presentation} {r r₂ : A} (hr : q.den = p.den * r) (hT : ∀ t ∈ p.num, t * r ∈ q.num) (hr₂ : w.den = q.den * r₂) (hT₂ : ∀ t ∈ q.num, t * r₂ ∈ w.num) : w.den = p.den * (r * r₂) ∧ ∀ t ∈ p.num, t * (r * r₂) ∈ w.num

The witness facts for a composite refinement: the cofactors multiply.

theorem TauCeti.Huber.PairOfDefinition.Presentation.RefinedBy.refl {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p : P.Presentation) : p.RefinedBy p

Every presentation refines itself, with cofactor 1.

theorem TauCeti.Huber.PairOfDefinition.Presentation.RefinedBy.trans {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} {p q w : P.Presentation} (hpq : p.RefinedBy q) (hqw : q.RefinedBy w) : p.RefinedBy w

Refinements compose: the cofactors multiply.

@[instance_reducible]

instance TauCeti.Huber.PairOfDefinition.instPreorderPresentation {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} : Preorder P.Presentation

Refinement is a preorder, by Presentation.RefinedBy.refl and Presentation.RefinedBy.trans.

These two stay as named theorems rather than being inlined into the fields below. The instance is public, so its body is exposed for typeclass resolution and cannot unfold RefinedBy, whose body this file deliberately does not export — inlining gives Invalid ⟨...⟩ notation: The expected type p.RefinedBy p is not an inductive type. A theorem body is not exposed, so it may unfold it; that asymmetry is what forces the two names.

Equations

• TauCeti.Huber.PairOfDefinition.instPreorderPresentation = { le := TauCeti.Huber.PairOfDefinition.Presentation.RefinedBy, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem TauCeti.Huber.PairOfDefinition.Presentation.le_def {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} {p q : P.Presentation} : p ≤ q ↔ ∃ (r : A), q.den = p.den * r ∧ ∀ t ∈ p.num, t * r ∈ q.num

The refinement preorder, unfolded in one step: the single introduction/elimination lemma for ≤. The body of RefinedBy is not exported, so this is the route from p ≤ q to a cofactor.

le_def, not le_iff: this is the one-step definitional unfolding of a custom ≤, which is what Mathlib names le_def (Order/Quotient.lean, Order/Hom/Basic.lean, Order/Preorder/Finsupp.lean, several of them .rfl as here). Bare le_iff there is reserved for characterisations that are not the definition.

noncomputable def TauCeti.Huber.PairOfDefinition.Presentation.commonRefinement {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p q : P.Presentation) : P.Presentation

The common refinement, refining both factors: the numerators are the pairwise products of the factors' numerator sets augmented by their own denominators, and the denominator is the product. The augmentation matches rationalSubset_inter's presentation of an intersection.

Presentation carries no openness or admissibility field, so nothing here tracks or preserves openness of the numerator ideal; a consumer that needs it — the structure presheaf's index — must carry and re-establish it itself.

Equations

• p.commonRefinement q = { num := insert p.den p.num * insert q.den q.num, den := p.den * q.den, hasDenominatorPower := ⋯ }

@[simp]

theorem TauCeti.Huber.PairOfDefinition.Presentation.commonRefinement_num {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p q : P.Presentation) : (p.commonRefinement q).num = insert p.den p.num * insert q.den q.num

The numerator equation for the common refinement. The body of commonRefinement is not exported, so this is how a consumer computes with it — in particular, how it is matched against rationalSubset_inter's presentation of an intersection.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.Presentation.commonRefinement_den {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p q : P.Presentation) : (p.commonRefinement q).den = p.den * q.den

The denominator equation for the common refinement.

theorem TauCeti.Huber.PairOfDefinition.Presentation.le_commonRefinement_left {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p q : P.Presentation) : p ≤ p.commonRefinement q

The common refinement refines its left factor, with cofactor the right denominator.

theorem TauCeti.Huber.PairOfDefinition.Presentation.le_commonRefinement_right {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} (p q : P.Presentation) : q ≤ p.commonRefinement q

The common refinement refines its right factor, with cofactor the left denominator.

instance TauCeti.Huber.PairOfDefinition.instIsDirectedPresentationLe {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : PairOfDefinition A} : IsDirected P.Presentation fun (x1 x2 : P.Presentation) => x1 ≤ x2

The refinement preorder is directed: any two presentations admit a common refinement, namely Presentation.commonRefinement. So presentations of the same rational subset never sit as independent factors in a limit over this order — both map onwards to a common refinement. The existential form is exists_ge_ge, which this instance supplies generically.

Comparing two presentations of the same subset

theorem TauCeti.Huber.PairOfDefinition.comp_eq_id_of_comp_toCompletionLoc_eq {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S) : Continuous ⇑g → Continuous ⇑h → g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden' → h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T s S hden → h.comp g = RingHom.id (UniformSpace.Completion S)

Compatible comparison maps between two presentations are mutually inverse. If g carries the structure map of A⟨T/s⟩ to that of A⟨T'/s'⟩ and h carries it back, then h ∘ g fixes the structure map of A⟨T/s⟩, so it is the identity.

noncomputable def TauCeti.Huber.PairOfDefinition.presentationRingEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S) : Continuous ⇑g → Continuous ⇑h → g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden' → h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T s S hden → UniformSpace.Completion S ≃+* UniformSpace.Completion S'

The comparison isomorphism between two presentations. Comparison maps in both directions that are compatible with the structure maps from A assemble into a ring isomorphism, because each composite fixes a structure map and is therefore the identity.

This is the canonical half of presentation independence: it says the comparison is an isomorphism and is determined by compatibility, not that the compatibility hypotheses hold for two presentations of the same rational subset. Supplying those is a separate step: TauCeti.ValuationSpectrum.presentationRingEquivOfEq derives them from an equality of rational subsets through Wedhorn's Proposition 8.2(1).

Equations

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

theorem TauCeti.Huber.PairOfDefinition.eq_comp_of_comp_toCompletionLoc_eq_three {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (T'' : Finset A) (s'' : A) (S'' : Type u_4) [CommRing S''] [Algebra A S''] [IsLocalization.Away s'' S''] (hden'' : P.HasDenominatorPower T'' s'' S'') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S'') (k : UniformSpace.Completion S →+* UniformSpace.Completion S'') : Continuous ⇑g → Continuous ⇑h → Continuous ⇑k → g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden' → h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T'' s'' S'' hden'' → k.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T'' s'' S'' hden'' → k = h.comp g

Compatibility for three presentations. A comparison map from the first presentation to the third is the composite of the comparisons through the second, whenever all three are compatible with the structure maps from A. This is the cocycle condition that makes the comparisons a coherent system rather than a family of unrelated isomorphisms.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.presentationRingEquiv_coe {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S) (hg : Continuous ⇑g) (hh : Continuous ⇑h) (hgc : g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden') (hhc : h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T s S hden) : ↑(P.presentationRingEquiv T s S hden T' s' S' hden' g h hg hh hgc hhc) = g

The comparison isomorphism is the map it was built from. The characteristic equation of presentationRingEquiv: it does not introduce a new map, it packages g together with the inverse supplied by h.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.presentationRingEquiv_symm_coe {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S) (hg : Continuous ⇑g) (hh : Continuous ⇑h) (hgc : g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden') (hhc : h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T s S hden) : ↑(P.presentationRingEquiv T s S hden T' s' S' hden' g h hg hh hgc hhc).symm = h

The inverse of the comparison isomorphism is the backward map it was built from.

theorem TauCeti.Huber.PairOfDefinition.continuous_presentationRingEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S) (hg : Continuous ⇑g) (hh : Continuous ⇑h) (hgc : g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden') (hhc : h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T s S hden) : Continuous ⇑(P.presentationRingEquiv T s S hden T' s' S' hden' g h hg hh hgc hhc)

The comparison isomorphism is continuous, being g.

theorem TauCeti.Huber.PairOfDefinition.continuous_presentationRingEquiv_symm {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S) (hg : Continuous ⇑g) (hh : Continuous ⇑h) (hgc : g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden') (hhc : h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T s S hden) : Continuous ⇑(P.presentationRingEquiv T s S hden T' s' S' hden' g h hg hh hgc hhc).symm

The comparison isomorphism has a continuous inverse, being h. With continuous_presentationRingEquiv this makes it an isomorphism of topological rings.

theorem TauCeti.Huber.PairOfDefinition.presentationRingEquiv_coe_comp_toCompletionLoc {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (h : UniformSpace.Completion S' →+* UniformSpace.Completion S) (hg : Continuous ⇑g) (hh : Continuous ⇑h) (hgc : g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden') (hhc : h.comp (P.toCompletionLoc T' s' S' hden') = P.toCompletionLoc T s S hden) : (↑(P.presentationRingEquiv T s S hden T' s' S' hden' g h hg hh hgc hhc)).comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T' s' S' hden'

The comparison isomorphism is compatible with the structure maps from A, which is the property that determines it.