Smash powers of pointed simplicial sets and the sphere sequence

The smash power X^∧ι of a pointed simplicial set X, indexed by a type ι, is the degreewise smash power of pointed types: its n-simplices are the basepoint and the families of n-simplices of X avoiding the basepoint in every coordinate. Bijections of the index type act by reindexing coordinates, concatenation of families identifies X^∧ι ∧ X^∧κ with X^∧(ι ⊕ κ), and the smash power indexed by an empty type is the unit S⁰. A based map X ⟶ Y acts on smash powers coordinatewise, compatibly with these operations, and the smash power indexed by a type with a unique element is X itself.

Indexing by the finite-bijection groupoid gives the symmetric sequence PointedSSet.smashPowFunctor X : FiniteBijection ⥤ PointedSSet, n ↦ X^∧n, on which Equiv.Perm (Fin n) acts by permuting the smash factors. Block concatenation X^∧p ∧ X^∧q ≅ X^∧(p + q) and the identification S⁰ ≅ X^∧0 make it a braided strong monoidal functor from the block-sum symmetric monoidal structure on FiniteBijection to the smash product of pointed simplicial sets: the block swap of FiniteBijection corresponds to swapping the two smash factors.

For X the simplicial circle S¹ = Δ[1]/∂Δ[1] this is the sphere sequence PointedSSet.smashPowFunctor PointedSSet.circle, n ↦ S^n = (S¹)^∧n, with its coordinate-permutation actions and block-concatenation multiplication S^p ∧ S^q → S^(p+q). Under Day convolution along the block sum, lax braided monoidal functors out of FiniteBijection are the commutative monoids of symmetric sequences, and symmetric spectra are the modules over the sphere sequence.

Main definitions

• PointedSSet.smashPow X ι: the smash power X^∧ι.
• PointedSSet.smashPowMk: the class of a family of simplices.
• PointedSSet.smashPowLift: the based map out of a smash power induced by degreewise functions of families sending the families with a coordinate at the basepoint to the basepoint.
• PointedSSet.smashPowReindex, PointedSSet.smashPowReindexIso: the action of a bijection of index types.
• PointedSSet.smashPowMap, PointedSSet.smashPowMapIso: functoriality in the pointed simplicial set, applying a based map in every coordinate.
• PointedSSet.smashPowAppendIso: concatenation X^∧ι ⊗ X^∧κ ≅ X^∧(ι ⊕ κ).
• PointedSSet.smashPowUnitIso: the identification 𝟙_ ≅ X^∧ι for empty ι.
• PointedSSet.smashPowUniqueIso: the identification X^∧ι ≅ X for ι with a unique element.
• PointedSSet.smashPowFunctor X: the symmetric sequence n ↦ X^∧n, with its Functor.Monoidal and Functor.Braided instances.
• PointedSSet.sphere k: the simplicial k-sphere S^k = (S¹)^∧k.

References

• M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Sections 1 and 2.
• S. Schwede, Symmetric spectra, book project, Chapter I.

The smash power

noncomputable def TauCeti.PointedSSet.smashPow (X : PointedSSet) (ι : Type) : PointedSSet

The smash power X^∧ι of a pointed simplicial set, formed degreewise: its n-simplices are the basepoint and the families ι → X_n avoiding the basepoint in every coordinate.

noncomputable def TauCeti.PointedSSet.smashPowMk {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} (f : ι → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.Under.right (X.smashPow ι)).obj n

The class in the smash power X^∧ι of a family of n-simplices of X. It is the basepoint exactly when some coordinate is the basepoint.

@[simp]

theorem TauCeti.PointedSSet.map_smashPowMk {X : PointedSSet} {ι : Type} {n m : SimplexCategoryᵒᵖ} (g : n ⟶ m) (f : ι → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right (X.smashPow ι)).map g)) (smashPowMk f) = smashPowMk (⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right X).map g)) ∘ f)

@[simp]

theorem TauCeti.PointedSSet.smashPowMk_eq_point_iff {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} {f : ι → (CategoryTheory.Under.right X).obj n} : smashPowMk f = (X.smashPow ι).point n ↔ ∃ (i : ι), f i = X.point n

A family represents the basepoint exactly when some coordinate is the basepoint.

