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-03-20.

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
     \   /
      V V
       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

In a commuting triangle of the form

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

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

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 g) (s : retraction h)
  where

  map-retraction-left-map-triangle : X  A
  map-retraction-left-map-triangle = map-retraction-comp g h r s

  is-retraction-map-retraction-left-map-triangle :
    is-retraction f map-retraction-left-map-triangle
  is-retraction-map-retraction-left-map-triangle =
    ( map-retraction-comp g h r s ·l H) ∙h
    ( is-retraction-map-retraction-comp g h r s)

  retraction-left-map-triangle : retraction f
  pr1 retraction-left-map-triangle =
    map-retraction-left-map-triangle
  pr2 retraction-left-map-triangle =
    is-retraction-map-retraction-left-map-triangle

See also

Recent changes