Sequential colimits

Content created by Vojtěch Štěpančík and Fredrik Bakke.

Created on 2023-12-05.
Last modified on 2024-04-20.

module synthetic-homotopy-theory.sequential-colimits where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.commuting-triangles-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.propositions
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.coequalizers
open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.dependent-universal-property-sequential-colimits
open import synthetic-homotopy-theory.sequential-diagrams
open import synthetic-homotopy-theory.universal-property-sequential-colimits

Idea

Given a sequential diagram (A, a), we can construct its standard sequential colimit A∞, which is a cocone under it satisfying the universal property of sequential colimits.

In other words, the sequential colimit universally completes the diagram

     a₀      a₁      a₂
 A₀ ---> A₁ ---> A₂ ---> ⋯ ---> A∞ .

We often abuse notation and write A∞ for just the codomain of the universal cocone. You may also see the colimit written as colimₙ Aₙ.

Definitions

Homotopies between maps out of sequential colimits

module _
  { l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2}
  ( c : cocone-sequential-diagram A X)
  where

  htpy-out-of-sequential-colimit : {Y : UU l3} (f g : X → Y) → UU (l1 ⊔ l3)
  htpy-out-of-sequential-colimit f g =
    htpy-cocone-sequential-diagram
      ( cocone-map-sequential-diagram c f)
      ( cocone-map-sequential-diagram c g)

  equiv-htpy-htpy-out-of-sequential-colimit :
    universal-property-sequential-colimit c →
    {Y : UU l3} (f g : X → Y) →
    htpy-out-of-sequential-colimit f g ≃ (f ~ g)
  equiv-htpy-htpy-out-of-sequential-colimit up-c f g =
    ( inv-equiv
      ( equiv-dependent-universal-property-sequential-colimit
        ( dependent-universal-property-universal-property-sequential-colimit c
          ( up-c)))) ∘e
    ( equiv-tot
      ( λ K →
        equiv-Π-equiv-family
          ( λ n →
            equiv-Π-equiv-family
              ( λ a →
                compute-dependent-identification-eq-value-function f g
                  ( coherence-cocone-sequential-diagram c n a)
                  ( K n a)
                  ( K (succ-ℕ n) (map-sequential-diagram A n a))))))

Components of a homotopy between maps out of sequential colimits

module _
  { l1 l2 l3 : Level} {A : sequential-diagram l1} {X : UU l2}
  { c : cocone-sequential-diagram A X}
  ( up-c : universal-property-sequential-colimit c) {Y : UU l3} {f g : X → Y}
  ( H : htpy-out-of-sequential-colimit c f g)
  where

  htpy-htpy-out-of-sequential-colimit : f ~ g
  htpy-htpy-out-of-sequential-colimit =
    map-equiv (equiv-htpy-htpy-out-of-sequential-colimit c up-c f g) H

Properties

All sequential diagrams admit a standard colimit

The standard colimit may be constructed from coequalizers, because we have shown that cocones of sequential diagrams correspond to a certain class of coforks, and the coequalizers correspond to sequential colimits. Since all coequalizers exist, we conclude that all sequential colimits exist.

abstract
  standard-sequential-colimit : {l : Level} (A : sequential-diagram l) → UU l
  standard-sequential-colimit A =
    standard-coequalizer (double-arrow-sequential-diagram A)

  cocone-standard-sequential-colimit :
    { l : Level} (A : sequential-diagram l) →
    cocone-sequential-diagram A (standard-sequential-colimit A)
  cocone-standard-sequential-colimit A =
    cocone-sequential-diagram-cofork
      ( cofork-standard-coequalizer (double-arrow-sequential-diagram A))

  dup-standard-sequential-colimit :
    { l : Level} {A : sequential-diagram l} →
    dependent-universal-property-sequential-colimit
      ( cocone-standard-sequential-colimit A)
  dup-standard-sequential-colimit {A = A} =
    dependent-universal-property-sequential-colimit-dependent-universal-property-coequalizer
      ( cocone-standard-sequential-colimit A)
      ( dup-standard-coequalizer (double-arrow-sequential-diagram A))

  up-standard-sequential-colimit :
    { l : Level} {A : sequential-diagram l} →
    universal-property-sequential-colimit
      ( cocone-standard-sequential-colimit A)
  up-standard-sequential-colimit {A = A} =
    universal-property-dependent-universal-property-sequential-colimit
      ( cocone-standard-sequential-colimit A)
      ( dup-standard-sequential-colimit)

module _
  { l : Level} {A : sequential-diagram l}
  where

  map-cocone-standard-sequential-colimit :
    ( n : ℕ) → family-sequential-diagram A n → standard-sequential-colimit A
  map-cocone-standard-sequential-colimit =
    map-cocone-sequential-diagram (cocone-standard-sequential-colimit A)

  coherence-cocone-standard-sequential-colimit :
    ( n : ℕ) →
    coherence-triangle-maps
      ( map-cocone-standard-sequential-colimit n)
      ( map-cocone-standard-sequential-colimit (succ-ℕ n))
      ( map-sequential-diagram A n)
  coherence-cocone-standard-sequential-colimit =
    coherence-cocone-sequential-diagram
      ( cocone-standard-sequential-colimit A)