theorem TauCeti.PointedSSet.smashPowMk_eq_smashPowMk_iff {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} {f g : ι → (CategoryTheory.Under.right X).obj n} : smashPowMk f = smashPowMk g ↔ f = g ∨ (∃ (i : ι), f i = X.point n) ∧ ∃ (i : ι), g i = X.point n

Two families have the same class exactly when they are equal or both have a coordinate at the basepoint.

theorem TauCeti.PointedSSet.smashPowMk_induction {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} {motive : (CategoryTheory.Under.right (X.smashPow ι)).obj n → Prop} (point : motive ((X.smashPow ι).point n)) (mk : ∀ (f : ι → (CategoryTheory.Under.right X).obj n), motive (smashPowMk f)) (a : (CategoryTheory.Under.right (X.smashPow ι)).obj n) : motive a

Induction on the simplices of a smash power: it suffices to treat the basepoint and the classes of families.

theorem TauCeti.PointedSSet.smashPow_hom_ext {X : PointedSSet} {ι : Type} {Y : PointedSSet} {f g : X.smashPow ι ⟶ Y} (h : ∀ (n : SimplexCategoryᵒᵖ) (x : ι → (CategoryTheory.Under.right X).obj n), (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) (smashPowMk x) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) (smashPowMk x)) : f = g

Based maps out of a smash power are determined by their values on classes of families.

theorem TauCeti.PointedSSet.smashPow_hom_ext_iff {X : PointedSSet} {ι : Type} {Y : PointedSSet} {f g : X.smashPow ι ⟶ Y} : f = g ↔ ∀ (n : SimplexCategoryᵒᵖ) (x : ι → (CategoryTheory.Under.right X).obj n), (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) (smashPowMk x) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) (smashPowMk x)

theorem TauCeti.PointedSSet.smashPow_tensor_hom_ext {X : PointedSSet} {ι κ : Type} {Y Z : PointedSSet} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (X.smashPow ι) (Y.smashPow κ) ⟶ Z} (h : ∀ (n : SimplexCategoryᵒᵖ) (x : ι → (CategoryTheory.Under.right X).obj n) (y : κ → (CategoryTheory.Under.right Y).obj n), (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) (smashMk (smashPowMk x) (smashPowMk y)) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) (smashMk (smashPowMk x) (smashPowMk y))) : f = g

Based maps out of a smash product of two smash powers are determined by their values on pairs of classes of families.

noncomputable def TauCeti.PointedSSet.smashPowLift {X : PointedSSet} {ι : Type} {Z : PointedSSet} (F : (n : SimplexCategoryᵒᵖ) → (ι → (CategoryTheory.Under.right X).obj n) → (CategoryTheory.Under.right Z).obj n) (hF : ∀ (n : SimplexCategoryᵒᵖ) (f : ι → (CategoryTheory.Under.right X).obj n) (i : ι), f i = X.point n → F n f = Z.point n) (nat : ∀ (n m : SimplexCategoryᵒᵖ) (g : n ⟶ m) (f : ι → (fun (X : Type u) => X) ((CategoryTheory.Under.right X).obj n)), F m (⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right X).map g)) ∘ f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right Z).map g)) (F n f)) : X.smashPow ι ⟶ Z

The based map out of the smash power X^∧ι induced by degreewise functions of families that send the families with a coordinate at the basepoint to the basepoint and commute with the simplicial operators.

@[simp]

theorem TauCeti.PointedSSet.smashPowLift_app_smashPowMk {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} {Z : PointedSSet} (F : (n : SimplexCategoryᵒᵖ) → (ι → (CategoryTheory.Under.right X).obj n) → (CategoryTheory.Under.right Z).obj n) (hF : ∀ (n : SimplexCategoryᵒᵖ) (f : ι → (CategoryTheory.Under.right X).obj n) (i : ι), f i = X.point n → F n f = Z.point n) (nat : ∀ (n m : SimplexCategoryᵒᵖ) (g : n ⟶ m) (f : ι → (fun (X : Type u) => X) ((CategoryTheory.Under.right X).obj n)), F m (⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right X).map g)) ∘ f) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right Z).map g)) (F n f)) (f : ι → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (smashPowLift F hF nat)).app n)) (smashPowMk f) = F n f

