A⟨T/s⟩ is a complete separated topological ring

The adic structure presheaf (roadmap Layer 3.3) assigns A⟨T/s⟩ to the rational subset R(T/s), and its values are required to be complete separated topological rings (Adic Spaces, arXiv:1910.05934v1, §8.1–§8.2). This module supplies the categorical packaging that assignment needs: it exhibits A⟨T/s⟩ as an object of CompleteSeparatedTopCommRingCat, lifts continuous comparison maps to morphisms, and packages mutually compatible comparisons as isomorphisms.

No presheaf exists yet, and the objects here remain presentationwise: they depend on the data (T, s, S, hden) presenting the localisation, not only on the subset R(T/s). The isomorphism constructed here is conditional on compatible comparison maps in both directions. Producing those maps from equality of rational subsets, and constructing restriction maps from containments, are separate steps.

Nothing here is deep — A⟨T/s⟩ is a separated completion, so it is complete and Hausdorff for its own uniformity, and CompleteSeparatedTopCommRingCat.of bundles exactly that. What the module supplies is the bookkeeping: locTopology is not an instance, so the uniform structures on Aₛ are not in scope by inference, and a consumer would otherwise repeat the three-declaration preamble locUniformSpace, isUniformAddGroup_locUniformSpace, isTopologicalRing_locUniformSpace at every use. The definition below carries it once.

Main definitions

• TauCeti.Huber.PairOfDefinition.completionLocObj : A⟨T/s⟩ as an object of CompleteSeparatedTopCommRingCat, presentationwise in (T, s, S, hden).
• TauCeti.Huber.PairOfDefinition.completionLocObjHom : a continuous comparison map as a morphism between presentationwise objects.
• TauCeti.Huber.PairOfDefinition.completionLocObjIso : compatible comparisons in both directions as an isomorphism of complete separated topological rings.

Main results

• TauCeti.Huber.PairOfDefinition.completionLocObj_obj : the underlying TopCommRingCat of that object is UniformSpace.Completion S with the topology locUniformSpace induces.
• TauCeti.Huber.PairOfDefinition.completionLocObj_congr_pairOfDefinition : the object does not depend on the pair of definition.
• TauCeti.Huber.PairOfDefinition.completionLocObjHom_eq_id and TauCeti.Huber.PairOfDefinition.completionLocObjHom_eq_comp : identity and composition for comparison morphisms compatible with the structure maps from A.

Provenance

The packaging here is this repository's own, built on the localisation topology of LocalizationTopology.Basic, which is the AINTLIB port — see that module's Provenance section for the source file and commit. AINTLIB's own structure-presheaf files supplied nothing here: it carries the codomain fact inside its presheaf construction rather than as a separate object, so there was nothing at this granularity to port.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1–§8.2, where the structure presheaf of an adic space is built with complete separated topological rings as its codomain.
• T. Wedhorn, Adic Spaces, Proposition and Definition 5.51, §5.6, for A⟨T/s⟩ itself, which LocalizationTopology.Completion constructs.

A⟨T/s⟩ as an object of CompleteSeparatedTopCommRingCat

noncomputable def TauCeti.Huber.PairOfDefinition.completionLocObj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : CompleteSeparatedTopCommRingCat

A⟨T/s⟩ as an object of CompleteSeparatedTopCommRingCat: the separated completion of Aₛ under locTopology, which is complete and Hausdorff for its own uniformity.

This is the object the adic structure presheaf is intended to take on the rational subset R(T/s); it is presentationwise, depending on (T, s, S, hden) and not yet known to depend only on R(T/s), and the restriction maps are later work.

completionLocObj_obj identifies the underlying object; the body is not exported, so that is how a consumer computes with it.

Equations

• P.completionLocObj T s S hden = TauCeti.CompleteSeparatedTopCommRingCat.of (UniformSpace.Completion S)

@[simp]

theorem TauCeti.Huber.PairOfDefinition.completionLocObj_obj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) : (P.completionLocObj T s S hden).obj = ↧(UniformSpace.Completion S)

The underlying topological ring of completionLocObj is A⟨T/s⟩ itself: the completion of Aₛ for the uniformity locUniformSpace.

