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} [] [Ring R] [] (I : ) :

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

Equations
• I.closure = let __src := I.topologicalClosure; { carrier := closure I, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem Ideal.coe_closure {R : Type u_1} [] [Ring R] [] (I : ) :
I.closure = closure I
theorem Ideal.closure_eq_of_isClosed {R : Type u_1} [] [Ring R] [] (I : ) (hI : IsClosed I) :
I.closure = I
instance topologicalRingQuotientTopology {R : Type u_1} [] [] (N : ) :
Equations
• = instTopologicalSpaceQuotient
theorem QuotientRing.isOpenMap_coe {R : Type u_1} [] [] (N : ) [] :
theorem QuotientRing.quotientMap_coe_coe {R : Type u_1} [] [] (N : ) [] :
QuotientMap fun (p : R × R) => ( p.1, p.2)
instance topologicalRing_quotient {R : Type u_1} [] [] (N : ) [] :
Equations
• =