Equifibered sequential diagrams

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

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

module synthetic-homotopy-theory.equifibered-sequential-diagrams 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.dependent-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams

Idea

An equifibered sequential diagram over a sequential diagram (A, a) consists of a type family B : (n : ℕ) → Aₙ → 𝒰 equipped with a family of fiberwise equivalences

bₙ : (a : Aₙ) → Bₙ a ≃ Bₙ₊₁ (aₙ a) .

The term “equifibered” comes from the equivalent definition as dependent sequential diagrams over (A, a)

     b₀      b₁      b₂
 B₀ ---> B₁ ---> B₂ ---> ⋯
 |       |       |
 |       |       |
 ↡       ↡       ↡
 A₀ ---> A₁ ---> A₂ ---> ⋯ ,
     a₀      a₁      a₂

which are said to be “fibered over A”, whose maps bₙ are equivalences.

Definitions

Equifibered sequential diagrams

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

  equifibered-sequential-diagram : (l : Level) → UU (l1 ⊔ lsuc l)
  equifibered-sequential-diagram l =
    Σ ( (n : ℕ) → family-sequential-diagram A n → UU l)
      ( λ B →
        (n : ℕ) (a : family-sequential-diagram A n) →
        B n a ≃ B (succ-ℕ n) (map-sequential-diagram A n a))

Components of an equifibered sequential diagram

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

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

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

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

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

  dependent-sequential-diagram-equifibered-sequential-diagram :
    dependent-sequential-diagram A l2
  pr1 dependent-sequential-diagram-equifibered-sequential-diagram =
    family-equifibered-sequential-diagram
  pr2 dependent-sequential-diagram-equifibered-sequential-diagram =
    map-equifibered-sequential-diagram

The predicate on dependent sequential diagrams of being equifibered

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

  is-equifibered-dependent-sequential-diagram :
    (B : dependent-sequential-diagram A l2) → UU (l1 ⊔ l2)
  is-equifibered-dependent-sequential-diagram B =
    (n : ℕ) (a : family-sequential-diagram A n) →
    is-equiv (map-dependent-sequential-diagram B n a)

  is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram :
    (B : equifibered-sequential-diagram A l2) →
    is-equifibered-dependent-sequential-diagram
      ( dependent-sequential-diagram-equifibered-sequential-diagram B)
  is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram B =
    is-equiv-map-equifibered-sequential-diagram B

Properties

Dependent sequential diagrams which are equifibered are equifibered sequential diagrams

To construct an equifibered sequential diagram over A, it suffices to construct a dependent sequential diagram (B, b) over A, and show that the maps bₙ are equivalences.

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

  equifibered-sequential-diagram-dependent-sequential-diagram :
    is-equifibered-dependent-sequential-diagram B →
    equifibered-sequential-diagram A l2
  pr1 (equifibered-sequential-diagram-dependent-sequential-diagram _) =
    family-dependent-sequential-diagram B
  pr2 (equifibered-sequential-diagram-dependent-sequential-diagram is-equiv-map)
    n a =
    (map-dependent-sequential-diagram B n a , is-equiv-map n a)

Recent changes