Reindexing

noncomputable def TauCeti.PointedSSet.smashPowReindex (X : PointedSSet) {ι κ : Type} (e : ι ≃ κ) : X.smashPow ι ⟶ X.smashPow κ

The action of a bijection e : ι ≃ κ on smash powers, sending the class of a family f to the class of f ∘ e.symm.

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_app_smashPowMk {X : PointedSSet} {ι κ : Type} {n : SimplexCategoryᵒᵖ} (e : ι ≃ κ) (f : ι → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (X.smashPowReindex e)).app n)) (smashPowMk f) = smashPowMk (f ∘ ⇑e.symm)

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_refl {X : PointedSSet} {ι : Type} : X.smashPowReindex (Equiv.refl ι) = CategoryTheory.CategoryStruct.id (X.smashPow ι)

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_trans {X : PointedSSet} {ι κ μ : Type} (e : ι ≃ κ) (e' : κ ≃ μ) : X.smashPowReindex (e.trans e') = CategoryTheory.CategoryStruct.comp (X.smashPowReindex e) (X.smashPowReindex e')

noncomputable def TauCeti.PointedSSet.smashPowReindexIso (X : PointedSSet) {ι κ : Type} (e : ι ≃ κ) : X.smashPow ι ≅ X.smashPow κ

The isomorphism of smash powers induced by a bijection of index types.

@[simp]

theorem TauCeti.PointedSSet.smashPowReindexIso_hom {X : PointedSSet} {ι κ : Type} (e : ι ≃ κ) : (X.smashPowReindexIso e).hom = X.smashPowReindex e

@[simp]

theorem TauCeti.PointedSSet.smashPowReindexIso_inv {X : PointedSSet} {ι κ : Type} (e : ι ≃ κ) : (X.smashPowReindexIso e).inv = X.smashPowReindex e.symm

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_comp_smashPowReindex_symm {X : PointedSSet} {ι κ : Type} (e : ι ≃ κ) : CategoryTheory.CategoryStruct.comp (X.smashPowReindex e) (X.smashPowReindex e.symm) = CategoryTheory.CategoryStruct.id (X.smashPow ι)

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_comp_smashPowReindex_symm_assoc {X : PointedSSet} {ι κ : Type} (e : ι ≃ κ) {Z : PointedSSet} (h : X.smashPow ι ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowReindex e) (CategoryTheory.CategoryStruct.comp (X.smashPowReindex e.symm) h) = h

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_symm_comp_smashPowReindex {X : PointedSSet} {ι κ : Type} (e : ι ≃ κ) : CategoryTheory.CategoryStruct.comp (X.smashPowReindex e.symm) (X.smashPowReindex e) = CategoryTheory.CategoryStruct.id (X.smashPow κ)

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_symm_comp_smashPowReindex_assoc {X : PointedSSet} {ι κ : Type} (e : ι ≃ κ) {Z : PointedSSet} (h : X.smashPow κ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowReindex e.symm) (CategoryTheory.CategoryStruct.comp (X.smashPowReindex e) h) = h

Concatenation

noncomputable def TauCeti.PointedSSet.smashPowAppend (X : PointedSSet) (ι κ : Type) : CategoryTheory.MonoidalCategoryStruct.tensorObj (X.smashPow ι) (X.smashPow κ) ⟶ X.smashPow (ι ⊕ κ)

Concatenation of families, the based map X^∧ι ⊗ X^∧κ ⟶ X^∧(ι ⊕ κ).

@[simp]

theorem TauCeti.PointedSSet.smashPowAppend_app_smashMk {X : PointedSSet} {ι κ : Type} {n : SimplexCategoryᵒᵖ} (f : ι → (CategoryTheory.Under.right X).obj n) (g : κ → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (X.smashPowAppend ι κ)).app n)) (smashMk (smashPowMk f) (smashPowMk g)) = smashPowMk (Sum.elim f g)

noncomputable def TauCeti.PointedSSet.smashPowSplit (X : PointedSSet) (ι κ : Type) : X.smashPow (ι ⊕ κ) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (X.smashPow ι) (X.smashPow κ)

