Coherently invertible maps

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, Raymond Baker, fernabnor and louismntnu.

Created on 2022-02-07.
Last modified on 2023-09-12.

module foundation-core.coherently-invertible-maps where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.invertible-maps
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.whiskering-homotopies

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. Therefore we include a coherence condition for the homotopies of an inverse. A coherently invertible map f : A → B is a map equipped with a two-sided inverse and this additional coherence law. They are also called half-adjoint equivalences.

Definition

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

  coherence-is-coherently-invertible :
    (f : A → B) (g : B → A) (G : (f ∘ g) ~ id) (H : (g ∘ f) ~ id) → UU (l1 ⊔ l2)
  coherence-is-coherently-invertible f g G H = (G ·r f) ~ (f ·l H)

  is-coherently-invertible : (A → B) → UU (l1 ⊔ l2)
  is-coherently-invertible f =
    Σ ( B → A)
      ( λ g → Σ ((f ∘ g) ~ id)
        ( λ G → Σ ((g ∘ f) ~ id)
          ( λ H → coherence-is-coherently-invertible f g G H)))

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

  map-inv-is-coherently-invertible : B → A
  map-inv-is-coherently-invertible = pr1 H

  is-retraction-is-coherently-invertible :
    (f ∘ map-inv-is-coherently-invertible) ~ id
  is-retraction-is-coherently-invertible = pr1 (pr2 H)

  is-section-is-coherently-invertible :
    (map-inv-is-coherently-invertible ∘ f) ~ id
  is-section-is-coherently-invertible = pr1 (pr2 (pr2 H))

  coh-is-coherently-invertible :
    coherence-is-coherently-invertible f
      ( map-inv-is-coherently-invertible)
      ( is-retraction-is-coherently-invertible)
      ( is-section-is-coherently-invertible)
  coh-is-coherently-invertible = pr2 (pr2 (pr2 H))

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

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

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

Properties

Invertible maps are coherently invertible

Lemma: A coherence for homotopies to an identity map

coh-is-coherently-invertible-id :
  {l : Level} {A : UU l} {f : A → A} (H : f ~ (λ x → x)) →
  (x : A) → H (f x) ＝ ap f (H x)
coh-is-coherently-invertible-id {_} {A} {f} H x =
  is-injective-concat' (H x)
    ( ( ap (concat (H (f x)) x) (inv (ap-id (H x)))) ∙
      ( nat-htpy H (H x)))

The proof that invertible maps are coherently invertible

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

  abstract
    is-section-map-inv-is-invertible :
      (H : is-invertible f) → (f ∘ map-inv-is-invertible H) ~ id
    is-section-map-inv-is-invertible H y =
      ( inv (is-retraction-is-invertible H (f (map-inv-is-invertible H y)))) ∙
      ( ( ap f (is-section-is-invertible H (map-inv-is-invertible H y))) ∙
        ( is-retraction-is-invertible H y))

    is-retraction-map-inv-is-invertible :
      (H : is-invertible f) → (map-inv-is-invertible H ∘ f) ~ id
    is-retraction-map-inv-is-invertible = is-section-is-invertible

    coherence-map-inv-is-invertible :
      ( H : is-invertible f) →
      ( is-section-map-inv-is-invertible H ·r f) ~
      ( f ·l is-retraction-map-inv-is-invertible H)
    coherence-map-inv-is-invertible H x =
      inv
        ( left-transpose-eq-concat
          ( is-retraction-is-invertible H (f (map-inv-is-invertible H (f x))))
          ( ap f (is-section-is-invertible H x))
          ( ( ap f
              ( is-section-is-invertible H (map-inv-is-invertible H (f x)))) ∙
            ( is-retraction-is-invertible H (f x)))
          ( coherence-square-identifications-top-paste
            ( is-retraction-is-invertible H (f (map-inv-is-invertible H (f x))))
            ( ap f (is-section-is-invertible H x))
            ( ( ap
                ( f ∘ (map-inv-is-invertible H ∘ f))
                ( is-section-is-invertible H x)))
            ( is-retraction-is-invertible H (f x))
            ( ( ap-comp f
                ( map-inv-is-invertible H ∘ f)
                ( is-section-is-invertible H x)) ∙
              ( inv
                ( ap
                  ( ap f)
                  ( coh-is-coherently-invertible-id
                    ( is-section-is-invertible H) x))))
            ( nat-htpy
              ( htpy-right-whisk (is-retraction-is-invertible H) f)
              ( is-section-is-invertible H x))))

  abstract
    is-coherently-invertible-is-invertible :
      (H : is-invertible f) → is-coherently-invertible f
    pr1 (is-coherently-invertible-is-invertible H) =
      map-inv-is-invertible H
    pr1 (pr2 (is-coherently-invertible-is-invertible H)) =
      is-section-map-inv-is-invertible H
    pr1 (pr2 (pr2 (is-coherently-invertible-is-invertible H))) =
      is-retraction-map-inv-is-invertible H
    pr2 (pr2 (pr2 (is-coherently-invertible-is-invertible H))) =
      coherence-map-inv-is-invertible H

See also

Recent changes