From c90b557c37357c9ecbebf0ac1eac567db2645838 Mon Sep 17 00:00:00 2001
From: Jeremy Tan Jie Rui <e0191785@u.nus.edu>
Date: Thu, 6 Apr 2023 16:41:17 +0000
Subject: [PATCH] feat: port Topology.Algebra.UniformFilterBasis (#3310)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
---
 Mathlib.lean                                  |  1 +
 .../Topology/Algebra/UniformFilterBasis.lean  | 57 +++++++++++++++++++
 2 files changed, 58 insertions(+)
 create mode 100644 Mathlib/Topology/Algebra/UniformFilterBasis.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index d0f75b42c00a3..072264a10fea0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1654,6 +1654,7 @@ import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.Ring.Ideal
 import Mathlib.Topology.Algebra.Semigroup
 import Mathlib.Topology.Algebra.Star
+import Mathlib.Topology.Algebra.UniformFilterBasis
 import Mathlib.Topology.Algebra.UniformGroup
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.Algebra.UniformRing
diff --git a/Mathlib/Topology/Algebra/UniformFilterBasis.lean b/Mathlib/Topology/Algebra/UniformFilterBasis.lean
new file mode 100644
index 0000000000000..c1e1311735913
--- /dev/null
+++ b/Mathlib/Topology/Algebra/UniformFilterBasis.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2021 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot
+
+! This file was ported from Lean 3 source module topology.algebra.uniform_filter_basis
+! leanprover-community/mathlib commit 531db2ef0fdddf8b3c8dcdcd87138fe969e1a81a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Algebra.FilterBasis
+import Mathlib.Topology.Algebra.UniformGroup
+
+/-!
+# Uniform properties of neighborhood bases in topological algebra
+
+This files contains properties of filter bases on algebraic structures that also require the theory
+of uniform spaces.
+
+The only result so far is a characterization of Cauchy filters in topological groups.
+
+-/
+
+
+open uniformity Filter
+
+open Filter
+
+namespace AddGroupFilterBasis
+
+variable {G : Type _} [AddCommGroup G] (B : AddGroupFilterBasis G)
+
+/-- The uniform space structure associated to an abelian group filter basis via the associated
+topological abelian group structure. -/
+protected def uniformSpace : UniformSpace G :=
+  @TopologicalAddGroup.toUniformSpace G _ B.topology B.isTopologicalAddGroup
+#align add_group_filter_basis.uniform_space AddGroupFilterBasis.uniformSpace
+
+/-- The uniform space structure associated to an abelian group filter basis via the associated
+topological abelian group structure is compatible with its group structure. -/
+protected theorem uniformAddGroup : @UniformAddGroup G B.uniformSpace _ :=
+  @comm_topologicalAddGroup_is_uniform G _ B.topology B.isTopologicalAddGroup
+#align add_group_filter_basis.uniform_add_group AddGroupFilterBasis.uniformAddGroup
+
+theorem cauchy_iff {F : Filter G} :
+    @Cauchy G B.uniformSpace F ↔
+      F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ (x) (_ : x ∈ M) (y) (_ : y ∈ M), y - x ∈ U := by
+  letI := B.uniformSpace
+  haveI := B.uniformAddGroup
+  suffices F ×ᶠ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ (x) (_ : x ∈ M) (y) (_ : y ∈ M), y - x ∈ U by
+    constructor <;> rintro ⟨h', h⟩ <;> refine' ⟨h', _⟩ <;> [rwa [← this], rwa [this]]
+  rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
+  change Tendsto _ _ _ ↔ _
+  simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_swap (_ ∈ _) G]
+#align add_group_filter_basis.cauchy_iff AddGroupFilterBasis.cauchy_iff
+
+end AddGroupFilterBasis