Localization of topological rings

The topological localization of a topological commutative ring R at a submonoid M is the ring Localization M endowed with the final ring topology of the natural homomorphism sending x : R to the equivalence class of (x, 1) in the localization of R at an M.

Main Results

• Localization.ringTopology: The localization of a topological commutative ring at a submonoid is a topological ring.

def Localization.ringTopology {R : Type u_1} [CommRing R] [TopologicalSpace R] {M : Submonoid R} : RingTopology (Localization M)

The ring topology on Localization M coinduced from the natural homomorphism sending x : R to the equivalence class of (x, 1).

Equations

• Localization.ringTopology = RingTopology.coinduced (↑(Localization.monoidOf M).toMonoidHom).toFun

instance instTopologicalSpaceLocalizationToCommMonoid {R : Type u_1} [CommRing R] [TopologicalSpace R] {M : Submonoid R} : TopologicalSpace (Localization M)

Equations

• instTopologicalSpaceLocalizationToCommMonoid = Localization.ringTopology.toTopologicalSpace

instance instTopologicalRingLocalizationToCommMonoidInstTopologicalSpaceLocalizationToCommMonoidToNonUnitalNonAssocRingToNonUnitalNonAssocCommRingToNonUnitalCommRingInstCommRingLocalizationToCommMonoid {R : Type u_1} [CommRing R] [TopologicalSpace R] {M : Submonoid R} : TopologicalRing (Localization M)

Equations

• (_ : TopologicalRing (Localization M)) = (_ : TopologicalRing (Localization M))