Equivalences 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-02-19.

module synthetic-homotopy-theory.equivalences-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.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.univalence
open import foundation.universe-levels

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

Idea

An equivalence of sequential diagrams (A, a) and (B, b) is a sequence of equivalences eₙ : Aₙ ≃ Bₙ such that their underlying maps form a morphism of sequential diagrams.

Specifically, the underlying maps need to satisfy the same naturality condition.

Definitions

Equivalences of sequential diagrams

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

  equiv-sequential-diagram : UU (l1 ⊔ l2)
  equiv-sequential-diagram =
    Σ ( ( n : ℕ) →
        family-sequential-diagram A n ≃ family-sequential-diagram B n)
      ( λ e → naturality-hom-sequential-diagram A B (map-equiv ∘ e))

Components of equivalences of sequential diagrams

Implementation note: As mentioned in morphisms-sequential-diagrams, Agda can't infer both the domain and the codomain when we use accessors for the equivalences, and the codomain needs to be provided explicitly.

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

  equiv-equiv-sequential-diagram :
    ( n : ℕ) →
    family-sequential-diagram A n ≃ family-sequential-diagram B n
  equiv-equiv-sequential-diagram = pr1 e

  map-equiv-sequential-diagram :
    ( n : ℕ) →
    family-sequential-diagram A n → family-sequential-diagram B n
  map-equiv-sequential-diagram n = map-equiv (equiv-equiv-sequential-diagram n)

  naturality-equiv-sequential-diagram :
    naturality-hom-sequential-diagram A B map-equiv-sequential-diagram
  naturality-equiv-sequential-diagram = pr2 e

  hom-equiv-sequential-diagram : hom-sequential-diagram A B
  pr1 hom-equiv-sequential-diagram = map-equiv-sequential-diagram
  pr2 hom-equiv-sequential-diagram = naturality-equiv-sequential-diagram

  is-equiv-map-equiv-sequential-diagram :
    ( n : ℕ) →
    is-equiv (map-equiv-sequential-diagram n)
  is-equiv-map-equiv-sequential-diagram n =
    is-equiv-map-equiv (equiv-equiv-sequential-diagram n)

The identity equivalence of sequential diagrams

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

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

