The action on Cauchy approximations of short maps between pseudometric spaces

Content created by malarbol.

Created on 2025-12-25.
Last modified on 2025-12-25.

module metric-spaces.action-on-cauchy-approximations-short-maps-pseudometric-spaces where
Imports 
open import elementary-number-theory.addition-positive-rational-numbers
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.cauchy-approximations-pseudometric-spaces
open import metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces
open import metric-spaces.isometries-pseudometric-spaces
open import metric-spaces.pseudometric-spaces
open import metric-spaces.short-functions-pseudometric-spaces

Idea

Short maps between pseudometric spaces act on cauchy approximations and induce a short map between the Cauchy pseudocompletions.

Definitions

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-cauchy-approximation-short-function-Pseudometric-Space :
    cauchy-approximation-Pseudometric-Space A →
    cauchy-approximation-Pseudometric-Space B
  map-cauchy-approximation-short-function-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 ε δ))

Properties

The action of short maps on Cauchy approximations is short

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

  abstract
    preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space :
      is-short-function-Pseudometric-Space
        ( cauchy-pseudocompletion-Pseudometric-Space A)
        ( cauchy-pseudocompletion-Pseudometric-Space B)
        ( map-cauchy-approximation-short-function-Pseudometric-Space A B f)
    preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space
      d x y Nxy α β =
      is-short-map-short-function-Pseudometric-Space A B f
        ( α +ℚ⁺ β +ℚ⁺ d)
        ( map-cauchy-approximation-Pseudometric-Space A x α)
        ( map-cauchy-approximation-Pseudometric-Space A y β)
        ( Nxy α β)

  short-map-cauchy-approximation-short-function-Pseudometric-Space :
    short-function-Pseudometric-Space
      ( cauchy-pseudocompletion-Pseudometric-Space A)
      ( cauchy-pseudocompletion-Pseudometric-Space B)
  short-map-cauchy-approximation-short-function-Pseudometric-Space =
    ( map-cauchy-approximation-short-function-Pseudometric-Space A B f ,
      preserves-neighborhoods-map-cauchy-approximation-short-function-Pseudometric-Space)

Recent changes