Dependent inverse sequential diagrams of types

Content created by Fredrik Bakke.

Created on 2024-01-11.
Last modified on 2024-04-25.

module foundation.dependent-inverse-sequential-diagrams where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.inverse-sequential-diagrams
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies

Idea

A dependent inverse sequential diagram B over a base inverse sequential diagram A is a sequence of families over each Aₙ together with maps of fibers

  gₙ : (xₙ₊₁ : Aₙ₊₁) → Bₙ₊₁(xₙ₊₁) → Bₙ(fₙ(xₙ₊₁)),

where f is the sequence of maps of the base inverse sequential diagram, giving a dependent sequential diagram of maps that extend infinitely to the left:

     g₃      g₂      g₁      g₀
  ⋯ ---> B₃ ---> B₂ ---> B₁ ---> B₀.

Definitions

Dependent inverse sequential diagrams of types

sequence-map-dependent-inverse-sequential-diagram :
  {l1 l2 : Level} (A : inverse-sequential-diagram l1) →
  ((n : ℕ) → family-inverse-sequential-diagram A n → UU l2) → UU (l1 ⊔ l2)
sequence-map-dependent-inverse-sequential-diagram A B =
  (n : ℕ) (x : family-inverse-sequential-diagram A (succ-ℕ n)) →
  B (succ-ℕ n) x → B n (map-inverse-sequential-diagram A n x)

dependent-inverse-sequential-diagram :
  {l1 : Level} (l2 : Level) (A : inverse-sequential-diagram l1) →
  UU (l1 ⊔ lsuc l2)
dependent-inverse-sequential-diagram l2 A =
  Σ ( (n : ℕ) → family-inverse-sequential-diagram A n → UU l2)
    ( sequence-map-dependent-inverse-sequential-diagram A)

family-dependent-inverse-sequential-diagram :
  {l1 l2 : Level} {A : inverse-sequential-diagram l1} →
  dependent-inverse-sequential-diagram l2 A →
  (n : ℕ) → family-inverse-sequential-diagram A n → UU l2
family-dependent-inverse-sequential-diagram = pr1

map-dependent-inverse-sequential-diagram :
  {l1 l2 : Level} {A : inverse-sequential-diagram l1}
  (B : dependent-inverse-sequential-diagram l2 A) →
  (n : ℕ) (x : family-inverse-sequential-diagram A (succ-ℕ n)) →
  family-dependent-inverse-sequential-diagram B (succ-ℕ n) x →
  family-dependent-inverse-sequential-diagram B n
    ( map-inverse-sequential-diagram A n x)
map-dependent-inverse-sequential-diagram = pr2

Constant dependent inverse sequential diagrams of types

const-dependent-inverse-sequential-diagram :
  {l1 l2 : Level}
  (A : inverse-sequential-diagram l1) → inverse-sequential-diagram l2 →
  dependent-inverse-sequential-diagram l2 A
pr1 (const-dependent-inverse-sequential-diagram A B) n _ =
  family-inverse-sequential-diagram B n
pr2 (const-dependent-inverse-sequential-diagram A B) n _ =
  map-inverse-sequential-diagram B n

Sections of a dependent inverse sequential diagram

A section of a dependent inverse sequential diagram (B , g) over (A , f) is a choice of sections hₙ of each Bₙ that vary naturally over A, by which we mean that the diagrams

            gₙ
      Bₙ₊₁ ---> Bₙ
      ∧         ∧
  hₙ₊₁|         | hₙ
      |         |
      Aₙ₊₁ ---> Aₙ
            fₙ

