Cauchy approximations in pseudometric spaces

Content created by Louis Wasserman and malarbol.

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

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

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

open import metric-spaces.pseudometric-spaces
open import metric-spaces.short-functions-pseudometric-spaces

Idea

A Cauchy approximation in a pseudometric space A is a map f from ℚ⁺ to the carrier type of A such that for all positive rationals ε and δ, f ε and f δ are in a (ε + δ)-neighborhood, i.e., the distance between f ε and f δ is bounded by ε + δ.

Definitions

Cauchy approximations in pseudometric spaces

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

  is-cauchy-approximation-prop-Pseudometric-Space :
    (ℚ⁺ → type-Pseudometric-Space A) → Prop l2
  is-cauchy-approximation-prop-Pseudometric-Space f =
    Π-Prop
      ( ℚ⁺)
      ( λ ε →
        Π-Prop
          ( ℚ⁺)
          ( λ δ →
            neighborhood-prop-Pseudometric-Space A (ε +ℚ⁺ δ) (f ε) (f δ)))

  is-cauchy-approximation-Pseudometric-Space :
    (ℚ⁺ → type-Pseudometric-Space A) → UU l2
  is-cauchy-approximation-Pseudometric-Space =
    type-Prop ∘ is-cauchy-approximation-prop-Pseudometric-Space

  cauchy-approximation-Pseudometric-Space : UU (l1 ⊔ l2)
  cauchy-approximation-Pseudometric-Space =
    type-subtype is-cauchy-approximation-prop-Pseudometric-Space

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (f : cauchy-approximation-Pseudometric-Space A)
  where

  map-cauchy-approximation-Pseudometric-Space :
    ℚ⁺ → type-Pseudometric-Space A
  map-cauchy-approximation-Pseudometric-Space = pr1 f

  is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space :
    (ε δ : ℚ⁺) →
    neighborhood-Pseudometric-Space
      ( A)
      ( ε +ℚ⁺ δ)
      ( map-cauchy-approximation-Pseudometric-Space ε)
      ( map-cauchy-approximation-Pseudometric-Space δ)
  is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space = pr2 f

Properties

Constant maps in pseudometric spaces are Cauchy approximations

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (x : type-Pseudometric-Space A)
  where

  const-cauchy-approximation-Pseudometric-Space :
    cauchy-approximation-Pseudometric-Space A
  pr1 const-cauchy-approximation-Pseudometric-Space _ = x
  pr2 const-cauchy-approximation-Pseudometric-Space ε δ =
    refl-neighborhood-Pseudometric-Space A (ε +ℚ⁺ δ) x

The action of short maps on Cauchy approximations

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

  map-short-function-cauchy-approximation-Pseudometric-Space :
    cauchy-approximation-Pseudometric-Space A →
    cauchy-approximation-Pseudometric-Space B
  map-short-function-cauchy-approximation-Pseudometric-Space (u , H) =
    ( map-short-function-Pseudometric-Space A B f ∘ u ,
      λ ε δ →
        is-short-map-short-function-Pseudometric-Space
          ( A)
          ( B)
          ( f)
          ( ε +ℚ⁺ δ)
          ( u ε)
          ( u δ)
          ( H ε δ))

Homotopic Cauchy approximations are equal

module _
  { l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  { f g : cauchy-approximation-Pseudometric-Space A}
  ( f~g :
    map-cauchy-approximation-Pseudometric-Space A f ~
    map-cauchy-approximation-Pseudometric-Space A g)
  where

  eq-htpy-cauchy-approximation-Pseudometric-Space : f ＝ g
  eq-htpy-cauchy-approximation-Pseudometric-Space =
    eq-type-subtype
      ( is-cauchy-approximation-prop-Pseudometric-Space A)
      ( eq-htpy f~g)

References

Our definition of Cauchy approximation follows Definition 4.5.5 of [Boo20] and Definition 11.2.10 of [UF13].

[Boo20]
Auke Bart Booij. Analysis in univalent type theory. PhD thesis, University of Birmingham, 2020. URL: https://etheses.bham.ac.uk/id/eprint/10411/7/Booij20PhD.pdf.
[UF13]
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.

Recent changes