Retractions

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

Created on 2022-02-04.
Last modified on 2024-04-25.

module foundation-core.retractions 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.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types

Idea

A retraction of a map f : A → B consists of a map r : B → A equipped with a homotopy r ∘ f ~ id. In other words, a retraction of a map f is a left inverse of f.

Definitions

The type of retractions

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

  is-retraction : (f : A → B) (g : B → A) → UU l1
  is-retraction f g = g ∘ f ~ id

  retraction : (f : A → B) → UU (l1 ⊔ l2)
  retraction f = Σ (B → A) (is-retraction f)

  map-retraction : (f : A → B) → retraction f → B → A
  map-retraction f = pr1

  is-retraction-map-retraction :
    (f : A → B) (r : retraction f) → map-retraction f r ∘ f ~ id
  is-retraction-map-retraction f = pr2

Properties

For any map `i : A → B`, a retraction of `i` induces a retraction of the action on identifications of `i`

Proof: Suppose that H : r ∘ i ~ id and p : i x ＝ i y is an identification in B. Then we get the identification

     (H x)⁻¹           ap r p           H y
  x ========= r (i x) ======== r (i y) ===== y

This defines a map s : (i x ＝ i y) → x ＝ y. To see that s ∘ ap i ~ id, i.e., that the concatenation

     (H x)⁻¹           ap r (ap i p)           H y
  x ========= r (i x) =============== r (i y) ===== y

is identical to p : x ＝ y for all p : x ＝ y, we proceed by identification elimination. Then it suffices to show that (H x)⁻¹ ∙ (H x) is identical to refl, which is indeed the case by the left inverse law of concatenation of identifications.

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B)
  (r : B → A) (H : r ∘ i ~ id)
  where

  is-injective-has-retraction :
    {x y : A} → i x ＝ i y → x ＝ y
  is-injective-has-retraction {x} {y} p = inv (H x) ∙ (ap r p ∙ H y)

  is-retraction-is-injective-has-retraction :
    {x y : A} → is-injective-has-retraction ∘ ap i {x} {y} ~ id
  is-retraction-is-injective-has-retraction {x} refl = left-inv (H x)

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B) (R : retraction i)
  where

  is-injective-retraction :
    {x y : A} → i x ＝ i y → x ＝ y
  is-injective-retraction =
    is-injective-has-retraction i
      ( map-retraction i R)
      ( is-retraction-map-retraction i R)

  is-retraction-is-injective-retraction :
    {x y : A} → is-injective-retraction ∘ ap i {x} {y} ~ id
  is-retraction-is-injective-retraction =
    is-retraction-is-injective-has-retraction i
      ( map-retraction i R)
      ( is-retraction-map-retraction i R)

  retraction-ap : {x y : A} → retraction (ap i {x} {y})
  pr1 retraction-ap = is-injective-retraction
  pr2 retraction-ap = is-retraction-is-injective-retraction

Composites of retractions are retractions

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (g : B → X) (h : A → B) (r : retraction g) (s : retraction h)
  where

  map-retraction-comp : X → A
  map-retraction-comp = map-retraction h s ∘ map-retraction g r

  is-retraction-map-retraction-comp : is-retraction (g ∘ h) map-retraction-comp
  is-retraction-map-retraction-comp =
    ( map-retraction h s ·l (is-retraction-map-retraction g r ·r h)) ∙h
    ( is-retraction-map-retraction h s)

  retraction-comp : retraction (g ∘ h)
  pr1 retraction-comp = map-retraction-comp
  pr2 retraction-comp = is-retraction-map-retraction-comp

If `g ∘ f` has a retraction then `f` has a retraction

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (g : B → X) (h : A → B) (r : retraction (g ∘ h))
  where

  map-retraction-right-factor : B → A
  map-retraction-right-factor = map-retraction (g ∘ h) r ∘ g

  is-retraction-map-retraction-right-factor :
    is-retraction h map-retraction-right-factor
  is-retraction-map-retraction-right-factor =
    is-retraction-map-retraction (g ∘ h) r

  retraction-right-factor : retraction h
  pr1 retraction-right-factor = map-retraction-right-factor
  pr2 retraction-right-factor = is-retraction-map-retraction-right-factor

In a commuting triangle `f ~ g ∘ h`, any retraction of the left map `f` induces a retraction of the top map `h`

In a commuting triangle of the form

       h
  A ------> B
   \       /
   f\     /g
     \   /
      ∨ ∨
       X,

if r : X → A is a retraction of the map f on the left, then r ∘ g is a retraction of the top map h.

Note: In this file we are unable to use the definition of commuting triangles, because that would result in a cyclic module dependency.

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h)
  (r : retraction f)
  where

  map-retraction-top-map-triangle : B → A
  map-retraction-top-map-triangle = map-retraction f r ∘ g

  is-retraction-map-retraction-top-map-triangle :
    is-retraction h map-retraction-top-map-triangle
  is-retraction-map-retraction-top-map-triangle =
    ( inv-htpy (map-retraction f r ·l H)) ∙h
    ( is-retraction-map-retraction f r)

  retraction-top-map-triangle : retraction h
  pr1 retraction-top-map-triangle =
    map-retraction-top-map-triangle
  pr2 retraction-top-map-triangle =
    is-retraction-map-retraction-top-map-triangle

In a commuting triangle `f ~ g ∘ h`, retractions of `g` and `h` compose to a retraction of `f`