theorem TauCeti.Huber.PairOfDefinition.completionLocObj_congr_pairOfDefinition {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P P' : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hden' : P'.HasDenominatorPower T s S) : P.completionLocObj T s S hden = P'.completionLocObj T s S hden'

A⟨T/s⟩ does not depend on the pair of definition. Two pairs of definition for which (T, s) satisfies the standing hypothesis HasDenominatorPower give the same object of CompleteSeparatedTopCommRingCat. When T spans an open ideal, hasDenominatorPower_of_isOpen_span supplies that hypothesis for every pair of definition.

The corresponding equalities on Aₛ are locTopology_congr_pairOfDefinition (topologies) and locUniformSpace_congr_pairOfDefinition (uniformities). Compare completionLocObjIso, which instead changes the presentation (T, s) and gives an isomorphism from compatible comparison maps.

Comparison morphisms between presentationwise objects

noncomputable def TauCeti.Huber.PairOfDefinition.completionLocObjHom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') : Continuous ⇑g → (P.completionLocObj T s S hden ⟶ P.completionLocObj T' s' S' hden')

A continuous ring homomorphism between two completed localisations, as a morphism between their presentationwise objects in CompleteSeparatedTopCommRingCat.

No compatibility with the structure maps from A is required merely to form the morphism. That compatibility is used by completionLocObjHom_eq_id, completionLocObjHom_eq_comp, and completionLocObjIso.

Equations

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

@[simp]

theorem TauCeti.Huber.PairOfDefinition.completionLocObjHom_hom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (g : UniformSpace.Completion S →+* UniformSpace.Completion S') (hg : Continuous ⇑g) : (P.completionLocObjHom T s S hden T' s' S' hden' g hg).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ⟨g, hg⟩ (CategoryTheory.eqToHom ⋯))

The underlying morphism of completionLocObjHom is the given ring homomorphism, transported across completionLocObj_obj at its source and target.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.completionLocObjHom_eq_id {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (g : UniformSpace.Completion S →+* UniformSpace.Completion S) (hg : Continuous ⇑g) : g.comp (P.toCompletionLoc T s S hden) = P.toCompletionLoc T s S hden → P.completionLocObjHom T s S hden T s S hden g hg = CategoryTheory.CategoryStruct.id (P.completionLocObj T s S hden)

A comparison endomorphism compatible with the structure map from A is the identity morphism of the presentationwise complete separated object.

theorem TauCeti.Huber.PairOfDefinition.completionLocObjHom_eq_comp {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u) [CommRing S'] [Algebra A S'] [IsLocalization.Away s' S'] (hden' : P.HasDenominatorPower T' s' S') (T'' : Finset A) (s'' : A) (S'' : Type u) [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'') (hg : Continuous ⇑g) (hh : Continuous ⇑h) (hk : 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'' → P.completionLocObjHom T s S hden T'' s'' S'' hden'' k hk = CategoryTheory.CategoryStruct.comp (P.completionLocObjHom T s S hden T' s' S' hden' g hg) (P.completionLocObjHom T' s' S' hden' T'' s'' S'' hden'' h hh)

Comparison morphisms compatible with the structure maps from A compose categorically. This is the cocycle law for presentationwise objects in CompleteSeparatedTopCommRingCat.

Isomorphisms between presentationwise objects

noncomputable def TauCeti.Huber.PairOfDefinition.completionLocObjIso {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u) [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 → (P.completionLocObj T s S hden ≅ P.completionLocObj T' s' S' hden')

Compatible comparison maps in both directions give an isomorphism between the associated objects of CompleteSeparatedTopCommRingCat.

This is the categorical form of presentationRingEquiv. As there, the construction is conditional: equality of rational subsets must separately supply the two comparison maps and their compatibility with the structure maps from A.

Equations

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

@[simp]

theorem TauCeti.Huber.PairOfDefinition.completionLocObjIso_hom {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u) [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.completionLocObjIso T s S hden T' s' S' hden' g h hg hh hgc hhc).hom = P.completionLocObjHom T s S hden T' s' S' hden' g hg

The forward morphism of completionLocObjIso is the packaged forward comparison map.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.completionLocObjIso_inv {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (s' : A) (S' : Type u) [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.completionLocObjIso T s S hden T' s' S' hden' g h hg hh hgc hhc).inv = P.completionLocObjHom T' s' S' hden' T s S hden h hh

The inverse morphism of completionLocObjIso is the packaged backward comparison map.