# Ideals and quotients of topological rings #

In this file we define `Ideal.closure`

to be the topological closure of an ideal in a topological
ring. We also define a `TopologicalSpace`

structure on the quotient of a topological ring by an
ideal and prove that the quotient is a topological ring.

def
Ideal.closure
{R : Type u_1}
[TopologicalSpace R]
[Ring R]
[TopologicalRing R]
(I : Ideal R)
:

Ideal R

The closure of an ideal in a topological ring as an ideal.

## Instances For

@[simp]

theorem
Ideal.coe_closure
{R : Type u_1}
[TopologicalSpace R]
[Ring R]
[TopologicalRing R]
(I : Ideal R)
:

↑(Ideal.closure I) = closure ↑I

theorem
Ideal.closure_eq_of_isClosed
{R : Type u_1}
[TopologicalSpace R]
[Ring R]
[TopologicalRing R]
(I : Ideal R)
(hI : IsClosed ↑I)
:

Ideal.closure I = I

instance
topologicalRingQuotientTopology
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
:

TopologicalSpace (R ⧸ N)

theorem
QuotientRing.isOpenMap_coe
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
[TopologicalRing R]
:

theorem
QuotientRing.quotientMap_coe_coe
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
[TopologicalRing R]
:

QuotientMap fun p => (↑(Ideal.Quotient.mk N) p.fst, ↑(Ideal.Quotient.mk N) p.snd)

instance
topologicalRing_quotient
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
[TopologicalRing R]
:

TopologicalRing (R ⧸ N)