Corollaries of the universal property of sequential colimits

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

  equiv-up-standard-sequential-colimit :
    { X : UU l2} →
    (standard-sequential-colimit A → X) ≃ (cocone-sequential-diagram A X)
  pr1 equiv-up-standard-sequential-colimit =
    cocone-map-sequential-diagram (cocone-standard-sequential-colimit A)
  pr2 (equiv-up-standard-sequential-colimit) =
    up-standard-sequential-colimit _

  cogap-standard-sequential-colimit :
    { X : UU l2} →
    cocone-sequential-diagram A X → standard-sequential-colimit A → X
  cogap-standard-sequential-colimit =
    map-inv-equiv equiv-up-standard-sequential-colimit

  equiv-dup-standard-sequential-colimit :
    { P : standard-sequential-colimit A → UU l2} →
    ( (x : standard-sequential-colimit A) → P x) ≃
    ( dependent-cocone-sequential-diagram
      ( cocone-standard-sequential-colimit A)
      ( P))
  pr1 equiv-dup-standard-sequential-colimit =
    dependent-cocone-map-sequential-diagram
      ( cocone-standard-sequential-colimit A)
      ( _)
  pr2 equiv-dup-standard-sequential-colimit =
    dup-standard-sequential-colimit _

  dependent-cogap-standard-sequential-colimit :
    { P : standard-sequential-colimit A → UU l2} →
    dependent-cocone-sequential-diagram
      ( cocone-standard-sequential-colimit A)
      ( P) →
    ( x : standard-sequential-colimit A) → P x
  dependent-cogap-standard-sequential-colimit =
    map-inv-equiv equiv-dup-standard-sequential-colimit

The small predicate of being a sequential colimit cocone

The proposition is-sequential-colimit is the assertion that the cogap map is an equivalence. Note that this proposition is small, whereas the universal property is a large proposition.

module _
  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  (c : cocone-sequential-diagram A X)
  where

  is-sequential-colimit : UU (l1 ⊔ l2)
  is-sequential-colimit = is-equiv (cogap-standard-sequential-colimit c)

  is-prop-is-sequential-colimit : is-prop is-sequential-colimit
  is-prop-is-sequential-colimit =
    is-property-is-equiv (cogap-standard-sequential-colimit c)

  is-sequential-colimit-Prop : Prop (l1 ⊔ l2)
  pr1 is-sequential-colimit-Prop = is-sequential-colimit
  pr2 is-sequential-colimit-Prop = is-prop-is-sequential-colimit

Homotopies between maps from the standard sequential colimit

Maps from the standard sequential colimit induce cocones under the sequential diagrams, and a homotopy between the maps is exactly a homotopy of the cocones.

module _
  { l1 l2 : Level} (A : sequential-diagram l1) {X : UU l2}
  ( f g : standard-sequential-colimit A → X)
  where

  htpy-out-of-standard-sequential-colimit : UU (l1 ⊔ l2)
  htpy-out-of-standard-sequential-colimit =
    htpy-out-of-sequential-colimit (cocone-standard-sequential-colimit A) f g

  equiv-htpy-htpy-out-of-standard-sequential-colimit :
    htpy-out-of-standard-sequential-colimit ≃ (f ~ g)
  equiv-htpy-htpy-out-of-standard-sequential-colimit =
    equiv-htpy-htpy-out-of-sequential-colimit
      ( cocone-standard-sequential-colimit A)
      ( up-standard-sequential-colimit)
      ( f)
      ( g)

We may then obtain a homotopy of maps from a homotopy of their induced cocones.

module _
  { l1 l2 : Level} (A : sequential-diagram l1) {X : UU l2}
  { f g : standard-sequential-colimit A → X}
  ( H : htpy-out-of-standard-sequential-colimit A f g)
  where

  htpy-htpy-out-of-standard-sequential-colimit : f ~ g
  htpy-htpy-out-of-standard-sequential-colimit =
    htpy-htpy-out-of-sequential-colimit
      ( up-standard-sequential-colimit)
      ( H)

A type satisfies is-sequential-colimit if and only if it has the (dependent) universal property of sequential colimits

module _
  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  (c : cocone-sequential-diagram A X)
  where

  universal-property-is-sequential-colimit :
    is-sequential-colimit c → universal-property-sequential-colimit c
  universal-property-is-sequential-colimit =
    universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit
      ( cocone-standard-sequential-colimit A)
      ( c)
      ( cogap-standard-sequential-colimit c)
      ( htpy-cocone-universal-property-sequential-colimit
        ( up-standard-sequential-colimit)
        ( c))
      ( up-standard-sequential-colimit)

  dependent-universal-property-is-sequential-colimit :
    is-sequential-colimit c →
    dependent-universal-property-sequential-colimit c
  dependent-universal-property-is-sequential-colimit =
    dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit
      ( cocone-standard-sequential-colimit A)
      ( c)
      ( cogap-standard-sequential-colimit c)
      ( htpy-cocone-universal-property-sequential-colimit
        ( up-standard-sequential-colimit)
        ( c))
      ( dup-standard-sequential-colimit)

  is-sequential-colimit-universal-property :
    universal-property-sequential-colimit c → is-sequential-colimit c
  is-sequential-colimit-universal-property =
    is-equiv-universal-property-sequential-colimit-universal-property-sequential-colimit
      ( cocone-standard-sequential-colimit A)
      ( c)
      ( cogap-standard-sequential-colimit c)
      ( htpy-cocone-universal-property-sequential-colimit
        ( up-standard-sequential-colimit)
        ( c))
      ( up-standard-sequential-colimit)

  is-sequential-colimit-dependent-universal-property :
    dependent-universal-property-sequential-colimit c →
    is-sequential-colimit c
  is-sequential-colimit-dependent-universal-property =
    is-equiv-dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit
      ( cocone-standard-sequential-colimit A)
      ( c)
      ( cogap-standard-sequential-colimit c)
      ( htpy-cocone-universal-property-sequential-colimit
        ( up-standard-sequential-colimit)
        ( c))
      ( dup-standard-sequential-colimit)

Recent changes