The simplex category

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

In Mathlib.AlgebraicTopology.SimplexCategory.Basic, 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]

def SimplexCategory : Type

The simplex category:

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

Equations

• SimplexCategory = ℕ

def SimplexCategory.mk (n : ℕ) : SimplexCategory

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

Equations

• SimplexCategory.mk n = n

def Simplicial.«term⦋_⦌» : Lean.ParserDescr

the n-dimensional simplex can be denoted ⦋n⦌

Equations

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

def SimplexCategory.len (n : SimplexCategory) : ℕ

The length of an object of SimplexCategory.

Equations

• n.len = n

theorem SimplexCategory.ext (a b : SimplexCategory) : a.len = b.len → a = b

@[simp]

theorem SimplexCategory.len_mk (n : ℕ) : (mk n).len = n

@[simp]

theorem SimplexCategory.mk_len (n : SimplexCategory) : mk n.len = n

def SimplexCategory.rec {F : SimplexCategory → Sort u_1} (h : (n : ℕ) → F (mk n)) (X : SimplexCategory) : F X

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

Equations

• SimplexCategory.rec h n = h n.len

@[irreducible]

def SimplexCategory.Hom (a b : SimplexCategory) : Type

Morphisms in the SimplexCategory.

Equations

• a.Hom b = (Fin (a.len + 1) →o Fin (b.len + 1))

def SimplexCategory.Hom.mk {a 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

• SimplexCategory.Hom.mk f = f

def SimplexCategory.Hom.toOrderHom {a 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

theorem SimplexCategory.Hom.ext' {a b : SimplexCategory} (f g : a.Hom b) : f.toOrderHom = g.toOrderHom → f = g

@[simp]

theorem SimplexCategory.Hom.mk_toOrderHom {a b : SimplexCategory} (f : a.Hom b) : mk f.toOrderHom = f

@[simp]

theorem SimplexCategory.Hom.toOrderHom_mk {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) : (mk f).toOrderHom = f

theorem SimplexCategory.Hom.mk_toOrderHom_apply {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) (i : Fin (a.len + 1)) : (mk f).toOrderHom i = f i

def SimplexCategory.Hom.id (a : SimplexCategory) : a.Hom a

Identity morphisms of SimplexCategory.

Equations

• SimplexCategory.Hom.id a = SimplexCategory.Hom.mk OrderHom.id

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

Composition of morphisms of SimplexCategory.

Equations

• f.comp g = SimplexCategory.Hom.mk (f.toOrderHom.comp g.toOrderHom)

instance SimplexCategory.smallCategory : CategoryTheory.SmallCategory SimplexCategory

Equations

• SimplexCategory.smallCategory = CategoryTheory.Category.mk @SimplexCategory.smallCategory.proof_1 @SimplexCategory.smallCategory.proof_2 @SimplexCategory.smallCategory.proof_3

@[simp]

theorem SimplexCategory.id_toOrderHom (a : SimplexCategory) : Hom.toOrderHom (CategoryTheory.CategoryStruct.id a) = OrderHom.id

@[simp]

theorem SimplexCategory.comp_toOrderHom {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c) : Hom.toOrderHom (CategoryTheory.CategoryStruct.comp f g) = (Hom.toOrderHom g).comp (Hom.toOrderHom f)

theorem SimplexCategory.Hom.ext {a b : SimplexCategory} (f g : a ⟶ b) : toOrderHom f = toOrderHom g → f = g

def SimplexCategory.Truncated (n : ℕ) : Type

The truncated simplex category.

Equations

• SimplexCategory.Truncated n = CategoryTheory.FullSubcategory fun (a : SimplexCategory) => a.len ≤ n

instance SimplexCategory.instSmallCategoryTruncated (n : ℕ) : CategoryTheory.SmallCategory (Truncated n)

Equations

• SimplexCategory.instSmallCategoryTruncated n = CategoryTheory.FullSubcategory.category fun (a : SimplexCategory) => a.len ≤ n

instance SimplexCategory.Truncated.instInhabited {n : ℕ} : Inhabited (Truncated n)

Equations

• SimplexCategory.Truncated.instInhabited = { default := { obj := SimplexCategory.mk 0, property := ⋯ } }

def SimplexCategory.Truncated.inclusion (n : ℕ) : CategoryTheory.Functor (Truncated n) SimplexCategory

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

Equations

• SimplexCategory.Truncated.inclusion n = CategoryTheory.fullSubcategoryInclusion fun (a : SimplexCategory) => a.len ≤ n

instance SimplexCategory.Truncated.instFullInclusion (n : ℕ) : (inclusion n).Full

instance SimplexCategory.Truncated.instFaithfulInclusion (n : ℕ) : (inclusion n).Faithful

noncomputable def SimplexCategory.Truncated.inclusion.fullyFaithful (n : ℕ) : (inclusion n).op.FullyFaithful

A proof that the full subcategory inclusion is fully faithful

Equations

• SimplexCategory.Truncated.inclusion.fullyFaithful n = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful (SimplexCategory.Truncated.inclusion n).op

theorem SimplexCategory.Truncated.Hom.ext {n : ℕ} {a b : Truncated n} (f g : a ⟶ b) : Hom.toOrderHom f = Hom.toOrderHom g → f = g