The simplex category

We construct a skeletal model of the simplex category, with an object ⦋n⦌ for each n : ℕ, and morphisms ⦋n⦌ ⟶ ⦋m⦌ identify to 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

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.

structure SimplexCategory : Type

The simplex category:

• for each n : ℕ, there is an object ⦋n⦌;
• morphisms ⦋n⦌ ⟶ ⦋m⦌ are monotone functions Fin (n+1) → Fin (m+1)

• len : ℕ

  The length of an object in SimplexCategory

theorem SimplexCategory.ext_iff {x y : SimplexCategory} : x = y ↔ x.len = y.len

theorem SimplexCategory.ext {x y : SimplexCategory} (len : x.len = y.len) : x = y

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.

theorem SimplexCategory.len_mk (n : ℕ) : { len := n }.len = n

@[simp]

theorem SimplexCategory.mk_len (n : SimplexCategory) : { len := n.len } = n

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

@[implicit_reducible]

instance SimplexCategory.smallCategory : CategoryTheory.SmallCategory SimplexCategory

Equations

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

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

Equations

• SimplexCategory.homEquivOrderHom = { toFun := SimplexCategory.Hom.toOrderHom, invFun := SimplexCategory.Hom.mk, left_inv := ⋯, right_inv := ⋯ }

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.

Equations

• SimplexCategory.homEquivFunctor = SimplexCategory.homEquivOrderHom.trans OrderHom.equivFunctor

@[reducible, inline]

abbrev SimplexCategory.Truncated (n : ℕ) : Type

The truncated simplex category.

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

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) (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).

Equations

• SimplexCategory.Truncated.tacticTrunc = Lean.ParserDescr.node `SimplexCategory.Truncated.tacticTrunc 1024 (Lean.ParserDescr.nonReservedSymbol "trunc" false)

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⦌ₙ.

Equations

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

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

Equations

• SimplexCategory.Truncated.Hom.tr f ha hb = CategoryTheory.ObjectProperty.homMk 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)

@[reducible, inline]

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

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

Equations

• SimplexCategory.Truncated.incl n m h = CategoryTheory.ObjectProperty.ιOfLE ⋯

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

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

Equations

• SimplexCategory.Truncated.inclCompInclusion h = CategoryTheory.Iso.refl ((SimplexCategory.Truncated.incl n m ⋯).comp (SimplexCategory.Truncated.inclusion m))