Homotopy Type Theory
spectrum (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed



A prespectrum is a sequence of pointed types? E:𝒰 *E: \mathbb{Z} \to \mathcal{U}_* and a sequence of pointed maps e:(n:)E nΩE n+1e : (n : \mathbb{Z}) \to E_n \to \Omega E_{n+1}. Typically a prespectrum is denoted EE when it is clear.

A spectrum (or Ω\Omega-spectrum) is a prespectrum in which each e ne_n is an equivalence.

Spectrum E: Spectrum PreSpectrum n:IsEquiv(e n) \Spectrum \equiv \sum_{E : \Spectrum} \PreSpectrum} \prod_{n : \mathbb{Z}} \IsEquiv e_n) (e_n)


  • spectrification?
  • homotopy group of spectrum?
  • smash product of spectra?
  • coproduct of spectra?
  • product of spectra?
  • Eilienberg-MacLane spectrum?
  • Suspension spectrum?

See also


Last revised on December 18, 2018 at 08:11:00. See the history of this page for a list of all contributions to it.