# 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.

## Equations

## Instances For

@[simp]

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

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

I.closure = I

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

TopologicalSpace (R ⧸ N)

## Equations

- topologicalRingQuotientTopology N = instTopologicalSpaceQuotient

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 : R × R) => ((Ideal.Quotient.mk N) p.1, (Ideal.Quotient.mk N) p.2)

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

TopologicalRing (R ⧸ N)

## Equations

- ⋯ = ⋯