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)
:
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.isOpenQuotientMap_mk
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
[TopologicalRing R]
:
theorem
QuotientRing.isQuotientMap_coe_coe
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
[TopologicalRing R]
:
Topology.IsQuotientMap fun (p : R × R) => ((Ideal.Quotient.mk N) p.1, (Ideal.Quotient.mk N) p.2)
@[deprecated QuotientRing.isQuotientMap_coe_coe]
theorem
QuotientRing.quotientMap_coe_coe
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
[TopologicalRing R]
:
Topology.IsQuotientMap fun (p : R × R) => ((Ideal.Quotient.mk N) p.1, (Ideal.Quotient.mk N) p.2)
Alias of QuotientRing.isQuotientMap_coe_coe
.
theorem
topologicalRing_quotient
{R : Type u_1}
[TopologicalSpace R]
[CommRing R]
(N : Ideal R)
[TopologicalRing R]
:
TopologicalRing (R ⧸ N)