# Suspension prespectra

Content created by Fredrik Bakke.

Created 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

{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 =