Simplicial sets #
A simplicial set is just a simplicial object in Type,
i.e. a Type-valued presheaf on the simplex category.
(One might be tempted to call these "simplicial types" when working in type-theoretic foundations, but this would be unnecessarily confusing given the existing notion of a simplicial type in homotopy type theory.)
The category of simplicial sets.
This is the category of contravariant functors from
SimplexCategory to Type u.
Equations
Instances For
- CategoryTheory.SimplicialCategory.instMonoidalClosedSSet_infinityCosmos
- CategoryTheory.SimplicialCategory.instSSet_infinityCosmos
- CategoryTheory.SimplicialCategory.instSymmetricCategorySSet_infinityCosmos
- SSet.hasColimits
- SSet.hasLimits
- SSet.instChosenFiniteProducts
- SSet.instCoeOutSubcomplex
- SSet.instInhabited
- SSet.largeCategory
Equations
The constant map of simplicial sets X ⟶ Y induced by a simplex y : Y _[0].
Equations
- SSet.const y = { app := fun (n : SimplexCategoryᵒᵖ) (x : X.obj n) => Y.map ((Opposite.unop n).const (SimplexCategory.mk 0) 0).op y, naturality := ⋯ }
The ulift functor SSet.{u} ⥤ SSet.{max u v} on simplicial sets.
Equations
- SSet.uliftFunctor = (CategoryTheory.SimplicialObject.whiskering (Type ?u.7) (Type (max ?u.7 ?u.8))).obj CategoryTheory.uliftFunctor.{?u.8, ?u.7}
Truncated simplicial sets.
Equations
Equations
The ulift functor SSet.Truncated.{u} ⥤ SSet.Truncated.{max u v} on truncated
simplicial sets.
Equations
- SSet.Truncated.uliftFunctor k = (CategoryTheory.whiskeringRight (SimplexCategory.Truncated k)ᵒᵖ (Type ?u.17) (Type (max ?u.17 ?u.18))).obj CategoryTheory.uliftFunctor.{?u.18, ?u.17}
The truncation functor on simplicial sets.
Equations
The n-skeleton as a functor SSet.Truncated n ⥤ SSet.
The n-coskeleton as a functor SSet.Truncated n ⥤ SSet.
The adjunction between the n-skeleton and n-truncation.
Equations
The adjunction between n-truncation and the n-coskeleton.
Equations
Since Truncated.inclusion is fully faithful, so is right Kan extension along it.
Since Truncated.inclusion is fully faithful, so is left Kan extension along it.
The category of augmented simplicial sets, as a particular case of augmented simplicial objects.