Limits of symmetric spectra

Symmetric sequences have limits computed in pointed simplicial sets at each level. The forgetful functor from sphere modules creates limits, so the native category of symmetric spectra has all small limits, with its sphere action induced by the universal property. SymmetricSpectrum.isLimitOfLevelwise recognizes limiting cones by their levels.

For a level n, compose Mod.forget SymmetricSequence.sphere, the functor of DayFunctor.equiv FiniteBijection PointedSSet, and (evaluation FiniteBijection PointedSSet).obj (FiniteBijection.mk n). This composite preserves limits. Mathlib's preservesLimitIso identifies the level of a spectral limit with the limit of its levels; preservesLimitIso_hom_π and preservesLimitIso_inv_π identify its projections. These are strict categorical limits.

The construction uses Mathlib's DayFunctor.equiv, functor-category limits, and the generic limit creation theorem for module objects.

References

• M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 2.2.

noncomputable def TauCeti.SymmetricSpectrum.isLimitOfLevelwise {J : Type w} [CategoryTheory.Category.{v, w} J] {F : CategoryTheory.Functor J SymmetricSpectrum} (c : CategoryTheory.Limits.Cone F) (h : (n : ℕ) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation FiniteBijection PointedSSet).obj { len := n }).mapCone ((CategoryTheory.MonoidalCategory.DayFunctor.equiv FiniteBijection PointedSSet).functor.mapCone ((CategoryTheory.Mod.forget SymmetricSequence.sphere).mapCone c)))) : CategoryTheory.Limits.IsLimit c

A cone of symmetric spectra is limiting if its cone of pointed simplicial sets is limiting at every level. In particular, the limiting maps respect the sphere action.