The smash product of pointed simplicial sets

The smash product X ∧ Y of pointed simplicial sets is the degreewise smash product of pointed types: its n-simplices are the classes of pairs of n-simplices of X and Y, with every pair having a coordinate at the basepoint collapsed to the basepoint. Equivalently it is the degreewise quotient of the cartesian product X × Y by the wedge X ∨ Y. With unit S⁰ = Δ[0]₊, the smash product makes PointedSSet a symmetric monoidal category, whose braiding swaps the two factors.

The monoidal structure is transported from the pointwise smash product of simplicial objects in Pointed along PointedSSet.simplicialPointedEquivalence, so all coherence equations come from those of Pointed. This file supplies the simplex-level description of the structure.

Main definitions

• PointedSSet.smashMk x y: the class in X ⊗ Y of a pair of simplices of the same degree.
• PointedSSet.tensorUnitSimplex n: the non-basepoint n-simplex of the unit S⁰.
• PointedSSet.smashLift: the based map out of X ⊗ Y induced by a simplicial map out of the cartesian product sending the wedge to the basepoint.
• PointedSSet.wedge X Y: the wedge X ∨ Y, as a subcomplex of the cartesian product.
• PointedSSet.smashProj X Y: the quotient map from the cartesian product onto X ⊗ Y.

Main statements

• The instances MonoidalCategory PointedSSet and SymmetricCategory PointedSSet.
• PointedSSet.tensor_ext: based maps out of X ⊗ Y are determined on classes of pairs.
• PointedSSet.isPushout_smashProj: X ⊗ Y is the pushout of X × Y ← X ∨ Y → Δ[0].

References

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

@[instance_reducible]

instance TauCeti.PointedSSet.monoidalCategory : CategoryTheory.MonoidalCategory PointedSSet

The degreewise smash product makes pointed simplicial sets a monoidal category, with unit S⁰ = Δ[0]₊.

@[instance_reducible]

instance TauCeti.PointedSSet.symmetricCategory : CategoryTheory.SymmetricCategory PointedSSet

The swap of factors makes the degreewise smash product symmetric monoidal.

@[instance_reducible]

noncomputable instance TauCeti.PointedSSet.simplicialPointedEquivalenceMonoidal : simplicialPointedEquivalence.functor.Monoidal

The degreewise pointed presentation is strong monoidal for the smash product.

@[simp]

theorem TauCeti.PointedSSet.simplicialPointedEquivalence_μ (X Y : PointedSSet) : CategoryTheory.Functor.LaxMonoidal.μ simplicialPointedEquivalence.functor X Y = simplicialPointedEquivalence.counitIso.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (simplicialPointedEquivalence.functor.obj X) (simplicialPointedEquivalence.functor.obj Y))

The tensor comparison is the inverse counit on the degreewise smash product.

@[simp]

theorem TauCeti.PointedSSet.simplicialPointedEquivalence_δ (X Y : PointedSSet) : CategoryTheory.Functor.OplaxMonoidal.δ simplicialPointedEquivalence.functor X Y = simplicialPointedEquivalence.counitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (simplicialPointedEquivalence.functor.obj X) (simplicialPointedEquivalence.functor.obj Y))

The inverse tensor comparison is the counit on the degreewise smash product.

@[simp]

theorem TauCeti.PointedSSet.simplicialPointedEquivalence_ε : CategoryTheory.Functor.LaxMonoidal.ε simplicialPointedEquivalence.functor = simplicialPointedEquivalence.counitIso.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.SimplicialObject Pointed))

The unit comparison is the inverse counit on the constant pointed unit.

@[simp]

theorem TauCeti.PointedSSet.simplicialPointedEquivalence_η : CategoryTheory.Functor.OplaxMonoidal.η simplicialPointedEquivalence.functor = simplicialPointedEquivalence.counitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.SimplicialObject Pointed))

The inverse unit comparison is the counit on the constant pointed unit.

def TauCeti.PointedSSet.smashMk {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).obj n

The class in the smash product X ⊗ Y of a pair of simplices of the same degree.

theorem TauCeti.PointedSSet.smashMk_surjective {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} : Function.Surjective fun (p : (CategoryTheory.Under.right X).obj n × (CategoryTheory.Under.right Y).obj n) => smashMk p.1 p.2

theorem TauCeti.PointedSSet.smashMk_induction {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} {motive : (CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).obj n → Prop} (h : ∀ (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n), motive (smashMk x y)) (a : (CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).obj n) : motive a

Induction on the simplices of a smash product: it suffices to treat classes of pairs.

@[simp]

theorem TauCeti.PointedSSet.map_smashMk {X Y : PointedSSet} {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).map f)) (smashMk x y) = smashMk ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right X).map f)) x) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right Y).map f)) y)

