Documentation

InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.Basic

Simplicial categories #

A simplicial category is a category C that is enriched over the category of simplicial sets in such a way that morphisms in C identify to the 0-simplices of the enriched hom.

TODO #

References #

A simplicial category is a category C that is enriched over the category of simplicial sets in such a way that morphisms in C identify to the 0-simplices of the enriched hom.

Instances
    @[reducible, inline]

    Abbreviation for the enriched hom of a simplicial category.

    Equations
    Instances For

      The bijection (K ⟶ L) ≃ sHom K L _[0] for all objects K and L in a simplicial category.

      Equations
      Instances For

        The morphism sHom K' L ⟶ sHom K L induced by a morphism K ⟶ K'.

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

          The morphism sHom K L ⟶ sHom K L' induced by a morphism L ⟶ L'.

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

            The bifunctor Cᵒᵖ ⥤ C ⥤ SSet.{v} which sends K : Cᵒᵖ and L : C to sHom K.unop L.

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