mathlib3 documentation

topology.algebra.localization

Localization of topological rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 a M.

Main Results #

source
def localization.ring_topology {R : Type u_1} [comm_ring R] [topological_space R] {M : submonoid R} :
ring_topology (localization M)

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

Equations
source
@[protected, instance]
def localization.topological_space {R : Type u_1} [comm_ring R] [topological_space R] {M : submonoid R} :
topological_space (localization M)
Equations
source
@[protected, instance]
def localization.topological_ring {R : Type u_1} [comm_ring R] [topological_space R] {M : submonoid R} :
topological_ring (localization M)