The metric space of Cauchy approximations in a metric space

Content created by malarbol and Louis Wasserman.

Created on 2025-05-01.
Last modified on 2025-08-18.

module metric-spaces.metric-space-of-cauchy-approximations-metric-spaces where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.involutions
open import foundation.subtypes
open import foundation.universe-levels

open import metric-spaces.cauchy-approximations-metric-spaces
open import metric-spaces.dependent-products-metric-spaces
open import metric-spaces.equality-of-metric-spaces
open import metric-spaces.isometries-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.short-functions-metric-spaces
open import metric-spaces.subspaces-metric-spaces

Idea

The type of Cauchy approximations in a metric space A inherits the metric substructure of the constant product structure over A.

This is the metric space of Cauchy approximations in a metric space.

Definitions

The metric space of Cauchy approximations in a metric space

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

  metric-space-of-cauchy-approximations-Metric-Space : Metric-Space (l1 ⊔ l2) l2
  metric-space-of-cauchy-approximations-Metric-Space =
    subspace-Metric-Space
      ( Π-Metric-Space ℚ⁺ (λ _ → A))
      ( is-cauchy-approximation-prop-Metric-Space A)

Properties

The map (x : A) ↦ const x is an isometry between A and the metric space of cauchy approximations in A

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

  is-isometry-const-cauchy-approximation-Metric-Space :
    is-isometry-Metric-Space
      ( A)
      ( metric-space-of-cauchy-approximations-Metric-Space A)
      ( const-cauchy-approximation-Metric-Space A)
  is-isometry-const-cauchy-approximation-Metric-Space ε x y =
    ( λ Nxy η → Nxy) ,
    ( λ Nxy → Nxy one-ℚ⁺)

  isometry-const-cauchy-approximation-Metric-Space :
    isometry-Metric-Space
      ( A)
      ( metric-space-of-cauchy-approximations-Metric-Space A)
  isometry-const-cauchy-approximation-Metric-Space =
    ( const-cauchy-approximation-Metric-Space A ,
      is-isometry-const-cauchy-approximation-Metric-Space)

The action of short maps on Cauchy approximations is short

module _
  {l1 l2 l1' l2' : Level}
  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
  (f : short-function-Metric-Space A B)
  where

  is-short-map-short-function-cauchy-approximation-Metric-Space :
    is-short-function-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A)
      ( metric-space-of-cauchy-approximations-Metric-Space B)
      ( map-short-function-cauchy-approximation-Metric-Space A B f)
  is-short-map-short-function-cauchy-approximation-Metric-Space ε x y Nxy δ =
    is-short-map-short-function-Metric-Space A B f ε
      ( map-cauchy-approximation-Metric-Space A x δ)
      ( map-cauchy-approximation-Metric-Space A y δ)
      ( Nxy δ)

  short-map-short-function-cauchy-approximation-Metric-Space :
    short-function-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A)
      ( metric-space-of-cauchy-approximations-Metric-Space B)
  short-map-short-function-cauchy-approximation-Metric-Space =
    map-short-function-cauchy-approximation-Metric-Space A B f ,
    is-short-map-short-function-cauchy-approximation-Metric-Space

Swapping the arguments of a Cauchy approximation of Cauchy approximations produces a Cauchy approximation

