# Spectra

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-16.

module synthetic-homotopy-theory.spectra where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import structured-types.pointed-equivalences
open import structured-types.pointed-maps
open import structured-types.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.suspensions-of-types


## Idea

A spectrum is a sequence of pointed types A equipped with an equivalence

  Aₙ ≃∗ ΩAₙ₊₁


for each n : ℕ.

## Definition

### The predicate on prespectra of being a spectrum

is-spectrum-Prop : {l : Level} → Prespectrum l → Prop l
is-spectrum-Prop A =
Π-Prop ℕ
( λ n →

is-spectrum : {l : Level} → Prespectrum l → UU l
is-spectrum = type-Prop ∘ is-spectrum-Prop

is-prop-is-spectrum : {l : Level} (A : Prespectrum l) → is-prop (is-spectrum A)
is-prop-is-spectrum = is-prop-type-Prop ∘ is-spectrum-Prop


### The type of spectra

Spectrum : (l : Level) → UU (lsuc l)
Spectrum l = Σ (Prespectrum l) (is-spectrum)

module _
{l : Level} (A : Spectrum l)
where

prespectrum-Spectrum : Prespectrum l
prespectrum-Spectrum = pr1 A

pointed-type-Spectrum : ℕ → Pointed-Type l
pointed-type-Spectrum = pointed-type-Prespectrum prespectrum-Spectrum

type-Spectrum : ℕ → UU l
type-Spectrum = type-Prespectrum prespectrum-Spectrum

point-Spectrum : (n : ℕ) → type-Spectrum n
point-Spectrum = point-Prespectrum prespectrum-Spectrum

(n : ℕ) → pointed-type-Spectrum n →∗ Ω (pointed-type-Spectrum (succ-ℕ n))

(n : ℕ) → type-Spectrum n → type-Ω (pointed-type-Spectrum (succ-ℕ n))

(n : ℕ) →
adjoint-structure-map-Prespectrum (pr1 A) n (point-Prespectrum (pr1 A) n) ＝
refl-Ω (pointed-type-Prespectrum (pr1 A) (succ-ℕ n))

(n : ℕ) → is-pointed-equiv (pointed-adjoint-structure-map-Spectrum n)

structure-equiv-Spectrum :
(n : ℕ) → type-Spectrum n ≃ type-Ω (pointed-type-Spectrum (succ-ℕ n))
pr1 (structure-equiv-Spectrum n) = adjoint-structure-map-Spectrum n
pr2 (structure-equiv-Spectrum n) =

pointed-structure-equiv-Spectrum :
(n : ℕ) → pointed-type-Spectrum n ≃∗ Ω (pointed-type-Spectrum (succ-ℕ n))
pr1 (pointed-structure-equiv-Spectrum n) = structure-equiv-Spectrum n
pr2 (pointed-structure-equiv-Spectrum n) =


### The structure maps of a spectrum

module _
{l : Level} (A : Spectrum l) (n : ℕ)
where

pointed-structure-map-Spectrum :
suspension-Pointed-Type (pointed-type-Spectrum A n) →∗
pointed-type-Spectrum A (succ-ℕ n)
pointed-structure-map-Spectrum =
pointed-structure-map-Prespectrum (prespectrum-Spectrum A) n

structure-map-Spectrum :
suspension (type-Spectrum A n) → type-Spectrum A (succ-ℕ n)
structure-map-Spectrum = map-pointed-map pointed-structure-map-Spectrum

preserves-point-structure-map-Spectrum :
structure-map-Spectrum north-suspension ＝ point-Spectrum A (succ-ℕ n)
preserves-point-structure-map-Spectrum =
preserves-point-pointed-map pointed-structure-map-Spectrum


## References

[May99]
J. P. May. A Concise Course in Algebraic Topology. University of Chicago Press, 09 1999. ISBN 978-0-226-51183-2. URL: https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf.