# Invertible maps

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-11.

module foundation-core.invertible-maps where

Imports
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


## 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-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}
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-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


## Properties

### The invertible inverse of an invertible map

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

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)