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 a M.
Main Results #
localization.topological_ring: The localization of a topological commutative ring at a submonoid is a topological ring.
def
localization.ring_topology
{R : Type u_1}
[comm_ring R]
[topological_space R]
{M : submonoid R} :
The ring topology on localization M coinduced from the natural homomorphism sending x : R
to the equivalence class of (x, 1).
@[protected, instance]
def
localization.topological_space
{R : Type u_1}
[comm_ring R]
[topological_space R]
{M : submonoid R} :
@[protected, instance]
def
localization.topological_ring
{R : Type u_1}
[comm_ring R]
[topological_space R]
{M : submonoid R} :