Maps of prespectra

Content created by Fredrik Bakke and Egbert Rijke.

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

module synthetic-homotopy-theory.maps-of-prespectra where
Imports 
open import elementary-number-theory.natural-numbers

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

open import structured-types.commuting-squares-of-pointed-maps
open import structured-types.pointed-maps

open import synthetic-homotopy-theory.functoriality-loop-spaces
open import synthetic-homotopy-theory.prespectra

Idea

A map of prespectra f : A → B is a sequence of pointed maps

  fₙ : Aₙ →∗ Bₙ

such that the squares

        fₙ
  Aₙ --------> Bₙ
  |            |
  |            |
  |            |
  ∨            ∨
  ΩAₙ₊₁ -----> ΩBₙ₊₁
        Ωfₙ₊₁

commute in the category of pointed types.

Definition

coherence-map-Prespectrum :
  {l1 l2 : Level} (n : ℕ) (A : Prespectrum l1) (B : Prespectrum l2) →
  ( (n : ℕ) →
    pointed-type-Prespectrum A n →∗ pointed-type-Prespectrum B n) →
  UU (l1 ⊔ l2)
coherence-map-Prespectrum n A B f =
  coherence-square-pointed-maps
    ( f n)
    ( pointed-adjoint-structure-map-Prespectrum A n)
    ( pointed-adjoint-structure-map-Prespectrum B n)
    ( pointed-map-Ω (f (succ-ℕ n)))

map-Prespectrum :
  {l1 l2 : Level} (A : Prespectrum l1) (B : Prespectrum l2) →
  UU (l1 ⊔ l2)
map-Prespectrum A B =
  Σ ( (n : ℕ) →
      pointed-type-Prespectrum A n →∗ pointed-type-Prespectrum B n)
    ( λ f → (n : ℕ) → coherence-map-Prespectrum n A B f)

References

[May99]
J. P. May. A Concise Course in Algebraic Topology. University of Chicago Press, 09 1999. ISBN 978-0-226-51183-2. URL: https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf.

Recent changes