Equality of metric spaces

Content created by Fredrik Bakke and malarbol.

Created on 2024-09-28.
Last modified on 2024-09-28.

module metric-spaces.equality-of-metric-spaces where
Imports 
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import metric-spaces.equality-of-premetric-spaces
open import metric-spaces.isometric-equivalences-premetric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.premetric-spaces

Idea

Equality of metric spaces is equivalent to equality of their carrier premetric spaces; therefore, isometric equality between metric spaces characterizes their equality, which in turn means that equality is characterized by isometric equivalence between their carrier premetric spaces.

Definitions

Equality of metric spaces is equivalent to equality of their carrier premetric spaces

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

  equiv-eq-premetric-Metric-Space :
    (A ＝ B) ≃ (premetric-Metric-Space A ＝ premetric-Metric-Space B)
  equiv-eq-premetric-Metric-Space =
    extensionality-type-subtype' is-metric-prop-Premetric-Space A B

Isometric equality of metric spaces

module _
  {l1 l2 l2' : Level}
  (A : Metric-Space l1 l2) (B : Metric-Space l1 l2')
  where

  isometric-eq-Metric-Space : UU (lsuc l1 ⊔ l2 ⊔ l2')
  isometric-eq-Metric-Space =
    isometric-eq-Premetric-Space
      (premetric-Metric-Space A)
      (premetric-Metric-Space B)

Isometric equivalence of metric spaces

module _
  {l1 l2 l1' l2' : Level}
  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
  where

  isometric-equiv-Metric-Space : UU (l1 ⊔ l2 ⊔ l1' ⊔ l2')
  isometric-equiv-Metric-Space =
    isometric-equiv-Premetric-Space
      (premetric-Metric-Space A)
      (premetric-Metric-Space B)

Isometric equivalences between metric spaces

module _
  {l1 l2 l1' l2' : Level}
  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
  where

  isometric-equiv-Metric-Space' : UU (l1 ⊔ l2 ⊔ l1' ⊔ l2')
  isometric-equiv-Metric-Space' =
    isometric-equiv-Premetric-Space'
      (premetric-Metric-Space A)
      (premetric-Metric-Space B)

Properties

Equality of metric spaces is equivalent to isometric equality of their carrier types

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

  equiv-isometric-eq-eq-Metric-Space : (A ＝ B) ≃ isometric-eq-Metric-Space A B
  equiv-isometric-eq-eq-Metric-Space =
    ( equiv-isometric-eq-eq-Premetric-Space
      ( premetric-Metric-Space A)
      ( premetric-Metric-Space B)) ∘e
    ( equiv-eq-premetric-Metric-Space A B)

  eq-isometric-eq-Metric-Space : isometric-eq-Metric-Space A B → A ＝ B
  eq-isometric-eq-Metric-Space =
    map-inv-equiv equiv-isometric-eq-eq-Metric-Space

Isometric equality is torsorial

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

  is-torsorial-isometric-eq-Metric-Space :
    is-torsorial (isometric-eq-Metric-Space A)
  is-torsorial-isometric-eq-Metric-Space =
    is-contr-equiv'
      ( Σ (Metric-Space l1 l2) (Id A))
      ( equiv-tot (equiv-isometric-eq-eq-Metric-Space A))
      ( is-torsorial-Id A)

Equality of metric spaces is equivalent to isometric equivalence of their carrier types

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

  equiv-isometric-equiv-eq-Metric-Space :
    (A ＝ B) ≃ isometric-equiv-Metric-Space A B
  equiv-isometric-equiv-eq-Metric-Space =
    ( equiv-isometric-equiv-eq-Premetric-Space
      ( premetric-Metric-Space A)
      ( premetric-Metric-Space B)) ∘e
    ( equiv-eq-premetric-Metric-Space A B)

  eq-isometric-equiv-Metric-Space : isometric-equiv-Metric-Space A B → A ＝ B
  eq-isometric-equiv-Metric-Space =
    map-inv-equiv equiv-isometric-equiv-eq-Metric-Space

Isometric equivalence between metric spaces is torsorial

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

  is-torsorial-isometric-equiv-Metric-Space :
    is-torsorial (isometric-equiv-Metric-Space A)
  is-torsorial-isometric-equiv-Metric-Space =
    is-contr-equiv'
      ( Σ (Metric-Space l1 l2) (Id A))
      ( equiv-tot (equiv-isometric-equiv-eq-Metric-Space A))
      ( is-torsorial-Id A)

Equality of metric spaces is equivalent to the existence of isometric equivalence between their carrier types

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

  equiv-isometric-equiv-eq-Metric-Space' :
    (A ＝ B) ≃ isometric-equiv-Metric-Space' A B
  equiv-isometric-equiv-eq-Metric-Space' =
    ( equiv-isometric-equiv-eq-Premetric-Space'
      ( premetric-Metric-Space A)
      ( premetric-Metric-Space B)) ∘e
    ( equiv-eq-premetric-Metric-Space A B)

  eq-isometric-equiv-Metric-Space' :
    isometric-equiv-Metric-Space' A B → A ＝ B
  eq-isometric-equiv-Metric-Space' =
    map-inv-equiv equiv-isometric-equiv-eq-Metric-Space'

The existence of invertibe isometries between metric spaces is torsorial

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

  is-torsorial-isometric-equiv-Metric-Space' :
    is-torsorial (isometric-equiv-Metric-Space' A)
  is-torsorial-isometric-equiv-Metric-Space' =
    is-contr-equiv'
      ( Σ (Metric-Space l1 l2) (Id A))
      ( equiv-tot (equiv-isometric-equiv-eq-Metric-Space' A))
      ( is-torsorial-Id A)

Recent changes