Documentation

Mathlib.AlgebraicTopology.SimplicialSet

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.)

We define the standard simplices Δ[n] as simplicial sets, and their boundaries ∂Δ[n] and horns Λ[n, i]. (The notations are available via Open Simplicial.)

Future work #

There isn't yet a complete API for simplices, boundaries, and horns. As an example, we should have a function that constructs from a non-surjective order preserving function Fin n → Fin n a morphism Δ[n] ⟶ ∂Δ[n].

def SSet :
Type (u + 1)

The category of simplicial sets. This is the category of contravariant functors from SimplexCategory to Type u.

Instances For
    theorem SSet.hom_ext {X : SSet} {Y : SSet} {f : X Y} {g : X Y} (w : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) :
    f = g

    The n-th standard simplex Δ[n] associated with a nonempty finite linear order n is the Yoneda embedding of n.

    Instances For

      The m-simplices of the n-th standard simplex are the monotone maps from Fin (m+1) to Fin (n+1).

      Instances For

        The boundary ∂Δ[n] of the n-th standard simplex consists of all m-simplices of standardSimplex n that are not surjective (when viewed as monotone function m → n).

        Instances For

          The inclusion of the boundary of the n-th standard simplex into that standard simplex.

          Instances For
            def SSet.horn (n : ) (i : Fin (n + 1)) :

            horn n i (or Λ[n, i]) is the i-th horn of the n-th standard simplex, where i : n. It consists of all m-simplices α of Δ[n] for which the union of {i} and the range of α is not all of n (when viewing α as monotone function m → n).

            Instances For

              The inclusion of the i-th horn of the n-th standard simplex into that standard simplex.

              Instances For
                noncomputable def SSet.S1 :

                The simplicial circle.

                Instances For
                  def SSet.Truncated (n : ) :
                  Type (u + 1)

                  Truncated simplicial sets.

                  Instances For
                    theorem SSet.Truncated.hom_ext {n : } {X : SSet.Truncated n} {Y : SSet.Truncated n} {f : X Y} {g : X Y} (w : ∀ (n : (SimplexCategory.Truncated n)ᵒᵖ), f.app n = g.app n) :
                    f = g

                    The skeleton functor on simplicial sets.

                    Instances For
                      @[inline, reducible]
                      abbrev SSet.Augmented :
                      Type (u + 1)

                      The category of augmented simplicial sets, as a particular case of augmented simplicial objects.

                      Instances For

                        The functor which sends [n] to the simplicial set Δ[n] equipped by the obvious augmentation towards the terminal object of the category of sets.

                        Instances For

                          The functor associating the singular simplicial set to a topological space.

                          Instances For

                            The geometric realization functor.

                            Instances For

                              Geometric realization is left adjoint to the singular simplicial set construction.

                              Instances For

                                The geometric realization of the representable simplicial sets agree with the usual topological simplices.

                                Instances For