commute for each n : ℕ.

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

  naturality-section-dependent-inverse-sequential-diagram :
    (h :
      (n : ℕ) (x : family-inverse-sequential-diagram A n) →
      family-dependent-inverse-sequential-diagram B n x)
    (n : ℕ) → UU (l1 ⊔ l2)
  naturality-section-dependent-inverse-sequential-diagram h n =
    h n ∘ map-inverse-sequential-diagram A n ~
    map-dependent-inverse-sequential-diagram B n _ ∘ h (succ-ℕ n)

  section-dependent-inverse-sequential-diagram : UU (l1 ⊔ l2)
  section-dependent-inverse-sequential-diagram =
    Σ ( (n : ℕ) (x : family-inverse-sequential-diagram A n) →
        family-dependent-inverse-sequential-diagram B n x)
      ( λ h → (n : ℕ) →
        naturality-section-dependent-inverse-sequential-diagram h n)

  map-section-dependent-inverse-sequential-diagram :
    section-dependent-inverse-sequential-diagram →
    (n : ℕ) (x : family-inverse-sequential-diagram A n) →
    family-dependent-inverse-sequential-diagram B n x
  map-section-dependent-inverse-sequential-diagram = pr1

  naturality-map-section-dependent-inverse-sequential-diagram :
    (f : section-dependent-inverse-sequential-diagram) (n : ℕ) →
    naturality-section-dependent-inverse-sequential-diagram
      ( map-section-dependent-inverse-sequential-diagram f)
      ( n)
  naturality-map-section-dependent-inverse-sequential-diagram = pr2

Operations

Right shifting a dependent inverse sequential diagram

We can right shift a dependent inverse sequential diagram of types by forgetting the first terms.

right-shift-dependent-inverse-sequential-diagram :
  {l1 l2 : Level} {A : inverse-sequential-diagram l1} →
  dependent-inverse-sequential-diagram l2 A →
  dependent-inverse-sequential-diagram l2
    ( right-shift-inverse-sequential-diagram A)
pr1 (right-shift-dependent-inverse-sequential-diagram B) n =
  family-dependent-inverse-sequential-diagram B (succ-ℕ n)
pr2 (right-shift-dependent-inverse-sequential-diagram B) n =
  map-dependent-inverse-sequential-diagram B (succ-ℕ n)

Left shifting a dependent inverse sequential diagram

We can left shift a dependent inverse sequential diagram of types by padding it with the terminal type unit.

left-shift-dependent-inverse-sequential-diagram :
    {l1 l2 : Level} {A : inverse-sequential-diagram l1} →
  dependent-inverse-sequential-diagram l2 A →
  dependent-inverse-sequential-diagram l2
    ( left-shift-inverse-sequential-diagram A)
pr1 (left-shift-dependent-inverse-sequential-diagram {l2 = l2} B) 0 x =
  raise-unit l2
pr1 (left-shift-dependent-inverse-sequential-diagram B) (succ-ℕ n) =
  family-dependent-inverse-sequential-diagram B n
pr2 (left-shift-dependent-inverse-sequential-diagram B) 0 x =
  raise-terminal-map (family-dependent-inverse-sequential-diagram B 0 x)
pr2 (left-shift-dependent-inverse-sequential-diagram B) (succ-ℕ n) =
  map-dependent-inverse-sequential-diagram B n

Table of files about sequential limits

The following table lists files that are about sequential limits as a general concept.

ConceptFile
Inverse sequential diagrams of typesfoundation.inverse-sequential-diagrams
Dependent inverse sequential diagrams of typesfoundation.dependent-inverse-sequential-diagrams
Composite maps in inverse sequential diagramsfoundation.composite-maps-in-inverse-sequential-diagrams
Morphisms of inverse sequential diagramsfoundation.morphisms-inverse-sequential-diagrams
Equivalences of inverse sequential diagramsfoundation.equivalences-inverse-sequential-diagrams
Cones over inverse sequential diagramsfoundation.cones-over-inverse-sequential-diagrams
The universal property of sequential limitsfoundation.universal-property-sequential-limits
Sequential limitsfoundation.sequential-limits
Functoriality of sequential limitsfoundation.functoriality-sequential-limits
Transfinite cocomposition of mapsfoundation.transfinite-cocomposition-of-maps

Recent changes