feat: fine uniformity

Mathlib.lean

@@ -6197,6 +6197,7 @@ import Mathlib.Topology.UniformSpace.Dini
 import Mathlib.Topology.UniformSpace.DiscreteUniformity
 import Mathlib.Topology.UniformSpace.Equicontinuity
 import Mathlib.Topology.UniformSpace.Equiv
+import Mathlib.Topology.UniformSpace.FineUniformity
 import Mathlib.Topology.UniformSpace.HeineCantor
 import Mathlib.Topology.UniformSpace.Matrix
 import Mathlib.Topology.UniformSpace.OfCompactT2
@@ -6210,6 +6211,7 @@ import Mathlib.Topology.UniformSpace.Ultra.Constructions
 import Mathlib.Topology.UniformSpace.UniformConvergence
 import Mathlib.Topology.UniformSpace.UniformConvergenceTopology
 import Mathlib.Topology.UniformSpace.UniformEmbedding
+import Mathlib.Topology.UniformSpace.Uniformizable
 import Mathlib.Topology.UnitInterval
 import Mathlib.Topology.UrysohnsBounded
 import Mathlib.Topology.UrysohnsLemma

Mathlib/Topology/UniformSpace/FineUniformity.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2025 Aaron Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Liu
+-/
+import Mathlib.Topology.UniformSpace.Uniformizable
+
+/-!
+# Fine Uniformity
+
+The fine uniformity on a topological space is the finest uniformity
+compatible with the given topology. In general the topology generated by this uniformity
+is coarser than the ambient topology, they coincide only for completely regular spaces.
+
+The fine uniformity can be seen as a functor from the category of topological spaces and
+continuous maps to the category of uniform spaces and uniformly continuous maps,
+and when seen this way it is the left adjoint to the forgetful functor.
+
+## References
+
+* <https://en.wikipedia.org/wiki/Uniformizable_space#Fine_uniformity>
+-/
+
+variable {α β : Type*} {ι : Sort*}
+
+open Topology Uniformity Set
+
+section
+
+variable (α) in
+/--
+The fine uniformity on a topological space is the finest uniformity
+compatible with the given topology. In general the topology generated by this uniformity
+is coarser than the ambient topology, they coincide only for completely regular spaces.
+-/
+def fineUniformity [TopologicalSpace α] : UniformSpace α :=
+  ⨅ (u : UniformSpace α) (_ : ‹TopologicalSpace α› ≤ u.toTopologicalSpace), u
+
+theorem fineUniformity_mono {t₁ t₂ : TopologicalSpace α} (h : t₁ ≤ t₂) :
+    @fineUniformity α t₁ ≤ @fineUniformity α t₂ :=
+  biInf_mono fun _ => h.trans
+
+theorem monotone_fineUniformity : Monotone (@fineUniformity α) :=
+  @fineUniformity_mono α
+
+theorem gc_fineUniformity :
+    GaloisConnection (@fineUniformity α) (@UniformSpace.toTopologicalSpace α) := by
+  apply GaloisConnection.monotone_intro
+  · exact @UniformSpace.toTopologicalSpace_mono α
+  · exact monotone_fineUniformity
+  · simp [UniformSpace.toTopologicalSpace_iInf]
+  · intro a
+    unfold fineUniformity
+    -- fixme: why does this timeout
+    -- exact iInf₂_le (f := fun u (b : a.toTopologicalSpace ≤ u.toTopologicalSpace) => u) a le_rfl
+    trans ⨅ (_ : a.toTopologicalSpace ≤ a.toTopologicalSpace), a
+    · -- PS: why does `exact` timeout here
+      apply iInf_le (fun u => ⨅ (_ : a.toTopologicalSpace ≤ u.toTopologicalSpace), u) a
+    · exact iInf_le (fun _ => a) le_rfl
+
+theorem fineUniformity_le_iff {t : TopologicalSpace α} {u : UniformSpace α} :
+    @fineUniformity α t ≤ u ↔ t ≤ u.toTopologicalSpace := gc_fineUniformity.le_iff_le
+
+theorem fineUniformity_sup {t₁ t₂ : TopologicalSpace α} :
+    @fineUniformity α (t₁ ⊔ t₂) = @fineUniformity α t₁ ⊔ @fineUniformity α t₂ :=
+  gc_fineUniformity.l_sup
+
+theorem fineUniformity_iSup {t : ι → TopologicalSpace α} :
+    @fineUniformity α (iSup t) = ⨆ i, @fineUniformity α (t i) :=
+  gc_fineUniformity.l_iSup
+
+theorem fineUniformity_sSup {t : Set (TopologicalSpace α)} :
+    @fineUniformity α (sSup t) = ⨆ i ∈ t, @fineUniformity α i :=
+  gc_fineUniformity.l_sSup
+
+theorem fineUniformity_iSup₂ {κ : ι → Sort*} {t : (i : ι) → κ i → TopologicalSpace α} :
+    @fineUniformity α (⨆ (i) (j), t i j) = ⨆ (i) (j), @fineUniformity α (t i j) :=
+  gc_fineUniformity.l_iSup₂
+
+theorem fineUniformity_discrete [TopologicalSpace α] [DiscreteTopology α] :
+    fineUniformity α = ⊥ :=
+  ‹DiscreteTopology α›.eq_bot ▸ gc_fineUniformity.l_bot
+
+theorem toTopologicalSpace_fineUniformity_eq [TopologicalSpace α] [CompletelyRegularSpace α] :
+    (fineUniformity α).toTopologicalSpace = ‹TopologicalSpace α› :=
+  ((gc_fineUniformity.exists_eq_u _).mp
+    (CompletelyRegularSpace.exists_uniformity.elim fun u hu => ⟨u, hu.symm⟩)).symm
+
+theorem fineUniformity_top : @fineUniformity α ⊤ = ⊤ := by
+  ext s
+  rw [top_uniformity, Filter.mem_top]
+  constructor
+  · rw [eq_univ_iff_forall]
+    intro h a
+    have top : ∃ (u : UniformSpace α), ⊤ = u.toTopologicalSpace :=
+      ⟨⊤, UniformSpace.toTopologicalSpace_top⟩
+    rw [gc_fineUniformity.exists_eq_u] at top
+    have comap : Prod.mk a.fst ⁻¹' s ∈
+        Filter.comap (Prod.mk a.fst) (@uniformity α (@fineUniformity α ⊤)) := by
+      rw [Filter.mem_comap_iff_compl]
+      filter_upwards [h] with x hxs ⟨u, hu, hxu⟩
+      subst hxu
+      exact hu hxs
+    rw [← @nhds_eq_comap_uniformity, ← top, nhds_top, Filter.mem_top] at comap
+    change a.snd ∈ Prod.mk a.fst ⁻¹' s
+    rw [comap]
+    exact mem_univ a.snd
+  · rintro rfl
+    exact Filter.univ_mem
+
+theorem uniformContinuous_fineUniformity_iff {t : TopologicalSpace α} {u : UniformSpace β}
+    {f : α → β} : UniformContinuous[@fineUniformity α t, u] f ↔
+    Continuous[t, u.toTopologicalSpace] f := by
+  rw [uniformContinuous_iff, fineUniformity_le_iff, continuous_iff_le_induced,
+    UniformSpace.toTopologicalSpace_comap]
+
+theorem uniformContinuous_fineUniformity_fineUniformity
+    [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) :
+    UniformContinuous[fineUniformity α, fineUniformity β] f := by
+  rw [uniformContinuous_fineUniformity_iff]
+  rw [continuous_iff_coinduced_le] at hf ⊢
+  exact hf.trans (gc_fineUniformity.le_u_l _)
+
+end

