Documentation

Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Coskeletal simplicial sets #

In this file, we prove that if X is StrictSegal then X is 2-coskeletal, i.e. X ≅ (cosk 2).obj X. In particular, nerves of categories are 2-coskeletal.

This isomorphism follows from the fact that rightExtensionInclusion X 2 is a right Kan extension. In fact, we show that when X is StrictSegal then (rightExtensionInclusion X n).IsPointwiseRightKanExtension holds.

As an example, SimplicialObject.IsCoskeletal (nerve C) 2 shows that that nerves of categories are 2-coskeletal.

The identity natural transformation exhibits a simplicial set as a right extension of its restriction along (Truncated.inclusion (n := n)).op.

Equations
Instances For
    @[reducible, inline]

    A morphism in SimplexCategory with domain ⦋0⦌, ⦋1⦌, or ⦋2⦌ defines an object in the comma category StructuredArrow (op ⦋n⦌) (Truncated.inclusion (n := 2)).op.

    Equations
    Instances For

      Given a term in the cone over the diagram (proj (op ⦋n⦌) ((Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X) where X is Strict Segal, one can produce an n-simplex in X.

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

        A strict Segal simplicial set is 2-coskeletal.

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

          When X is StrictSegal, X is 2-coskeletal.

          The essential data of the nerve functor is contained in the 2-truncation, which is recorded by the composite functor nerveFunctor₂.

          Equations
          Instances For

            The natural isomorphism between nerveFunctor and nerveFunctor₂ ⋙ Truncated.cosk 2 whose components nerve C ≅ (Truncated.cosk 2).obj (nerveFunctor₂.obj C) shows that nerves of categories are 2-coskeletal.

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