Theorems · Definition · algebraic topology
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.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Oppositestatement · cited by 8,081
- SimplexCategorystatement · cited by 2,204
- SSetstatement and proof · cited by 1,283
- SSet.Subcomplexstatement and proof · cited by 461
- SSet.Subcomplex.toSSetstatement and proof · cited by 315
- CategoryTheory.MonoidalCategory.curriedTensorstatement · cited by 170
- SSet.Subcomplex.ιstatement and proof · cited by 136
- SSet.Subcomplex.unionProdproof · cited by 96
- CategoryTheory.Functor.PushoutObjObjstatement · cited by 54
- SSet.Subcomplex.unionProd.ι₁proof · cited by 6
- SSet.Subcomplex.unionProd.ι₂proof · cited by 6
- SSet.Subcomplex.unionProd.isPushoutproof · cited by 2
Cited by10
Results whose statement or proof uses this declaration.
- SSet.Subcomplex.unionProd.pushoutObjObj_ιstatement and proof · cited by 2
- SSet.innerFibration_pullbackObjObjπproof · cited by 1
- SSet.fibration_pullbackObjObjπproof · cited by 1
- SSet.Subcomplex.unionProd.pushoutObjObj_inlstatement and proof · cited by 0
- SSet.Subcomplex.unionProd.pushoutObjObj_inrstatement and proof · cited by 0
- SSet.Subcomplex.unionProd.pushoutObjObj_ptstatement and proof · cited by 0
- SSet.innerAnodyneExtensions_unionProd_ιproof · cited by 0
- SSet.anodyneExtensions_unionProd_ιproof · cited by 0
- SSet.anodyneExtensions_unionProd_ι'proof · cited by 0
- SSet.innerAnodyneExtensions_unionProd_ι'proof · cited by 0