Symmetric sequences of pointed simplicial sets

A symmetric sequence of pointed simplicial sets is a functor X from the finite-bijection groupoid to pointed simplicial sets: a sequence of pointed simplicial sets X_n, the value at the standard finite set Fin n, with a based action of the symmetric group Σ_n on each.

Symmetric sequences carry the Day convolution product along the block sum of finite sets. Its n-th level is the left Kan extension (X ⊗ Y)_n = colim_{Fin p ⊕ Fin q ≃ Fin n} X_p ∧ Y_q, which Hovey, Shipley and Smith write as the wedge ⋁_{p+q=n} (Σ_n)₊ ∧_{Σ_p × Σ_q} (X_p ∧ Y_q) of induced representations. This wedge formula is DayFunctor.isColimitShuffleCofan: the level (X ⊗ Y)_n is the wedge over the subsets S of Fin n of X_{#S} ∧ Y_{#Sᶜ}, included along the shuffles of S, which represent the cosets Σ_n / (Σ_p × Σ_q). We define SymmetricSequence as Mathlib's type synonym FiniteBijection ⊛⥤ PointedSSet carrying the Day convolution monoidal structure, and check that the hypotheses of Mathlib's construction hold:

• pointed simplicial sets have all small colimits, as an undercategory of simplicial sets, so the Day convolution and its unit exist as pointwise left Kan extensions;
• the smash product of pointed simplicial sets is closed and symmetric, so smashing with a fixed pointed simplicial set on either side preserves colimits.

As the block sum on finite sets and the smash product are symmetric, Day convolution makes symmetric sequences a symmetric monoidal category. Its unit is the zero sphere S⁰ in level zero and the point in every positive level: the instance DayFunctor.isIso_ν identifies level zero with S⁰, and SymmetricSequence.isInitialUnitObj shows that each positive level, which receives no bijection from Fin 0, is initial, that is, isomorphic to the one-point pointed simplicial set.

Pointed simplicial sets are complete and closed, so this symmetric monoidal structure is closed: the internal hom of symmetric sequences has levels Hom(X, Y)_n = ∫_k Map_*(X_k, Y_(k+n)), the end over the finite-bijection groupoid. Hovey, Shipley and Smith write it as the product ∏_k Map_{Σ_k}(X_k, Y_(k+n)) of equivariant mapping spaces; that identification is not formalized here.

Symmetric spectra are the modules over the commutative monoid of spheres in this symmetric monoidal category. Limits and colimits of symmetric sequences are computed levelwise, using the equivalence DayFunctor.equiv with the underlying functor category. Day convolution preserves colimits separately in each variable.

Main definitions

• SymmetricSequence: symmetric sequences of pointed simplicial sets, with the Day convolution product.
• The symmetric monoidal structure on SymmetricSequence, the instance DayFunctor.symmetricCategory, and its closed structure, the instance DayFunctor.monoidalClosed.

Main statements

• SymmetricSequence.isInitialUnitObj: the unit symmetric sequence is initial in every positive level.

References

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

@[reducible, inline]

abbrev TauCeti.SymmetricSequence : Type (u + 1)

Symmetric sequences of pointed simplicial sets: functors from the finite-bijection groupoid to pointed simplicial sets, with the Day convolution product along the block sum.

instance TauCeti.SymmetricSequence.hasLimitsOfShape (J : Type w) [CategoryTheory.Category.{v, w} J] [CategoryTheory.Limits.HasLimitsOfShape J PointedSSet] : CategoryTheory.Limits.HasLimitsOfShape J SymmetricSequence

Limits of symmetric sequences are the limits of their underlying functors.

instance TauCeti.SymmetricSequence.hasLimits : CategoryTheory.Limits.HasLimits SymmetricSequence

Symmetric sequences of small pointed simplicial sets have all small limits.

instance TauCeti.SymmetricSequence.hasColimitsOfShape (J : Type w) [CategoryTheory.Category.{v, w} J] [CategoryTheory.Limits.HasColimitsOfShape J PointedSSet] : CategoryTheory.Limits.HasColimitsOfShape J SymmetricSequence

Colimits of symmetric sequences are the colimits of their underlying functors.

instance TauCeti.SymmetricSequence.hasColimits : CategoryTheory.Limits.HasColimits SymmetricSequence

Symmetric sequences have all colimits small in the universe of their simplices.

instance TauCeti.SymmetricSequence.preservesColimitsOfShape_tensorLeft (J : Type w) [CategoryTheory.Category.{v, w} J] [CategoryTheory.Limits.HasColimitsOfShape J PointedSSet] (X : SymmetricSequence) : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MonoidalCategory.tensorLeft X)

Day convolution with a fixed symmetric sequence preserves levelwise colimits.

instance TauCeti.SymmetricSequence.preservesColimits_tensorLeft (X : SymmetricSequence) : CategoryTheory.Limits.PreservesColimits (CategoryTheory.MonoidalCategory.tensorLeft X)

Day convolution preserves all colimits small in the simplex universe.

instance TauCeti.SymmetricSequence.preservesColimits_tensorRight (X : SymmetricSequence) : CategoryTheory.Limits.PreservesColimits (CategoryTheory.MonoidalCategory.tensorRight X)

Day convolution with a fixed symmetric sequence on the right also preserves colimits small in the simplex universe, by the braiding.

noncomputable def TauCeti.SymmetricSequence.isInitialUnitObj (n : ℕ) : CategoryTheory.Limits.IsInitial ((CategoryTheory.MonoidalCategoryStruct.tensorUnit SymmetricSequence).functor.obj { len := n + 1 })

The unit symmetric sequence is initial, the point, in every positive level n + 1: no bijection reaches Fin (n + 1) from Fin 0.