Homotopy Type Theory
spectrum (changes)

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

Idea

Definition

A prespectrum spectrum is (or a sequence ofpointed types?Ω\Omega -E:𝒰 *E: \mathbb{Z} \to \mathcal{U}_*spectrum ) and is a sequence of pointed mapse:(n:)E nΩE n+1e : (n : \mathbb{Z}) \to E_n \to \Omega E_{n+1}prespectrum . Typically a prespectrum is denotedEE when in it which is each clear. pointed mape ne_n is an equivalence.

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

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

Properties

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

See also

References

Last revised on May 1, 2022 at 19:21:25. See the history of this page for a list of all contributions to it.