Descent data for sequential colimits

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

Created on 2024-04-16.
Last modified on 2024-04-16.

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

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.dependent-sequential-diagrams
open import synthetic-homotopy-theory.equifibered-sequential-diagrams
open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams
open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams

Idea

Given a sequential diagram (A, a), we may ask how to construct type families over its sequential colimit.

The data required to construct a type family is called descent data for sequential colimits, and it is exactly an equifibered sequential diagram.

The fact that the type of descent data for a sequential diagram is equivalent to the type of type families over its colimit is recorded in descent-property-sequential-colimits.

Definitions

Descent data for sequential colimits

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

  descent-data-sequential-colimit : (l2 : Level) → UU (l1 ⊔ lsuc l2)
  descent-data-sequential-colimit =
    equifibered-sequential-diagram A

Components of descent data for sequential colimits

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

  family-descent-data-sequential-colimit :
    (n : ℕ) → family-sequential-diagram A n → UU l2
  family-descent-data-sequential-colimit = pr1 B

  equiv-family-descent-data-sequential-colimit :
    (n : ℕ) (a : family-sequential-diagram A n) →
    family-descent-data-sequential-colimit n a ≃
    family-descent-data-sequential-colimit
      ( succ-ℕ n)
      ( map-sequential-diagram A n a)
  equiv-family-descent-data-sequential-colimit = pr2 B

  map-family-descent-data-sequential-colimit :
    (n : ℕ) (a : family-sequential-diagram A n) →
    family-descent-data-sequential-colimit n a →
    family-descent-data-sequential-colimit
      ( succ-ℕ n)
      ( map-sequential-diagram A n a)
  map-family-descent-data-sequential-colimit n a =
    map-equiv (equiv-family-descent-data-sequential-colimit n a)

  is-equiv-map-family-descent-data-sequential-colimit :
    (n : ℕ) (a : family-sequential-diagram A n) →
    is-equiv (map-family-descent-data-sequential-colimit n a)
  is-equiv-map-family-descent-data-sequential-colimit n a =
    is-equiv-map-equiv (equiv-family-descent-data-sequential-colimit n a)

  dependent-sequential-diagram-descent-data : dependent-sequential-diagram A l2
  dependent-sequential-diagram-descent-data =
    dependent-sequential-diagram-equifibered-sequential-diagram B

Morphisms of descent data for sequential colimits

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

  hom-descent-data-sequential-colimit : UU (l1 ⊔ l2 ⊔ l3)
  hom-descent-data-sequential-colimit =
    hom-dependent-sequential-diagram
      ( dependent-sequential-diagram-equifibered-sequential-diagram B)
      ( dependent-sequential-diagram-equifibered-sequential-diagram C)

Equivalences of descent data for sequential colimits

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

  equiv-descent-data-sequential-colimit : UU (l1 ⊔ l2 ⊔ l3)
  equiv-descent-data-sequential-colimit =
    equiv-dependent-sequential-diagram
      ( dependent-sequential-diagram-equifibered-sequential-diagram B)
      ( dependent-sequential-diagram-equifibered-sequential-diagram C)

  module _
    (e : equiv-descent-data-sequential-colimit)
    where

    equiv-equiv-descent-data-sequential-colimit :
      (n : ℕ) (a : family-sequential-diagram A n) →
      family-descent-data-sequential-colimit B n a ≃
      family-descent-data-sequential-colimit C n a
    equiv-equiv-descent-data-sequential-colimit =
      equiv-equiv-dependent-sequential-diagram
        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
        ( e)

    map-equiv-descent-data-sequential-colimit :
      (n : ℕ) (a : family-sequential-diagram A n) →
      family-descent-data-sequential-colimit B n a →
      family-descent-data-sequential-colimit C n a
    map-equiv-descent-data-sequential-colimit =
      map-equiv-dependent-sequential-diagram
        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
        ( e)

    is-equiv-map-equiv-descent-data-sequential-colimit :
      (n : ℕ) (a : family-sequential-diagram A n) →
      is-equiv (map-equiv-descent-data-sequential-colimit n a)
    is-equiv-map-equiv-descent-data-sequential-colimit =
      is-equiv-map-equiv-dependent-sequential-diagram
        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
        ( e)

    coh-equiv-descent-data-sequential-colimit :
      coherence-equiv-dependent-sequential-diagram
        ( dependent-sequential-diagram-equifibered-sequential-diagram B)
        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
        ( equiv-equiv-descent-data-sequential-colimit)
    coh-equiv-descent-data-sequential-colimit =
      coh-equiv-dependent-sequential-diagram
        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
        ( e)

    hom-equiv-descent-data-sequential-colimit :
      hom-descent-data-sequential-colimit B C
    hom-equiv-descent-data-sequential-colimit =
      hom-equiv-dependent-sequential-diagram
        ( dependent-sequential-diagram-equifibered-sequential-diagram C)
        ( e)

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

  id-equiv-descent-data-sequential-colimit :
    equiv-descent-data-sequential-colimit B B
  id-equiv-descent-data-sequential-colimit =
    id-equiv-dependent-sequential-diagram
      ( dependent-sequential-diagram-equifibered-sequential-diagram B)

Descent data induced by families over cocones under sequential diagrams

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

  descent-data-family-cocone-sequential-diagram :
    {l3 : Level} → (X → UU l3) → descent-data-sequential-colimit A l3
  descent-data-family-cocone-sequential-diagram =
    equifibered-sequential-diagram-family-cocone c

Recent changes