Induced metric space of pseudometric spaces

[malarbol]

This PR introduces the induced metric space of a pseudometric space M: the metric space whose points are
quotient classes of M by the similarity relation and neighborhoods given by neighborhoods of inhabitants of the quotient classes: two quotient classes X, Y are in a d-neighborhood if for all x ∈ X and y ∈ Y, x and y are d-neighbors in the pseudometric space.

Co-authored-by: Louis Wasserman [email protected]

[fredrik-bakke]

This PR should be marked as a draft until #1482 is merged.

[fredrik-bakke]

oops, I started my review in the wrong PR, my bad!

[fredrik-bakke]

I'm wondering about the name of this concept. Should it not be called the quotient metric space associated to a pseudometric space or the (universal) metric space generated by a pseudometric space?

[malarbol]

I'm wondering about the name of this concept. Should it not be called the quotient metric space associated to a pseudometric space or the (universal) metric space generated by a pseudometric space?

Sure. I kept the original name by @lowasser in https://github.com/lowasser/agda-unimath/blob/induced-metric-space-pseudometric/src/metric-spaces/induced-metric-space-of-pseudometric-spaces.lagda.md but I guess we can change it.
I quite like "quotient metric space associated to a pseudometric space". Do you like metric-quotient-Pseudometric-Space for the name of the construction?

[fredrik-bakke]

Completion (and maybe even saturation) are used in some other contexts too, I know. How do you feel about metric-completion-Pseudometric-Space?

[malarbol]

Completion (and maybe even saturation) are used in some other contexts too, I know. How do you feel about metric-completion-Pseudometric-Space?

mmh. I don't really like this 😅. I think it could bring confusion with the concept of Cauchy completion of (pseudo)metric spaces (which we are also trying to define). Moreover, a "completion" construction is more about "adding new points to fill the voids". Here we're doing the opposite, shrinking the space identifying similar elements. So I don't think "completion" is appropriate. "Saturation" is also already used in another context so, for the same reason, it's not really an option.

What don't you like about metric-quotient-Pseudometric-Space?

[fredrik-bakke]

Ah, yes, fair point. I don't have anything against "quotient", I was just spitting ideas

[malarbol]

Ah, yes, fair point. I don't have anything against "quotient", I was just spitting ideas

It seems like the name comes from the wikipedia page: "[...] called the metric space induced by the pseudometric space [...]" but I must confess I still prefer metric-quotient-Pseudometric-Space.

BTW, is it ok to link to specific sections of a wikipedia page like this in a ## See also section?

[fredrik-bakke]

External links, yes

[malarbol]

Restarting this in #1507.