Skip to content

Metric semigroups #1447

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 11 commits into
base: master
Choose a base branch
from
+872 −0
Draft

Metric semigroups #1447

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
22ebc6e
metric-semigroups
malarbol Jun 17, 2025
6e27015
fix name
malarbol Jun 17, 2025
4fff98a
move metric-semigroups -> analysis
malarbol Jun 18, 2025
9e36ee4
fetch products-metric-spaces from lowasser/add-real-uniform-continuous
malarbol Jun 20, 2025
ac05ffd
WIP CCC metric spaces and short maps
malarbol Jun 21, 2025
617f9d1
results
malarbol Jun 21, 2025
8ff1357
lemma-is-short-map-ind-short-function-Metric-Space
malarbol Jun 21, 2025
e10913d
is-uniformly-continuous-map-ind-short-function-product-Metric-Space
malarbol Jun 22, 2025
51bc7b0
Merge branch 'master' into metric-semigroups
malarbol Jun 22, 2025
86f1767
Merge branch 'master' into metric-semigroups
malarbol Jul 8, 2025
0adc641
Merge branch 'master' into metric-semigroups
malarbol Jul 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/metric-spaces.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ open import metric-spaces.limits-of-sequences-metric-spaces public
open import metric-spaces.limits-of-sequences-premetric-spaces public
open import metric-spaces.limits-of-sequences-pseudometric-spaces public
open import metric-spaces.lipschitz-functions-metric-spaces public
open import metric-spaces.metric-semigroups public
open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public
open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public
open import metric-spaces.metric-space-of-cauchy-approximations-saturated-complete-metric-spaces public
Expand Down
187 changes: 187 additions & 0 deletions src/metric-spaces/metric-semigroups.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,187 @@
# Metric semigroups

```agda
module metric-spaces.metric-semigroups where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.semigroups

open import metric-spaces.metric-space-of-short-functions-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.short-functions-metric-spaces
```

</details>

## Idea

