Universal property of metric quotients of pseudometric spaces and short maps

Content created by malarbol.

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

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

module metric-spaces.universal-property-short-maps-metric-quotients-of-pseudometric-spaces where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.binary-transport
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.set-quotients
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universal-property-set-quotients
open import foundation.universe-levels

open import metric-spaces.maps-metric-spaces
open import metric-spaces.metric-quotients-of-pseudometric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.pseudometric-spaces
open import metric-spaces.rational-neighborhood-relations
open import metric-spaces.short-maps-metric-spaces
open import metric-spaces.short-maps-pseudometric-spaces
open import metric-spaces.similarity-of-elements-pseudometric-spaces

Idea

Precomposition with the natural isometry from a pseudometric space P into its metric quotient

  q : P → [P]

maps short maps [P] → M to a metric space to short maps from P to the underlying pseudometric space of M.

This action is an equivalence, so short maps from a pseudometric space to a metric space are equivalent to short maps from its metric quotient.

Equivalently, the metric quotient satisfies the universal property of metric quotients and short maps: for any short map f : P → M from a pseudometric space in a metric space, there uniquely exists an extension of f along q, i.e., a short map g : [P] → M such that

  g ∘ q ~ f.

Definitions

Precomposition of short maps by the metric quotient isometry

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  where

  precomp-short-map-metric-quotient-Pseudometric-Space :
    short-map-Metric-Space (metric-quotient-Pseudometric-Space P) M →
    short-map-Pseudometric-Space P (pseudometric-Metric-Space M)
  precomp-short-map-metric-quotient-Pseudometric-Space f =
    comp-short-map-Pseudometric-Space
      ( P)
      ( pseudometric-metric-quotient-Pseudometric-Space P)
      ( pseudometric-Metric-Space M)
      ( f)
      ( short-map-metric-quotient-Pseudometric-Space P)

The induced map from the quotient metric space by a short map in a metric space

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where

  map-exten-short-map-metric-quotient-Pseudometric-space :
    map-Metric-Space
      ( metric-quotient-Pseudometric-Space P)
      ( M)
  map-exten-short-map-metric-quotient-Pseudometric-space =
    inv-precomp-set-quotient
      ( equivalence-relation-sim-Pseudometric-Space P)
      ( set-Metric-Space M)
      ( reflecting-map-short-map-metric-space-Pseudometric-Space P M f)

  is-extension-exten-short-map-metric-quotient-Pseudometric-Space :
    map-exten-short-map-metric-quotient-Pseudometric-space ∘
    map-metric-quotient-Pseudometric-Space P ~
    map-short-map-Pseudometric-Space P (pseudometric-Metric-Space M) f
  is-extension-exten-short-map-metric-quotient-Pseudometric-Space =
    is-section-inv-precomp-set-quotient
      ( equivalence-relation-sim-Pseudometric-Space P)
      ( set-Metric-Space M)
      ( reflecting-map-short-map-metric-space-Pseudometric-Space P M f)

  compute-map-exten-short-map-metric-quotient-Pseudometric-Space :
    (X : type-metric-quotient-Pseudometric-Space P) →
    {x : type-Pseudometric-Space P} →
    is-in-class-metric-quotient-Pseudometric-Space P X x →
    map-exten-short-map-metric-quotient-Pseudometric-space X ＝
    map-short-map-Pseudometric-Space P (pseudometric-Metric-Space M) f x
  compute-map-exten-short-map-metric-quotient-Pseudometric-Space X {x} x∈X =
    tr
      ( λ Y →
        map-exten-short-map-metric-quotient-Pseudometric-space Y ＝
        map-short-map-Pseudometric-Space
          ( P)
          ( pseudometric-Metric-Space M)
          ( f)
          ( x))
      ( eq-set-quotient-equivalence-class-set-quotient
        ( equivalence-relation-sim-Pseudometric-Space P)
        ( X)
        ( x∈X))
      ( is-extension-exten-short-map-metric-quotient-Pseudometric-Space x)

