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 2023-09-12.

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

Idea

A retraction is a map that has a right inverse, i.e. a section. Thus, r : B → A is a retraction of f : A → B if the composition r ∘ f is homotopic to the identity at A. Moreover, in this case we say that A is a retract of B.

Definition

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

  retraction : (f : A  B)  UU (l1  l2)
  retraction f = Σ (B  A)  r  (r  f) ~ id)

  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

_retract-of_ :
  {l1 l2 : Level}  UU l1  UU l2  UU (l1  l2)
A retract-of B = Σ (A  B) retraction

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

  section-retract-of : A retract-of B  A  B
  section-retract-of = pr1

  retraction-section-retract-of :
    (R : A retract-of B)  retraction (section-retract-of R)
  retraction-section-retract-of = pr2

  retraction-retract-of : (A retract-of B)  B  A
  retraction-retract-of R = pr1 (retraction-section-retract-of R)

  is-retraction-retraction-retract-of :
    (R : A retract-of B) 
    (retraction-retract-of R  section-retract-of R) ~ id
  is-retraction-retraction-retract-of R = pr2 (retraction-section-retract-of R)

Properties

If A is a retraction of B, then the identity types of A are retractions of the identity types of B

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

  ap-retraction :
    (i : A  B) (r : B  A) (H : (r  i) ~ id)
    (x y : A)  i x  i y  x  y
  ap-retraction i r H x y p =
      ( inv (H x))  ((ap r p)  (H y))

  is-retraction-ap-retraction :
    (i : A  B) (r : B  A) (H : (r  i) ~ id)
    (x y : A)  ((ap-retraction i r H x y)  (ap i {x} {y})) ~ id
  is-retraction-ap-retraction i r H x .x refl = left-inv (H x)

  retraction-ap :
    (i : A  B)  retraction i  (x y : A)  retraction (ap i {x} {y})
  pr1 (retraction-ap i (pair r H) x y) = ap-retraction i r H x y
  pr2 (retraction-ap i (pair r H) x y) = is-retraction-ap-retraction i r H x y

  retract-eq :
    (R : A retract-of B)  (x y : A)  (x  y) retract-of (pr1 R x  pr1 R y)
  pr1 (retract-eq (pair i (pair r H)) x y) = ap i
  pr2 (retract-eq (pair i (pair r H)) x y) = retraction-ap i (pair r H) x y

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

  retraction-right-factor :
    (g : B  X) (h : A  B)  retraction (g  h)  retraction h
  pr1 (retraction-right-factor g h retraction-gh) = pr1 retraction-gh  g
  pr2 (retraction-right-factor g h retraction-gh) = pr2 retraction-gh

  retraction-right-factor-htpy :
    (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
    retraction f  retraction h
  pr1 (retraction-right-factor-htpy f g h H retraction-f) =
    pr1 retraction-f  g
  pr2 (retraction-right-factor-htpy f g h H retraction-f) =
    (inv-htpy ((pr1 retraction-f) ·l H)) ∙h (pr2 retraction-f)

Composites of retractions are retractions

  retraction-comp :
    (g : B  X) (h : A  B)  retraction g  retraction h  retraction (g  h)
  pr1 (retraction-comp g h retraction-g retraction-h) =
    pr1 retraction-h  pr1 retraction-g
  pr2 (retraction-comp g h retraction-g retraction-h) =
    ((pr1 retraction-h) ·l (pr2 retraction-g ·r h)) ∙h (pr2 retraction-h)

  retraction-comp-htpy :
    (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h)) 
    retraction g  retraction h  retraction f
  pr1 (retraction-comp-htpy f g h H retraction-g retraction-h) =
    pr1 (retraction-comp g h retraction-g retraction-h)
  pr2 (retraction-comp-htpy f g h H retraction-g retraction-h) =
    ( pr1 (retraction-comp g h retraction-g retraction-h) ·l H) ∙h
    pr2 (retraction-comp g h retraction-g retraction-h)

  inv-triangle-retraction :
    (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h))
    (retraction-g : retraction g)  ((pr1 retraction-g)  f) ~ h
  inv-triangle-retraction f g h H retraction-g =
    (pr1 retraction-g ·l H) ∙h (pr2 retraction-g ·r h)

  triangle-retraction :
    (f : A  X) (g : B  X) (h : A  B) (H : f ~ (g  h))
    (retraction-g : retraction g)  h ~ ((pr1 retraction-g)  f)
  triangle-retraction f g h H retraction-g =
    inv-htpy (inv-triangle-retraction f g h H retraction-g)

Recent changes