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] [IsTopologicalRing 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] [IsTopologicalRing R] (I : Ideal R) : ↑I.closure = closure ↑I

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

This is not @[simp] since otherwise it causes timeouts downstream as simp tries and fails to generate an IsClosed instance. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234852.20heartbeats.20of.20the.20linter

def Ideal.connectedComponentOfZero (R : Type u_1) [TopologicalSpace R] [Ring R] [IsTopologicalRing R] : Ideal R

The connected component of zero in a topological ring as an ideal.

Equations

• Ideal.connectedComponentOfZero R = { toAddSubmonoid := (AddSubgroup.connectedComponentOfZero R).toAddSubmonoid, smul_mem' := ⋯ }

@[simp]

theorem Ideal.coe_connectedComponentOfZero (R : Type u_1) [TopologicalSpace R] [Ring R] [IsTopologicalRing R] : ↑(connectedComponentOfZero R) = connectedComponent 0

@[instance_reducible]

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

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

theorem QuotientRing.isQuotientMap_coe_coe {R : Type u_1} [TopologicalSpace R] [CommRing R] (N : Ideal R) [IsTopologicalRing R] : Topology.IsQuotientMap 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) [IsTopologicalRing R] : IsTopologicalRing (R ⧸ N)

instance instCompactSpaceQuotientIdeal {R : Type u_1} [TopologicalSpace R] [CommRing R] (N : Ideal R) [CompactSpace R] : CompactSpace (R ⧸ N)