The evaluation functor on subcomplexes

We define an evaluation functor SSet.Subcomplex.evaluation : X.Subcomplex ⥤ Set (X.obj j) when X : SSet and j : SimplexCategoryᵒᵖ. We use it to show that the functor Subcomplex.toSSetFunctor : X.Subcomplex ⥤ SSet preserves filtered colimits.

def SSet.Subcomplex.evaluation (X : SSet) (j : SimplexCategoryᵒᵖ) : CategoryTheory.Functor X.Subcomplex (Set (X.obj j))

The evaluation functor X.Subcomplex ⥤ Set (X.obj j) when X : SSet and j : SimplexCategoryᵒᵖ.

Equations

• SSet.Subcomplex.evaluation X j = { obj := fun (A : X.Subcomplex) => A.obj j, map := fun {X_1 Y : X.Subcomplex} (f : X_1 ⟶ Y) => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem SSet.Subcomplex.evaluation_obj (X : SSet) (j : SimplexCategoryᵒᵖ) (A : X.Subcomplex) : (evaluation X j).obj A = A.obj j

@[simp]

theorem SSet.Subcomplex.evaluation_map (X : SSet) (j : SimplexCategoryᵒᵖ) {X✝ Y✝ : X.Subcomplex} (f : X✝ ⟶ Y✝) : (evaluation X j).map f = CategoryTheory.homOfLE ⋯

instance SSet.Subcomplex.instPreservesColimitsOfShapeToSSetFunctorOfIsFilteredOrEmpty {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {X : SSet} [CategoryTheory.IsFilteredOrEmpty J] : CategoryTheory.Limits.PreservesColimitsOfShape J toSSetFunctor