# Invertible maps

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-11.

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)