nLab stable homotopy type

Definition

A pointed homotopy type $X_\ast$ could be called linear (following the terminology of linear model category) if the canonical morphism

$$\Sigma \Omega X \longrightarrow X$$

from the suspension object of its loop space object is an equivalence.

By Goodwillie calculus the tangent (∞,1)-topos $T\mathbf{H}$ of some (∞,1)-topos $\mathbf{H}$ is the localization of the classifying (∞,1)-topos $\mathbf{H}[X_\ast]$ (of pointed objects), that regard each pointed finite powering $X_\ast^\bullet$ of the generic pointed object $X_\ast$ as a linear homotopy type.

See at excisive functor – Characterization via the generic pointed object.

Therefore a pointed homotopy type $X_\ast$ such that all its finite pointed powers are linear could be called a stable homotopy type.

For $\mathbf{H}$ an (∞,1)-topos and $T \mathbf{H}$ its tangent (∞,1)-topos, then all homotopy types in $T_\ast \mathbf{H} \hookrightarrow T \mathbf{H}$ are stable in this sense, these are equivalently the spectrum objects in $\mathbf{H}$.

Related concepts

• sequential spectrum type

• dependent linear type theory

• equivariant homotopy type

• modal homotopy type

• geometric homotopy type, cohesive homotopy type

References

An account using modal homotopy type theory is in

• Mitchell Riley, Eric Finster, Daniel Licata, Synthetic Spectra via a Monadic and Comonadic Modality, (arXiv:2102.04099)