Ideals and quotients of topological rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define ideal.closure to be the topological closure of an ideal in a topological ring. We also define a topological_space structure on the quotient of a topological ring by an ideal and prove that the quotient is a topological ring.

source

@[protected]

def ideal.closure {R : Type u_1} [topological_space R] [ring R] [topological_ring 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' := _}

source

@[simp]

theorem ideal.coe_closure {R : Type u_1} [topological_space R] [ring R] [topological_ring R] (I : ideal R) :

↑(I.closure) = closure ↑I

source

@[simp]

theorem ideal.closure_eq_of_is_closed {R : Type u_1} [topological_space R] [ring R] [topological_ring R] (I : ideal R) [hI : is_closed ↑I] :

I.closure = I

source

@[protected, instance]

def topological_ring_quotient_topology {R : Type u_1} [topological_space R] [comm_ring R] (N : ideal R) :

topological_space (R ⧸ N)

Equations

topological_ring_quotient_topology N = quotient.topological_space

source

theorem quotient_ring.is_open_map_coe {R : Type u_1} [topological_space R] [comm_ring R] (N : ideal R) [topological_ring R] :

is_open_map ⇑(ideal.quotient.mk N)

source

theorem quotient_ring.quotient_map_coe_coe {R : Type u_1} [topological_space R] [comm_ring R] (N : ideal R) [topological_ring R] :

quotient_map (λ (p : R × R), (⇑(ideal.quotient.mk N) p.fst, ⇑(ideal.quotient.mk N) p.snd))

source

@[protected, instance]

def topological_ring_quotient {R : Type u_1} [topological_space R] [comm_ring R] (N : ideal R) [topological_ring R] :

topological_ring (R ⧸ N)