Splitting a family into its two blocks, the based map X^∧(ι ⊕ κ) ⟶ X^∧ι ⊗ X^∧κ inverse to concatenation.

@[simp]

theorem TauCeti.PointedSSet.smashPowSplit_app_smashPowMk {X : PointedSSet} {ι κ : Type} {n : SimplexCategoryᵒᵖ} (h : ι ⊕ κ → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (X.smashPowSplit ι κ)).app n)) (smashPowMk h) = smashMk (smashPowMk (h ∘ Sum.inl)) (smashPowMk (h ∘ Sum.inr))

noncomputable def TauCeti.PointedSSet.smashPowAppendIso (X : PointedSSet) (ι κ : Type) : CategoryTheory.MonoidalCategoryStruct.tensorObj (X.smashPow ι) (X.smashPow κ) ≅ X.smashPow (ι ⊕ κ)

Concatenation of families identifies X^∧ι ⊗ X^∧κ with X^∧(ι ⊕ κ).

@[simp]

theorem TauCeti.PointedSSet.smashPowAppendIso_hom {X : PointedSSet} {ι κ : Type} : (X.smashPowAppendIso ι κ).hom = X.smashPowAppend ι κ

@[simp]

theorem TauCeti.PointedSSet.smashPowAppendIso_inv {X : PointedSSet} {ι κ : Type} : (X.smashPowAppendIso ι κ).inv = X.smashPowSplit ι κ

@[simp]

theorem TauCeti.PointedSSet.smashPowAppend_comp_smashPowSplit {X : PointedSSet} {ι κ : Type} : CategoryTheory.CategoryStruct.comp (X.smashPowAppend ι κ) (X.smashPowSplit ι κ) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (X.smashPow ι) (X.smashPow κ))

@[simp]

theorem TauCeti.PointedSSet.smashPowAppend_comp_smashPowSplit_assoc {X : PointedSSet} {ι κ : Type} {Z : PointedSSet} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (X.smashPow ι) (X.smashPow κ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowAppend ι κ) (CategoryTheory.CategoryStruct.comp (X.smashPowSplit ι κ) h) = h

@[simp]

theorem TauCeti.PointedSSet.smashPowSplit_comp_smashPowAppend {X : PointedSSet} {ι κ : Type} : CategoryTheory.CategoryStruct.comp (X.smashPowSplit ι κ) (X.smashPowAppend ι κ) = CategoryTheory.CategoryStruct.id (X.smashPow (ι ⊕ κ))

@[simp]

theorem TauCeti.PointedSSet.smashPowSplit_comp_smashPowAppend_assoc {X : PointedSSet} {ι κ : Type} {Z : PointedSSet} (h : X.smashPow (ι ⊕ κ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowSplit ι κ) (CategoryTheory.CategoryStruct.comp (X.smashPowAppend ι κ) h) = h

The unit

noncomputable def TauCeti.PointedSSet.smashPowToUnit (X : PointedSSet) (ι : Type) [IsEmpty ι] : X.smashPow ι ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet

The based map X^∧ι ⟶ S⁰ for empty ι, sending the class of the empty family to the non-basepoint simplex.

@[simp]

theorem TauCeti.PointedSSet.smashPowToUnit_app_smashPowMk {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} [IsEmpty ι] (f : ι → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (X.smashPowToUnit ι)).app n)) (smashPowMk f) = tensorUnitSimplex n

instance TauCeti.PointedSSet.instIsIsoSmashPowToUnit {X : PointedSSet} {ι : Type} [IsEmpty ι] : CategoryTheory.IsIso (X.smashPowToUnit ι)

noncomputable def TauCeti.PointedSSet.smashPowUnitIso (X : PointedSSet) (ι : Type) [IsEmpty ι] : CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet ≅ X.smashPow ι

The smash power indexed by an empty type is the unit S⁰.

@[simp]

theorem TauCeti.PointedSSet.smashPowUnitIso_inv {X : PointedSSet} {ι : Type} [IsEmpty ι] : (X.smashPowUnitIso ι).inv = X.smashPowToUnit ι

@[simp]

theorem TauCeti.PointedSSet.smashPowUnitIso_hom_comp_smashPowToUnit {X : PointedSSet} {ι : Type} [IsEmpty ι] : CategoryTheory.CategoryStruct.comp (X.smashPowUnitIso ι).hom (X.smashPowToUnit ι) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet)

