Uniform homeomorphisms between metric spaces

Content created by Louis Wasserman.

Created on 2026-01-09.
Last modified on 2026-01-09.

{-# OPTIONS --lossy-unification #-}

module metric-spaces.uniform-homeomorphisms-metric-spaces where
Imports 
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import logic.functoriality-existential-quantification

open import metric-spaces.action-on-cauchy-sequences-uniformly-continuous-maps-metric-spaces
open import metric-spaces.cauchy-sequences-complete-metric-spaces
open import metric-spaces.cauchy-sequences-metric-spaces
open import metric-spaces.complete-metric-spaces
open import metric-spaces.limits-of-cauchy-sequences-metric-spaces
open import metric-spaces.maps-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.uniformly-continuous-maps-metric-spaces

Idea

A uniform homeomorphism f from a metric space X to a metric space Y is an equivalence between X and Y that is uniformly continuous in each direction.

Definition

module _
  {l1 l2 l3 l4 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (f : map-Metric-Space X Y)
  where

  is-uniform-homeo-prop-map-Metric-Space : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-uniform-homeo-prop-map-Metric-Space =
    Σ-Prop
      ( is-equiv-Prop f)
      ( λ H →
        ( is-uniformly-continuous-prop-map-Metric-Space X Y f) ∧
        ( is-uniformly-continuous-prop-map-Metric-Space
          ( Y)
          ( X)
          ( map-inv-is-equiv H)))

  is-uniform-homeo-prop-Metric-Space : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  is-uniform-homeo-prop-Metric-Space =
    type-Prop is-uniform-homeo-prop-map-Metric-Space

uniform-homeo-Metric-Space :
  {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
uniform-homeo-Metric-Space X Y =
  type-subtype (is-uniform-homeo-prop-map-Metric-Space X Y)

module _
  {l1 l2 l3 l4 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (f : uniform-homeo-Metric-Space X Y)
  where

  map-uniform-homeo-Metric-Space : map-Metric-Space X Y
  map-uniform-homeo-Metric-Space = pr1 f

  is-equiv-map-uniform-homeo-Metric-Space :
    is-equiv map-uniform-homeo-Metric-Space
  is-equiv-map-uniform-homeo-Metric-Space = pr1 (pr2 f)

  equiv-uniform-homeo-Metric-Space :
    type-Metric-Space X ≃ type-Metric-Space Y
  equiv-uniform-homeo-Metric-Space =
    ( map-uniform-homeo-Metric-Space ,
      is-equiv-map-uniform-homeo-Metric-Space)

  map-inv-uniform-homeo-Metric-Space : map-Metric-Space Y X
  map-inv-uniform-homeo-Metric-Space =
    map-inv-is-equiv is-equiv-map-uniform-homeo-Metric-Space

  is-section-map-inv-uniform-homeo-Metric-Space :
    is-section
      ( map-uniform-homeo-Metric-Space)
      ( map-inv-uniform-homeo-Metric-Space)
  is-section-map-inv-uniform-homeo-Metric-Space =
    is-section-map-inv-equiv
      ( equiv-uniform-homeo-Metric-Space)

  is-retraction-map-inv-uniform-homeo-Metric-Space :
    is-retraction
      ( map-uniform-homeo-Metric-Space)
      ( map-inv-uniform-homeo-Metric-Space)
  is-retraction-map-inv-uniform-homeo-Metric-Space =
    is-retraction-map-inv-equiv
      ( equiv-uniform-homeo-Metric-Space)

  is-uniformly-continuous-map-uniform-homeo-Metric-Space :
    is-uniformly-continuous-map-Metric-Space
      ( X)
      ( Y)
      ( map-uniform-homeo-Metric-Space)
  is-uniformly-continuous-map-uniform-homeo-Metric-Space =
    pr1 (pr2 (pr2 f))

  uniformly-continuous-map-uniform-homeo-Metric-Space :
    uniformly-continuous-map-Metric-Space X Y
  uniformly-continuous-map-uniform-homeo-Metric-Space =
    ( map-uniform-homeo-Metric-Space ,
      is-uniformly-continuous-map-uniform-homeo-Metric-Space)

  is-uniformly-continuous-map-inv-uniform-homeo-Metric-Space :
    is-uniformly-continuous-map-Metric-Space
      ( Y)
      ( X)
      ( map-inv-uniform-homeo-Metric-Space)
  is-uniformly-continuous-map-inv-uniform-homeo-Metric-Space =
    pr2 (pr2 (pr2 f))

  uniformly-continuous-map-inv-uniform-homeo-Metric-Space :
    uniformly-continuous-map-Metric-Space Y X
  uniformly-continuous-map-inv-uniform-homeo-Metric-Space =
    ( map-inv-uniform-homeo-Metric-Space ,
      is-uniformly-continuous-map-inv-uniform-homeo-Metric-Space)

  is-equiv-map-inv-uniform-homeo-Metric-Space :
    is-equiv map-inv-uniform-homeo-Metric-Space
  is-equiv-map-inv-uniform-homeo-Metric-Space =
    is-equiv-map-inv-is-equiv
      ( is-equiv-map-uniform-homeo-Metric-Space)

  inv-uniform-homeo-Metric-Space :
    uniform-homeo-Metric-Space Y X
  inv-uniform-homeo-Metric-Space =
    ( map-inv-uniform-homeo-Metric-Space ,
      is-equiv-map-inv-uniform-homeo-Metric-Space ,
      is-uniformly-continuous-map-inv-uniform-homeo-Metric-Space ,
      is-uniformly-continuous-map-uniform-homeo-Metric-Space)

Properties

Given a uniform homeomorphism between X and Y, if X is complete, so is Y

module _
  {l1 l2 l3 l4 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (f : uniform-homeo-Metric-Space X Y)
  where

  abstract
    is-complete-metric-space-uniform-homeo-Metric-Space :
      is-complete-Metric-Space X → is-complete-Metric-Space Y
    is-complete-metric-space-uniform-homeo-Metric-Space H =
      let
        open do-syntax-trunc-Prop (is-complete-prop-Metric-Space Y)
      in do
        (μXY , is-mod-μXY) ←
          is-uniformly-continuous-map-uniform-homeo-Metric-Space X Y f
        is-complete-metric-space-cauchy-sequences-have-limits-Metric-Space
          ( Y)
          ( λ uY →
            let
              uX =
                map-cauchy-sequence-uniformly-continuous-map-Metric-Space
                  ( Y)
                  ( X)
                  ( uniformly-continuous-map-inv-uniform-homeo-Metric-Space
                    ( X)
                    ( Y)
                    ( f))
                  ( uY)
              lim-uX = lim-cauchy-sequence-Complete-Metric-Space (X , H) uX
              lim-uY = map-uniform-homeo-Metric-Space X Y f lim-uX
            in
              ( lim-uY ,
                map-exists
                  ( _)
                  ( λ μ-uX → μ-uX ∘ μXY)
                  ( λ μ-uX is-mod-lim-μ-uX ε n μ-uXμXY≤n →
                    tr
                      ( λ y → neighborhood-Metric-Space Y ε y lim-uY)
                      ( is-section-map-inv-uniform-homeo-Metric-Space
                        ( X)
                        ( Y)
                        ( f)
                        ( sequence-cauchy-sequence-Metric-Space Y uY n))
                      ( is-mod-μXY
                        ( map-inv-uniform-homeo-Metric-Space
                          ( X)
                          ( Y)
                          ( f)
                          ( sequence-cauchy-sequence-Metric-Space Y uY n))
                        ( ε)
                        ( lim-uX)
                        ( is-mod-lim-μ-uX
                          ( μXY ε)
                          ( n)
                          ( μ-uXμXY≤n))))
                  ( is-limit-lim-cauchy-sequence-Complete-Metric-Space
                    ( X , H)
                    ( uX))))

Recent changes