Functorial action on short maps of Cauchy pseudocompletions of pseudometric spaces

Content created by malarbol.

Created on 2026-02-12.
Last modified on 2026-05-01.

module metric-spaces.functoriality-short-maps-cauchy-pseudocompletions-of-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-pseudocompletions-of-pseudometric-spaces
open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces
open import metric-spaces.maps-pseudometric-spaces
open import metric-spaces.pseudometric-spaces
open import metric-spaces.short-maps-pseudometric-spaces

Idea

The functorial action of Cauchy pseudocompletions on short maps between pseudometric spaces is the action on Cauchy approximations induced by the postcomposition with short.

It maps short maps between pseudometric spaces to short maps between their Cauchy pseudocompletions.

Definitions

The action on short maps on Cauchy pseudocompletions

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

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

Properties

The action on short maps is short

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

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

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

The action on short maps of Cauchy pseudocompletions preserves homotopies

module _
  {l1 l2 l1' l2' : Level}
  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
  (f g : short-map-Pseudometric-Space A B)
  (f~g : htpy-map-short-map-Pseudometric-Space A B f g)
  where

  htpy-map-short-map-cauchy-pseudocompletion-Pseudometric-Space :
    htpy-map-short-map-Pseudometric-Space
      ( cauchy-pseudocompletion-Pseudometric-Space A)
      ( cauchy-pseudocompletion-Pseudometric-Space B)
      ( short-map-cauchy-pseudocompletion-Pseudometric-Space A B f)
      ( short-map-cauchy-pseudocompletion-Pseudometric-Space A B g)
  htpy-map-short-map-cauchy-pseudocompletion-Pseudometric-Space u =
    eq-htpy-cauchy-approximation-Pseudometric-Space B
      ( f~g ∘ map-cauchy-approximation-Pseudometric-Space A u)

The unit of cauchy pseudocompletions is a natural transformation

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

  naturality-short-map-unit-cauchy-pseudocompletion-Pseudometric-Space :
    ( map-short-map-cauchy-pseudocompletion-Pseudometric-Space A B f ∘
      map-unit-cauchy-pseudocompletion-Pseudometric-Space A) ~
    ( map-unit-cauchy-pseudocompletion-Pseudometric-Space B ∘
      map-short-map-Pseudometric-Space A B f)
  naturality-short-map-unit-cauchy-pseudocompletion-Pseudometric-Space x =
    eq-htpy-cauchy-approximation-Pseudometric-Space B refl-htpy

The action on short maps of Cauchy pseudocompletions preserves limits

module _
  {l1 l2 l1' l2' : Level}
  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
  (f : short-map-Pseudometric-Space A B)
  (a : cauchy-approximation-Pseudometric-Space A)
  (lim : type-Pseudometric-Space A)
  where abstract

  preserves-limit-map-short-map-cauchy-pseudocompletion-Pseudometric-Space :
    is-limit-cauchy-approximation-Pseudometric-Space A a lim →
    is-limit-cauchy-approximation-Pseudometric-Space
      ( B)
      ( map-short-map-cauchy-pseudocompletion-Pseudometric-Space A B f a)
      ( map-short-map-Pseudometric-Space A B f lim)
  preserves-limit-map-short-map-cauchy-pseudocompletion-Pseudometric-Space
    is-lim-a ε δ =
    is-short-map-short-map-Pseudometric-Space A B
      ( f)
      ( ε +ℚ⁺ δ)
      ( map-cauchy-approximation-Pseudometric-Space A a ε)
      ( lim)
      ( is-lim-a ε δ)

Recent changes