Theorems · Definition · algebraic topology
SSet.stdSimplex
CategoryTheory.CosimplicialObject SSet
The functor SimplexCategory ⥤ SSet which sends ⦋n⦌ to the standard simplex Δ[n] is a
cosimplicial object in the category of simplicial sets. (This functor is essentially given by the
Yoneda embedding).
- Cited by
- 499 results in Mathlib
- Foundations
- Depth 32 from the axioms, rests on 348 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 1,283
- CategoryTheory.CosimplicialObjectstatement · cited by 125
- CategoryTheory.uliftYonedaproof · cited by 84
Cited by648
Results whose statement or proof uses this declaration.
- SSet.hornstatement and proof · cited by 162
- SSet.boundarystatement and proof · cited by 141
- SSet.stdSimplex.facestatement and proof · cited by 77
- SSet.stdSimplex.objEquivstatement · cited by 59
- SSet.yonedaEquivstatement · cited by 55
- SSet.stdSimplex.faceSingletonComplIsostatement · cited by 30
- SSet.prodStdSimplex.pairingCore.IsIndexstatement · cited by 26
- SSet.prodStdSimplex.objEquivstatement and proof · cited by 21
- SSet.Subcomplex.Pairing.RankFunction.sigmaStdSimplexproof · cited by 21
- SSet.horn.IsCompatiblestatement and proof · cited by 20
- SSet.Subcomplex.Pairing.RankFunction.Cell.hornstatement · cited by 19
- SSet.PtSimplex.MulStruct.mapstatement · cited by 18
Showing the 200 most cited of 648.