The sphere prespectrum

Content created by Fredrik Bakke.

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

module synthetic-homotopy-theory.sphere-prespectrum where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.prespectra
open import synthetic-homotopy-theory.suspension-prespectra

open import univalent-combinatorics.standard-finite-types

Idea

The spheres Sⁿ define a prespectrum

  Sⁿ →∗ ΩSⁿ⁺¹

which we call the sphere prespectrum.

Note: Even though the sphere 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

The sphere prespectrum

sphere-Prespectrum : Prespectrum lzero
sphere-Prespectrum = suspension-Prespectrum (Fin 2 , zero-Fin 1)

Recent changes