Consider using a limit-based metric on the metric space of Cauchy approximations

[lowasser]

Currently, the metric space on Cauchy approximations defined in agda-unimath uses the product metric: two Cauchy approximations x, y in a metric space M are in a d-neighborhood if for all epsilon, x epsilon and y epsilon are in a d-neighborhood in M.

It's not obvious to me that this is the best, or even the most standard, metric. For example, consider x epsilon = epsilon and y epsilon = neg-Q epsilon. These both have limit 0 in the standard metric space on the rational numbers, but by the product metric they have unbounded distance from each other.

I would generally expect the most standard metric on the space of Cauchy approximations would say these approximations are indistinguishable and are in d-neighborhoods for every d. I believe the appropriate definition is that two approximations are in d-neighborhoods if for every delta, epsilon, x delta and y epsilon are in d+delta+epsilon-neighborhoods of each other.

(This definition would lend itself well to defining the completion of a metric space, and from there to defining the Cauchy real numbers as the completion of Q.)

[malarbol]

I've given this a lot of thoughts too and I agree the neighborhood relation
N-cauchy d f g = (ε δ : ℚ⁺) → N (ε + δ + d) (f ε) (g δ)
is very interesting. (I strongly suggest you put the d on the right, it makes a lot of things easier).

However, I don't think it's a metric structure but only pseudometric (incidentally, the definition of Cauchy approximation is exactly what makes reflexivity work). I've tried a few times to work with it (I called it the Cauchy pseudometric structure on the space of Cauchy approximations) but I haven't pushed anything yet. My hope was to get #1450 merged before and write this in the new settings.