Composition of equivalences of sequential diagrams

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

  comp-equiv-sequential-diagram :
    equiv-sequential-diagram B C →
    equiv-sequential-diagram A B →
    equiv-sequential-diagram A C
  pr1 (comp-equiv-sequential-diagram e e') n =
    ( equiv-equiv-sequential-diagram C e n) ∘e
    ( equiv-equiv-sequential-diagram B e' n)
  pr2 (comp-equiv-sequential-diagram e e') =
    naturality-map-hom-sequential-diagram C
      ( comp-hom-sequential-diagram A B C
        ( hom-equiv-sequential-diagram C e)
        ( hom-equiv-sequential-diagram B e'))

Inverses of equivalences of sequential diagrams

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

  inv-equiv-sequential-diagram : equiv-sequential-diagram B A
  pr1 inv-equiv-sequential-diagram n =
    inv-equiv (equiv-equiv-sequential-diagram B e n)
  pr2 inv-equiv-sequential-diagram n =
    vertical-inv-equiv-coherence-square-maps
      ( map-sequential-diagram A n)
      ( equiv-equiv-sequential-diagram B e n)
      ( equiv-equiv-sequential-diagram B e (succ-ℕ n))
      ( map-sequential-diagram B n)
      ( naturality-map-hom-sequential-diagram B
        ( hom-equiv-sequential-diagram B e)
        ( n))

  map-inv-equiv-sequential-diagram :
    ( n : ℕ) →
    family-sequential-diagram B n → family-sequential-diagram A n
  map-inv-equiv-sequential-diagram =
    map-equiv-sequential-diagram A inv-equiv-sequential-diagram

  hom-inv-equiv-sequential-diagram : hom-sequential-diagram B A
  hom-inv-equiv-sequential-diagram =
    hom-equiv-sequential-diagram A inv-equiv-sequential-diagram

Properties

Characterization of equality of sequential diagrams

Equality of sequential diagrams is captured by an equivalence between them.

equiv-eq-sequential-diagram :
  { l1 : Level} (A B : sequential-diagram l1) →
  A ＝ B → equiv-sequential-diagram A B
equiv-eq-sequential-diagram A .A refl = id-equiv-sequential-diagram A

abstract
  is-torsorial-equiv-sequential-diagram :
    { l1 : Level} (A : sequential-diagram l1) →
    is-torsorial (equiv-sequential-diagram {l2 = l1} A)
  is-torsorial-equiv-sequential-diagram A =
    is-torsorial-Eq-structure
      ( is-torsorial-Eq-Π
        ( λ n → is-torsorial-equiv (family-sequential-diagram A n)))
      ( family-sequential-diagram A , λ n → id-equiv)
      ( is-torsorial-Eq-Π
        ( λ n → is-torsorial-htpy' (map-sequential-diagram A n)))

  is-equiv-equiv-eq-sequential-diagram :
    { l1 : Level} (A B : sequential-diagram l1) →
    is-equiv (equiv-eq-sequential-diagram A B)
  is-equiv-equiv-eq-sequential-diagram A =
    fundamental-theorem-id
      ( is-torsorial-equiv-sequential-diagram A)
      ( equiv-eq-sequential-diagram A)

extensionality-sequential-diagram :
  { l1 : Level} (A B : sequential-diagram l1) →
  ( A ＝ B) ≃ equiv-sequential-diagram A B
pr1 (extensionality-sequential-diagram A B) = equiv-eq-sequential-diagram A B
pr2 (extensionality-sequential-diagram A B) =
  is-equiv-equiv-eq-sequential-diagram A B

eq-equiv-sequential-diagram :
  { l1 : Level} (A B : sequential-diagram l1) →
  equiv-sequential-diagram A B → (A ＝ B)
eq-equiv-sequential-diagram A B =
  map-inv-equiv (extensionality-sequential-diagram A B)

Inverses of equivalences are inverses with respect to composition of morphisms of sequential diagrams

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

  is-section-inv-equiv-sequential-diagram :
    htpy-hom-sequential-diagram B
      ( comp-hom-sequential-diagram B A B
        ( hom-equiv-sequential-diagram B e)
        ( hom-inv-equiv-sequential-diagram B e))
      ( id-hom-sequential-diagram B)
  pr1 is-section-inv-equiv-sequential-diagram n =
    is-section-map-inv-equiv (equiv-equiv-sequential-diagram B e n)
  pr2 is-section-inv-equiv-sequential-diagram n =
    inv-htpy
      ( right-inverse-law-pasting-vertical-coherence-square-maps
        ( map-sequential-diagram A n)
        ( equiv-equiv-sequential-diagram B e n)
        ( equiv-equiv-sequential-diagram B e (succ-ℕ n))
        ( map-sequential-diagram B n)
        ( naturality-equiv-sequential-diagram B e n))

  is-retraction-inv-equiv-sequential-diagram :
    htpy-hom-sequential-diagram A
      ( comp-hom-sequential-diagram A B A
        ( hom-inv-equiv-sequential-diagram B e)
        ( hom-equiv-sequential-diagram B e))
      ( id-hom-sequential-diagram A)
  pr1 is-retraction-inv-equiv-sequential-diagram n =
    is-retraction-map-inv-equiv (equiv-equiv-sequential-diagram B e n)
  pr2 is-retraction-inv-equiv-sequential-diagram n =
    inv-htpy
      ( left-inverse-law-pasting-vertical-coherence-square-maps
        ( map-sequential-diagram A n)
        ( equiv-equiv-sequential-diagram B e n)
        ( equiv-equiv-sequential-diagram B e (succ-ℕ n))
        ( map-sequential-diagram B n)
        ( naturality-equiv-sequential-diagram B e n))

  retraction-equiv-sequential-diagram :
    retraction-hom-sequential-diagram A B
      ( hom-equiv-sequential-diagram B e)
  pr1 retraction-equiv-sequential-diagram = hom-inv-equiv-sequential-diagram B e
  pr2 retraction-equiv-sequential-diagram =
    is-retraction-inv-equiv-sequential-diagram

Equivalences of sequential diagrams induce retracts of sequential diagrams

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

  retract-equiv-sequential-diagram : retract-sequential-diagram B A
  pr1 retract-equiv-sequential-diagram = hom-equiv-sequential-diagram B e
  pr2 retract-equiv-sequential-diagram = retraction-equiv-sequential-diagram B e

Recent changes