Pseudometric def of uniform space

Stream: Is there code for X?

[Adam Topaz]

I'm wondering about the pseudometric definition of a uniform space:
https://en.wikipedia.org/wiki/Uniform_space#Pseudometrics_definition

I.e. the fact that any family of pseudometrics gives rise to a uniform space structure, and conversely, that any uniform space structure arises from some such family. (Of course, this converse is the more interesting direction!)

I'm quite sure we don't have anything like this in mathlib, but I suppose it doesn't hurt to ask.

Assuming we don't have this, let's also discuss how to formulate this in Lean.

[Yaël Dillies]

That sounds like seminorms to me. I suggest writing a hom type pseudo_metric and its corresponding hom class that would be inserted under seminorms

[Adam Topaz]

seminorms give pseudometrics, but they're not the same.

[Adam Topaz]

we do have docs#pseudo_metric_space

[Yaël Dillies]

No, I mean this is similar to how we treat families of seminorms.

[Adam Topaz]

what do you mean by the "corresponding hom class" of a pseudo metric?

[Yaël Dillies]

A topological vector space is locally convex if and only if its topology is induced by a family of seminorms.

is the normed world statement that's similar to yours (cf Wikipedia).

[Adam Topaz]

Anyway, I don't think introducing a whole new type of pseudo-metrics is necessary. We can just talk about families of terms of docs#pseudo_metric_space

[Patrick Massot]

Why are you interested in this definition of uniform structures?

[Adam Topaz]