@[simp]

theorem TauCeti.PointedSSet.smashPowUnitIso_hom_comp_smashPowToUnit_assoc {X : PointedSSet} {ι : Type} [IsEmpty ι] {Z : PointedSSet} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowUnitIso ι).hom (CategoryTheory.CategoryStruct.comp (X.smashPowToUnit ι) h) = h

@[simp]

theorem TauCeti.PointedSSet.smashPowToUnit_comp_smashPowUnitIso_hom {X : PointedSSet} {ι : Type} [IsEmpty ι] : CategoryTheory.CategoryStruct.comp (X.smashPowToUnit ι) (X.smashPowUnitIso ι).hom = CategoryTheory.CategoryStruct.id (X.smashPow ι)

@[simp]

theorem TauCeti.PointedSSet.smashPowToUnit_comp_smashPowUnitIso_hom_assoc {X : PointedSSet} {ι : Type} [IsEmpty ι] {Z : PointedSSet} (h : X.smashPow ι ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowToUnit ι) (CategoryTheory.CategoryStruct.comp (X.smashPowUnitIso ι).hom h) = h

@[simp]

theorem TauCeti.PointedSSet.smashPowUnitIso_hom_app_tensorUnitSimplex {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} [IsEmpty ι] : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (X.smashPowUnitIso ι).hom).app n)) (tensorUnitSimplex n) = smashPowMk fun (a : ι) => isEmptyElim a

Functoriality in the pointed simplicial set

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

The based map X^∧ι ⟶ Y^∧ι induced by a based map f : X ⟶ Y, applying f in every coordinate.

@[simp]

theorem TauCeti.PointedSSet.smashPowMap_app_smashPowMk {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} {Y : PointedSSet} (f : X ⟶ Y) (x : ι → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (smashPowMap f ι)).app n)) (smashPowMk x) = smashPowMk (⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) ∘ x)

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_comp_smashPowMap {X : PointedSSet} {ι κ : Type} {Y : PointedSSet} (f : X ⟶ Y) (e : ι ≃ κ) : CategoryTheory.CategoryStruct.comp (X.smashPowReindex e) (smashPowMap f κ) = CategoryTheory.CategoryStruct.comp (smashPowMap f ι) (Y.smashPowReindex e)

Applying a based map in every coordinate commutes with reindexing the coordinates.

@[simp]

theorem TauCeti.PointedSSet.smashPowReindex_comp_smashPowMap_assoc {X : PointedSSet} {ι κ : Type} {Y : PointedSSet} (f : X ⟶ Y) (e : ι ≃ κ) {Z : PointedSSet} (h : Y.smashPow κ ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowReindex e) (CategoryTheory.CategoryStruct.comp (smashPowMap f κ) h) = CategoryTheory.CategoryStruct.comp (smashPowMap f ι) (CategoryTheory.CategoryStruct.comp (Y.smashPowReindex e) h)

Applying a based map in every coordinate commutes with reindexing the coordinates.

@[simp]

theorem TauCeti.PointedSSet.smashPowAppend_comp_smashPowMap {X : PointedSSet} {ι κ : Type} {Y : PointedSSet} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (X.smashPowAppend ι κ) (smashPowMap f (ι ⊕ κ)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (smashPowMap f ι) (smashPowMap f κ)) (Y.smashPowAppend ι κ)

Applying a based map in every coordinate commutes with concatenation of families.

@[simp]

