mathlib documentation

algebraic_topology.simplex_category

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 simplex_category and simplex_category.hom are marked as irreducible.

We provide the following functions to work with these objects:

  1. simplex_category.mk creates an object of simplex_category out of a natural number. Use the notation [n] in the simplicial locale.
  2. simplex_category.len gives the "length" of an object of simplex_category, as a natural.
  3. simplex_category.hom.mk makes a morphism out of a monotone map between fin's.
  4. simplex_category.hom.to_preorder_hom gives the underlying monotone map associated to a term of simplex_category.hom.
def simplex_category  :
Type u

The simplex category:

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

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

Equations

The length of an object of simplex_category.

Equations
@[ext]
theorem simplex_category.ext (a b : simplex_category) :
a.len = b.lena = b
@[simp]
@[nolint]
def simplex_category.hom (a b : simplex_category) :
Type u

Morphisms in the simplex_category.

Equations
def simplex_category.hom.mk {a b : simplex_category} (f : fin (a.len + 1) →ₘ fin (b.len + 1)) :
a.hom b

Make a moprhism in simplex_category from a monotone map of fin's.

Equations

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

Equations
@[ext]
theorem simplex_category.hom.ext {a b : simplex_category} (f g : a.hom b) :
@[simp]
def simplex_category.hom.comp {a b c : simplex_category} (f : b.hom c) (g : a.hom b) :
a.hom c

Composition of morphisms of simplex_category.

Equations
@[instance]
Equations
@[simp]
theorem simplex_category.small_category_comp (_x _x_1 _x_2 : simplex_category) (f : _x _x_1) (g : _x_1 _x_2) :
@[simp]

The constant morphism from [0].

Equations
@[simp]
@[simp]

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

Equations

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

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

Equations

The generic case of the first simplicial identity

The special case of the first simplicial identity

The first part of the third simplicial identity

The second part of the third simplicial identity

The functor that exhibits simplex_category as skeleton of NonemptyFinLinOrd

Equations
def simplex_category.truncated (n : ) :
Type u

The truncated simplex category.

Equations

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

Equations
@[instance]
Equations

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

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

A monomorphism in simplex_category must increase lengths

An epimorphism in simplex_category must decrease lengths