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

• I.closure = { carrier := closure ↑I, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

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

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] : IsOpenMap ⇑(Ideal.Quotient.mk N)

theorem QuotientRing.isOpenQuotientMap_mk {R : Type u_1} [TopologicalSpace R] [CommRing R] (N : Ideal R) [TopologicalRing R] : IsOpenQuotientMap ⇑(Ideal.Quotient.mk N)

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

• ⋯ = ⋯