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
- One or more equations did not get rendered due to their size.
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)
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 => (↑(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)