module _
  { l1 l2 : Level} (A : Metric-Space l1 l2)
  ( U : cauchy-approximation-Metric-Space
    ( metric-space-of-cauchy-approximations-Metric-Space A))
  where

  map-swap-map-cauchy-approximation-Metric-Space :
    ℚ⁺ → ℚ⁺ → type-Metric-Space A
  map-swap-map-cauchy-approximation-Metric-Space η ε =
    map-cauchy-approximation-Metric-Space
      ( A)
      ( map-cauchy-approximation-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A)
        ( U)
        ( ε))
      ( η)

  is-cauchy-map-swap-map-cauchy-approximation-Metric-Space :
    (η : ℚ⁺) →
    is-cauchy-approximation-Metric-Space
      ( A)
      ( map-swap-map-cauchy-approximation-Metric-Space η)
  is-cauchy-map-swap-map-cauchy-approximation-Metric-Space η ε δ =
    is-cauchy-approximation-map-cauchy-approximation-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A)
      ( U)
      ( ε)
      ( δ)
      ( η)

  map-swap-cauchy-approximation-Metric-Space :
    ℚ⁺ → cauchy-approximation-Metric-Space A
  map-swap-cauchy-approximation-Metric-Space η =
    ( map-swap-map-cauchy-approximation-Metric-Space η ,
      is-cauchy-map-swap-map-cauchy-approximation-Metric-Space η)

  is-cauchy-map-swap-cauchy-approximation-Metric-Space :
    is-cauchy-approximation-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A)
      ( map-swap-cauchy-approximation-Metric-Space)
  is-cauchy-map-swap-cauchy-approximation-Metric-Space ε δ η =
    is-cauchy-approximation-map-cauchy-approximation-Metric-Space
      ( A)
      ( map-cauchy-approximation-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A)
        ( U)
        ( η))
      ( ε)
      ( δ)

  swap-cauchy-approximation-Metric-Space :
    cauchy-approximation-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A)
  swap-cauchy-approximation-Metric-Space =
    ( map-swap-cauchy-approximation-Metric-Space ,
      is-cauchy-map-swap-cauchy-approximation-Metric-Space)

Swapping the arguments of a Cauchy approximation of Cauchy approximations is an involution

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

  is-involution-swap-cauchy-approximation-Metric-Space :
    is-involution
      ( swap-cauchy-approximation-Metric-Space A)
  is-involution-swap-cauchy-approximation-Metric-Space U =
    eq-htpy-cauchy-approximation-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A)
      ( λ ε →
        eq-htpy-cauchy-approximation-Metric-Space
          ( A)
          ( λ δ → refl))

  is-equiv-swap-cauchy-approximation-Metric-Space :
    is-equiv (swap-cauchy-approximation-Metric-Space A)
  is-equiv-swap-cauchy-approximation-Metric-Space =
    is-equiv-is-involution
      is-involution-swap-cauchy-approximation-Metric-Space

  equiv-swap-cauchy-approximation-Metric-Space :
    ( cauchy-approximation-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A)) ≃
    ( cauchy-approximation-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space A))
  equiv-swap-cauchy-approximation-Metric-Space =
    ( swap-cauchy-approximation-Metric-Space A ,
      is-equiv-swap-cauchy-approximation-Metric-Space)

Swapping the arguments of a Cauchy approximation of Cauchy approximations is a short map

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

  is-short-swap-cauchy-approximation-Metric-Space :
    is-short-function-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A))
      ( metric-space-of-cauchy-approximations-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A))
      ( swap-cauchy-approximation-Metric-Space A)
  is-short-swap-cauchy-approximation-Metric-Space ε U V Nuv δ η =
    Nuv η δ

Swapping the arguments of a Cauchy approximation of Cauchy approximations is an isometry

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

  is-isometry-swap-cauchy-approximation-Metric-Space :
    is-isometry-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A))
      ( metric-space-of-cauchy-approximations-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A))
      ( swap-cauchy-approximation-Metric-Space A)
  is-isometry-swap-cauchy-approximation-Metric-Space ε U V =
    ( is-short-swap-cauchy-approximation-Metric-Space A ε U V ,
      is-short-swap-cauchy-approximation-Metric-Space
        ( A)
        ( ε)
        ( swap-cauchy-approximation-Metric-Space A U)
        ( swap-cauchy-approximation-Metric-Space A V))

Swapping the arguments of a Cauchy approximation of Cauchy approximations is an isometric equivalence

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

  isometric-equiv-swap-cauchy-approximation-Metric-Space :
    isometric-equiv-Metric-Space
      ( metric-space-of-cauchy-approximations-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A))
      ( metric-space-of-cauchy-approximations-Metric-Space
        ( metric-space-of-cauchy-approximations-Metric-Space A))
  isometric-equiv-swap-cauchy-approximation-Metric-Space =
    ( equiv-swap-cauchy-approximation-Metric-Space A ,
      is-isometry-swap-cauchy-approximation-Metric-Space A)

Recent changes