Invertible maps

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-11.
Last modified on 2023-09-11.

module foundation-core.invertible-maps where
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.retractions
open import foundation-core.sections


An inverse for a map f : A → B is a map g : B → A equipped with homotopies (f ∘ g) ~ id and (g ∘ f) ~ id. Such data, however is structure on the map f, and not generally a property.


The predicate that a map g is an inverse of a map f

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

  is-inverse : (A  B)  (B  A)  UU (l1  l2)
  is-inverse f g = ((f  g) ~ id) × ((g  f) ~ id)

  is-section-is-inverse :
    {f : A  B} {g : B  A}  is-inverse f g  (f  g) ~ id
  is-section-is-inverse = pr1

  is-retraction-is-inverse :
    {f : A  B} {g : B  A}  is-inverse f g  (g  f) ~ id
  is-retraction-is-inverse = pr2

The predicate that a map f is invertible

is-invertible :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}  (A  B)  UU (l1  l2)
is-invertible {A = A} {B} f = Σ (B  A) (is-inverse f)

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} (g : is-invertible f)

  map-inv-is-invertible : B  A
  map-inv-is-invertible = pr1 g

  is-inverse-map-inv-is-invertible : is-inverse f map-inv-is-invertible
  is-inverse-map-inv-is-invertible = pr2 g

  is-retraction-is-invertible : (f  map-inv-is-invertible) ~ id
  is-retraction-is-invertible = pr1 is-inverse-map-inv-is-invertible

  is-section-is-invertible : (map-inv-is-invertible  f) ~ id
  is-section-is-invertible = pr2 is-inverse-map-inv-is-invertible

  section-is-invertible : section f
  pr1 section-is-invertible = map-inv-is-invertible
  pr2 section-is-invertible = is-retraction-is-invertible

  retraction-is-invertible : retraction f
  pr1 retraction-is-invertible = map-inv-is-invertible
  pr2 retraction-is-invertible = is-section-is-invertible

The type of invertible maps

invertible-map : {l1 l2 : Level} (A : UU l1) (B : UU l2)  UU (l1  l2)
invertible-map A B = Σ (A  B) (is-invertible)

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

  map-invertible-map : invertible-map A B  A  B
  map-invertible-map = pr1

  is-invertible-map-invertible-map :
    (f : invertible-map A B)  is-invertible (map-invertible-map f)
  is-invertible-map-invertible-map = pr2

  map-inv-invertible-map : invertible-map A B  B  A
  map-inv-invertible-map =
    map-inv-is-invertible  is-invertible-map-invertible-map

  is-section-map-invertible-map :
    (f : invertible-map A B) 
    (map-inv-invertible-map f  map-invertible-map f) ~ id
  is-section-map-invertible-map =
    is-section-is-invertible  is-invertible-map-invertible-map

  is-retraction-map-invertible-map :
    (f : invertible-map A B) 
    (map-invertible-map f  map-inv-invertible-map f) ~ id
  is-retraction-map-invertible-map =
    is-retraction-is-invertible  is-invertible-map-invertible-map


The invertible inverse of an invertible map

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}

  inv-is-inverse : {g : B  A}  is-inverse f g  is-inverse g f
  pr1 (inv-is-inverse {g} H) = is-section-is-invertible (g , H)
  pr2 (inv-is-inverse {g} H) = is-retraction-is-invertible (g , H)

  inv-is-invertible :
    (g : is-invertible f)  is-invertible (map-inv-is-invertible g)
  pr1 (inv-is-invertible g) = f
  pr2 (inv-is-invertible g) =
    inv-is-inverse (is-inverse-map-inv-is-invertible g)

See also

Recent changes