Mathlib/Topology/UniformSpace/Uniformizable.lean

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2025 Aaron Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Liu
+-/
+import Mathlib.Topology.Separation.CompletelyRegular
+
+/-!
+# Uniformizable Spaces
+
+A topological space is uniformizable (there exists a uniformity that
+generates the same topology) if it is completely regular.
+
+TODO: Prove the reverse implication too.
+
+## References
+
+* [S. Willard, *General Topology*][Wil04]
+-/
+
+variable {α : Type*}
+
+open Filter Set
+
+section UniformSpace
+variable [UniformSpace α]
+
+proof_wanted UniformSpace.completelyRegularSpace : CompletelyRegularSpace α
+
+end UniformSpace
+
+section TopologicalSpace
+variable [TopologicalSpace α]
+open Real
+
+variable (α) in
+/-
+This definition could be useful in other places, but I've not seen a use yet
+so this is private for now (mainly so I don't have to write api).
+-/
+private def inducedUniformity : UniformSpace α :=
+  UniformSpace.ofCore {
+    uniformity := ⨅ (f : C(α, ℝ)) (ε : ℝ) (_ : ε > 0),
+      principal ((fun p => dist (f p.fst) (f p.snd)) ⁻¹' Iio ε)
+    refl := by
+      simp_rw [le_iInf_iff]
+      simp +contextual
+    symm := by
+      rw [tendsto_iff_comap]
+      apply le_of_eq
+      simp_rw [Filter.comap_iInf, comap_principal, preimage_preimage,
+        Prod.fst_swap, Prod.snd_swap, dist_comm]
+    -- this proof takes four seconds to elaborate on my machine
+    -- TODO: speed this up
+    comp := by
+      intro s hs
+      simp_rw [mem_iInf, iInf_eq_if] at hs
+      obtain ⟨I, hI, U, hs, rfl⟩ := hs
+      have := hI.to_subtype
+      choose J hJ V hs hU using hs
+      have := fun i => (hJ i).to_subtype
+      replace hU : U = fun i => ⋂ j, V i j := funext hU
+      subst hU
+      suffices h : ((fun s => compRel s s) <| ⋂ (i : I) (j : J i) (_ : j.val > 0),
+          (fun p ↦ dist (i.val p.fst) (i.val p.snd)) ⁻¹' Iio (j / 2)) ⊆ ⋂ (i) (j), V i j by
+        refine mem_of_superset ?_ h
+        apply mem_lift'
+        simp_rw [mem_iInf, iInf_eq_if, mem_ite, mem_principal, mem_top]
+        refine ⟨I, hI, _, fun i => ?_, rfl⟩
+        refine ⟨(· / 2) '' J i, (hJ i).image (· / 2),
+          fun j => ⋂ (_ : j.val > 0), (fun p ↦ dist (i.val p.fst) (i.val p.snd)) ⁻¹' Iio j,
+            fun j => ⟨fun hj => ?_, fun hj => by simp [hj]⟩, ?_⟩
+        · simp_rw [iInter_eq_if, if_pos hj, subset_rfl]
+        · apply iInter_congr_of_surjective _ surjective_onto_image
+          intro j
+          simp only [imageFactorization]
+          exact iInter_congr_Prop (by simp) fun _ => rfl
+      simp_rw [subset_iInter_iff]
+      intro i j
+      specialize hs i j
+      split_ifs at hs with hj
+      · intro x hx
+        apply hs
+        rw [mem_compRel] at hx
+        obtain ⟨z, hxz, hzx⟩ := hx
+        simp_rw [mem_iInter] at hxz hzx
+        apply (dist_triangle (i.val x.fst) (i.val z) (i.val x.snd)).trans_lt
+        rw [← add_halves j.val]
+        exact add_lt_add (hxz i j hj) (hzx i j hj)
+      · rw [mem_top] at hs
+        simp [hs]
+  }
+
+private theorem le_u_l :
+    ‹TopologicalSpace α› ≤ (inducedUniformity α).toTopologicalSpace := by
+  intro s hs
+  rw [isOpen_iff_forall_mem_open]
+  rw [@isOpen_iff_ball_subset] at hs
+  intro x hx
+  obtain ⟨V, hV, hVs⟩ := hs x hx
+  change V ∈ iInf _ at hV
+  simp_rw [mem_iInf] at hV
+  obtain ⟨I, hI, U, hU, rfl⟩ := hV
+  have := hI.to_subtype
+  choose J hJ V hV hU using hU
+  have := fun i => (hJ i).to_subtype
+  replace hU : U = fun i => ⋂ j, V i j := funext hU
+  subst hU
+  refine ⟨⋂ (i : I) (j : J i) (_ : j.val > 0), (fun y => dist (i.val x) (i.val y)) ⁻¹' Iio j,
+    ?_, ?_, ?_⟩
+  · apply hVs.trans'
+    simp_rw [UniformSpace.ball, preimage_iInter]
+    apply iInter₂_mono
+    intro i j
+    simp_rw [iInf_eq_if, mem_ite, mem_principal, mem_top] at hV
+    rw [iInter_eq_if]
+    split_ifs with hj
+    · apply (preimage_mono ((hV i j).left hj)).trans'
+      intro y hy
+      simpa using hy
+    · simp [(hV i j).right hj]
+  · exact isOpen_iInter_of_finite fun i =>
+      isOpen_iInter_of_finite fun j =>
+        isOpen_iInter_of_finite fun hj =>
+          isOpen_Iio.preimage (continuous_const.dist i.val.continuous)
+  · simp_rw [mem_iInter]
+    intro i j hj
+    simp [hj]
+
+section CompletelyRegularSpace
+variable [CompletelyRegularSpace α]
+
+private theorem u_l_le :
+    (inducedUniformity α).toTopologicalSpace ≤ ‹TopologicalSpace α› := by
+  intro s hs
+  rw [@isOpen_iff_ball_subset]
+  intro x hx
+  obtain ⟨f, hf, hf0, hf1⟩ :=
+    CompletelyRegularSpace.completely_regular x sᶜ hs.isClosed_compl (not_mem_compl_iff.mpr hx)
+  use ((fun p : α × α => dist (f p.fst : ℝ) (f p.snd)) ⁻¹' Iio 2⁻¹)
+  constructor
+  · have hf' : Continuous (fun i => (f i : ℝ)) := continuous_subtype_val.comp hf
+    suffices h : (_ : Filter _) ≤ _ from h (mem_principal_self _)
+    apply iInf₂_le_of_le ⟨_, hf'⟩ 2⁻¹
+    exact iInf_le _ (by norm_num)
+  · rw [UniformSpace.ball]
+    intro a ha
+    by_contra has
+    norm_num [hf0, hf1 has] at ha
+
+theorem CompletelyRegularSpace.exists_uniformity :
+    ∃ (u : UniformSpace α), u.toTopologicalSpace = ‹TopologicalSpace α› :=
+  ⟨inducedUniformity α, u_l_le.antisymm le_u_l⟩
+
+end CompletelyRegularSpace
+
+end TopologicalSpace