theorem TauCeti.PointedSSet.point_tensorObj {X Y : PointedSSet} (n : SimplexCategoryᵒᵖ) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).point n = smashMk (X.point n) (Y.point n)

theorem TauCeti.PointedSSet.smashMk_eq_smashMk_iff {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} {x x' : (CategoryTheory.Under.right X).obj n} {y y' : (CategoryTheory.Under.right Y).obj n} : smashMk x y = smashMk x' y' ↔ x = x' ∧ y = y' ∨ (x = X.point n ∨ y = Y.point n) ∧ (x' = X.point n ∨ y' = Y.point n)

Two pairs have the same class exactly when they are equal or both lie in the wedge.

@[simp]

theorem TauCeti.PointedSSet.smashMk_eq_point_iff {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} {x : (CategoryTheory.Under.right X).obj n} {y : (CategoryTheory.Under.right Y).obj n} : smashMk x y = (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).point n ↔ x = X.point n ∨ y = Y.point n

A pair represents the basepoint exactly when it lies in the wedge.

@[simp]

theorem TauCeti.PointedSSet.smashMk_point_left {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (y : (CategoryTheory.Under.right Y).obj n) : smashMk (X.point n) y = (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).point n

@[simp]

theorem TauCeti.PointedSSet.smashMk_point_right {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) : smashMk x (Y.point n) = (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).point n

theorem TauCeti.PointedSSet.tensor_ext {X Y Z : PointedSSet} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ 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 x y) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) (smashMk x y)) : f = g

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

theorem TauCeti.PointedSSet.tensor_ext_iff {X Y Z : PointedSSet} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z} : f = g ↔ ∀ (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 x y) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) (smashMk x y)

@[simp]

theorem TauCeti.PointedSSet.tensorHom_app_smashMk {X Y X' Y' : PointedSSet} {n : SimplexCategoryᵒᵖ} (f : X ⟶ X') (g : Y ⟶ Y') (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).app n)) (smashMk x y) = smashMk ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) x) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) y)

@[simp]

theorem TauCeti.PointedSSet.whiskerLeft_app_smashMk {X Y Y' : PointedSSet} {n : SimplexCategoryᵒᵖ} (g : Y ⟶ Y') (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)).app n)) (smashMk x y) = smashMk x ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right g).app n)) y)

@[simp]

theorem TauCeti.PointedSSet.whiskerRight_app_smashMk {X Y X' : PointedSSet} {n : SimplexCategoryᵒᵖ} (f : X ⟶ X') (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)).app n)) (smashMk x y) = smashMk ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right f).app n)) x) y

@[simp]

theorem TauCeti.PointedSSet.associator_hom_app_smashMk {X Y Z : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) (z : (CategoryTheory.Under.right Z).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom).app n)) (smashMk (smashMk x y) z) = smashMk x (smashMk y z)

@[simp]

theorem TauCeti.PointedSSet.associator_inv_app_smashMk {X Y Z : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) (z : (CategoryTheory.Under.right Z).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv).app n)) (smashMk x (smashMk y z)) = smashMk (smashMk x y) z

@[simp]

theorem TauCeti.PointedSSet.braiding_hom_app_smashMk {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (β_ X Y).hom).app n)) (smashMk x y) = smashMk y x

@[simp]

theorem TauCeti.PointedSSet.braiding_inv_app_smashMk {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (β_ X Y).inv).app n)) (smashMk y x) = smashMk x y

The unit S⁰

noncomputable def TauCeti.PointedSSet.tensorUnitSimplex (n : SimplexCategoryᵒᵖ) : (CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet)).obj n

The non-basepoint n-simplex of the unit S⁰ = Δ[0]₊.

@[simp]

theorem TauCeti.PointedSSet.tensorUnitSimplex_ne_point (n : SimplexCategoryᵒᵖ) : tensorUnitSimplex n ≠ (CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet).point n

theorem TauCeti.PointedSSet.eq_point_or_eq_tensorUnitSimplex {n : SimplexCategoryᵒᵖ} (s : (CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet)).obj n) : s = (CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet).point n ∨ s = tensorUnitSimplex n

Every simplex of the unit S⁰ is the basepoint or the non-basepoint simplex.

@[simp]

theorem TauCeti.PointedSSet.map_tensorUnitSimplex {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorUnit PointedSSet)).map f)) (tensorUnitSimplex n) = tensorUnitSimplex m

@[simp]

theorem TauCeti.PointedSSet.leftUnitor_hom_app_smashMk {X : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom).app n)) (smashMk (tensorUnitSimplex n) x) = x

@[simp]

theorem TauCeti.PointedSSet.leftUnitor_inv_app_apply {X : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv).app n)) x = smashMk (tensorUnitSimplex n) x

@[simp]

theorem TauCeti.PointedSSet.rightUnitor_hom_app_smashMk {X : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom).app n)) (smashMk x (tensorUnitSimplex n)) = x

