Retracts of sequential diagrams

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-05.
Last modified on 2024-01-28.

module synthetic-homotopy-theory.retracts-of-sequential-diagrams where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.retractions
open import foundation.retracts-of-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.morphisms-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams

Idea

A retract of sequential diagrams A of B is a morphism of sequential diagrams B → A that is a retraction.

Definitions

The predicate of being a retraction of sequential diagrams

module _
  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
  (i : hom-sequential-diagram A B) (r : hom-sequential-diagram B A)
  where

  is-retraction-hom-sequential-diagram : UU l1
  is-retraction-hom-sequential-diagram =
    htpy-hom-sequential-diagram A
      ( comp-hom-sequential-diagram A B A r i)
      ( id-hom-sequential-diagram A)

The type of retractions of a morphism of sequential diagrams

module _
  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
  (i : hom-sequential-diagram A B)
  where

  retraction-hom-sequential-diagram : UU (l1 ⊔ l2)
  retraction-hom-sequential-diagram =
    Σ (hom-sequential-diagram B A) (is-retraction-hom-sequential-diagram A B i)

  module _
    (r : retraction-hom-sequential-diagram)
    where

    hom-retraction-hom-sequential-diagram : hom-sequential-diagram B A
    hom-retraction-hom-sequential-diagram = pr1 r

    is-retraction-hom-retraction-hom-sequential-diagram :
      is-retraction-hom-sequential-diagram A B i
        ( hom-retraction-hom-sequential-diagram)
    is-retraction-hom-retraction-hom-sequential-diagram = pr2 r

The predicate that a sequential diagram A is a retract of a sequential diagram B

retract-sequential-diagram :
  {l1 l2 : Level} (B : sequential-diagram l2) (A : sequential-diagram l1) →
  UU (l1 ⊔ l2)
retract-sequential-diagram B A =
  Σ (hom-sequential-diagram A B) (retraction-hom-sequential-diagram A B)

The higher coherence in the definition of retracts of sequential diagrams

module _
  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
  (i : hom-sequential-diagram A B) (r : hom-sequential-diagram B A)
  where

  coherence-retract-sequential-diagram :
    ( (n : ℕ) →
      is-retraction
        ( map-hom-sequential-diagram B i n)
        ( map-hom-sequential-diagram A r n)) →
    UU l1
  coherence-retract-sequential-diagram =
    coherence-htpy-hom-sequential-diagram A
      ( comp-hom-sequential-diagram A B A r i)
      ( id-hom-sequential-diagram A)

The binary relation A B ↦ A retract-of-sequential-diagram B asserting that A is a retract of the sequential diagram B

module _
  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
  where

  infix 6 _retract-of-sequential-diagram_

  _retract-of-sequential-diagram_ : UU (l1 ⊔ l2)
  _retract-of-sequential-diagram_ = retract-sequential-diagram B A

module _
  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
  (R : A retract-of-sequential-diagram B)
  where

  inclusion-retract-sequential-diagram : hom-sequential-diagram A B
  inclusion-retract-sequential-diagram = pr1 R

  map-inclusion-retract-sequential-diagram :
    (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n
  map-inclusion-retract-sequential-diagram =
    map-hom-sequential-diagram B inclusion-retract-sequential-diagram

  naturality-inclusion-retract-sequential-diagram :
    naturality-hom-sequential-diagram A B
      ( map-inclusion-retract-sequential-diagram)
  naturality-inclusion-retract-sequential-diagram =
    naturality-map-hom-sequential-diagram B
      ( inclusion-retract-sequential-diagram)

  retraction-retract-sequential-diagram :
    retraction-hom-sequential-diagram A B inclusion-retract-sequential-diagram
  retraction-retract-sequential-diagram = pr2 R

  hom-retraction-retract-sequential-diagram : hom-sequential-diagram B A
  hom-retraction-retract-sequential-diagram =
    hom-retraction-hom-sequential-diagram A B
      ( inclusion-retract-sequential-diagram)
      ( retraction-retract-sequential-diagram)

  map-hom-retraction-retract-sequential-diagram :
    (n : ℕ) → family-sequential-diagram B n → family-sequential-diagram A n
  map-hom-retraction-retract-sequential-diagram =
    map-hom-sequential-diagram A hom-retraction-retract-sequential-diagram

  naturality-hom-retraction-retract-sequential-diagram :
    naturality-hom-sequential-diagram B A
      ( map-hom-retraction-retract-sequential-diagram)
  naturality-hom-retraction-retract-sequential-diagram =
    naturality-map-hom-sequential-diagram A
      ( hom-retraction-retract-sequential-diagram)

  is-retraction-hom-retraction-retract-sequential-diagram :
    is-retraction-hom-sequential-diagram A B
      ( inclusion-retract-sequential-diagram)
      ( hom-retraction-retract-sequential-diagram)
  is-retraction-hom-retraction-retract-sequential-diagram =
    is-retraction-hom-retraction-hom-sequential-diagram A B
      ( inclusion-retract-sequential-diagram)
      ( retraction-retract-sequential-diagram)

  is-retraction-map-hom-retraction-retract-sequential-diagram :
    (n : ℕ) →
    is-retraction
      ( map-inclusion-retract-sequential-diagram n)
      ( map-hom-retraction-retract-sequential-diagram n)
  is-retraction-map-hom-retraction-retract-sequential-diagram =
    htpy-htpy-hom-sequential-diagram A
      ( is-retraction-hom-retraction-retract-sequential-diagram)

  retract-family-retract-sequential-diagram :
    (n : ℕ) →
    ( family-sequential-diagram A n) retract-of
    ( family-sequential-diagram B n)
  pr1 (retract-family-retract-sequential-diagram n) =
    map-inclusion-retract-sequential-diagram n
  pr1 (pr2 (retract-family-retract-sequential-diagram n)) =
    map-hom-retraction-retract-sequential-diagram n
  pr2 (pr2 (retract-family-retract-sequential-diagram n)) =
    is-retraction-map-hom-retraction-retract-sequential-diagram n

  coh-retract-sequential-diagram :
    coherence-retract-sequential-diagram A B
      ( inclusion-retract-sequential-diagram)
      ( hom-retraction-retract-sequential-diagram)
      ( is-retraction-map-hom-retraction-retract-sequential-diagram)
  coh-retract-sequential-diagram =
    coherence-htpy-htpy-hom-sequential-diagram A
      ( is-retraction-hom-retraction-retract-sequential-diagram)

See also

Recent changes