theorem TauCeti.PointedSSet.smashPowAppend_comp_smashPowMap_assoc {X : PointedSSet} {ι κ : Type} {Y : PointedSSet} (f : X ⟶ Y) {Z : PointedSSet} (h : Y.smashPow (ι ⊕ κ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.smashPowAppend ι κ) (CategoryTheory.CategoryStruct.comp (smashPowMap f (ι ⊕ κ)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (smashPowMap f ι) (smashPowMap f κ)) (CategoryTheory.CategoryStruct.comp (Y.smashPowAppend ι κ) h)

Applying a based map in every coordinate commutes with concatenation of families.

@[simp]

theorem TauCeti.PointedSSet.smashPowMap_comp_smashPowToUnit {X : PointedSSet} {ι : Type} {Y : PointedSSet} [IsEmpty ι] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (smashPowMap f ι) (Y.smashPowToUnit ι) = X.smashPowToUnit ι

Applying a based map in every coordinate of the smash power indexed by an empty type is compatible with the identifications with the unit S⁰.

@[simp]

theorem TauCeti.PointedSSet.smashPowMap_comp_smashPowToUnit_assoc {X : PointedSSet} {ι : Type} {Y : PointedSSet} [IsEmpty ι] (f : X ⟶ Y) {Z : PointedSSet} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (smashPowMap f ι) (CategoryTheory.CategoryStruct.comp (Y.smashPowToUnit ι) h) = CategoryTheory.CategoryStruct.comp (X.smashPowToUnit ι) h

Applying a based map in every coordinate of the smash power indexed by an empty type is compatible with the identifications with the unit S⁰.

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

The isomorphism X^∧ι ≅ Y^∧ι induced by an isomorphism e : X ≅ Y, applying e in every coordinate.

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.PointedSSet.smashPowMap_hom_comp_smashPowMap_inv {X : PointedSSet} {ι : Type} {Y : PointedSSet} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp (smashPowMap e.hom ι) (smashPowMap e.inv ι) = CategoryTheory.CategoryStruct.id (X.smashPow ι)

@[simp]

theorem TauCeti.PointedSSet.smashPowMap_hom_comp_smashPowMap_inv_assoc {X : PointedSSet} {ι : Type} {Y : PointedSSet} (e : X ≅ Y) {Z : PointedSSet} (h : X.smashPow ι ⟶ Z) : CategoryTheory.CategoryStruct.comp (smashPowMap e.hom ι) (CategoryTheory.CategoryStruct.comp (smashPowMap e.inv ι) h) = h

@[simp]

theorem TauCeti.PointedSSet.smashPowMap_inv_comp_smashPowMap_hom {X : PointedSSet} {ι : Type} {Y : PointedSSet} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp (smashPowMap e.inv ι) (smashPowMap e.hom ι) = CategoryTheory.CategoryStruct.id (Y.smashPow ι)

@[simp]

theorem TauCeti.PointedSSet.smashPowMap_inv_comp_smashPowMap_hom_assoc {X : PointedSSet} {ι : Type} {Y : PointedSSet} (e : X ≅ Y) {Z : PointedSSet} (h : Y.smashPow ι ⟶ Z) : CategoryTheory.CategoryStruct.comp (smashPowMap e.inv ι) (CategoryTheory.CategoryStruct.comp (smashPowMap e.hom ι) h) = h

A single smash factor

noncomputable def TauCeti.PointedSSet.smashPowUniqueIso (X : PointedSSet) (ι : Type) [Unique ι] : X.smashPow ι ≅ X

The smash power indexed by a type with a unique element is the pointed simplicial set itself: the class of a family corresponds to its only coordinate.

@[simp]

theorem TauCeti.PointedSSet.smashPowUniqueIso_hom_app_smashPowMk {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} [Unique ι] (x : ι → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (X.smashPowUniqueIso ι).hom).app n)) (smashPowMk x) = x default

@[simp]

theorem TauCeti.PointedSSet.smashPowUniqueIso_inv_app {X : PointedSSet} {ι : Type} {n : SimplexCategoryᵒᵖ} [Unique ι] (x : (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (X.smashPowUniqueIso ι).inv).app n)) x = smashPowMk fun (x_1 : ι) => x

The symmetric sequence of smash powers

@[reducible, inline]

noncomputable abbrev TauCeti.PointedSSet.smashPowFunctor (X : PointedSSet) : CategoryTheory.Functor FiniteBijection PointedSSet

The symmetric sequence n ↦ X^∧n of smash powers of a pointed simplicial set, on which a bijection Fin n ≃ Fin m acts by permuting the smash factors.

noncomputable def TauCeti.PointedSSet.smashPowFunctorCoreMonoidal (X : PointedSSet) : X.smashPowFunctor.CoreMonoidal

Block concatenation and S⁰ ≅ X^∧0 make the symmetric sequence of smash powers a (strong) monoidal functor.

