The commutative monoid of smash powers

For a pointed simplicial set X, the symmetric sequence n ↦ X^∧n of smash powers, with Σ_n permuting the smash factors and block concatenation X^∧p ∧ X^∧q ≅ X^∧(p+q), is a commutative monoid for the Day convolution product (SymmetricSequence.smashPow X). This is Hovey's symmetric algebra Sym(X), the free commutative monoid on X placed in level one, whose modules are the symmetric spectra based on X. A based map X ⟶ Y applied in every coordinate is a morphism of these monoids.

Main definitions

• SymmetricSequence.smashPow X: the commutative monoid n ↦ X^∧n of smash powers. Its commutative monoid structure is the instance DayFunctor.monObj, with commutativity DayFunctor.isCommMonObj.
• SymmetricSequence.smashPowMap f: the morphism of monoids induced by a based map f.
• SymmetricSequence.smashPowMapIso e: the isomorphism of monoids induced by an isomorphism e.

Main statements

• SymmetricSequence.smashPow_mul_app_smashMk: the multiplication of the smash powers concatenates coordinates.

References

• M. Hovey, Spectra and symmetric spectra in general model categories, J. Pure Appl. Algebra 165 (2001), 63–127.

@[reducible, inline]

noncomputable abbrev TauCeti.SymmetricSequence.smashPow (X : PointedSSet) : SymmetricSequence

The symmetric sequence n ↦ X^∧n of smash powers of a pointed simplicial set, with Σ_n permuting the smash factors. Block concatenation X^∧p ∧ X^∧q ≅ X^∧(p+q) and S⁰ ≅ X^∧0 make it a commutative monoid for the Day convolution product, through the instances DayFunctor.monObj and DayFunctor.isCommMonObj.

theorem TauCeti.SymmetricSequence.smashPow_mul_app_smashMk {X : PointedSSet} {k l : FiniteBijection} {n : SimplexCategoryᵒᵖ} (x : Fin k.len → (CategoryTheory.Under.right X).obj n) (y : Fin l.len → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayFunctor.η (smashPow X) (smashPow X)).app (k, l)) (CategoryTheory.MonObj.mul.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj k l)))).app n)) (PointedSSet.smashMk (PointedSSet.smashPowMk x) (PointedSSet.smashPowMk y)) = PointedSSet.smashPowMk (Fin.append x y)

The multiplication X^∧k ∧ X^∧l → X^∧(k+l) of the monoid of smash powers, restricted along the Day convolution unit, concatenates families of simplices.

noncomputable def TauCeti.SymmetricSequence.smashPowMap {X Y : PointedSSet} (f : X ⟶ Y) : smashPow X ⟶ smashPow Y

The morphism X^∧n ⟶ Y^∧n of symmetric sequences of smash powers induced by a based map f : X ⟶ Y, applying f in every coordinate. It is a morphism of monoids, through the instance DayFunctor.isMonHom.

@[simp]

theorem TauCeti.SymmetricSequence.smashPowMap_natTrans {X Y : PointedSSet} (f : X ⟶ Y) : (smashPowMap f).natTrans = PointedSSet.smashPowFunctorMap f

instance TauCeti.SymmetricSequence.instIsMonoidalFiniteBijectionPointedSSetNatTransSmashPowMap {X Y : PointedSSet} (f : X ⟶ Y) : CategoryTheory.NatTrans.IsMonoidal (smashPowMap f).natTrans

Applying a based map in every coordinate is a monoidal natural transformation.

@[simp]

theorem TauCeti.SymmetricSequence.smashPowMap_id {X : PointedSSet} : smashPowMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (smashPow X)

@[simp]

theorem TauCeti.SymmetricSequence.smashPowMap_comp {X Y Z : PointedSSet} (f : X ⟶ Y) (g : Y ⟶ Z) : smashPowMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (smashPowMap f) (smashPowMap g)

noncomputable def TauCeti.SymmetricSequence.smashPowMapIso {X Y : PointedSSet} (e : X ≅ Y) : smashPow X ≅ smashPow Y

The isomorphism of monoids of smash powers induced by an isomorphism e : X ≅ Y.

@[simp]

theorem TauCeti.SymmetricSequence.smashPowMapIso_hom {X Y : PointedSSet} (e : X ≅ Y) : (smashPowMapIso e).hom = smashPowMap e.hom

@[simp]

theorem TauCeti.SymmetricSequence.smashPowMapIso_inv {X Y : PointedSSet} (e : X ≅ Y) : (smashPowMapIso e).inv = smashPowMap e.inv

instance TauCeti.SymmetricSequence.instIsMonHomHomSmashPowMapIso {X Y : PointedSSet} (e : X ≅ Y) : CategoryTheory.IsMonHom (smashPowMapIso e).hom

The isomorphism of smash powers induced by an isomorphism is an isomorphism of monoids.