Documentation

Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject

The category of simplicial objects is simplicial #

In CategoryTheory.Functor.FunctorHom, it was shown that a category of functors C ⥤ D is enriched over a suitable category C ⥤ Type _ of functors to types.

In this file, we deduce that SimplicialObject D is enriched over SSet.{v} D (when D : Type u and [Category.{v} D]) and that SimplicialObject D is actually a simplicial category. In particular, the category of simplicial sets is a simplicial category.

Equations
  • One or more equations did not get rendered due to their size.
Equations