Specifically, I have a situation with a (uniform) topological ring (satisfying some additional hypotheses which I won't spell out) and I would like to relate it to valuation theory. One reasonable first step is to consider such a family of pseudometrics which give the uniform structure. (The way such a thing is usually related to valuation theory in the literature is somewhat different, but I would like to see whether this approach would offer a cleaner formalization.)

[Anatole Dedecker]

We don’t need anything new to formulate this

[Adam Topaz]

yeah I agree.

[Anatole Dedecker]

The uniform space defined by a family of pseudo metrics is juste the infimum of the uniform spaces for each pseudo metric right ?

[Adam Topaz]

Yes, I think that's right.

[Anatole Dedecker]

Actually a similar thing could have been done for seminorms, we just have to take the infimum of the topologies generated by each one individually. But we need docs#with_seminorms because saying « this topology is generated by these seminorms » is extremely frequent, but I don’t think that is the case for pseudo metrics, is that right?

[Anatole Dedecker]

I think I remember seeing the proof of it in Bourbaki but I’m not home and my iPad has no battery left…

[Adam Topaz]

It is indeed in Bourbaki

[Adam Topaz]

From wiki: Bourbaki: General Topology Chapter IX §1 no. 4

[Anatole Dedecker]

Oh but we almost have it, give me a few minutes

[Anatole Dedecker]

Okay maybe a bit more than a few minutes but it should definitely not be too hard

[Anatole Dedecker]

Ok so this is extremely ugly and impractical to use, but basically here is the proof :

import topology.metric_space.metrizable_uniformity

open set topological_space
open_locale uniformity

example {X : Type*} (u : uniform_space X) : ∃ D : (@uniformity X u).sets → (pseudo_metric_space X),
  u = ⨅ V, (D V).to_uniform_space :=
begin
  let 𝓑 : (@uniformity X u).sets → ℕ → (@uniformity X u).sets :=
    λ V, @nat.rec (λ _, (@uniformity X u).sets)
    ⟨symmetrize_rel V.1, symmetrize_mem_uniformity V.2⟩
    (λ _ U, ⟨classical.some $ comp_symm_mem_uniformity_sets U.2,
      (classical.some_spec $ comp_symm_mem_uniformity_sets U.2).fst⟩),
  have 𝓑_comp : ∀ V n, (𝓑 V (n+1) : set $ X × X) ○ 𝓑 V (n+1) ⊆ 𝓑 V n,
  { intros V n,
    induction n with n hn;
    [set m := 0, set m := n.succ];
    exact (classical.some_spec $ comp_symm_mem_uniformity_sets (𝓑 V m).2).snd.2, },
  have 𝓑_symmetric : ∀ V n, symmetric_rel (𝓑 V n : set $ X × X),
  { intros V n,
    induction n with n hn,
    { exact symmetric_symmetrize_rel _ },
    { exact (classical.some_spec $ comp_symm_mem_uniformity_sets (𝓑 V n).2).snd.1 } },
  have 𝓑_zero_V : ∀ V, (𝓑 V 0 : set $ X × X) ⊆ V :=
    λ V, symmetrize_rel_subset_self V,
  have 𝓑_decreasing' : ∀ V n, 𝓑 V (n+1) ≤ 𝓑 V n,
  { intros V n x hx,
    refine 𝓑_comp V n (subset_comp_self _ hx),
    rw id_rel_subset,
    exact λ y, refl_mem_uniformity (𝓑 V $ n+1).2 },
  have 𝓑_decreasing : ∀ V, antitone (𝓑 V) :=
    λ V, antitone_nat_of_succ_le (𝓑_decreasing' V),
  have 𝓑_is_basis : ∀ V, filter.is_basis (λ _, true) (subtype.val ∘ 𝓑 V),
  { rintros V,
    refine ⟨⟨0, true.intro⟩, λ i j _ _, ⟨max i j, true.intro, subset_inter
      (𝓑_decreasing V _) (𝓑_decreasing V _)⟩⟩;
    simp only [le_max_iff, le_refl, true_or, or_true] },
  let 𝒰 : (@uniformity X u).sets → uniform_space X :=
    λ V, uniform_space.of_core (uniform_space.core.mk_of_basis (𝓑_is_basis V).filter_basis
      (by {rintros r ⟨n, -, rfl⟩ x, exact refl_mem_uniformity (𝓑 V n).2})
      (by {rintros r ⟨n, -, rfl⟩, exact ⟨𝓑 V n, ⟨n, true.intro, rfl⟩, (𝓑_symmetric V n).ge⟩})
      (by {rintros r ⟨n, -, rfl⟩, exact ⟨𝓑 V (n+1), ⟨n+1, true.intro, rfl⟩, 𝓑_comp V n⟩ })),
  have 𝒰_basis : ∀ V, (@uniformity X (𝒰 V)).has_basis (λ _, true) (subtype.val ∘ 𝓑 V) :=
    λ V, (𝓑_is_basis V).has_basis,
  have V_mem_𝒰 : ∀ V : (@uniformity X u).sets, V.1 ∈ (@uniformity X (𝒰 V)),
  { intro V,
    rw (𝒰_basis V).mem_iff,
    exact ⟨0, true.intro, 𝓑_zero_V V⟩ },
  have u_eq_𝒰 : u = ⨅ V, 𝒰 V,
  { refine le_antisymm (le_infi $ λ V, _) (λ V hV, _),
    { change @uniformity X u ≤ @uniformity X (𝒰 V),
      rw (𝒰_basis V).ge_iff,
      exact λ n _, (𝓑 V n).2 },
    { rw infi_uniformity,
      exact filter.mem_infi_of_mem _ (V_mem_𝒰 (⟨V, hV⟩ : (@uniformity X u).sets)) } },
  have 𝒰_exists_dist : ∀ V, ∃ d : pseudo_metric_space X, 𝒰 V = d.to_uniform_space,
  { intro V,
    letI : uniform_space X := 𝒰 V,
    have : (𝓤 X).has_countable_basis (λ _, true) (subtype.val ∘ 𝓑 V) :=
    { countable := to_countable _,
      ..𝒰_basis V },
    haveI : (𝓤 X).is_countably_generated := this.is_countably_generated,
    exact ⟨uniform_space.pseudo_metric_space X, rfl⟩ },
  choose D hD using 𝒰_exists_dist,
  use D,
  convert u_eq_𝒰,
  ext V : 1,
  exact (hD V).symm
end

[Anatole Dedecker]

I will clean it and make a PR in the next few fays, which gives some time to discuss how we should state it to make it usable

[Anatole Dedecker]

(The reason it is so big is because it should be splitted in a lot of intermediate constructions, with each have being a lemma basically)

[Adam Topaz]

I was under the impression that there should be a "canonical" family of pseudometrics that does the job. Something like the collection of all pseudometrics for which the associated map $X \times X \to\mathbb{R}$ is uniformly continuous.

[Adam Topaz]

But what you have is also canonical, and doesn't involve a "large" family!

[Anatole Dedecker]

Oh, you are probably right, and I should have thought about it because I was thinking about a similar thing just a week ago while reviewing #15035 (but I didn't take the time to write my thoughts yet, sorry @Moritz Doll :sweat_smile: ). Anyway, I will think about it between my lectures tomorrow (and of course not during the lectures, who would do that) and see if I can make it work