Documentation

Mathlib.AlgebraicTopology.SimplicialSet

Simplicial sets #

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.

Equations
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 ulift functor SSet.{u} ⥤ SSet.{max u v} on simplicial sets.

    Equations
    Instances For

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

      Equations
      Instances For

        Pretty printer defined by notation3 command.

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

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

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

            Simplices of the standard simplex identify to morphisms in SimplexCategory.

            Equations
            Instances For
              @[reducible, inline]

              Constructor for simplices of the standard simplex which takes a OrderHom as an input.

              Equations
              Instances For

                The canonical bijection (standardSimplex.obj n ⟶ X) ≃ X.obj (op n).

                Equations
                Instances For

                  The (degenerate) m-simplex in the standard simplex concentrated in vertex k.

                  Equations
                  Instances For
                    def SSet.standardSimplex.edge (n : ) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) :

                    The edge of the standard simplex with endpoints a and b.

                    Equations
                    Instances For
                      theorem SSet.standardSimplex.coe_edge_down_toOrderHom (n : ) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) :
                      def SSet.standardSimplex.triangle {n : } (a : Fin (n + 1)) (b : Fin (n + 1)) (c : Fin (n + 1)) (hab : a b) (hbc : b c) :

                      The triangle in the standard simplex with vertices a, b, and c.

                      Equations
                      Instances For
                        theorem SSet.standardSimplex.coe_triangle_down_toOrderHom {n : } (a : Fin (n + 1)) (b : Fin (n + 1)) (c : Fin (n + 1)) (hab : a b) (hbc : b c) :
                        def SSet.asOrderHom {n : } {m : SimplexCategoryᵒᵖ} (α : (SSet.standardSimplex.obj (SimplexCategory.mk n)).obj m) :
                        Fin ((Opposite.unop m).len + 1) →o Fin (n + 1)

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

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

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

                            The boundary ∂Δ[n] of the n-th standard simplex

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

                              Pretty printer defined by notation3 command.

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

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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).

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

                                    Pretty printer defined by notation3 command.

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

                                      The i-th horn Λ[n, i] of the standard n-simplex

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

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem SSet.horn.const_coe (n : ) (i : Fin (n + 3)) (k : Fin (n + 3)) (m : SimplexCategoryᵒᵖ) :
                                          def SSet.horn.const (n : ) (i : Fin (n + 3)) (k : Fin (n + 3)) (m : SimplexCategoryᵒᵖ) :
                                          (SSet.horn (n + 2) i).obj m

                                          The (degenerate) subsimplex of Λ[n+2, i] concentrated in vertex k.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem SSet.horn.edge_coe (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : {i, a, b}.card n) :
                                            (SSet.horn.edge n i a b hab H) = SSet.standardSimplex.edge n a b hab
                                            def SSet.horn.edge (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : {i, a, b}.card n) :

                                            The edge of Λ[n, i] with endpoints a and b.

                                            This edge only exists if {i, a, b} has cardinality less than n.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem SSet.horn.edge₃_coe_down (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : 3 n) :
                                              ((SSet.horn.edge₃ n i a b hab H)).down = SimplexCategory.Hom.mk { toFun := ![a, b], monotone' := }
                                              def SSet.horn.edge₃ (n : ) (i : Fin (n + 1)) (a : Fin (n + 1)) (b : Fin (n + 1)) (hab : a b) (H : 3 n) :

                                              Alternative constructor for the edge of Λ[n, i] with endpoints a and b, assuming 3 ≤ n.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem SSet.horn.primitiveEdge_coe_down {n : } {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) :
                                                ((SSet.horn.primitiveEdge h₀ hₙ j)).down = SimplexCategory.Hom.mk { toFun := ![j.castSucc, j.succ], monotone' := }
                                                def SSet.horn.primitiveEdge {n : } {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) :

                                                The edge of Λ[n, i] with endpoints j and j+1.

                                                This constructor assumes 0 < i < n, which is the type of horn that occurs in the horn-filling condition of quasicategories.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem SSet.horn.primitiveTriangle_coe {n : } (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ) (h : k < n + 2) :
                                                  (SSet.horn.primitiveTriangle i h₀ hₙ k h) = SSet.standardSimplex.triangle k, k + 1, k + 2,
                                                  def SSet.horn.primitiveTriangle {n : } (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ) (h : k < n + 2) :

                                                  The triangle in the standard simplex with vertices k, k+1, and k+2.

                                                  This constructor assumes 0 < i < n, which is the type of horn that occurs in the horn-filling condition of quasicategories.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem SSet.horn.face_coe {n : } (i : Fin (n + 2)) (j : Fin (n + 2)) (h : j i) :
                                                    def SSet.horn.face {n : } (i : Fin (n + 2)) (j : Fin (n + 2)) (h : j i) :

                                                    The jth subface of the i-th horn.

                                                    Equations
                                                    Instances For
                                                      theorem SSet.horn.hom_ext {n : } {i : Fin (n + 2)} {S : SSet} (σ₁ : SSet.horn (n + 1) i S) (σ₂ : SSet.horn (n + 1) i S) (h : ∀ (j : Fin (n + 2)) (h : j i), σ₁.app (Opposite.op (SimplexCategory.mk n)) (SSet.horn.face i j h) = σ₂.app (Opposite.op (SimplexCategory.mk n)) (SSet.horn.face i j h)) :
                                                      σ₁ = σ₂

                                                      Two morphisms from a horn are equal if they are equal on all suitable faces.

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

                                                      Truncated simplicial sets.

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

                                                        The skeleton functor on simplicial sets.

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

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

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem SSet.Augmented.standardSimplex_map_right :
                                                            ∀ {X Y : SimplexCategory} (θ : X Y) (a : ((fun (Δ : SimplexCategory) => { left := SSet.standardSimplex.obj Δ, right := ⊤_ Type u, hom := { app := fun (Δ' : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.standardSimplex.obj Δ)).obj Δ'), naturality := } }) X).right), (SSet.Augmented.standardSimplex.map θ).right a = CategoryTheory.Limits.terminal.from ((fun (Δ : SimplexCategory) => { left := SSet.standardSimplex.obj Δ, right := ⊤_ Type u, hom := { app := fun (Δ' : SimplexCategoryᵒᵖ) => CategoryTheory.Limits.terminal.from (((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject (Type u))).obj (SSet.standardSimplex.obj Δ)).obj Δ'), naturality := } }) X).right a

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

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