feat(Topology/UniformSpace/DiscreteUniformity): discrete uniformity (#23067)

Author: AntoineChambert-Loir

Mathlib.lean

@@ -6051,6 +6051,7 @@ import Mathlib.Topology.UniformSpace.CompleteSeparated
 import Mathlib.Topology.UniformSpace.Completion
 import Mathlib.Topology.UniformSpace.Defs
 import Mathlib.Topology.UniformSpace.Dini
+import Mathlib.Topology.UniformSpace.DiscreteUniformity
 import Mathlib.Topology.UniformSpace.Equicontinuity
 import Mathlib.Topology.UniformSpace.Equiv
 import Mathlib.Topology.UniformSpace.HeineCantor

Mathlib/RingTheory/LaurentSeries.lean

@@ -11,7 +11,7 @@ import Mathlib.RingTheory.HahnSeries.Summable
 import Mathlib.RingTheory.PowerSeries.Inverse
 import Mathlib.RingTheory.PowerSeries.Trunc
 import Mathlib.RingTheory.Localization.FractionRing
-import Mathlib.Topology.UniformSpace.Cauchy
+import Mathlib.Topology.UniformSpace.DiscreteUniformity
 import Mathlib.Algebra.Group.Int.TypeTags
 
 
@@ -738,12 +738,12 @@ theorem uniformContinuous_coeff {uK : UniformSpace K} (d : ℤ) :
 in `K` converges to a principal filter -/
 def Cauchy.coeff {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) : ℤ → K :=
   let _ : UniformSpace K := ⊥
-  fun d ↦ UniformSpace.DiscreteUnif.cauchyConst rfl <| hℱ.map (uniformContinuous_coeff d)
+  fun d ↦ DiscreteUniformity.cauchyConst <| hℱ.map (uniformContinuous_coeff d)
 
 theorem Cauchy.coeff_tendsto {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) (D : ℤ) :
     Tendsto (fun f : K⸨X⸩ ↦ f.coeff D) ℱ (𝓟 {coeff hℱ D}) :=
   let _ : UniformSpace K := ⊥
-  le_of_eq <| UniformSpace.DiscreteUnif.eq_const_of_cauchy (by rfl)
+  le_of_eq <| DiscreteUniformity.eq_pure_cauchyConst
     (hℱ.map (uniformContinuous_coeff D)) ▸ (principal_singleton _).symm
 
 /- For every Cauchy filter of Laurent series, there is a `N` such that the `n`-th coefficient

Mathlib/Topology/UniformSpace/Cauchy.lean

@@ -814,29 +814,4 @@ theorem secondCountable_of_separable [SeparableSpace α] : SecondCountableTopolo
     refine ⟨_, ⟨y, hys, k, rfl⟩, (hts k).subset hxy, fun z hz => ?_⟩
     exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))
 
