[Merged by Bors] - feat(analysis/normed_space/units): maximal ideals in complete normed rings are closed

[j-loreaux]

---

[ADedecker]

Is there a good reason to rely on balls and not just on units.is_open? I mean it doesn't change anything deep but I think it would look cleaner.
Also, I know we have this rule of splitting things into small lemmas, but for example ideal.is_maximal.closure_eq should not be stated separately imo.

For reference, here is my proof:

lemma ideal.is_maximal.is_closed {A : ideal R} (hA : A.is_maximal) : is_closed (A : set R) :=
begin
  have : (A : set R) ⊆ {x | is_unit x}ᶜ,
  { rw set.subset_compl_comm,
    exact λ x hx hxA, hA.ne_top (ideal.eq_top_of_is_unit_mem _ hxA hx) },
  have : _root_.closure (A : set R) ⊆ {x | is_unit x}ᶜ := closure_minimal this
    (is_closed_compl_iff.mpr units.is_open),
  exact is_closed_of_closure_subset (show A.topological_closure ≤ A, from
    ge_of_eq $ hA.eq_of_le ((ideal.ne_top_iff_one _).mpr $ λ h, this h is_unit_one) subset_closure)
end

(I didn't know about nonunits, we should add a lemma saying that it is closed; also I agree that ideal.closure_ne_top should be kept separate like you did because it could be useful)

[j-loreaux]

Thanks for the comments. As for balls, I just did it that way because that's the way I normally think about why it's true. However, as you point out, just going through the fact that nonunits is closed is cleaner, so I've done that. I inserted a lemma that nonunits is closed. I did leave two lemmas about balls that I thought would be useful: nonunits.subset_compl_ball and ideal.eq_top_of_norm_lt_one. As for the two closure lemmas, I left them both because they serve different purposes. The former ideal.is_maximal.closure_eq is useful for rewriting, whereas ideal.is_maximal.is_closed is what you need for quotients to be normed instead of seminormed. As such I made the latter an instance.

[ADedecker]

LGTM 🎉

[dupuisf]

Looks good!

bors d+

[bors]

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests