The localisation topology: the universal property

A ring homomorphism out of Aₛ is continuous as soon as its restriction along algebraMap is and the fractions t/s go to power-bounded elements; and Aₛ is the universal such target. This is the second half of Wedhorn's Proposition and Definition 5.51.

The construction of the topology is in LocalizationTopology.Basic, and the completion A⟨T/s⟩ in LocalizationTopology.Completion.

The power-boundedness prerequisites this needs — isPowerBounded_of_mem_locSubring and isPowerBounded_divBy, which say every element of D, in particular each fraction t/s, is power-bounded — are in LocalizationTopology.Basic and imported from there.

Main results

• continuous_of_continuous_algebraMap_of_isPowerBounded: a sufficient criterion for a ring homomorphism out of Aₛ to be continuous. The converse is not proved here.
• locTopology_congr_pairOfDefinition: the topology on Aₛ does not depend on the pair of definition.
• existsUnique_continuous_ringHom_locTopology: the universal property — a continuous φ : A →+* B inverting s and sending each t/s to a power-bounded element extends to Aₛ in exactly one continuous way.

Provenance

The declarations here other than locTopology_congr_pairOfDefinition are relocated from the AINTLIB port recorded in LocalizationTopology.Basic; see that module's Provenance section for the source file and commit.

References

• T. Wedhorn, Adic Spaces, Proposition and Definition 5.51, §5.6

A sufficient criterion for continuity

theorem TauCeti.Huber.PairOfDefinition.continuous_of_continuous_algebraMap_of_isPowerBounded {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [Ring B] [TopologicalSpace B] [NonarchimedeanRing B] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (f : S →+* B) (hf : Continuous ⇑(f.comp (algebraMap A S))) (hpow : ∀ t ∈ T, IsPowerBounded (f (Localization.divBy t s))) : Continuous ⇑f

A ring homomorphism out of Aₛ is continuous for the localisation topology as soon as its restriction along algebraMap is continuous and the fractions t/s are sent to power-bounded elements. This is a sufficient criterion only; no converse is proved here.

The second hypothesis does real work rather than following from the first: D is generated over A₀ by exactly those fractions, so continuity of f ∘ algebraMap alone says nothing about the image of D.

theorem TauCeti.Huber.PairOfDefinition.locTopology_congr_pairOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P 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) (hden' : P'.HasDenominatorPower T s S) : P.locTopology T s S hden = P'.locTopology T s S hden'

The localisation topology does not depend on the pair of definition. Two pairs of definition for which (T, s) satisfies the standing hypothesis HasDenominatorPower give Aₛ the same topology. Wedhorn's Proposition and Definition 5.51 characterises A(T/s) by a universal property that names no pair of definition; this is the corresponding fact for locTopology, which is built from one.

Compare locTopology_congr, which instead fixes the pair of definition and changes the presentation (T, s) to one with the same ring of definition. When T spans an open ideal, hasDenominatorPower_of_isOpen_span supplies both standing hypotheses.

The universal property

theorem TauCeti.Huber.PairOfDefinition.existsUnique_continuous_ringHom_locTopology {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [NonarchimedeanRing B] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_3) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {φ : A →+* B} (hφ : ContinuousAt (⇑φ) 0) (hs : IsUnit (φ s)) (hpow : ∀ t ∈ T, IsPowerBounded (φ t * ↑hs.unit⁻¹)) : ∃! f : S →+* B, Continuous ⇑f ∧ f.comp (algebraMap A S) = φ

Wedhorn 5.51, the universal property of Aₛ under locTopology. A ring homomorphism φ : A →+* B into a nonarchimedean ring extends to Aₛ in exactly one continuous way, provided φ is continuous, φ s is a unit, and each fraction φ t / φ s is power-bounded.

The condition on the fractions is stated as sufficient, and only that. It is not forced by continuity: a continuous ring homomorphism need not carry power-bounded elements to power-bounded elements — IsBounded.image in Huber/Bounded.lean is stated for the image under a map, and IsBounded.image_of_isOpenMap needs openness on top, precisely because continuity alone does not suffice. Whether some weaker condition is also necessary is not addressed here.

The map itself is Mathlib's IsLocalization.Away.lift, which is purely algebraic and needs no topology; the topology's contribution is that this lift is continuous, supplied by continuous_of_continuous_algebraMap_of_isPowerBounded. Uniqueness is IsLocalization.ringHom_ext and is algebraic too: a homomorphism out of a localisation is already determined by its restriction along algebraMap, so nothing topological enters there.