Suspension and loops of pointed simplicial sets

The simplicial suspension of a pointed simplicial set is its smash product with the simplicial circle on the left. Its right adjoint is the pointed mapping simplicial set out of that circle. This file names these two functors and their adjunction, fixing the left-coordinate convention used by spectra and reduced cohomology.

Main definitions

• PointedSSet.suspension: the functor X ↦ S¹ ∧ X.
• PointedSSet.loops: the functor Y ↦ Map_*(S¹, Y).
• PointedSSet.suspensionLoopAdjunction: the adjunction S¹ ∧ - ⊣ Map_*(S¹, -).

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.PointedSSet.suspension : CategoryTheory.Functor PointedSSet PointedSSet

Simplicial suspension, with the circle as the left smash factor.

@[reducible, inline]

noncomputable abbrev TauCeti.PointedSSet.loops : CategoryTheory.Functor PointedSSet PointedSSet

The pointed simplicial loop-space functor Map_*(S¹, -).

@[reducible, inline]

noncomputable abbrev TauCeti.PointedSSet.suspensionLoopAdjunction : suspension ⊣ loops

Smash with the simplicial circle is left adjoint to the pointed mapping simplicial set out of the circle.