-section DiscreteUniformity
-
-open Filter
-
-/-- A Cauchy filter in a discrete uniform space is contained in a principal filter. -/
-theorem DiscreteUnif.cauchy_le_pure {X : Type*} {uX : UniformSpace X}
-    (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : ∃ x : X, α = pure x := by
-  rcases hα with ⟨α_ne_bot, α_le⟩
-  rw [hX, bot_uniformity, le_principal_iff, mem_prod_iff] at α_le
-  obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := α_le
-  obtain ⟨x, rfl⟩ := eq_singleton_left_of_prod_subset_idRel (α_ne_bot.nonempty_of_mem hS)
-    (Filter.nonempty_of_mem hT) H
-  exact ⟨x, α_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩
-
-/-- A constant to which a Cauchy filter in a discrete uniform space converges. -/
-noncomputable def DiscreteUnif.cauchyConst {X : Type*} {uX : UniformSpace X}
-    (hX : uX = ⊥) {α : Filter X} (hα : Cauchy α) : X :=
-  (DiscreteUnif.cauchy_le_pure hX hα).choose
-
-theorem DiscreteUnif.eq_const_of_cauchy {X : Type*} {uX : UniformSpace X} (hX : uX = ⊥)
-    {α : Filter X} (hα : Cauchy α) : α = pure (DiscreteUnif.cauchyConst hX hα) :=
-  (DiscreteUnif.cauchy_le_pure hX hα).choose_spec
-
-end DiscreteUniformity
-
 end UniformSpace

Mathlib/Topology/UniformSpace/DiscreteUniformity.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2024 Antoine Chambert-Loir, María Inés de Frutos Fernández. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro, Antoine Chambert-Loir, María Inés de Frutos Fernández
+-/
+import Mathlib.Topology.UniformSpace.Cauchy
+import Mathlib.Topology.Algebra.UniformGroup.Defs
+
+/-! # Discrete uniformity
+
+The discrete uniformity is the smallest possible uniformity, the one for which
+the diagonal is an entourage of itself.
+
+It induces the discrete topology.
+
+It is complete.
+
+-/
+
+open Filter UniformSpace
+
+/-- The discrete uniformity -/
+@[mk_iff discreteUniformity_iff_eq_bot]
+class DiscreteUniformity (X : Type*) [u : UniformSpace X] : Prop where
+  eq_bot : u = ⊥
+
+namespace DiscreteUniformity
+
+/-- The bot uniformity is the discrete uniformity. -/
+instance (X : Type*) : @DiscreteUniformity X ⊥ :=
+  @DiscreteUniformity.mk X ⊥ rfl
+
+variable (X : Type*) [u : UniformSpace X] [DiscreteUniformity X]
+
+theorem _root_.discreteUniformity_iff_eq_principal_idRel {X : Type*} [UniformSpace X] :
+    DiscreteUniformity X ↔ uniformity X = principal idRel := by
+  rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]
+
+theorem eq_principal_idRel : uniformity X = principal idRel :=
+  discreteUniformity_iff_eq_principal_idRel.mp inferInstance
+
+/-- The discrete uniformity induces the discrete topology. -/
+instance : DiscreteTopology X where
+  eq_bot := by
+    rw [DiscreteUniformity.eq_bot (X := X), UniformSpace.toTopologicalSpace_bot]
+
+theorem _root_.discreteUniformity_iff_idRel_mem_uniformity {X : Type*} [UniformSpace X] :
+    DiscreteUniformity X ↔ idRel ∈ uniformity X := by
+  rw [← uniformSpace_eq_bot, discreteUniformity_iff_eq_bot]
+
+theorem idRel_mem_uniformity : idRel ∈ uniformity X :=
+  discreteUniformity_iff_idRel_mem_uniformity.mp inferInstance
+
+variable {X} in
+/-- A product of spaces with discrete uniformity has a discrete uniformity. -/
+instance {Y : Type*} [UniformSpace Y] [DiscreteUniformity Y] :
+    DiscreteUniformity (X × Y) := by
+  simp [discreteUniformity_iff_eq_principal_idRel, uniformity_prod_eq_comap_prod,
+    eq_principal_idRel, idRel, Set.prod_eq, Prod.ext_iff, Set.setOf_and]
+
+variable {x} in
+/-- On a space with a discrete uniformity, any function is uniformly continuous. -/
+theorem uniformContinuous {Y : Type*} [UniformSpace Y] (f : X → Y) :
+    UniformContinuous f := by
+  simp only [uniformContinuous_iff, DiscreteUniformity.eq_bot, bot_le]
+
+/-- The discrete uniformity makes a group a `UniformGroup. -/
+@[to_additive "The discrete uniformity makes an additive group a `UniformAddGroup`."]
+instance [Group X] : UniformGroup X where
+  uniformContinuous_div := uniformContinuous (X × X) fun p ↦ p.1 / p.2
+
+variable {X} in
+/-- A Cauchy filter in a discrete uniform space is contained in the principal filter
+of a point. -/
+theorem eq_pure_of_cauchy {α : Filter X} (hα : Cauchy α) : ∃ x : X, α = pure x := by
+  rcases hα with ⟨α_ne_bot, α_le⟩
+  simp only [DiscreteUniformity.eq_principal_idRel, le_principal_iff, mem_prod_iff] at α_le
+  obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := α_le
+  obtain ⟨x, rfl⟩ := eq_singleton_left_of_prod_subset_idRel (α_ne_bot.nonempty_of_mem hS)
+    (Filter.nonempty_of_mem hT) H
+  exact ⟨x, α_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩
+
+@[deprecated (since := "2025-03-23")]
+alias _root_.UniformSpace.DiscreteUnif.cauchy_le_pure := eq_pure_of_cauchy
+
+/-- The discrete uniformity makes a space complete. -/
+instance : CompleteSpace X where
+  complete {f} hf := by
+    obtain ⟨x, rfl⟩ := eq_pure_of_cauchy hf
+    exact ⟨x, pure_le_nhds x⟩
+
+variable {X}
+
+/-- A constant to which a Cauchy filter in a discrete uniform space converges. -/
+noncomputable def cauchyConst {α : Filter X} (hα : Cauchy α) : X :=
+  (eq_pure_of_cauchy hα).choose
+
+@[deprecated (since := "2025-03-23")]
+alias _root_.UniformSpace.DiscreteUnif.cauchyConst := cauchyConst
+
+theorem eq_pure_cauchyConst {α : Filter X} (hα : Cauchy α) : α = pure (cauchyConst hα) :=
+  (eq_pure_of_cauchy hα).choose_spec
+
+@[deprecated (since := "2025-03-23")]
+alias _root_.UniformSpace.DiscreteUnif.eq_const_of_cauchy := eq_pure_cauchyConst
+
+end DiscreteUniformity