Suspension prespectra

Content created by Fredrik Bakke.

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

module synthetic-homotopy-theory.suspension-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.pointed-maps
open import structured-types.pointed-types

open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types
open import synthetic-homotopy-theory.loop-spaces
open import synthetic-homotopy-theory.prespectra
open import synthetic-homotopy-theory.suspensions-of-pointed-types
open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types

Idea

Given a pointed type A, the sequence of iterated suspensions of A

  A   Σ¹A   Σ²A   Σ³A   ...

defines a prespectrum Σ^∞A that we call the suspension prespectrum of A. Its structure map is defined degreewise by the identity

  Σⁿ⁺¹A = Σⁿ⁺¹A   ↝   ΣⁿA →∗ ΩΣⁿ⁺¹A

Note: Even though the suspension prespectrum is defined degreewise by the adjoint to the identity map, it is not in general a spectrum, as the transposing map of the loop-suspension adjunction does not generally send equivalences to equivalences.

Definition

pointed-structure-map-suspension-Prespectrum :
  {l : Level} (A : Pointed-Type l) (n : ℕ) →
  suspension-Pointed-Type (iterated-suspension-Pointed-Type n A) →∗
  iterated-suspension-Pointed-Type (succ-ℕ n) A
pointed-structure-map-suspension-Prespectrum A n = id-pointed-map

pointed-adjoint-structure-map-suspension-Prespectrum :
  {l : Level} (A : Pointed-Type l) (n : ℕ) →
  iterated-suspension-Pointed-Type n A →∗
  Ω (iterated-suspension-Pointed-Type (succ-ℕ n) A)
pointed-adjoint-structure-map-suspension-Prespectrum A n =
  transpose-suspension-loop-adjunction
    ( iterated-suspension-Pointed-Type n A)
    ( iterated-suspension-Pointed-Type (succ-ℕ n) A)
    ( pointed-structure-map-suspension-Prespectrum A n)

suspension-Prespectrum : {l : Level} → Pointed-Type l → Prespectrum l
pr1 (suspension-Prespectrum A) n = iterated-suspension-Pointed-Type n A
pr2 (suspension-Prespectrum A) =
  pointed-adjoint-structure-map-suspension-Prespectrum A

Recent changes