# 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 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]

The simplex category:

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

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

Equations
Instances For

the n-dimensional simplex can be denoted [n]

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

The length of an object of SimplexCategory.

Equations
• n.len = n
Instances For
theorem SimplexCategory.ext (a : SimplexCategory) (b : SimplexCategory) :
a.len = b.lena = b
@[simp]
theorem SimplexCategory.len_mk (n : ) :
.len = n
def SimplexCategory.rec {F : } (h : (n : ) → F ) (X : SimplexCategory) :
F X

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

Equations
• = h n.len
Instances For
@[irreducible]

Morphisms in the SimplexCategory.

Equations
Instances For
def SimplexCategory.Hom.mk {a : SimplexCategory} {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
Instances For
def SimplexCategory.Hom.toOrderHom {a : SimplexCategory} {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
Instances For
theorem SimplexCategory.Hom.ext' {a : SimplexCategory} {b : SimplexCategory} (f : a.Hom b) (g : a.Hom b) :
f.toOrderHom = g.toOrderHomf = g
@[simp]
@[simp]
theorem SimplexCategory.Hom.toOrderHom_mk {a : SimplexCategory} {b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) :
.toOrderHom = f
theorem SimplexCategory.Hom.mk_toOrderHom_apply {a : SimplexCategory} {b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) (i : Fin (a.len + 1)) :
.toOrderHom i = f i

Identity morphisms of SimplexCategory.

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

Composition of morphisms of SimplexCategory.

Equations
Instances For
@[simp]
theorem SimplexCategory.id_toOrderHom (a : SimplexCategory) :
= OrderHom.id
@[simp]
theorem SimplexCategory.Hom.ext {a : SimplexCategory} {b : SimplexCategory} (f : a b) (g : a b) :
def SimplexCategory.const (x : SimplexCategory) (y : SimplexCategory) (i : Fin (y.len + 1)) :
x y

The constant morphism from [0].

Equations
Instances For
@[simp]
theorem SimplexCategory.const_eq_id :
.const 0 =
@[simp]
theorem SimplexCategory.const_apply (x : SimplexCategory) (y : SimplexCategory) (i : Fin (y.len + 1)) (a : Fin (x.len + 1)) :
(SimplexCategory.Hom.toOrderHom (x.const y i)) a = i
@[simp]
theorem SimplexCategory.const_comp (x : SimplexCategory) {y : SimplexCategory} {z : SimplexCategory} (f : y z) (i : Fin (y.len + 1)) :
CategoryTheory.CategoryStruct.comp (x.const y i) f = x.const z ()
def SimplexCategory.mkHom {n : } {m : } (f : Fin (n + 1) →o Fin (m + 1)) :

Make a morphism [n] ⟶ [m] from a monotone map between fin's. This is useful for constructing morphisms between [n] directly without identifying n with [n].len.

Equations
Instances For

## Generating maps for the simplex category #

TODO: prove that the simplex category is equivalent to one given by the following generators and relations.

def SimplexCategory.δ {n : } (i : Fin (n + 2)) :

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

Equations
Instances For
def SimplexCategory.σ {n : } (i : Fin (n + 1)) :

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

Equations
Instances For
theorem SimplexCategory.δ_comp_δ {n : } {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i j) :

The generic case of the first simplicial identity

theorem SimplexCategory.δ_comp_δ' {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) :
theorem SimplexCategory.δ_comp_δ'' {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) :
theorem SimplexCategory.δ_comp_δ_self_assoc {n : } {i : Fin (n + 2)} {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1 + 1) Z) :
=
theorem SimplexCategory.δ_comp_δ_self {n : } {i : Fin (n + 2)} :

The special case of the first simplicial identity

theorem SimplexCategory.δ_comp_δ_self'_assoc {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1 + 1) Z) :
theorem SimplexCategory.δ_comp_δ_self' {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) :
theorem SimplexCategory.δ_comp_σ_of_le_assoc {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1) Z) :
theorem SimplexCategory.δ_comp_σ_of_le {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) :

The second simplicial identity

theorem SimplexCategory.δ_comp_σ_self_assoc {n : } {i : Fin (n + 1)} {Z : SimplexCategory} (h : ) :
= h
theorem SimplexCategory.δ_comp_σ_self {n : } {i : Fin (n + 1)} :

The first part of the third simplicial identity

theorem SimplexCategory.δ_comp_σ_self'_assoc {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) {Z : SimplexCategory} (h : ) :
theorem SimplexCategory.δ_comp_σ_self' {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) :
theorem SimplexCategory.δ_comp_σ_succ_assoc {n : } {i : Fin (n + 1)} {Z : SimplexCategory} (h : ) :
theorem SimplexCategory.δ_comp_σ_succ {n : } {i : Fin (n + 1)} :

The second part of the third simplicial identity

theorem SimplexCategory.δ_comp_σ_succ'_assoc {n : } (j : Fin (n + 2)) (i : Fin (n + 1)) (H : j = i.succ) {Z : SimplexCategory} (h : ) :
theorem SimplexCategory.δ_comp_σ_succ' {n : } (j : Fin (n + 2)) (i : Fin (n + 1)) (H : j = i.succ) :
theorem SimplexCategory.δ_comp_σ_of_gt_assoc {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1) Z) :
theorem SimplexCategory.δ_comp_σ_of_gt {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :

The fourth simplicial identity

theorem SimplexCategory.δ_comp_σ_of_gt' {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
theorem SimplexCategory.σ_comp_σ_assoc {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i j) {Z : SimplexCategory} (h : ) :
=
theorem SimplexCategory.σ_comp_σ {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i j) :

The fifth simplicial identity

def SimplexCategory.factor_δ {m : } {n : } (f : ) (j : Fin (n + 2)) :

If f : [m] ⟶ [n+1] is a morphism and j is not in the range of f, then factor_δ f j is a morphism [m] ⟶ [n] such that factor_δ f j ≫ δ j = f (as witnessed by factor_δ_spec).

Equations
Instances For
theorem SimplexCategory.factor_δ_spec {m : } {n : } (f : ) (j : Fin (n + 2)) (hj : ∀ (k : Fin (m + 1)), ) :
@[simp]

The functor that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

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

The equivalence that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

Equations
Instances For

The truncated simplex category.

Equations
Instances For
Equations
• SimplexCategory.Truncated.instInhabited = { default := { obj := , property := } }

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

Equations
Instances For
instance SimplexCategory.Truncated.instFullInclusion (n : ) :
SimplexCategory.Truncated.inclusion.Full
Equations
• =
instance SimplexCategory.Truncated.instFaithfulInclusion (n : ) :
SimplexCategory.Truncated.inclusion.Faithful
Equations
• =
Equations
• One or more equations did not get rendered due to their size.

A morphism in SimplexCategory is a monomorphism precisely when it is an injective function

A morphism in SimplexCategory is an epimorphism if and only if it is a surjective function

theorem SimplexCategory.len_le_of_mono {x : SimplexCategory} {y : SimplexCategory} {f : x y} :
x.len y.len

A monomorphism in SimplexCategory must increase lengths

theorem SimplexCategory.le_of_mono {n : } {m : } {f : } :
n m
theorem SimplexCategory.len_le_of_epi {x : SimplexCategory} {y : SimplexCategory} {f : x y} :
y.len x.len

An epimorphism in SimplexCategory must decrease lengths

theorem SimplexCategory.le_of_epi {n : } {m : } {f : } :
m n
instance SimplexCategory.instMonoδ {n : } {i : Fin (n + 2)} :
Equations
• =
instance SimplexCategory.instEpiσ {n : } {i : Fin (n + 1)} :
Equations
• =
instance SimplexCategory.instReflectsIsomorphismsForget :
.ReflectsIsomorphisms
Equations
def SimplexCategory.orderIsoOfIso {x : SimplexCategory} {y : SimplexCategory} (e : x y) :
Fin (x.len + 1) ≃o Fin (y.len + 1)

An isomorphism in SimplexCategory induces an OrderIso.

Equations
• = { toFun := (), invFun := (), left_inv := , right_inv := }.toOrderIso
Instances For
theorem SimplexCategory.eq_σ_comp_of_not_injective' {n : } {Δ' : SimplexCategory} (θ : SimplexCategory.mk (n + 1) Δ') (i : Fin (n + 1)) (hi : i.castSucc = i.succ) :
∃ (θ' : ),
theorem SimplexCategory.eq_σ_comp_of_not_injective {n : } {Δ' : SimplexCategory} (θ : SimplexCategory.mk (n + 1) Δ') :
∃ (i : Fin (n + 1)) (θ' : ),
theorem SimplexCategory.eq_comp_δ_of_not_surjective' {n : } {Δ : SimplexCategory} (θ : Δ SimplexCategory.mk (n + 1)) (i : Fin (n + 2)) (hi : ∀ (x : Fin (Δ.len + 1)), ) :
∃ (θ' : ),
theorem SimplexCategory.eq_comp_δ_of_not_surjective {n : } {Δ : SimplexCategory} (θ : Δ SimplexCategory.mk (n + 1)) :
∃ (i : Fin (n + 2)) (θ' : ),
theorem SimplexCategory.eq_σ_of_epi {n : } (θ : ) :
∃ (i : Fin (n + 1)),
theorem SimplexCategory.eq_δ_of_mono {n : } (θ : ) :
∃ (i : Fin (n + 2)),
theorem SimplexCategory.len_lt_of_mono {Δ' : SimplexCategory} {Δ : SimplexCategory} (i : Δ' Δ) [hi : ] (hi' : Δ Δ') :
Δ'.len < Δ.len
noncomputable instance SimplexCategory.instSplitEpiCategory :
Equations
Equations
• =
theorem SimplexCategory.image_eq {Δ : SimplexCategory} {Δ' : SimplexCategory} {Δ'' : SimplexCategory} {φ : Δ Δ''} {e : Δ Δ'} {i : Δ' Δ''} (fac : ) :
theorem SimplexCategory.image_ι_eq {Δ : SimplexCategory} {Δ'' : SimplexCategory} {φ : Δ Δ''} {e : } {i : } (fac : ) :
theorem SimplexCategory.factorThruImage_eq {Δ : SimplexCategory} {Δ'' : SimplexCategory} {φ : Δ Δ''} {e : } {i : } (fac : ) :
@[simp]
theorem SimplexCategory.toCat_map :
∀ {X Y : SimplexCategory} (f : X Y), = .functor
@[simp]
theorem SimplexCategory.toCat_obj (X : SimplexCategory) :
= CategoryTheory.Cat.of ( (.obj (.obj ( (NonemptyFinLinOrd.of (Fin (X.len + 1)))))))

This functor SimplexCategory ⥤ Cat sends [n] (for n : ℕ) to the category attached to the ordered set {0, 1, ..., n}

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