feat(RingTheory): IsAdicComplete I R ↔ CompleteSpace R ∧ T2Space R (leanprover-community#30124)

Author: erdOne

Mathlib/Order/Filter/Bases/Basic.lean

@@ -174,6 +174,9 @@ protected theorem generate (B : FilterBasis α) : generate B.sets = B.filter :=
   · rw [le_generate_iff]
     apply mem_filter_of_mem
 
+lemma ker_filter (F : FilterBasis α) : F.filter.ker = ⋂₀ F.sets := by
+  aesop (add simp [ker, FilterBasis.filter])
+
 end FilterBasis
 
 namespace Filter

Mathlib/RingTheory/AdicCompletion/Basic.lean

@@ -44,6 +44,7 @@ class IsPrecomplete : Prop where
     ∃ L : M, ∀ n, f n ≡ L [SMOD (I ^ n • ⊤ : Submodule R M)]
 
 /-- A module `M` is `I`-adically complete if it is Hausdorff and precomplete. -/
+@[mk_iff]
 class IsAdicComplete : Prop extends IsHausdorff I M, IsPrecomplete I M
 
 variable {I M}

Mathlib/RingTheory/AdicCompletion/Topology.lean

@@ -13,9 +13,23 @@ import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
 ## Main results
 - `IsAdic.isPrecomplete_iff`:
   `IsPrecomplete I R` is equivalent to `CompleteSpace R` in the adic topology.
+- `IsAdic.isAdicComplete_iff`:
+  `IsAdicComplete I R` is equivalent to `CompleteSpace R` and `T2Space R` in the adic topology.
 
 -/
 
+section TopologicalSpace
+
+variable {R : Type*} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsAdic I)
+
+include hI in
+/-- `IsHausdorff I R` is equivalent to being Hausdorff in the adic topology. -/
+protected lemma IsAdic.isHausdorff_iff : IsHausdorff I R ↔ T2Space R := by
+  rw [I.ringFilterBasis.t2Space_iff_sInter_subset hI.symm, isHausdorff_iff]
+  simp [SModEq.zero, Ideal.ringFilterBasis, RingSubgroupsBasis.toRingFilterBasis]
+
+end TopologicalSpace
+
 section UniformSpace
 
 open Topology Uniformity
@@ -53,4 +67,9 @@ protected lemma IsAdic.isPrecomplete_iff : IsPrecomplete I R ↔ CompleteSpace R
       simpa [sub_eq_neg_add] using (hI.hasBasis_nhds L).tendsto_right_iff.mp hL i
     simpa using Ideal.add_mem _ (hN (max i N) le_sup_right) (hf (le_max_left i N))
 
+include hI in
+/-- `IsAdicComplete I R` is equivalent to being complete and hausdorff in the adic topology. -/
+protected lemma IsAdic.isAdicComplete_iff : IsAdicComplete I R ↔ CompleteSpace R ∧ T2Space R := by
+  rw [isAdicComplete_iff, hI.isHausdorff_iff, hI.isPrecomplete_iff, and_comm]
+
 end UniformSpace

Mathlib/Topology/Algebra/FilterBasis.lean

@@ -206,6 +206,20 @@ instance (priority := 100) isTopologicalGroup (B : GroupFilterBasis G) :
     intro U U_in
     exact conj x₀ U_in
 
+@[to_additive]
+lemma t2Space_iff [t : TopologicalSpace G] (F : GroupFilterBasis G)
+    (hG : F.topology = t) : T2Space G ↔ ⋂₀ F.sets = {1} := by
+  have : IsTopologicalGroup G := hG ▸ F.isTopologicalGroup
+  rw [IsTopologicalGroup.t2Space_iff_one_closed, ← closure_eq_iff_isClosed,
+    R0Space.closure_singleton, ← hG, F.nhds_one_eq, FilterBasis.ker_filter]
+
+@[to_additive]
+lemma t2Space_iff_sInter_subset [t : TopologicalSpace G] (F : GroupFilterBasis G)
+    (hG : F.topology = t) : T2Space G ↔ ⋂₀ F.sets ⊆ {1} := by
+  rw [F.t2Space_iff hG, subset_antisymm_iff, and_iff_left_iff_imp]
+  rintro -
+  simpa using fun _ ↦ F.one
+
 end GroupFilterBasis
 
 /-- A `RingFilterBasis` on a ring is a `FilterBasis` satisfying some additional axioms.

Mathlib/Topology/Separation/Basic.lean

@@ -293,6 +293,9 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i,
     R0Space (∀ i, X i) where
   specializes_symmetric _ _ h := specializes_pi.2 fun i ↦ (specializes_pi.1 h i).symm
 
+lemma R0Space.closure_singleton (x : X) : closure {x} = (𝓝 x).ker := by
+  ext; simp [ker_nhds_eq_specializes, ← specializes_iff_mem_closure, specializes_comm]
+
 /-- In an R₀ space, the closure of a singleton is a compact set. -/
 theorem isCompact_closure_singleton : IsCompact (closure {x}) := by
   refine isCompact_of_finite_subcover fun U hUo hxU ↦ ?_