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.lean, 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.

Notation

• ⦋n⦌ denotes the n-dimensional simplex. This notation is available with open Simplicial.
• ⦋m⦌ₙ denotes the m-dimensional simplex in the n-truncated simplex category. The truncation proof p : m ≤ n can also be provided using the syntax ⦋m, p⦌ₙ. This notation is available with open SimplexCategory.Truncated.

@[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)

def SimplexCategory.mk (n : ℕ) : SimplexCategory

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

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

the n-dimensional simplex can be denoted ⦋n⦌

def SimplexCategory.len (n : SimplexCategory) : ℕ

The length of an object of SimplexCategory.

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

theorem SimplexCategory.ext_iff {a b : SimplexCategory} : a = b ↔ a.len = b.len

@[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.

@[irreducible]

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

Morphisms in the SimplexCategory.

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.

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.

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.

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

Composition of morphisms of SimplexCategory.

instance SimplexCategory.smallCategory : CategoryTheory.SmallCategory SimplexCategory

@[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

theorem SimplexCategory.Hom.ext_iff {a b : SimplexCategory} {f g : a ⟶ b} : f = g ↔ toOrderHom f = toOrderHom g

def SimplexCategory.homEquivOrderHom {a b : SimplexCategory} : (a ⟶ b) ≃ (Fin (a.len + 1) →o Fin (b.len + 1))

Homs in SimplexCategory are equivalent to order-preserving functions of finite linear orders.

def SimplexCategory.homEquivFunctor {a b : SimplexCategory} : (a ⟶ b) ≃ CategoryTheory.Functor (Fin (a.len + 1)) (Fin (b.len + 1))

Homs in SimplexCategory are equivalent to functors between finite linear orders.

@[reducible, inline]

abbrev SimplexCategory.Truncated (n : ℕ) : Type

The truncated simplex category.

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

@[reducible, inline]

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

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

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

A proof that the full subcategory inclusion is fully faithful

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

theorem SimplexCategory.Truncated.Hom.ext_iff {n : ℕ} {a b : Truncated n} {f g : a ⟶ b} : f = g ↔ Hom.toOrderHom f.hom = Hom.toOrderHom g.hom

def SimplexCategory.Truncated.tacticTrunc : Lean.ParserDescr

A quick attempt to prove that ⦋m⦌ is n-truncated (⦋m⦌.len ≤ n).

def SimplexCategory.Truncated.mkNotation : Lean.ParserDescr

For m ≤ n, ⦋m⦌ₙ is the m-dimensional simplex in Truncated n. The proof p : m ≤ n can also be provided using the syntax ⦋m, p⦌ₙ.

@[reducible, inline]

abbrev SimplexCategory.Truncated.Hom.tr {n : ℕ} {a b : SimplexCategory} (f : a ⟶ b) (ha : a.len ≤ n := by trunc) (hb : b.len ≤ n := by trunc) : { obj := a, property := ha } ⟶ { obj := b, property := hb }

Make a morphism in Truncated n from a morphism in SimplexCategory. This is equivalent to @id (⦋a⦌ₙ ⟶ ⦋b⦌ₙ) f.

@[simp]

theorem SimplexCategory.Truncated.Hom.tr_id {n : ℕ} (a : SimplexCategory) (ha : a.len ≤ n := by trunc) : tr (CategoryTheory.CategoryStruct.id a) ha ha = CategoryTheory.CategoryStruct.id { obj := a, property := ha }

theorem SimplexCategory.Truncated.Hom.tr_comp {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c) (ha : a.len ≤ n := by trunc) (hb : b.len ≤ n := by trunc) (hc : c.len ≤ n := by trunc) : tr (CategoryTheory.CategoryStruct.comp f g) ha hc = CategoryTheory.CategoryStruct.comp (tr f ha hb) (tr g hb hc)

theorem SimplexCategory.Truncated.Hom.tr_comp_assoc {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c) (ha : a.len ≤ n := by trunc) (hb : b.len ≤ n := by trunc) (hc : c.len ≤ n := by trunc) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ n} (h : { obj := c, property := hc } ⟶ Z) : CategoryTheory.CategoryStruct.comp (tr (CategoryTheory.CategoryStruct.comp f g) ha hc) h = CategoryTheory.CategoryStruct.comp (tr f ha hb) (CategoryTheory.CategoryStruct.comp (tr g hb hc) h)

theorem SimplexCategory.Truncated.Hom.tr_comp' {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) {hb : b.len ≤ n} {hc : c.len ≤ n} (g : { obj := b, property := hb } ⟶ { obj := c, property := hc }) (ha : a.len ≤ n := by trunc) : tr (CategoryTheory.CategoryStruct.comp f g.hom) ha hc = CategoryTheory.CategoryStruct.comp (tr f ha hb) g

theorem SimplexCategory.Truncated.Hom.tr_comp'_assoc {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) {hb : b.len ≤ n} {hc : c.len ≤ n} (g : { obj := b, property := hb } ⟶ { obj := c, property := hc }) (ha : a.len ≤ n := by trunc) {Z : CategoryTheory.ObjectProperty.FullSubcategory fun (a : SimplexCategory) => a.len ≤ n} (h : { obj := c, property := hc } ⟶ Z) : CategoryTheory.CategoryStruct.comp (tr (CategoryTheory.CategoryStruct.comp f g.hom) ha hc) h = CategoryTheory.CategoryStruct.comp (tr f ha hb) (CategoryTheory.CategoryStruct.comp g h)

def SimplexCategory.Truncated.incl (n m : ℕ) (h : n ≤ m := by omega) : CategoryTheory.Functor (Truncated n) (Truncated m)

The inclusion of Truncated n into Truncated m when n ≤ m.

def SimplexCategory.Truncated.inclCompInclusion {n m : ℕ} (h : n ≤ m) : (incl n m h).comp (inclusion m) ≅ inclusion n

For all n ≤ m, inclusion n factors through Truncated m.