Documentation

Mathlib.AlgebraicTopology.SimplexCategory

The simplex category #

We construct a skeletal model of the simplex category, with objects and the morphism n ⟶ m being the monotone maps from Fin (n+1) to Fin (m+1).

We show that this category is equivalent to NonemptyFinLinOrd.

Remarks #

The definitions SimplexCategory and SimplexCategory.Hom are marked as irreducible.

We provide the following functions to work with these objects:

  1. SimplexCategory.mk creates an object of SimplexCategory out of a natural number. Use the notation [n] in the Simplicial locale.
  2. SimplexCategory.len gives the "length" of an object of SimplexCategory, as a natural.
  3. SimplexCategory.Hom.mk makes a morphism out of a monotone map between Fin's.
  4. SimplexCategory.Hom.toOrderHom gives the underlying monotone map associated to a term of SimplexCategory.Hom.
@[irreducible]

The simplex category:

  • objects are natural numbers n : ℕ
  • morphisms from n to m are monotone functions Fin (n+1) → Fin (m+1)
Equations
Instances For

    Interpret a natural number as an object of the simplex category.

    Equations
    Instances For

      the n-dimensional simplex can be denoted [n]

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

        The length of an object of SimplexCategory.

        Equations
        • n.len = n
        Instances For
          theorem SimplexCategory.ext (a : SimplexCategory) (b : SimplexCategory) :
          a.len = b.lena = b
          @[simp]
          def SimplexCategory.rec {F : SimplexCategorySort u_1} (h : (n : ) → F (SimplexCategory.mk n)) (X : SimplexCategory) :
          F X

          A recursor for SimplexCategory. Use it as induction Δ using SimplexCategory.rec.

          Equations
          Instances For
            @[irreducible]

            Morphisms in the SimplexCategory.

            Equations
            Instances For
              def SimplexCategory.Hom.mk {a : SimplexCategory} {b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) :
              a.Hom b

              Make a morphism in SimplexCategory from a monotone map of Fin's.

              Equations
              Instances For
                def SimplexCategory.Hom.toOrderHom {a : SimplexCategory} {b : SimplexCategory} (f : a.Hom b) :
                Fin (a.len + 1) →o Fin (b.len + 1)

                Recover the monotone map from a morphism in the simplex category.

                Equations
                • f.toOrderHom = f
                Instances For
                  theorem SimplexCategory.Hom.ext' {a : SimplexCategory} {b : SimplexCategory} (f : a.Hom b) (g : a.Hom b) :
                  f.toOrderHom = g.toOrderHomf = g
                  @[simp]
                  @[simp]
                  theorem SimplexCategory.Hom.toOrderHom_mk {a : SimplexCategory} {b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) :
                  (SimplexCategory.Hom.mk f).toOrderHom = f
                  theorem SimplexCategory.Hom.mk_toOrderHom_apply {a : SimplexCategory} {b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) (i : Fin (a.len + 1)) :
                  (SimplexCategory.Hom.mk f).toOrderHom i = f i

                  Identity morphisms of SimplexCategory.

                  Equations
                  Instances For
                    def SimplexCategory.Hom.comp {a : SimplexCategory} {b : SimplexCategory} {c : SimplexCategory} (f : b.Hom c) (g : a.Hom b) :
                    a.Hom c

                    Composition of morphisms of SimplexCategory.

                    Equations
                    Instances For
                      def SimplexCategory.const (x : SimplexCategory) (y : SimplexCategory) (i : Fin (y.len + 1)) :
                      x y

                      The constant morphism from [0].

                      Equations
                      Instances For
                        @[simp]
                        theorem SimplexCategory.const_apply (x : SimplexCategory) (y : SimplexCategory) (i : Fin (y.len + 1)) (a : Fin (x.len + 1)) :
                        (SimplexCategory.Hom.toOrderHom (x.const y i)) a = i
                        @[simp]
                        theorem SimplexCategory.const_comp (x : SimplexCategory) {y : SimplexCategory} {z : SimplexCategory} (f : y z) (i : Fin (y.len + 1)) :

                        Make a morphism [n] ⟶ [m] from a monotone map between fin's. This is useful for constructing morphisms between [n] directly without identifying n with [n].len.

                        Equations
                        Instances For

                          Generating maps for the simplex category #

                          TODO: prove that the simplex category is equivalent to one given by the following generators and relations.

                          The i-th face map from [n] to [n+1]

                          Equations
                          Instances For

                            The i-th degeneracy map from [n+1] to [n]

                            Equations
                            Instances For

                              The generic case of the first simplicial identity

                              The second simplicial identity

                              The fourth simplicial identity

                              If f : [m] ⟶ [n+1] is a morphism and j is not in the range of f, then factor_δ f j is a morphism [m] ⟶ [n] such that factor_δ f j ≫ δ j = f (as witnessed by factor_δ_spec).

                              Equations
                              Instances For

                                The functor that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

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

                                  The truncated simplex category.

                                  Equations
                                  Instances For
                                    Equations
                                    • SimplexCategory.Truncated.instInhabited = { default := { obj := SimplexCategory.mk 0, property := } }

                                    The fully faithful inclusion of the truncated simplex category into the usual simplex category.

                                    Equations
                                    Instances For
                                      instance SimplexCategory.Truncated.instFullInclusion (n : ) :
                                      SimplexCategory.Truncated.inclusion.Full
                                      Equations
                                      • =
                                      instance SimplexCategory.Truncated.instFaithfulInclusion (n : ) :
                                      SimplexCategory.Truncated.inclusion.Faithful
                                      Equations
                                      • =
                                      Equations
                                      • One or more equations did not get rendered due to their size.

                                      A morphism in SimplexCategory is a monomorphism precisely when it is an injective function

                                      A morphism in SimplexCategory is an epimorphism if and only if it is a surjective function

                                      A monomorphism in SimplexCategory must increase lengths

                                      An epimorphism in SimplexCategory must decrease lengths

                                      Equations
                                      • =
                                      Equations
                                      • =
                                      def SimplexCategory.orderIsoOfIso {x : SimplexCategory} {y : SimplexCategory} (e : x y) :
                                      Fin (x.len + 1) ≃o Fin (y.len + 1)

                                      An isomorphism in SimplexCategory induces an OrderIso.

                                      Equations
                                      Instances For
                                        theorem SimplexCategory.len_lt_of_mono {Δ' : SimplexCategory} {Δ : SimplexCategory} (i : Δ' Δ) [hi : CategoryTheory.Mono i] (hi' : Δ Δ') :
                                        Δ'.len < Δ.len
                                        @[simp]
                                        theorem SimplexCategory.toCat_map :
                                        ∀ {X Y : SimplexCategory} (f : X Y), SimplexCategory.toCat.map f = .functor

                                        This functor SimplexCategory ⥤ Cat sends [n] (for n : ℕ) to the category attached to the ordered set {0, 1, ..., n}

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