# mathlib3documentation

algebraic_topology.simplex_category

# The simplex category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 simplex_category and simplex_category.hom are marked as irreducible.

We provide the following functions to work with these objects:

1. simplex_category.mk creates an object of simplex_category out of a natural number. Use the notation [n] in the simplicial locale.
2. simplex_category.len gives the "length" of an object of simplex_category, as a natural.
3. simplex_category.hom.mk makes a morphism out of a monotone map between fin's.
4. simplex_category.hom.to_order_hom gives the underlying monotone map associated to a term of simplex_category.hom.
@[protected, instance]
@[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 simplex_category

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

Equations

The length of an object of simplex_category.

Equations
@[ext]
theorem simplex_category.ext (a b : simplex_category) :
a.len = b.len a = b
@[simp]
theorem simplex_category.len_mk (n : ) :
= n
@[protected]
def simplex_category.rec {F : simplex_category Sort u_1} (h : Π (n : ), F ) (X : simplex_category) :
F X

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

Equations
@[protected, nolint, irreducible]

Morphisms in the simplex_category.

Equations
def simplex_category.hom.mk {a b : simplex_category} (f : fin (a.len + 1) →o fin (b.len + 1)) :
a.hom b

Make a moprhism in simplex_category from a monotone map of fin's.

Equations
def simplex_category.hom.to_order_hom {a b : simplex_category} (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
@[ext]
theorem simplex_category.hom.ext {a b : simplex_category} (f g : a.hom b) :
f = g
@[simp]
@[simp]
theorem simplex_category.hom.to_order_hom_mk {a b : simplex_category} (f : fin (a.len + 1) →o fin (b.len + 1)) :
theorem simplex_category.hom.mk_to_order_hom_apply {a b : simplex_category} (f : fin (a.len + 1) →o fin (b.len + 1)) (i : fin (a.len + 1)) :
= f i
@[simp]

Identity morphisms of simplex_category.

Equations
@[simp]
def simplex_category.hom.comp {a b c : simplex_category} (f : b.hom c) (g : a.hom b) :
a.hom c

Composition of morphisms of simplex_category.

Equations
@[protected, instance]
Equations
@[simp]
theorem simplex_category.small_category_comp (_x _x_1 _x_2 : simplex_category) (f : _x _x_1) (g : _x_1 _x_2) :
f g =
def simplex_category.const (x : simplex_category) (i : fin (x.len + 1)) :

The constant morphism from [0].

Equations
@[simp]
theorem simplex_category.const_comp (x y : simplex_category) (i : fin (x.len + 1)) (f : x y) :
x.const i f = y.const
@[simp]
def simplex_category.mk_hom {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 beetween [n] directly without identifying n with [n].len.

Equations

## Generating maps for the simplex category #

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

def simplex_category.δ {n : } (i : fin (n + 2)) :

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

Equations
Instances for simplex_category.δ
def simplex_category.σ {n : } (i : fin (n + 1)) :

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

Equations
Instances for simplex_category.σ
theorem simplex_category.δ_comp_δ {n : } {i j : fin (n + 2)} (H : i j) :

The generic case of the first simplicial identity

theorem simplex_category.δ_comp_δ' {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : < j) :
theorem simplex_category.δ_comp_δ'' {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : i ) :
theorem simplex_category.δ_comp_δ_self {n : } {i : fin (n + 2)} :

The special case of the first simplicial identity

theorem simplex_category.δ_comp_δ_self_assoc {n : } {i : fin (n + 2)} {X' : simplex_category} (f' : simplex_category.mk (n + 1 + 1) X') :
=
theorem simplex_category.δ_comp_δ_self' {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : j = ) :
theorem simplex_category.δ_comp_δ_self'_assoc {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : j = ) {X' : simplex_category} (f' : simplex_category.mk (n + 1 + 1) X') :
=
theorem simplex_category.δ_comp_σ_of_le {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : i ) :

The second simplicial identity

theorem simplex_category.δ_comp_σ_of_le_assoc {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : i ) {X' : simplex_category} (f' : simplex_category.mk (n + 1) X') :
=
theorem simplex_category.δ_comp_σ_self_assoc {n : } {i : fin (n + 1)} {X' : simplex_category} (f' : X') :
= f'
theorem simplex_category.δ_comp_σ_self {n : } {i : fin (n + 1)} :

The first part of the third simplicial identity

theorem simplex_category.δ_comp_σ_self' {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = ) :
theorem simplex_category.δ_comp_σ_self'_assoc {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = ) {X' : simplex_category} (f' : X') :
= f'
theorem simplex_category.δ_comp_σ_succ_assoc {n : } {i : fin (n + 1)} {X' : simplex_category} (f' : X') :
= f'
theorem simplex_category.δ_comp_σ_succ {n : } {i : fin (n + 1)} :

The second part of the third simplicial identity

theorem simplex_category.δ_comp_σ_succ'_assoc {n : } (j : fin (n + 2)) (i : fin (n + 1)) (H : j = i.succ) {X' : simplex_category} (f' : X') :
= f'
theorem simplex_category.δ_comp_σ_succ' {n : } (j : fin (n + 2)) (i : fin (n + 1)) (H : j = i.succ) :
theorem simplex_category.δ_comp_σ_of_gt_assoc {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : < i) {X' : simplex_category} (f' : simplex_category.mk (n + 1) X') :
=
theorem simplex_category.δ_comp_σ_of_gt {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : < i) :

The fourth simplicial identity

theorem simplex_category.δ_comp_σ_of_gt' {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : j.succ < i) :
theorem simplex_category.δ_comp_σ_of_gt'_assoc {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : j.succ < i) {X' : simplex_category} (f' : simplex_category.mk (n + 1) X') :
theorem simplex_category.σ_comp_σ {n : } {i j : fin (n + 1)} (H : i j) :

The fifth simplicial identity

theorem simplex_category.σ_comp_σ_assoc {n : } {i j : fin (n + 1)} (H : i j) {X' : simplex_category} (f' : X') :
=
@[simp]
theorem simplex_category.skeletal_functor_map (a b : simplex_category) (f : a b) :
= {to_fun := λ (i : (NonemptyFinLinOrd.of (ulift (fin (a.len + 1))))), {down := , monotone' := _}

The functor that exhibits simplex_category as skeleton of NonemptyFinLinOrd

Equations
Instances for simplex_category.skeletal_functor
theorem simplex_category.skeletal_functor.coe_map {Δ₁ Δ₂ : simplex_category} (f : Δ₁ Δ₂) :
= ulift.up
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations

The equivalence that exhibits simplex_category as skeleton of NonemptyFinLinOrd

Equations

simplex_category is a skeleton of NonemptyFinLinOrd.

Equations
@[protected, instance]

The truncated simplex category.

Equations
Instances for simplex_category.truncated
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]

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

Equations
Instances for simplex_category.truncated.inclusion
@[protected, instance]
Equations

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

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

A monomorphism in simplex_category must increase lengths

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

An epimorphism in simplex_category must decrease lengths

theorem simplex_category.le_of_epi {n m : }  :
m n
@[protected, instance]
@[protected, instance]
@[simp]
def simplex_category.order_iso_of_iso {x y : simplex_category} (e : x y) :
fin (x.len + 1) ≃o fin (y.len + 1)

An isomorphism in simplex_category induces an order_iso.

Equations
theorem simplex_category.eq_σ_comp_of_not_injective' {n : } {Δ' : simplex_category} (θ : simplex_category.mk (n + 1) Δ') (i : fin (n + 1)) (hi : = ) :
(θ' : Δ'), θ =
theorem simplex_category.eq_σ_comp_of_not_injective {n : } {Δ' : simplex_category} (θ : simplex_category.mk (n + 1) Δ')  :
(i : fin (n + 1)) (θ' : Δ'), θ =
theorem simplex_category.eq_comp_δ_of_not_surjective' {n : } {Δ : simplex_category} (θ : Δ simplex_category.mk (n + 1)) (i : fin (n + 2)) (hi : (x : fin (Δ.len + 1)), ) :
(θ' : , θ =
theorem simplex_category.eq_comp_δ_of_not_surjective {n : } {Δ : simplex_category} (θ : Δ simplex_category.mk (n + 1))  :
(i : fin (n + 2)) (θ' : , θ =
theorem simplex_category.eq_σ_of_epi {n : } (θ : simplex_category.mk (n + 1) )  :
(i : fin (n + 1)),
theorem simplex_category.eq_δ_of_mono {n : } (θ : simplex_category.mk (n + 1))  :
(i : fin (n + 2)),
theorem simplex_category.len_lt_of_mono {Δ' Δ : simplex_category} (i : Δ' Δ) [hi : category_theory.mono i] (hi' : Δ Δ') :
Δ'.len < Δ.len
@[protected, instance]
Equations
@[protected, instance]
theorem simplex_category.image_eq {Δ Δ' Δ'' : simplex_category} {φ : Δ Δ''} {e : Δ Δ'} {i : Δ' Δ''} (fac : e i = φ) :
theorem simplex_category.image_ι_eq {Δ Δ'' : simplex_category} {φ : Δ Δ''} {e : Δ } {i : Δ''} (fac : e i = φ) :
theorem simplex_category.factor_thru_image_eq {Δ Δ'' : simplex_category} {φ : Δ Δ''} {e : Δ } {i : Δ''} (fac : e i = φ) :
@[simp]
@[simp]
theorem simplex_category.to_Cat_map (_x _x_1 : simplex_category) (f : _x _x_1) :

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

Equations