Extensions of short maps along the natural inclusion into the metric quotient

The property of being the extension of a short map

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  (g : short-map-Metric-Space (metric-quotient-Pseudometric-Space P) M)
  where

  is-extension-prop-short-map-metric-quotient-Pseudometric-Space :
    Prop (l1 ⊔ l1')
  is-extension-prop-short-map-metric-quotient-Pseudometric-Space =
    Π-Prop
      ( type-Pseudometric-Space P)
      ( λ x →
        eq-prop-Metric-Space
          ( M)
          ( map-short-map-Pseudometric-Space
            ( P)
            ( pseudometric-Metric-Space M)
            ( precomp-short-map-metric-quotient-Pseudometric-Space P M g)
            ( x))
          ( map-short-map-Pseudometric-Space
            ( P)
            ( pseudometric-Metric-Space M)
            ( f)
            ( x)))

  is-extension-short-map-metric-quotient-Pseudometric-Space : UU (l1 ⊔ l1')
  is-extension-short-map-metric-quotient-Pseudometric-Space =
    type-Prop
      is-extension-prop-short-map-metric-quotient-Pseudometric-Space

  is-prop-is-extension-short-map-metric-quotient-Pseudometric-Space :
    is-prop
      is-extension-short-map-metric-quotient-Pseudometric-Space
  is-prop-is-extension-short-map-metric-quotient-Pseudometric-Space =
    is-prop-type-Prop
      is-extension-prop-short-map-metric-quotient-Pseudometric-Space

The type of extensions of short maps

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where

  extension-short-map-metric-quotient-Pseudometric-Space :
    UU (l1 ⊔ l2 ⊔ l1' ⊔ l2')
  extension-short-map-metric-quotient-Pseudometric-Space =
    Σ ( short-map-Metric-Space (metric-quotient-Pseudometric-Space P) M)
      ( is-extension-short-map-metric-quotient-Pseudometric-Space P M f)

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  (g : extension-short-map-metric-quotient-Pseudometric-Space P M f)
  where

  short-map-extension-short-map-metric-quotient-Pseudometric-Space :
    short-map-Metric-Space (metric-quotient-Pseudometric-Space P) M
  short-map-extension-short-map-metric-quotient-Pseudometric-Space = pr1 g

  map-extension-short-map-metric-quotient-Pseudometric-Space :
    map-Metric-Space (metric-quotient-Pseudometric-Space P) M
  map-extension-short-map-metric-quotient-Pseudometric-Space =
    map-short-map-Metric-Space
      ( metric-quotient-Pseudometric-Space P)
      ( M)
      ( short-map-extension-short-map-metric-quotient-Pseudometric-Space)

  is-extension-short-map-extension-short-map-metric-quotient-Pseudometric-Space :
    map-extension-short-map-metric-quotient-Pseudometric-Space ∘
    map-metric-quotient-Pseudometric-Space P ~
    map-short-map-Pseudometric-Space P (pseudometric-Metric-Space M) f
  is-extension-short-map-extension-short-map-metric-quotient-Pseudometric-Space
    = pr2 g

Properties

Extensions are fibers of the precomposition by the natural inclusion of metric quotients

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where

  compute-extension-fiber-precomp-short-map-metric-quotient-Pseudometric-Space :
    fiber (precomp-short-map-metric-quotient-Pseudometric-Space P M) f ≃
    extension-short-map-metric-quotient-Pseudometric-Space P M f
  compute-extension-fiber-precomp-short-map-metric-quotient-Pseudometric-Space =
    equiv-tot
      ( λ g →
        equiv-eq-htpy-map-short-map-Pseudometric-Space
          ( P)
          ( pseudometric-Metric-Space M)
          ( precomp-short-map-metric-quotient-Pseudometric-Space P M g)
          ( f))

The unique extension from the quotient metric space is short

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where abstract

  is-short-map-exten-short-map-metric-quotient-Pseudometric-Space :
    is-short-map-Metric-Space
      ( metric-quotient-Pseudometric-Space P)
      ( M)
      ( map-exten-short-map-metric-quotient-Pseudometric-space P M f)
  is-short-map-exten-short-map-metric-quotient-Pseudometric-Space
    d X Y N⟨X,Y⟩ =
    let
      open
        do-syntax-trunc-Prop
          ( neighborhood-prop-Metric-Space
            ( M)
            ( d)
            ( map-exten-short-map-metric-quotient-Pseudometric-space P M f X)
            ( map-exten-short-map-metric-quotient-Pseudometric-space P M f Y))
      in do
        ( x , x∈X) ←
          is-inhabited-subtype-set-quotient
            ( equivalence-relation-sim-Pseudometric-Space P)
            ( X)
        ( y , y∈Y) ←
          is-inhabited-subtype-set-quotient
            ( equivalence-relation-sim-Pseudometric-Space P)
            ( Y)

        binary-tr
          ( neighborhood-Metric-Space M d)
          ( inv
            ( compute-map-exten-short-map-metric-quotient-Pseudometric-Space
              ( P)
              ( M)
              ( f)
              ( X)
              ( x∈X)))
          ( inv
            ( compute-map-exten-short-map-metric-quotient-Pseudometric-Space
              ( P)
              ( M)
              ( f)
              ( Y)
              ( y∈Y)))
          ( is-short-map-short-map-Pseudometric-Space
            ( P)
            ( pseudometric-Metric-Space M)
            ( f)
            ( d)
            ( x)
            ( y)
            ( N⟨X,Y⟩ (x , x∈X) (y , y∈Y)))

The extension induced by a short map

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where

  short-map-exten-short-map-metric-quotient-Pseudometric-Space :
    short-map-Metric-Space (metric-quotient-Pseudometric-Space P) M
  short-map-exten-short-map-metric-quotient-Pseudometric-Space =
    ( map-exten-short-map-metric-quotient-Pseudometric-space P M f ,
      is-short-map-exten-short-map-metric-quotient-Pseudometric-Space P M f)

  exten-short-map-metric-quotient-Pseudometric-Space :
    extension-short-map-metric-quotient-Pseudometric-Space P M f
  exten-short-map-metric-quotient-Pseudometric-Space =
    ( short-map-exten-short-map-metric-quotient-Pseudometric-Space ,
      is-extension-exten-short-map-metric-quotient-Pseudometric-Space P M f)

All extensions are homotopic to the induced extension

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where abstract

  all-htpy-map-extension-short-map-metric-quotient-Pseudometric-Space :
    (g : extension-short-map-metric-quotient-Pseudometric-Space P M f) →
    htpy-map-short-map-Metric-Space
      ( metric-quotient-Pseudometric-Space P)
      ( M)
      ( short-map-exten-short-map-metric-quotient-Pseudometric-Space P M f)
      ( short-map-extension-short-map-metric-quotient-Pseudometric-Space
        ( P)
        ( M)
        ( f)
        ( g))
  all-htpy-map-extension-short-map-metric-quotient-Pseudometric-Space g X =
    let
      open
        do-syntax-trunc-Prop
          ( eq-prop-Metric-Space M
            ( map-exten-short-map-metric-quotient-Pseudometric-space P M f X)
            ( map-extension-short-map-metric-quotient-Pseudometric-Space
              ( P)
              ( M)
              ( f)
              ( g)
              ( X)))

    in do
      ( x , x∈X) ←
        is-inhabited-class-metric-quotient-Pseudometric-Space P X

      let
        lemma-lhs =
          compute-map-exten-short-map-metric-quotient-Pseudometric-Space
            ( P)
            ( M)
            ( f)
            ( X)
            ( x∈X)

        lemma-mhs =
          is-extension-short-map-extension-short-map-metric-quotient-Pseudometric-Space
            ( P)
            ( M)
            ( f)
            ( g)
            ( x)

        lemma-rhs =
          ap
            ( map-extension-short-map-metric-quotient-Pseudometric-Space
              ( P)
              ( M)
              ( f)
              ( g))
            ( eq-map-is-in-class-metric-quotient-Pseudometric-Space P X x∈X)

      lemma-lhs ∙ (inv lemma-mhs) ∙ lemma-rhs

All extensions are equal to the induced extension

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where abstract

  contraction-extension-short-map-metric-quotient-Pseudometric-Space :
    (g : extension-short-map-metric-quotient-Pseudometric-Space P M f) →
    exten-short-map-metric-quotient-Pseudometric-Space P M f ＝ g
  contraction-extension-short-map-metric-quotient-Pseudometric-Space g =
    eq-type-subtype
      ( is-extension-prop-short-map-metric-quotient-Pseudometric-Space P M f)
      ( eq-htpy-map-short-map-Metric-Space
        ( metric-quotient-Pseudometric-Space P)
        ( M)
        ( short-map-exten-short-map-metric-quotient-Pseudometric-Space P M f)
        ( short-map-extension-short-map-metric-quotient-Pseudometric-Space
          ( P)
          ( M)
          ( f)
          ( g))
        ( all-htpy-map-extension-short-map-metric-quotient-Pseudometric-Space
          ( P)
          ( M)
          ( f)
          ( g)))

The type of extensions of a short map is contractible

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M))
  where

  is-contr-extension-short-map-metric-quotient-Pseudometric-Space :
    is-contr
      ( extension-short-map-metric-quotient-Pseudometric-Space P M f)
  is-contr-extension-short-map-metric-quotient-Pseudometric-Space =
    ( exten-short-map-metric-quotient-Pseudometric-Space P M f ,
      contraction-extension-short-map-metric-quotient-Pseudometric-Space P M f)

