Zulip Chat Archive

Stream: general

Topic: Dropping uniformity

Anatole Dedecker (Jun 12 2022 at 12:12):

I've been working with uniform spaces quite a lot recently, and one really annoying thing that keeps coming over and over is that we have to used forms for talking about the uniformity filter :

  • docs#uniformity, with the nice notation 𝓤
  • uniform_space.to_core.uniformity, which quite a lot of lemmas are written for (see e.g docs#inf_uniformity, I introduced the primed version recently to use 𝓤), and more importantly, keeps coming over because using ext turns equalities of uniform spaces to equalities of their uniform_space.to_core.uniformity

I see too main options to fix that. The easy one is to declare that uniform_space.to_core.uniformity is an implementation detail, change all the lemmas to use docs#uniformity, including the @[ext] lemma docs#uniform_space_eq.

The more extreme solution would be to just remove docs#uniformity and use the nice notation for uniform_space.to_core.uniformity. I did that just for the basic file in draft PR #14694 if you want to have a look. Here are some pros and cons for this solution :

  • pro : all the current uses of the notation seem to continue working flawlessly
  • pro : when then uniform_space needs to be explicit, one can use u.uniformity instead of @uniformity _ u, but unfortunately
  • con : due to the usual problems of dot notation, when writing u.uniformity, an extra type annotation is often needed, like (u : uniform_space α).uniformity. That said, I do prefer type annotation over @s and _s, but that's a personal preference
  • con : the nice notation does not appear in the infoview (I guess this is because it's a "complicated" definition, in that it doesn't correspond to just one simple function application ?)

There might also be a solution involving abbreviation or reducible definitions, but I'm not familiar enough with this kind of things yet, so if you have any suggestion please let me know !

Anatole Dedecker (Jun 12 2022 at 12:12):

/poll Which option do you prefer ?
Make uniformity the preferred form, hide uniform_space.to_core.uniformity
Remove uniformity and assign notation to uniform_space.to_core.uniformity

Anatole Dedecker (Jun 12 2022 at 12:14):

cc @Patrick Massot @Sebastien Gouezel @Yury G. Kudryashov @Eric Wieser

Yury G. Kudryashov (Jun 12 2022 at 13:22):

You can introduce a notation like 𝓤[u] α similar to measurable_set[m] s.

Yury G. Kudryashov (Jun 12 2022 at 13:23):

(this applies to both solutions)

Eric Wieser (Jun 12 2022 at 15:27):

I think my comment on your PR fixes the second con

Yury G. Kudryashov (Jun 13 2022 at 07:59):

I have no opinion about your original question but I think that the user visible notation in the source files should be 𝓤 α and 𝓤[u] α. I'm not sure if we can use the latter notation in docs/infoview/...

Patrick Massot (Jun 13 2022 at 08:30):

I think it's nice to keep the notation in the info view. And uniform_space.to_core.uniformity is indeed an implementation detail.

Last updated: Dec 20 2023 at 11:08 UTC