A {{#concept "metric semigroup" Agda=Metric-Semigroup}} is a
[metric-space](metric-spaces.metric-spaces.md) equipped with a
[short](metric-spaces.short-functions-metric-spaces.md)
[associative binary operator](group-theory.semigroups.md).

## Definitions

### Associative short binary operators

```agda
module _
{l1 l2 : Level} (A : Metric-Space l1 l2)
where

mul-short-mul-Metric-Space :
short-function-Metric-Space
( A)
( metric-space-of-short-functions-Metric-Space A A) →
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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"?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise that might be a good sanity-check to formalize

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

@fredrik-bakke fredrik-bakke Jun 17, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems impossible to me that add-ℚ is not a short function viewed as product-Metric-Space ℚ ℚ → ℚ, considering it is commutative. Are you sure this is the case?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Based on this Wikipedia page, I propose you define the product metric space using the supremum, i.e. maximum distance of the coordinates, and then use short-function-Metric-Space (product-Metric-Space A A) A in your definitions. This should always be correct, and then we can later resolve the question of wheter short-function-Metric-Space A (metric-space-of-short-functions-Metric-Space A A) is equivalent or not.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Based on this Wikipedia page, I propose you define the product metric space using the supremum, i.e. maximum distance of the coordinates,

I think that's what this definition does: upper bounds of the "product distance" are upper bounds on each coordinates, i.e. upper bounds of the max if the distances. This is also coherent with the definition of "dependent product of metric spaces" where the distance is the supremum.

It seems impossible to me that add-ℚ is not a short function viewed as product-Metric-Space ℚ ℚ → ℚ, considering it is commutative.

I was surprised too, and I don't see how commutativity should help...

Are you sure this is the case?

Unless I'm mistaken, it basically boils down to proving that

|(x + y) - (x' + y')| ≤ max (|x - x'| , |y - y'|)

and I don't see a way out. It is a lipschitz-function-Metric-Space (product-Metric-Space A A) A though. Would that help?

then use short-function-Metric-Space (product-Metric-Space A A) A in your definitions. This should always be correct, and then we can later resolve the question of wheter short-function-Metric-Space A (metric-space-of-short-functions-Metric-Space A A) is equivalent or not.

So ℚ , add-ℚ will not be a metric semigroup?

type-Metric-Space A →
type-Metric-Space A →
type-Metric-Space A
mul-short-mul-Metric-Space f =
( map-short-function-Metric-Space A A) ∘
( map-short-function-Metric-Space
( A)
( metric-space-of-short-functions-Metric-Space A A)
( f))

is-associative-prop-short-mul-Metric-Space :
short-function-Metric-Space
( A)
( metric-space-of-short-functions-Metric-Space A A) →
Prop l1
is-associative-prop-short-mul-Metric-Space f =
let
μ : type-Metric-Space A → type-Metric-Space A → type-Metric-Space A
μ = mul-short-mul-Metric-Space f
in
Π-Prop
( type-Metric-Space A)
( λ x →
Π-Prop
( type-Metric-Space A)
( λ y →
Π-Prop
( type-Metric-Space A)
( λ z →
Id-Prop
( set-Metric-Space A)
( μ (μ x y) z)
( μ x (μ y z)))))
```

### Metric semigroups

```agda
Metric-Semigroup : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Metric-Semigroup l1 l2 =
Σ ( Metric-Space l1 l2)
( type-subtype ∘ is-associative-prop-short-mul-Metric-Space)

module _
{l1 l2 : Level} (M : Metric-Semigroup l1 l2)
where

metric-space-Metric-Semigroup : Metric-Space l1 l2
metric-space-Metric-Semigroup = pr1 M

set-Metric-Semigroup : Set l1
set-Metric-Semigroup = set-Metric-Space metric-space-Metric-Semigroup

type-Metric-Semigroup : UU l1
type-Metric-Semigroup = type-Metric-Space metric-space-Metric-Semigroup

short-associative-mul-Metric-Semigroup :
type-subtype
(is-associative-prop-short-mul-Metric-Space metric-space-Metric-Semigroup)
short-associative-mul-Metric-Semigroup = pr2 M

short-mul-Metric-Semigroup :
short-function-Metric-Space
( metric-space-Metric-Semigroup)
( metric-space-of-short-functions-Metric-Space
metric-space-Metric-Semigroup
metric-space-Metric-Semigroup)
short-mul-Metric-Semigroup = pr1 short-associative-mul-Metric-Semigroup

mul-Metric-Semigroup :
type-Metric-Semigroup → type-Metric-Semigroup → type-Metric-Semigroup
mul-Metric-Semigroup =
mul-short-mul-Metric-Space
metric-space-Metric-Semigroup
short-mul-Metric-Semigroup

mul-Metric-Semigroup' :
type-Metric-Semigroup → type-Metric-Semigroup → type-Metric-Semigroup
mul-Metric-Semigroup' x y =
mul-Metric-Semigroup y x

associative-mul-Metric-Semigroup :
(x y z : type-Metric-Semigroup) →
mul-Metric-Semigroup (mul-Metric-Semigroup x y) z ＝
mul-Metric-Semigroup x (mul-Metric-Semigroup y z)
associative-mul-Metric-Semigroup =
pr2 short-associative-mul-Metric-Semigroup

semigroup-Metric-Semigroup : Semigroup l1
semigroup-Metric-Semigroup =
set-Metric-Semigroup ,
mul-Metric-Semigroup ,
associative-mul-Metric-Semigroup
```

## Properties

### Multiplication in a metric semigroup is short

```agda
module _
{l1 l2 : Level} (M : Metric-Semigroup l1 l2) (x : type-Metric-Semigroup M)
where

is-short-mul-Metric-Semigroup :
is-short-function-Metric-Space
( metric-space-Metric-Semigroup M)
( metric-space-Metric-Semigroup M)
( mul-Metric-Semigroup M x)
is-short-mul-Metric-Semigroup =
is-short-map-short-function-Metric-Space
( metric-space-Metric-Semigroup M)
( metric-space-Metric-Semigroup M)
( map-short-function-Metric-Space
( metric-space-Metric-Semigroup M)
( metric-space-of-short-functions-Metric-Space
( metric-space-Metric-Semigroup M)
( metric-space-Metric-Semigroup M))
( short-mul-Metric-Semigroup M)
( x))

is-short-mul-Metric-Semigroup' :
is-short-function-Metric-Space
( metric-space-Metric-Semigroup M)
( metric-space-Metric-Semigroup M)
( mul-Metric-Semigroup' M x)
is-short-mul-Metric-Semigroup' d y z Nyz =
is-short-map-short-function-Metric-Space
( metric-space-Metric-Semigroup M)
( metric-space-of-short-functions-Metric-Space
( metric-space-Metric-Semigroup M)
( metric-space-Metric-Semigroup M))
( short-mul-Metric-Semigroup M)
( d)
( y)
( z)
( Nyz)
( x)
```