STABLE SPECTRA

The type models spectra in stable homotopy theory, sequences of types with structure maps , used in K-theory, cohomology, and quantum field theory. Spectra capture stable invariants and support operations like suspension and desuspension for defining shifted spectra such as .

In the cohesive type system, is a parameterless type in , not a universe, supporting operations like stabilization , suspension , desuspension , smash product , wedge sums , homomorphisms , and qubits . The category is stable and symmetric monoidal.

Formation

(-Formation). The type is a base type in , representing all spectra, stable under suspension and desuspension.

def Sp : U_{(0,0)}

Introduction

(-Introduction). Terms of type are introduced via a base constructor (sphere spectrum), or operations like stabilization (), suspension (), desuspension (), smash product (), wedge sums (), homomorphisms (), or qubits (), forming stable homotopy classes.

def sp : Sp
def stabilize (A : U_{(0,0)}) : Sp
def susp (E : Sp) : Sp
def desusp (E : Sp) : Sp
def tensor (E F : Sp) : Sp
def wedge (E F : Sp) : Sp
def hom_spec (E F : Sp) : Sp
def qubit (C H : U_{(0,0)}) : Sp

Elimination

(-Elimination). The eliminator maps terms to properties in , analyzing stable homotopy structure, including suspension and desuspension invariants.

def sp_ind (beta : Sp -> U_{(0,0)})
    (h : Π (E : Sp), beta E)
  : Π (E : Sp), beta E

Theorems

(Suspension Invariance). For , , preserving stable homotopy structure, with suspension and desuspension as equivalences.

def susp_inv (E : Sp) : susp E ≃ E

(Desuspension Invariance). For , , preserving stable homotopy structure, inverse to suspension.

def desusp_inv (E : Sp) : desusp E ≃ E

(Smash Product Closure). For , , the monoidal product in spectra.

def tensor_closure (E F : Sp) : Sp

(Wedge Sum Closure). For , , the coproduct in spectra.

def wedge_closure (E F : Sp) : Sp

(Homomorphism Spectrum). For , , the spectrum of stable maps.

def hom_closure (E F : Sp) : Sp

(Qubit as Spectrum). For , , connecting quantum states to spectra.

def qubit_spectrum (C H : U_{(0,0)}) : Sp

(Negative Suspension Spectrum). For , , the -fold desuspension of the sphere spectrum.

def neg_susp_spectrum (d : Nat) : Sp

[1]. Daniel Quillen. (1967). Axiomatic Homotopy Theory in Homotopical algebra
[2]. Kenneth Brown. (1973). Abstract Homotopy Theory and Generalized Sheaf Cohomology
[3]. M.A. Mandell, J.P. May S. Schwede, B. Shipley. (1999). Model Categories of Diagram Spectra
[4]. Stefan Schwede. (2012). Symmetric spectra
[5]. Maximilien Holmberg-Péroux. EFPL (2014). An Introduction to Stable Homotopy Theory
[6]. Mitchell Riley. (2022). A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory