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)

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

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.

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

• 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

def SimplexCategory.Truncated (n : ℕ) : Type

The truncated simplex category.

Equations

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

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

Equations

• SimplexCategory.instSmallCategoryTruncated n = CategoryTheory.ObjectProperty.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.ObjectProperty.ι 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

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

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 = f

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)

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.

Equations

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

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.

Equations

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