feat(analysis/normed_space/units): maximal ideals in complete normed …

…rings are closed (#16303)

src/analysis/normed_space/units.lean

@@ -81,6 +81,19 @@ is_open.mem_nhds units.is_open x.is_unit
 
 end units
 
+namespace nonunits
+
+/-- The `nonunits` in a complete normed ring are contained in the complement of the ball of radius
+`1` centered at `1 : R`. -/
+lemma subset_compl_ball : nonunits R ⊆ (metric.ball (1 : R) 1)ᶜ :=
+set.subset_compl_comm.mp $ λ x hx, by simpa [sub_sub_self, units.coe_one_sub] using
+  (units.one_sub (1 - x) (by rwa [metric.mem_ball, dist_eq_norm, norm_sub_rev] at hx)).is_unit
+
+/- The `nonunits` in a complete normed ring are a closed set -/
+protected lemma is_closed : is_closed (nonunits R) := units.is_open.is_closed_compl
+
+end nonunits
+
 namespace normed_ring
 open_locale classical big_operators
 open asymptotics filter metric finset ring
@@ -288,3 +301,25 @@ lemma open_embedding_coe : open_embedding (coe : Rˣ → R) :=
 open_embedding_of_continuous_injective_open continuous_coe ext is_open_map_coe
 
 end units
+
+namespace ideal
+
+/-- An ideal which contains an element within `1` of `1 : R` is the unit ideal. -/
+lemma eq_top_of_norm_lt_one (I : ideal R) {x : R} (hxI : x ∈ I) (hx : ∥1 - x∥ < 1) : I = ⊤ :=
+let u := units.one_sub (1 - x) hx in (I.eq_top_iff_one.mpr $
+  by simpa only [show u.inv * x = 1, by simp] using I.mul_mem_left u.inv hxI)
+
+/-- The `ideal.closure` of a proper ideal in a complete normed ring is proper. -/
+lemma closure_ne_top (I : ideal R) (hI : I ≠ ⊤) : I.closure ≠ ⊤ :=
+have h : _ := closure_minimal (coe_subset_nonunits hI) nonunits.is_closed,
+  by simpa only [I.closure.eq_top_iff_one, ne.def] using mt (@h 1) one_not_mem_nonunits
+
+/-- The `ideal.closure` of a maximal ideal in a complete normed ring is the ideal itself. -/
+lemma is_maximal.closure_eq {I : ideal R} (hI : I.is_maximal) : I.closure = I :=
+(hI.eq_of_le (I.closure_ne_top hI.ne_top) subset_closure).symm
+
+/-- Maximal ideals in complete normed rings are closed. -/
+instance is_maximal.is_closed {I : ideal R} [hI : I.is_maximal] : is_closed (I : set R) :=
+is_closed_of_closure_subset $ eq.subset $ congr_arg (coe : ideal R → set R) hI.closure_eq
+
+end ideal

src/topology/algebra/ring.lean

@@ -285,8 +285,8 @@ def subring.comm_ring_topological_closure [t2_space α] (s : subring α)
 
 end topological_semiring
 
-section topological_comm_ring
-variables {α : Type*} [topological_space α] [comm_ring α] [topological_ring α]
+section topological_ring
+variables {α : Type*} [topological_space α] [ring α] [topological_ring α]
 
 /-- The closure of an ideal in a topological ring as an ideal. -/
 def ideal.closure (S : ideal α) : ideal α :=
@@ -296,7 +296,7 @@ def ideal.closure (S : ideal α) : ideal α :=
 
 @[simp] lemma ideal.coe_closure (S : ideal α) : (S.closure : set α) = closure S := rfl
 
-end topological_comm_ring
+end topological_ring
 
 section topological_ring
 variables {α : Type*} [topological_space α] [comm_ring α] (N : ideal α)