@[simp]

theorem TauCeti.PointedSSet.rightUnitor_inv_app_apply {X : PointedSSet} {n : SimplexCategoryᵒᵖ} (x : (CategoryTheory.Under.right X).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv).app n)) x = smashMk x (tensorUnitSimplex n)

The smash product as a quotient of the cartesian product

def TauCeti.PointedSSet.smashLift {X Y Z : PointedSSet} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y) ⟶ CategoryTheory.Under.right Z) (hl : ∀ (n : SimplexCategoryᵒᵖ) (y : (CategoryTheory.Under.right Y).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (X.point n, y) = Z.point n) (hr : ∀ (n : SimplexCategoryᵒᵖ) (x : (CategoryTheory.Under.right X).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (x, Y.point n) = Z.point n) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z

The based map out of the smash product X ⊗ Y induced by a simplicial map out of the cartesian product sending the wedge X ∨ Y to the basepoint.

@[simp]

theorem TauCeti.PointedSSet.smashLift_app_smashMk {X Y Z : PointedSSet} {n : SimplexCategoryᵒᵖ} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y) ⟶ CategoryTheory.Under.right Z) (hl : ∀ (n : SimplexCategoryᵒᵖ) (y : (CategoryTheory.Under.right Y).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (X.point n, y) = Z.point n) (hr : ∀ (n : SimplexCategoryᵒᵖ) (x : (CategoryTheory.Under.right X).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (x, Y.point n) = Z.point n) (x : (CategoryTheory.Under.right X).obj n) (y : (CategoryTheory.Under.right Y).obj n) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Under.Hom.right (smashLift f hl hr)).app n)) (smashMk x y) = (CategoryTheory.ConcreteCategory.hom (f.app n)) (x, y)

def TauCeti.PointedSSet.wedge (X Y : PointedSSet) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y)).Subcomplex

The wedge X ∨ Y, as the subcomplex of the cartesian product X × Y of the pairs having a coordinate at the basepoint.

@[simp]

theorem TauCeti.PointedSSet.mem_wedge_iff {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y)).obj n) : z ∈ (X.wedge Y).obj n ↔ z.1 = X.point n ∨ z.2 = Y.point n

A simplex of the cartesian product lies in the wedge exactly when one of its coordinates is the basepoint.

def TauCeti.PointedSSet.smashProj (X Y : PointedSSet) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y) ⟶ CategoryTheory.Under.right (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The quotient map from the cartesian product X × Y onto the smash product X ⊗ Y.

@[simp]

theorem TauCeti.PointedSSet.smashProj_app_apply {X Y : PointedSSet} {n : SimplexCategoryᵒᵖ} (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y)).obj n) : (CategoryTheory.ConcreteCategory.hom ((X.smashProj Y).app n)) z = smashMk z.1 z.2

instance TauCeti.PointedSSet.instEpiSSetSmashProj {X Y : PointedSSet} : CategoryTheory.Epi (X.smashProj Y)

@[simp]

theorem TauCeti.PointedSSet.smashProj_comp_smashLift {X Y Z : PointedSSet} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y) ⟶ CategoryTheory.Under.right Z) (hl : ∀ (n : SimplexCategoryᵒᵖ) (y : (CategoryTheory.Under.right Y).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (X.point n, y) = Z.point n) (hr : ∀ (n : SimplexCategoryᵒᵖ) (x : (CategoryTheory.Under.right X).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (x, Y.point n) = Z.point n) : CategoryTheory.CategoryStruct.comp (X.smashProj Y) (CategoryTheory.Under.Hom.right (smashLift f hl hr)) = f

@[simp]

theorem TauCeti.PointedSSet.smashProj_comp_smashLift_assoc {X Y Z : PointedSSet} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Under.right X) (CategoryTheory.Under.right Y) ⟶ CategoryTheory.Under.right Z) (hl : ∀ (n : SimplexCategoryᵒᵖ) (y : (CategoryTheory.Under.right Y).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (X.point n, y) = Z.point n) (hr : ∀ (n : SimplexCategoryᵒᵖ) (x : (CategoryTheory.Under.right X).obj n), (CategoryTheory.ConcreteCategory.hom (f.app n)) (x, Y.point n) = Z.point n) {Z✝ : SSet} (h : CategoryTheory.Under.right Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (X.smashProj Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right (smashLift f hl hr)) h) = CategoryTheory.CategoryStruct.comp f h

theorem TauCeti.PointedSSet.isPushout_smashProj {X Y : PointedSSet} : CategoryTheory.IsPushout (X.wedge Y).ι (SSet.stdSimplex.isTerminalObj₀.from (X.wedge Y).toSSet) (X.smashProj Y) (CategoryTheory.Under.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

The smash product X ⊗ Y is the quotient of the cartesian product X × Y collapsing the wedge X ∨ Y to the basepoint.