Invertible maps

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-11.
Last modified on 2024-04-17.

module foundation-core.invertible-maps where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

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

Idea

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.

Definition

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

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

  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)
  where

  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-section-map-inv-is-invertible : f ∘ map-inv-is-invertible ~ id
  is-section-map-inv-is-invertible = pr1 is-inverse-map-inv-is-invertible

  is-retraction-map-inv-is-invertible : map-inv-is-invertible ∘ f ~ id
  is-retraction-map-inv-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-section-map-inv-is-invertible

  retraction-is-invertible : retraction f
  pr1 retraction-is-invertible = map-inv-is-invertible
  pr2 retraction-is-invertible = is-retraction-map-inv-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}
  where

  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-retraction-map-inv-invertible-map :
    (f : invertible-map A B) →
    map-inv-invertible-map f ∘ map-invertible-map f ~ id
  is-retraction-map-inv-invertible-map =
    is-retraction-map-inv-is-invertible ∘ is-invertible-map-invertible-map

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

Properties

The identity invertible map

module _
  {l1 : Level} {A : UU l1}
  where

  is-inverse-id : is-inverse id (id {A = A})
  pr1 is-inverse-id = refl-htpy
  pr2 is-inverse-id = refl-htpy

  is-invertible-id : is-invertible (id {A = A})
  pr1 is-invertible-id = id
  pr2 is-invertible-id = is-inverse-id

  id-invertible-map : invertible-map A A
  pr1 id-invertible-map = id
  pr2 id-invertible-map = is-invertible-id

The inverse of an invertible map

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

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

  is-invertible-map-inv-is-invertible :
    {f : A → B} (g : is-invertible f) → is-invertible (map-inv-is-invertible g)
  pr1 (is-invertible-map-inv-is-invertible {f} g) = f
  pr2 (is-invertible-map-inv-is-invertible {f} g) =
    is-inverse-inv-is-inverse {f} (is-inverse-map-inv-is-invertible g)

  is-invertible-map-inv-invertible-map :
    (f : invertible-map A B) → is-invertible (map-inv-invertible-map f)
  is-invertible-map-inv-invertible-map f =
    is-invertible-map-inv-is-invertible (is-invertible-map-invertible-map f)

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

The inversion operation on invertible maps is a strict involution

The inversion operation on invertible maps is a strict involution, where, by strict involution, we mean that inv-invertible-map (inv-invertible-map f) ≐ f syntactically. This can be observed by the fact that the type-checker accepts refl as proof of this equation.

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

  is-involution-inv-invertible-map :
    {f : invertible-map A B} → inv-invertible-map (inv-invertible-map f) ＝ f
  is-involution-inv-invertible-map = refl

Composition of invertible maps

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  (g : B → C) (f : A → B) (G : is-invertible g) (F : is-invertible f)
  where

  map-inv-is-invertible-comp : C → A
  map-inv-is-invertible-comp =
    map-inv-is-invertible F ∘ map-inv-is-invertible G

  is-section-map-inv-is-invertible-comp :
    is-section (g ∘ f) map-inv-is-invertible-comp
  is-section-map-inv-is-invertible-comp =
    is-section-map-section-comp g f
      ( section-is-invertible F)
      ( section-is-invertible G)

  is-retraction-map-inv-is-invertible-comp :
    is-retraction (g ∘ f) map-inv-is-invertible-comp
  is-retraction-map-inv-is-invertible-comp =
    is-retraction-map-retraction-comp g f
      ( retraction-is-invertible G)
      ( retraction-is-invertible F)

  is-invertible-comp : is-invertible (g ∘ f)
  is-invertible-comp =
    ( map-inv-is-invertible-comp ,
      is-section-map-inv-is-invertible-comp ,
      is-retraction-map-inv-is-invertible-comp)

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  where

  is-invertible-map-comp-invertible-map :
    (g : invertible-map B C) (f : invertible-map A B) →
    is-invertible (map-invertible-map g ∘ map-invertible-map f)
  is-invertible-map-comp-invertible-map g f =
    is-invertible-comp
      ( map-invertible-map g)
      ( map-invertible-map f)
      ( is-invertible-map-invertible-map g)
      ( is-invertible-map-invertible-map f)

  comp-invertible-map :
    invertible-map B C → invertible-map A B → invertible-map A C
  pr1 (comp-invertible-map g f) = map-invertible-map g ∘ map-invertible-map f
  pr2 (comp-invertible-map g f) = is-invertible-map-comp-invertible-map g f

Invertible maps are closed under homotopies

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

  is-section-map-inv-is-invertible-htpy :
    {f f' : A → B} (H : f' ~ f) (F : is-invertible f) →
    is-section f' (map-inv-is-invertible F)
  is-section-map-inv-is-invertible-htpy H (g , S , R) = H ·r g ∙h S

  is-retraction-map-inv-is-invertible-htpy :
    {f f' : A → B} (H : f' ~ f) (F : is-invertible f) →
    is-retraction f' (map-inv-is-invertible F)
  is-retraction-map-inv-is-invertible-htpy H (g , S , R) = g ·l H ∙h R

  is-invertible-htpy :
    {f f' : A → B} → f' ~ f → is-invertible f → is-invertible f'
  is-invertible-htpy H F =
    ( map-inv-is-invertible F ,
      is-section-map-inv-is-invertible-htpy H F ,
      is-retraction-map-inv-is-invertible-htpy H F)

  is-invertible-inv-htpy :
    {f f' : A → B} → f ~ f' → is-invertible f → is-invertible f'
  is-invertible-inv-htpy H = is-invertible-htpy (inv-htpy H)

  htpy-map-inv-is-invertible :
    {f g : A → B} (H : f ~ g) (F : is-invertible f) (G : is-invertible g) →
    map-inv-is-invertible F ~ map-inv-is-invertible G
  htpy-map-inv-is-invertible H F G =
    ( ( inv-htpy (is-retraction-map-inv-is-invertible G)) ·r
      ( map-inv-is-invertible F)) ∙h
    ( ( map-inv-is-invertible G) ·l
      ( ( inv-htpy H ·r map-inv-is-invertible F) ∙h
        ( is-section-map-inv-is-invertible F)))

Any section of an invertible map is homotopic to its inverse

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : invertible-map A B)
  where

  htpy-map-inv-invertible-map-section :
    (f : section (map-invertible-map e)) →
    map-inv-invertible-map e ~
    map-section (map-invertible-map e) f
  htpy-map-inv-invertible-map-section (f , H) =
    ( map-inv-invertible-map e ·l inv-htpy H) ∙h
    ( is-retraction-map-inv-invertible-map e ·r f)

Any retraction of an invertible map is homotopic to its inverse

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : invertible-map A B)
  where

  htpy-map-inv-invertible-map-retraction :
    (f : retraction (map-invertible-map e)) →
    map-inv-invertible-map e ~
    map-retraction (map-invertible-map e) f
  htpy-map-inv-invertible-map-retraction (f , H) =
    ( inv-htpy H ·r map-inv-invertible-map e) ∙h
    ( f ·l is-section-map-inv-invertible-map e)

Invertible maps are injective

The construction of the converse map of the action on identifications is a rerun of the proof that maps with retractions are injective (is-injective-retraction). We repeat the proof to avoid cyclic dependencies.

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

  is-injective-is-invertible : {x y : A} → f x ＝ f y → x ＝ y
  is-injective-is-invertible =
    is-injective-retraction f (retraction-is-invertible H)

See also

Recent changes