Theorems · Definition · algebraic topology
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse
(X Y : SSet.Truncated 2) →
CategoryTheory.Functor (X.HomotopyCategory × Y.HomotopyCategory)
(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategoryThe functor X.HomotopyCategory × Y.HomotopyCategory ⥤ (X ⊗ Y).HomotopyCategory
when X and Y are 2-truncated simplicial sets.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement · cited by 8,081
- CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
- SimplexCategorystatement · cited by 2,204
- SimplexCategory.lenstatement · cited by 542
- SimplexCategory.Truncatedstatement · cited by 236
- SSet.Truncatedstatement and proof · cited by 214
- CategoryTheory.Functor.uncurryproof · cited by 85
- SSet.Truncated.HomotopyCategorystatement · cited by 54
- SSet.Truncated.HomotopyCategory.BinaryProduct.curriedInverseproof · cited by 0
Cited by30
Results whose statement or proof uses this declaration.
- SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIsostatement and proof · cited by 3
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIsostatement and proof · cited by 3
- SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIsostatement and proof · cited by 2
- SSet.Truncated.HomotopyCategory.BinaryProduct.isoproof · cited by 2
- SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_appstatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.idProdMapHomotopyCategoryCompInverseIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategoryFstIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategorySndIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fststatement · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_sndstatement · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategoryProdIdCompInverseIsostatement and proof · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Isostatement and proof · cited by 1