Precomposing by the natual isometry of metric quotients is an equivalence

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  where abstract

  is-contr-map-precomp-short-map-metric-quotient-Pseudometric-Space :
    (f : short-map-Pseudometric-Space P (pseudometric-Metric-Space M)) →
    is-contr
      (fiber (precomp-short-map-metric-quotient-Pseudometric-Space P M) f)
  is-contr-map-precomp-short-map-metric-quotient-Pseudometric-Space f =
    is-contr-equiv
      ( extension-short-map-metric-quotient-Pseudometric-Space P M f)
      ( compute-extension-fiber-precomp-short-map-metric-quotient-Pseudometric-Space
        ( P)
        ( M)
        ( f))
      ( is-contr-extension-short-map-metric-quotient-Pseudometric-Space P M f)

  is-equiv-precomp-short-map-metric-quotient-Pseudometric-Space :
    is-equiv
      (precomp-short-map-metric-quotient-Pseudometric-Space P M)
  is-equiv-precomp-short-map-metric-quotient-Pseudometric-Space =
    is-equiv-is-contr-map
      is-contr-map-precomp-short-map-metric-quotient-Pseudometric-Space

The equivalence between short maps from a pseudometric space in a metric space and short maps from the metric quotient

module _
  {l1 l2 l1' l2' : Level}
  (P : Pseudometric-Space l1 l2)
  (M : Metric-Space l1' l2')
  where

  equiv-short-map-metric-quotient-Pseudometric-Space :
    short-map-Metric-Space (metric-quotient-Pseudometric-Space P) M ≃
    short-map-Pseudometric-Space P (pseudometric-Metric-Space M)
  equiv-short-map-metric-quotient-Pseudometric-Space =
    ( precomp-short-map-metric-quotient-Pseudometric-Space P M ,
      is-equiv-precomp-short-map-metric-quotient-Pseudometric-Space P M)

Recent changes