# mathlibdocumentation

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.
@[instance]
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]
theorem simplex_category.len_mk (n : ) :
= n
@[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) :
f = g
@[simp]
theorem simplex_category.hom.mk_to_preorder_hom_apply {a b : simplex_category} (f : fin (a.len + 1) →ₘ fin (b.len + 1)) (i : fin (a.len + 1)) :
= f i
@[simp]

Identity morphisms of simplex_category.

Equations
@[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_to_category_struct_comp (_x _x_1 _x_2 : simplex_category) (f : _x _x_1) (g : _x_1 _x_2) :
f g =
@[simp]
@[simp]
def simplex_category.mk_hom {n m : } (f : fin (n + 1) →ₘ fin (m + 1)) :

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.

def simplex_category.δ {n : } (i : fin (n + 2)) :

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

Equations
def simplex_category.σ {n : } (i : fin (n + 1)) :

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

Equations
theorem simplex_category.δ_comp_δ {n : } {i j : fin (n + 2)} (H : i j) :

The generic case of the first simplicial identity

theorem simplex_category.δ_comp_δ_self {n : } {i : fin (n + 2)} :

The special case of the first simplicial identity

theorem simplex_category.δ_comp_σ_of_le {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : i ) :

The second simplicial identity

theorem simplex_category.δ_comp_σ_self {n : } {i : fin (n + 1)} :

The first part of the third simplicial identity

theorem simplex_category.δ_comp_σ_succ {n : } {i : fin (n + 1)} :

The second part of the third simplicial identity

theorem simplex_category.δ_comp_σ_of_gt {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : < i) :

The fourth simplicial identity

theorem simplex_category.σ_comp_σ {n : } {i j : fin (n + 1)} (H : i j) :

The fifth simplicial identity

The functor that exhibits simplex_category as skeleton of NonemptyFinLinOrd

Equations
@[instance]
Equations
@[instance]
Equations

The equivalence that exhibits simplex_category as skeleton of NonemptyFinLinOrd

Equations

simplex_category is a skeleton of NonemptyFinLinOrd.

Equations
@[instance]
def simplex_category.truncated (n : ) :
Type u_1

The truncated simplex category.

Equations
@[instance]
Equations
@[instance]
@[instance]

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

Equations