Metric semigroups

[malarbol]

This PR introduces the notion of Metric-Semigroup, metric spaces with a short associative binary operator.

Credit @lowasser for 9e36ee4

[fredrik-bakke]

Is it formalized somewhere that metric-space-of-short-functions-Metric-Space A is right adjoint to "product-Metric-Space A", so that this can confidently be used for "binary short functions"?

[fredrik-bakke]

Otherwise that might be a good sanity-check to formalize

[malarbol]

Is it formalized somewhere that metric-space-of-short-functions-Metric-Space A is right adjoint to "product-Metric-Space A", so that this can confidently be used for "binary short functions"?

I don't think so, we didn't do much in the categorical POV of metric spaces. I don't think we even have the concept "product-Metric-Space A" Do you think it's true? If so, I guess we could add this result sometimes in the future. I've never worked with right adjoints and I'm still working on #1421 so I'll need some time to think about it.

[fredrik-bakke]

It might be true, and I think it is a question worth considering since you are defining what it means to be a binary short function here. If it is not true you may be giving a wrong definition. The adjointedness condition I mention is known in the literature as cartesian closedness, and means that we can observe collections of morphisms in the category as internal objects in the category itself. E.g., given that it is true, the metric space of short functions between two metric spaces represent in a concrete sense the collection of short functions viewed internally. The concrete way in which it represents this collection is precisely by the equivalence

$$\mathrm{Hom}(A \times B, C) \cong \mathrm{Hom}(A, C^B)$$

Where $\mathrm{Hom}$ is the type of short functions, $A \times B$ is the product metric space, and $C^B$ is the metric space of short functions. This equivalence is what the adjointedness condition I mention would unfold to.

[fredrik-bakke]

The question I'd like you to ask yourself is: what is the difference between

    short-function-Metric-Space A (metric-space-of-short-functions-Metric-Space A A)

and

    short-function-Metric-Space (product-Metric-Space A A) A

Are they the same? If so, there is no problem.

[malarbol]

Are they the same? If so, there is no problem.

I think they are but I'll need some time to think about it and write a proper proof. As I said, we don't really have product-Metric-Space yet so there are a lot of missing pieces.

[malarbol]

The question I'd like you to ask yourself is: what is the difference between

    short-function-Metric-Space A (metric-space-of-short-functions-Metric-Space A A)

and

    short-function-Metric-Space (product-Metric-Space A A) A

Are they the same? If so, there is no problem.

I've been working on this in ac05ffd. I can't quite finish the proof though; I'm not sure if I'm missing something or if it's simply not true?

[malarbol]

So, basically, I could construct an isometry

  isometry-ev-pair-short-function-product-Metric-Space :
    isometry-Metric-Space
      ( metric-space-of-short-functions-Metric-Space
        ( product-Metric-Space X Y)
        ( Z))
      ( metric-space-of-short-functions-Metric-Space
        ( X)
        ( metric-space-of-short-functions-Metric-Space Y Z))

and and inverse in the space of functions product-Metric-Space X Y -> Z

  map-ind-short-function-product-Metric-Space :
    short-function-Metric-Space
      ( X)
      ( metric-space-of-short-functions-Metric-Space Y Z) →
    map-type-Metric-Space
      ( product-Metric-Space X Y)
      ( Z)

If the latter takes value in the space of short functions, then we have

    metric-space-of-short-functions-Metric-Space
      ( product-Metric-Space X Y)
      ( Z) ＝
    metric-space-of-short-functions-Metric-Space
      ( X)
      ( metric-space-of-short-functions-Metric-Space Y Z)

but I don't know how to prove this last step. Do you have any idea how to complete this proof? Or maybe it's not always true?

[malarbol]

If anyone is reading this:

• with this setting, I can prove that map-ind-short-function-product-Metric-Space f is uniformly continuous, but still not short;
• I'm starting to believe it's not true: add-ℚ is a

short-function-Metric-Space
  ( ℚ)
  ( metric-space-of-short-functions-Metric-Space ℚ ℚ)

but I don't think it's short as a function product-Metric-Space ℚ ℚ → ℚ.

So, regarding #1447 (comment), let's assume they're not the same and we have a problem. How should we solve it?

NB: whatever the definition of Metric-Semigroup ends up being, I think we'd want ℚ , add-ℚ to be an instance of it.

[malarbol]

This is also a suggestion of prelude for some Analysis-Space mentioned in #1445. Actually, if we think of the analysis module as an intersection of algebraic structures (groups, rings, linear algebra) and convergence structures (metric-spaces, topological-spaces in the future, etc.), this could probably go to analysis/metric-semigroups.lagda.md.

[fredrik-bakke]

This is also a suggestion of prelude for some Analysis-Space mentioned in #1445.

I don't see the need for using such a generic term as Analysis-Space, when the object at hand seems to be essentially a Banach-Ring.

Actually, if we think of the analysis module as an intersection of algebraic structures (groups, rings, linear algebra) and convergence structures (metric-spaces, topological-spaces in the future, etc.), this could probably go to analysis/metric-semigroups.lagda.md.

I like this idea!

[malarbol]

This is also a suggestion of prelude for some Analysis-Space mentioned in #1445.

I don't see the need for using such a generic term as Analysis-Space, when the object at hand seems to be essentially a Banach-Ring.

Sure, at the moment Analysis-Space is just a placeholder name for the concept we are trying to pin out. It might as well be Complete-Metric-Ring. I think Banach-Space would fit better for complete metric spaces where all elements are at finite distance (what I formerly called total complete metric space) so that Banach fixed point theorem holds in Banach spaces.

Actually, if we think of the analysis module as an intersection of algebraic structures (groups, rings, linear algebra) and convergence structures (metric-spaces, topological-spaces in the future, etc.), this could probably go to analysis/metric-semigroups.lagda.md.

I like this idea!

Thanks. I'll move the module.

[fredrik-bakke]

Sure, at the moment Analysis-Space is just a placeholder name for the concept we are trying to pin out. It might as well be Complete-Metric-Ring. I think Banach-Space would fit better for complete metric spaces where all elements are at finite distance (what I formerly called total complete metric space) so that Banach fixed point theorem holds in Banach spaces.

Good, just wanted to make sure we are on the same page. Keep in mind that a banach space is also a vector space 👍