It enables a really nice interpretation of limits: f has limit l if it is similar (w.r.t this pseudometric) to the constant Cauchy approximation l. This makes some limit results automatic (e.g. limits of a Cauchy approximations are similar, hence equal) and satisfy what you seem to expect: similar Cauchy approximations have the same limits, i.e., if one converges, so does the other, to the same limit. (Note: you might need saturation at some point, but I hope I convinced you it's a good idea to make all metric spaces saturated).

As I said however, I don't think this defines a metric space, but my plan was to consider the quotient set under the similarity relation induced by this pseudometric structure. Hopefully, since similar elements have same neighborhoods, we should be able to define a quotient neighborhood relation on the quotient space where similar equivalent classes have similar elements, hence are equal in the quotient space, so the quotient neighborhood relation is extensional. Some kind of universal quotient metric space of a pseudometric space. Then, hopefully again, using ideas similar to the proof of "the metric space of Cauchy approximations in a complete metric space is complete" (need saturation), this metric space should be complete, and would be a very good candidate to the Cauchy completion of a metric space.

I think it's quite similar to the classical construction of Cauchy completion and I don't see how we can make this work without taking quotient at some point. I'm not even sure this works. What did you have in mind?

[lowasser]

After going ahead and starting to implement it, I agree this is a pseudometric and needs a quotient. Wikipedia defines some appropriate terminology here ("metric identification" as the name of the equivalence relation).

[malarbol]

After going ahead and starting to implement it, I agree this is a pseudometric and needs a quotient. Wikipedia defines some appropriate terminology here ("metric identification" as the name of the equivalence relation).

Yes, my plans were very similar to this construction. Working with "rational neighborhoods" instead of "distance functions" make it a slightly different, though, and I've never actually worked with set quotients so it hasn't been easy.

I'd be happy to work on something together, if you'd like. I already have a few things written that could help.

Did you have a look at #1450? I tried to address some issues raised in #1421 and I removed / renamed a few things. I think it could be nice to advance on #1421 before adding new results in the metric-spaces module.

[lowasser]

I haven't looked at #1450 yet, but I can prioritize that. It did look to me as though you need an additional term to bake in a closure: N-cauchy d f g = (θ ε δ : ℚ⁺) → N (ε + δ + θ + d) (f ε) (g δ).

The θ was necessary in my prototype to make the pseudometric triangular; to prove the triangle inequality between f g h, you compute f ε, g (θ/4), h δ, more or less. The standard triangle inequality in the underlying space then gives you (ε + θ/4 + θ/4 + dfg) + (δ + θ/4 + dgh + θ/4) which has the appropriate total sum. Saturation is also necessary, which I see is getting baked in. To deal with the quotient operation, the key is generally this universal property.

[lowasser]

Just as an example of how to use that universal property: this defines the unique sum of an unordered family of elements of a commutative monoid, using a proof that any ordering of the elements results in the same sum from commutativity. Presumably what we'll be doing is saying that two equivalence classes of Cauchy approximations X, Y are in a d-neighborhood if for every x : X , y : Y, x and y are in a d-neighborhood by the pseudometric we're building here, and we can use that universal property to prove that for any particular x and y in a d-neighborhood of each other, the equivalence class of x is in a d-neighborhood of the equivalence class of y.

[malarbol]

I haven't looked at #1450 yet, but I can prioritize that. It did look to me as though you need an additional term to bake in a closure: N-cauchy d f g = (θ ε δ : ℚ⁺) → N (ε + δ + θ + d) (f ε) (g δ).

The θ was necessary in my prototype to make the pseudometric triangular; to prove the triangle inequality between f g h, you compute f ε, g (θ/4), h δ, more or less. The standard triangle inequality in the underlying space then gives you (ε + θ/4 + θ/4 + dfg) + (δ + θ/4 + dgh + θ/4) which has the appropriate total sum. Saturation is also necessary, which I see is getting baked in.

Yes, I definitely wrote those things at some point. It seems to have gotten lost in my git history or something, so I guess we'll have to re-write this anyway. I think your θ thing is indeed what make the saturation hypothesis handy in metric spaces: (θ ε δ : ℚ⁺) → N (ε + δ + θ + d) (f ε) (g δ) becomes equivalent to (ε δ : ℚ⁺) → N (ε + δ + d) (f ε) (g δ) and this helps a lot for this kind of computation. It's the same trick used to show that "the limit map is short" etc.

I really hope we could merge #1450 first, so we can develop these new result in a better settings.

[lowasser]

For sure. I'm pausing work on this until we land that, and working on the review.

[lowasser]

Is it worth keeping the current metric spaces of Cauchy approximations at all? The product metric just seems so wrong for these.

[malarbol]

Is it worth keeping the current metric spaces of Cauchy approximations at all?

I believe so; what other metric spaces of Cauchy approximations would you suggest? (as we discussed, the cauchy-pseudometric-neighborhood is only a metric structure on the quotient metric space, not on the type of Cauchy approximations.). Moreover, the characterization "a metric space is complete iff its metric space of Cauchy approximations is complete" might be useful when working with completion of metric spaces (e.g. to prove that the completion off a complete metric space is itself, or that completion is idempotent). So, yes, I think it's worth keeping.

The product metric just seems so wrong for these.

Why? I don't see the problem with introducing another pseudometric structure on the type of Cauchy approximations, finer than the product metric, and work with that to construct the Cauchy completion of a metric space.

[lowasser]

I guess I'm just not especially convinced "the metric space of Cauchy approximations" with the product metric is a useful object to give its own file at all. Whenever we need it, it seems to me like it could reasonably just be referred to as the subspace (of functions from Q+ to M that are Cauchy approximations) of the product space. If the file for the "metric space of Cauchy approximations" actually used the discrete metric, instead of the product metric, it feels like it would make an equal amount of sense; the elements of the metric space being Cauchy approximations doesn't actually have anything to do with the metric being used.

(If we renamed the file "the metric space of Cauchy approximations under the product metric," I would think that a weird thing to need its own file, but would at least be happier.)

I'm also not at all convinced that this is the way to prove that completion is idempotent nor that the completion of a complete metric space is itself, but that's because I'm working on defining completion through the pathway outlined in this issue.

[malarbol]

I guess I'm just not especially convinced "the metric space of Cauchy approximations" with the product metric is a useful object to give its own file at all.

ok. what metric would you give it?

Whenever we need it, it seems to me like it could reasonably just be referred to as the subspace (of functions from Q+ to M that are Cauchy approximations) of the product space.

but if we end up needing it a lot, why not give it a name?

If the file for the "metric space of Cauchy approximations" actually used the discrete metric, instead of the product metric, it feels like it would make an equal amount of sense;

Would it? Would constant maps be isometry from a metric space to its metric space of Cauchy approximations? Would the map from a convergent Cauchy approximation to its limit short?

the elements of the metric space being Cauchy approximations doesn't actually have anything to do with the metric being used.

I think they do for results like the limit map is short.

(If we renamed the file "the metric space of Cauchy approximations under the product metric," I would think that a weird thing to need its own file, but would at least be happier.)

I'm curious about what other metric structure on the type of Cauchy approximations in a metric space you want to introduce.
Or do you feel there shouldn't be any "metric space of Cauchy approximations in a metric space" at all?

I'm also not at all convinced that this is the way to prove that completion is idempotent nor that the completion of a complete metric space is itself, but that's because I'm working on defining completion through the pathway outlined in this issue.

Well, I guess I was too hopeful with my plan. Does the "metric quotient of a pseudometric space" construction work? Or are you going a different route?

[malarbol]

It did look to me as though you need an additional term to bake in a closure: N-cauchy d f g = (θ ε δ : ℚ⁺) → N (ε + δ + θ + d) (f ε) (g δ).

I'm still not sure this additional term is needed. Given saturation (which you'll need anyway to prove that the inclusion const map is an isometry), this is plainly equivalent to N-cauchy d f g = (ε δ : ℚ⁺) → N (ε + δ + d) (f ε) (g δ) so maybe this should be the definition and, in the proof where you needed this θ, introduce/eliminate it using saturation of the underlying metric space.

I also think it make a few definitions cleaner. E.g. a Cauchy approximation in the pseudometric space of Cauchy approximations in M is basically a map U : ℚ⁺ → ℚ⁺ → M such that

• (ε δ θ : ℚ⁺) → N (δ + θ) (U ε δ) (U ε θ) (U ε is a Cauchy approximation in M)
• (ε δ d d' : ℚ⁺) → N (d + d' + ε + δ) (U ε d) (U δ d') (U is a Cauchy approximation of pseudometric space)

This additional term makes these way less symmetrical and sometimes less practical to work with (it forces you to use saturation where it would not be needed).