Maps of prespectra

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-12.
Last modified on 2023-10-16.

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ₙ
  |            |
  |            |
  |            |
  v            v
  Ω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

  • J. P. May, A Concise Course in Algebraic Topology, 1999 (pdf)

Recent changes