Cauchy pseudocompletions of (pseudo)metric spaces

[malarbol]

This PR introduces the following concepts:

• the Cauchy pseudocompletion of a pseudometric space M: the pseudometric space of Cauchy approximations in M where two Cauchy approximations x and y are in a d-neighborhood of one another if for all δ ε : ℚ⁺, x δ and y ε are in a δ + ε + d-neighborhood of one another in M;

• the Cauchy pseudocompletion of a metric space: the Cauchy pseudocompletion of its underlying pseudometric space.

Cauchy approximations in a Cauchy pseudocompletion have a limit; any complete metric space is a retract of its Cauchy pseudocompletion.

Co-authored-by: Louis Wasserman wasserman.louis@gmail.com

[fredrik-bakke]

To me the term "pseudometric completion" seems tautological when applied to pseudometrics. "Pseudometric completion" reads like "the universal way to turn something into a pseudometric", which it evidently isn't. Wouldn't a better term for this concept be simply "The completion of pseudometric spaces", or "Cauchy completion of pseudometric spaces"?

Is it not the case that the "pseudometric completion" of a metric space is a metric space? If so, maybe a better term is "(Cauchy) pseudocompletion"?

[malarbol]

Unfortunately I have no reference to give for the term "pseudometric completion".

Nonetheless it's some kind of canonical pseudometric space, isometric to the original one, where all Cauchy approximations have a limit; so it seemed appropriate.

On the other hand, we don't really have the concept of complete pseudometric space (limits aren't unique so this would not be a subtype of pseudometric spaces) so talking about "completion" of pseudometric spaces might be misleading.

We could also consider the names cauchy-neighborhood-relation-Pseudometric-Space and cauchy-pseudometric-space-Pseudometric-Space.

[fredrik-bakke]

Ah, I see, it freely adjoins a limit to every cauchy sequence? This is a nice construction!

I don't think "pseudometric completion" is good. The "pseudocompletion" or "Cauchy pseudocompletion" should work though, right? Unless if the construction already produces a metric space when applied to metric spaces. If so, you might as well call it the "completion" with no extra qualifier, or "Cauchy completion" if you prefer.

[malarbol]

To me the term "pseudometric completion" seems tautological when applied to pseudometrics. "Pseudometric completion" reads like "the universal way to turn something into a pseudometric", which it evidently isn't. Wouldn't a better term for this concept be simply "The completion of pseudometric spaces", or "Cauchy completion of pseudometric spaces"?

Yes. It's basically about constructing a natural pseudometric space, isometric to the original one, where all Cauchy approximations have a limit. I guess "Cauchy completion of pseudometric spaces" would be ok but there's no complete-pseudometric-spaces module so maybe it would be weird.

Is it not the case that the "pseudometric completion" of a metric space is a metric space? If so, maybe a better term is "(Cauchy) pseudocompletion"?

The term "(Cauchy) pseudocompletion" will appear later, namely as the metric quotient of these pseudometric Cauchy completions. There're the closest we could get to Cauchy completion but we can't prove they're complete, hence the name "pseudocompletion".

It's all in #1507 if you want to have a look.

[fredrik-bakke]

The term "(Cauchy) pseudocompletion" will appear later, namely as the metric quotient of these pseudometric Cauchy completions. There're the closest we could get to Cauchy completion but we can't prove they're complete, hence the name "pseudocompletion".

I would advise against using the qualifier "pseudo-" for that, since you are already using that extensively for your notion of a nonextensional metric space.

[fredrik-bakke]

Okay, so let's think. This PR contributes the universal construction of adjoining a limit point to every Cauchy sequence in a pseudometric space. I think "the (Cauchy) pseudocompletion" is a perfectly reasonable name for this construction, since it is the (Cauchy) completion up to similarity, which is exactly the failure of a pseudometric space, contra a metric space.

[malarbol]

The term "(Cauchy) pseudocompletion" will appear later, namely as the metric quotient of these pseudometric Cauchy completions. There're the closest we could get to Cauchy completion but we can't prove they're complete, hence the name "pseudocompletion".

I would advise against using the qualifier "pseudo-" for that, since you are already using that extensively for your notion of a nonextensional metric space.

ok. We'll have to think of a better name.

[fredrik-bakke]

Now, surely we can find a more suitable name for the quotient you describe that is coming in a later contribution. Though, why does it deserve a special name if it fails to satisfy the property you are after?

[malarbol]

Though, why does it deserve a special name if it fails to satisfy the property you are after?

It satisfies almost all properties you'd expect from a Cauchy completion but not exactly (without ACC for all we know). Maybe that's not the right concept.

In the meantime this construction still seems intrinsically interesting. Should it be called cauchy-pseudocompletion-Pseudometric-Space?

[fredrik-bakke]

In the meantime this construction still seems intrinsically interesting. Should it be called cauchy-pseudocompletion-Pseudometric-Space?

The concept you are contributing in this PR? Yes, I think that is the best name.

[fredrik-bakke]

It satisfies almost all properties you'd expect from a Cauchy completion but not exactly (with our ACC for all we know).

That's a bummer. And sorry I don't have a solution for you. maybe a reasonable name is the Cauchy quotient? Because it reminds everyone of the defining property/construction as well as the (potential) deficiency of it.

[malarbol]

Though, why does it deserve a special name if it fails to satisfy the property you are after?

It satisfies almost all properties you'd expect from a Cauchy completion but not exactly (with our ACC for all we know). Maybe that's not the right concept.

In the meantime this construction still seems intrinsically interesting. Should it be called cauchy-pseudocompletion-Pseudometric-Space?

It satisfies almost all properties you'd expect from a Cauchy completion but not exactly (with our ACC for all we know).

That's a bummer. And sorry I don't have a solution for you. maybe a reasonable name is the Cauchy quotient? Because it reminds everyone of the defining property/construction as well as the (potential) deficiency of it.

I'm not sure. The problem is not about the quotient (the metric quotient of a pseudometric space is indeed a well-defined metric space) but more about completeness itself. (we cannot show that the metric quotient of a pseudocomplete pseudometric space is complete).

[fredrik-bakke]

Right, hence why I suggested the juxtaposed Cauchy quotient. Anyways, it's just a suggestion.