Documentation

Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct

Pushout-products of simplicial sets #

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

source
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.
Instances For
    source
    theorem SSet.Subcomplex.unionProd.ιIso_inv_left {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) :
    (ιIso S T).inv.left = ⋯.isoPushout.inv
    source
    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
    source
    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
    source
    theorem SSet.Subcomplex.unionProd.ιIso_hom_left {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) :
    (ιIso S T).hom.left = ⋯.isoPushout.hom
    source
    noncomputable def SSet.Subcomplex.unionProd.pushoutObjObj {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) :
    (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj S.ι T.ι

    Given subcomplexes S and T of simplicial sets, this if a Functor.PushoutObjObj structure for the chosen binary products on SSet, with point S.unionProd T.

    Equations
    Instances For
      source
      @[simp]
      theorem SSet.Subcomplex.unionProd.pushoutObjObj_inl {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) :
      (pushoutObjObj S T).inl = ι₁ S T
      source
      @[simp]
      theorem SSet.Subcomplex.unionProd.pushoutObjObj_inr {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) :
      (pushoutObjObj S T).inr = ι₂ S T
      source
      @[simp]
      theorem SSet.Subcomplex.unionProd.pushoutObjObj_pt {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) :
      (pushoutObjObj S T).pt = (S.unionProd T).toSSet
      source
      @[simp]
      theorem SSet.Subcomplex.unionProd.pushoutObjObj_ι {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) :
      (pushoutObjObj S T).ι = (S.unionProd T).ι