Morphisms of sequential diagrams

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

Created on 2023-10-23.
Last modified on 2024-04-25.

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

open import foundation.binary-homotopies
open import foundation.commuting-squares-of-homotopies
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.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

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

Idea

A morphism between sequential diagrams f : (A, a) → (B, b) is a sequence of maps fₙ : Aₙ → Bₙ satisfying the naturality condition that all squares of the form

        aₙ
    Aₙ ---> Aₙ₊₁
    |       |
 fₙ |       | fₙ₊₁
    ∨       ∨
    Bₙ ---> Bₙ₊₁
        bₙ

commute.

Definitions

Morphisms of sequential diagrams

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

  naturality-hom-sequential-diagram :
    ( h :
      ( n : ℕ) →
      family-sequential-diagram A n → family-sequential-diagram B n) →
    UU (l1 ⊔ l2)
  naturality-hom-sequential-diagram h =
    ( n : ℕ) →
    ( map-sequential-diagram B n ∘ h n) ~
    ( h (succ-ℕ n) ∘ map-sequential-diagram A n)

  hom-sequential-diagram : UU (l1 ⊔ l2)
  hom-sequential-diagram =
    Σ ( (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n)
      ( naturality-hom-sequential-diagram)

Components of morphisms of sequential diagrams

Implementation note: Ideally we would have both the domain and codomain of a morphism of sequential diagrams inferred by Agda. Unfortunately that's not the case with the current implementation, and the codomain needs to be provided explicitly. This arises also in equivalences of sequential diagrams.

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

  map-hom-sequential-diagram :
    ( n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n
  map-hom-sequential-diagram = pr1 h

  naturality-map-hom-sequential-diagram :
    naturality-hom-sequential-diagram A B map-hom-sequential-diagram
  naturality-map-hom-sequential-diagram = pr2 h

The identity morphism of sequential diagrams

All sequential diagrams have an identity morphism constructed from the identity function on the underlying types.

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

  id-hom-sequential-diagram : hom-sequential-diagram A A
  pr1 id-hom-sequential-diagram n = id
  pr2 id-hom-sequential-diagram n = refl-htpy

Composition of morphisms of sequential diagrams

Composition of morphisms is induced by composition of the underlying maps and by pasting diagrams.

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

  comp-hom-sequential-diagram :
    hom-sequential-diagram B C →
    hom-sequential-diagram A B →
    hom-sequential-diagram A C
  pr1 (comp-hom-sequential-diagram g f) n =
    map-hom-sequential-diagram C g n ∘ map-hom-sequential-diagram B f n
  pr2 (comp-hom-sequential-diagram g f) n =
    pasting-vertical-coherence-square-maps
      ( map-sequential-diagram A n)
      ( map-hom-sequential-diagram B f n)
      ( map-hom-sequential-diagram B f (succ-ℕ n))
      ( map-sequential-diagram B n)
      ( map-hom-sequential-diagram C g n)
      ( map-hom-sequential-diagram C g (succ-ℕ n))
      ( map-sequential-diagram C n)
      ( naturality-map-hom-sequential-diagram B f n)
      ( naturality-map-hom-sequential-diagram C g n)

Homotopies between morphisms of sequential diagrams

A homotopy between morphisms f, g : (A, a) → (B, b) consists of a sequence of homotopies Hₙ : fₙ ~ gₙ and a coherence datum filling the cylinders

              aₙ
      Aₙ ----------> Aₙ₊₁
      / \            / \
     / Hₙ\          /Hₙ₊₁\
 fₙ |  => | gₙ fₙ₊₁ |  => | gₙ₊₁
     \   /          \   /
      \ /            \ /
      Bₙ ----------> Bₙ₊₁.
              bₙ

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

  coherence-htpy-hom-sequential-diagram :
    ( H :
      ( n : ℕ) →
      ( map-hom-sequential-diagram B f n) ~
      ( map-hom-sequential-diagram B g n)) →
    UU (l1 ⊔ l2)
  coherence-htpy-hom-sequential-diagram H =
    ( n : ℕ) →
    coherence-square-homotopies
      ( map-sequential-diagram B n ·l H n)
      ( naturality-map-hom-sequential-diagram B f n)
      ( naturality-map-hom-sequential-diagram B g n)
      ( H (succ-ℕ n) ·r map-sequential-diagram A n)

  htpy-hom-sequential-diagram : UU (l1 ⊔ l2)
  htpy-hom-sequential-diagram =
    Σ ( ( n : ℕ) →
        ( map-hom-sequential-diagram B f n) ~
        ( map-hom-sequential-diagram B g n))
      ( coherence-htpy-hom-sequential-diagram)

Components of homotopies between morphisms of sequential diagrams

module _
  { l1 l2 : Level} {A : sequential-diagram l1} (B : sequential-diagram l2)
  { f g : hom-sequential-diagram A B}
  ( H : htpy-hom-sequential-diagram B f g)
  where

  htpy-htpy-hom-sequential-diagram :
    ( n : ℕ) →
    ( map-hom-sequential-diagram B f n) ~
    ( map-hom-sequential-diagram B g n)
  htpy-htpy-hom-sequential-diagram = pr1 H

  coherence-htpy-htpy-hom-sequential-diagram :
    coherence-htpy-hom-sequential-diagram B f g htpy-htpy-hom-sequential-diagram
  coherence-htpy-htpy-hom-sequential-diagram = pr2 H

Properties

Characterization of equality of morphisms of sequential diagrams

Equality of morphisms of sequential diagrams is captured by a homotopy between them.

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

  refl-htpy-hom-sequential-diagram :
    ( f : hom-sequential-diagram A B) → htpy-hom-sequential-diagram B f f
  pr1 (refl-htpy-hom-sequential-diagram f) = ev-pair refl-htpy
  pr2 (refl-htpy-hom-sequential-diagram f) = ev-pair right-unit-htpy

  htpy-eq-sequential-diagram :
    ( f f' : hom-sequential-diagram A B) →
    ( f ＝ f') → htpy-hom-sequential-diagram B f f'
  htpy-eq-sequential-diagram f .f refl = refl-htpy-hom-sequential-diagram f

  abstract
    is-torsorial-htpy-sequential-diagram :
      ( f : hom-sequential-diagram A B) →
      is-torsorial (htpy-hom-sequential-diagram B f)
    is-torsorial-htpy-sequential-diagram f =
      is-torsorial-Eq-structure
        ( is-torsorial-binary-htpy (map-hom-sequential-diagram B f))
        ( map-hom-sequential-diagram B f , ev-pair refl-htpy)
        ( is-torsorial-Eq-Π
          ( λ n →
            is-torsorial-htpy
              ( naturality-map-hom-sequential-diagram B f n ∙h refl-htpy)))

    is-equiv-htpy-eq-sequential-diagram :
      ( f f' : hom-sequential-diagram A B) →
      is-equiv (htpy-eq-sequential-diagram f f')
    is-equiv-htpy-eq-sequential-diagram f =
      fundamental-theorem-id
        ( is-torsorial-htpy-sequential-diagram f)
        ( htpy-eq-sequential-diagram f)

  extensionality-hom-sequential-diagram :
    ( f f' : hom-sequential-diagram A B) →
    ( f ＝ f') ≃ htpy-hom-sequential-diagram B f f'
  pr1 (extensionality-hom-sequential-diagram f f') =
    htpy-eq-sequential-diagram f f'
  pr2 (extensionality-hom-sequential-diagram f f') =
    is-equiv-htpy-eq-sequential-diagram f f'

  eq-htpy-sequential-diagram :
    ( f f' : hom-sequential-diagram A B) →
    htpy-hom-sequential-diagram B f f' → (f ＝ f')
  eq-htpy-sequential-diagram f f' =
    map-inv-equiv (extensionality-hom-sequential-diagram f f')

Recent changes