@[instance_reducible]

noncomputable instance TauCeti.PointedSSet.instMonoidalFiniteBijectionSmashPowFunctor {X : PointedSSet} : X.smashPowFunctor.Monoidal

@[simp]

theorem TauCeti.PointedSSet.smashPowFunctor_μ {X : PointedSSet} (k l : FiniteBijection) : CategoryTheory.Functor.LaxMonoidal.μ X.smashPowFunctor k l = CategoryTheory.CategoryStruct.comp (X.smashPowAppend (Fin k.len) (Fin l.len)) (X.smashPowReindex finSumFinEquiv)

@[simp]

theorem TauCeti.PointedSSet.smashPowFunctor_δ {X : PointedSSet} (k l : FiniteBijection) : CategoryTheory.Functor.OplaxMonoidal.δ X.smashPowFunctor k l = CategoryTheory.CategoryStruct.comp (X.smashPowReindex finSumFinEquiv.symm) (X.smashPowSplit (Fin k.len) (Fin l.len))

@[simp]

theorem TauCeti.PointedSSet.smashPowFunctor_ε {X : PointedSSet} : CategoryTheory.Functor.LaxMonoidal.ε X.smashPowFunctor = (X.smashPowUnitIso (Fin 0)).hom

@[simp]

theorem TauCeti.PointedSSet.smashPowFunctor_η {X : PointedSSet} : CategoryTheory.Functor.OplaxMonoidal.η X.smashPowFunctor = X.smashPowToUnit (Fin 0)

theorem TauCeti.PointedSSet.smashPowFunctor_μ_app_smashMk {X : PointedSSet} {n : SimplexCategoryᵒᵖ} {k l : FiniteBijection} (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.Functor.LaxMonoidal.μ X.smashPowFunctor k l)).app n)) (smashMk (smashPowMk x) (smashPowMk y)) = smashPowMk (Fin.append x y)

The multiplication of the symmetric sequence of smash powers concatenates families.

theorem TauCeti.PointedSSet.smashPowFunctor_δ_app_smashPowMk {X : PointedSSet} {n : SimplexCategoryᵒᵖ} {k l : FiniteBijection} (h : Fin (CategoryTheory.MonoidalCategoryStruct.tensorObj k l).len → (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.Functor.OplaxMonoidal.δ X.smashPowFunctor k l)).app n)) (smashPowMk h) = smashMk (smashPowMk (h ∘ Fin.castAdd l.len)) (smashPowMk (h ∘ Fin.natAdd k.len))

The comultiplication of the symmetric sequence of smash powers splits a family into its two blocks.

@[instance_reducible]

noncomputable instance TauCeti.PointedSSet.instBraidedFiniteBijectionSmashPowFunctor {X : PointedSSet} : X.smashPowFunctor.Braided

The block swap of FiniteBijection acts on X^∧(k + l) as the swap of the two smash factors X^∧k ∧ X^∧l, so the symmetric sequence of smash powers is a braided monoidal functor.

noncomputable def TauCeti.PointedSSet.smashPowFunctorMap {X Y : PointedSSet} (f : X ⟶ Y) : X.smashPowFunctor ⟶ Y.smashPowFunctor

A based map f : X ⟶ Y induces the morphism X^∧n ⟶ Y^∧n of symmetric sequences of smash powers applying f in every coordinate. It is a monoidal natural transformation.

@[simp]

theorem TauCeti.PointedSSet.smashPowFunctorMap_app {X Y : PointedSSet} (f : X ⟶ Y) (k : FiniteBijection) : (smashPowFunctorMap f).app k = smashPowMap f (Fin k.len)

instance TauCeti.PointedSSet.instIsMonoidalFiniteBijectionSmashPowFunctorMap {X Y : PointedSSet} (f : X ⟶ Y) : CategoryTheory.NatTrans.IsMonoidal (smashPowFunctorMap f)

Applying a based map in every coordinate is compatible with block concatenation and with the identifications S⁰ ≅ X^∧0.

@[reducible, inline]

noncomputable abbrev TauCeti.PointedSSet.sphere (k : ℕ) : PointedSSet

The simplicial k-sphere S^k = (S¹)^∧k, the k-fold smash power of the simplicial circle.