Pushout-products of simplicial sets

Results about pushout-products and pullback-homs in the category of simplicial sets.

noncomputable def SSet.Subcomplex.unionProd.ιIso {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : CategoryTheory.Arrow.mk (S.unionProd T).ι ≅ CategoryTheory.Arrow.mk S.ι □ CategoryTheory.Arrow.mk T.ι

The inclusion (S.unionProd T).toSSet ⟶ X ⊗ Y is isomorphic to the pushout-product S.ι □ T.ι.

Equations

• One or more equations did not get rendered due to their size.

theorem SSet.Subcomplex.unionProd.ιIso_hom_left {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (ιIso S T).hom.left = ⋯.isoPushout.hom

theorem SSet.Subcomplex.unionProd.ιIso_hom_right_app_hom_apply {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) (X✝ : SimplexCategoryᵒᵖ) (a : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj X✝) : (CategoryTheory.ConcreteCategory.hom ((ιIso S T).hom.right.app X✝)) a = a

theorem SSet.Subcomplex.unionProd.ιIso_inv_right_app_hom_apply {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) (X✝ : SimplexCategoryᵒᵖ) (a : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj X✝) : (CategoryTheory.ConcreteCategory.hom ((ιIso S T).inv.right.app X✝)) a = a

theorem SSet.Subcomplex.unionProd.ιIso_inv_left {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) : (ιIso S T).inv.left = ⋯.isoPushout.inv