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]

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 : SimplexCategory) (b : SimplexCategory) : SimplexCategory.len a = SimplexCategory.len b → a = b

@[simp]

theorem SimplexCategory.len_mk (n : ℕ) : SimplexCategory.len (SimplexCategory.mk n) = n

@[simp]

theorem SimplexCategory.mk_len (n : SimplexCategory) : SimplexCategory.mk (SimplexCategory.len n) = n

def SimplexCategory.rec {F : SimplexCategory → Sort u_1} (h : (n : ℕ) → F (SimplexCategory.mk n)) (X : SimplexCategory) : F X

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

@[irreducible]

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

Morphisms in the SimplexCategory.

def SimplexCategory.Hom.mk {a : SimplexCategory} {b : SimplexCategory} (f : Fin (SimplexCategory.len a + 1) →o Fin (SimplexCategory.len b + 1)) : SimplexCategory.Hom a b

Make a moprhism in SimplexCategory from a monotone map of Fin's.

def SimplexCategory.Hom.toOrderHom {a : SimplexCategory} {b : SimplexCategory} (f : SimplexCategory.Hom a b) : Fin (SimplexCategory.len a + 1) →o Fin (SimplexCategory.len b + 1)

Recover the monotone map from a morphism in the simplex category.

theorem SimplexCategory.Hom.ext' {a : SimplexCategory} {b : SimplexCategory} (f : SimplexCategory.Hom a b) (g : SimplexCategory.Hom a b) : SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g → f = g

@[simp]

theorem SimplexCategory.Hom.mk_toOrderHom {a : SimplexCategory} {b : SimplexCategory} (f : SimplexCategory.Hom a b) : SimplexCategory.Hom.mk (SimplexCategory.Hom.toOrderHom f) = f

@[simp]

theorem SimplexCategory.Hom.toOrderHom_mk {a : SimplexCategory} {b : SimplexCategory} (f : Fin (SimplexCategory.len a + 1) →o Fin (SimplexCategory.len b + 1)) : SimplexCategory.Hom.toOrderHom (SimplexCategory.Hom.mk f) = f

theorem SimplexCategory.Hom.mk_toOrderHom_apply {a : SimplexCategory} {b : SimplexCategory} (f : Fin (SimplexCategory.len a + 1) →o Fin (SimplexCategory.len b + 1)) (i : Fin (SimplexCategory.len a + 1)) : ↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.Hom.mk f)) i = ↑f i

def SimplexCategory.Hom.id (a : SimplexCategory) : SimplexCategory.Hom a a

Identity morphisms of SimplexCategory.

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

Composition of morphisms of SimplexCategory.

@[simp]

theorem SimplexCategory.smallCategory_id (m : SimplexCategory) : CategoryTheory.CategoryStruct.id m = SimplexCategory.Hom.id m

@[simp]

theorem SimplexCategory.smallCategory_comp : ∀ {X Y Z : SimplexCategory} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = SimplexCategory.Hom.comp g f

instance SimplexCategory.smallCategory : CategoryTheory.SmallCategory SimplexCategory

theorem SimplexCategory.Hom.ext {a : SimplexCategory} {b : SimplexCategory} (f : a ⟶ b) (g : a ⟶ b) : SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g → f = g

def SimplexCategory.const (x : SimplexCategory) (i : Fin (SimplexCategory.len x + 1)) : SimplexCategory.mk 0 ⟶ x

The constant morphism from [0].

theorem SimplexCategory.const_comp (x : SimplexCategory) (y : SimplexCategory) (i : Fin (SimplexCategory.len x + 1)) (f : x ⟶ y) : CategoryTheory.CategoryStruct.comp (SimplexCategory.const x i) f = SimplexCategory.const y (↑(SimplexCategory.Hom.toOrderHom f) i)

def SimplexCategory.mkHom {n : ℕ} {m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) : SimplexCategory.mk n ⟶ SimplexCategory.mk m

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.

theorem SimplexCategory.hom_zero_zero (f : SimplexCategory.mk 0 ⟶ SimplexCategory.mk 0) : f = CategoryTheory.CategoryStruct.id (SimplexCategory.mk 0)

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)) : SimplexCategory.mk n ⟶ SimplexCategory.mk (n + 1)

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

def SimplexCategory.σ {n : ℕ} (i : Fin (n + 1)) : SimplexCategory.mk (n + 1) ⟶ SimplexCategory.mk n

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

theorem SimplexCategory.δ_comp_δ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ (Fin.succ j)) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.δ (Fin.castSucc i))

The generic case of the first simplicial identity

theorem SimplexCategory.δ_comp_δ' {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ j) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.pred j (_ : j = 0 → False))) (SimplexCategory.δ (Fin.castSucc i))

theorem SimplexCategory.δ_comp_δ'' {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.castLT i (_ : ↑i < n + 2))) (SimplexCategory.δ (Fin.succ j)) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.δ i)

theorem SimplexCategory.δ_comp_δ_self_assoc {n : ℕ} {i : Fin (n + 2)} {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.castSucc i)) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.succ i)) h)

theorem SimplexCategory.δ_comp_δ_self {n : ℕ} {i : Fin (n + 2)} : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ (Fin.castSucc i)) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ (Fin.succ i))

The special case of the first simplicial identity

theorem SimplexCategory.δ_comp_δ_self'_assoc {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = Fin.castSucc i) {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.succ i)) h)

theorem SimplexCategory.δ_comp_δ_self' {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = Fin.castSucc i) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ j) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ (Fin.succ i))

theorem SimplexCategory.δ_comp_σ_of_le_assoc {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.succ j)) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) h)

theorem SimplexCategory.δ_comp_σ_of_le {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.castSucc i)) (SimplexCategory.σ (Fin.succ j)) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ i)

The second simplicial identity

theorem SimplexCategory.δ_comp_σ_self_assoc {n : ℕ} {i : Fin (n + 1)} {Z : SimplexCategory} (h : SimplexCategory.mk n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) = h

theorem SimplexCategory.δ_comp_σ_self {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.castSucc i)) (SimplexCategory.σ i) = CategoryTheory.CategoryStruct.id (SimplexCategory.mk n)

The first part of the third simplicial identity

theorem SimplexCategory.δ_comp_σ_self'_assoc {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) {Z : SimplexCategory} (h : SimplexCategory.mk n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) = h

theorem SimplexCategory.δ_comp_σ_self' {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.σ i) = CategoryTheory.CategoryStruct.id (SimplexCategory.mk n)

theorem SimplexCategory.δ_comp_σ_succ_assoc {n : ℕ} {i : Fin (n + 1)} {Z : SimplexCategory} (h : SimplexCategory.mk n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.succ i)) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) = h

theorem SimplexCategory.δ_comp_σ_succ {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.succ i)) (SimplexCategory.σ i) = CategoryTheory.CategoryStruct.id (SimplexCategory.mk n)

The second part of the third simplicial identity

theorem SimplexCategory.δ_comp_σ_succ'_assoc {n : ℕ} (j : Fin (n + 2)) (i : Fin (n + 1)) (H : j = Fin.succ i) {Z : SimplexCategory} (h : SimplexCategory.mk n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h) = h

theorem SimplexCategory.δ_comp_σ_succ' {n : ℕ} (j : Fin (n + 2)) (i : Fin (n + 1)) (H : j = Fin.succ i) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.σ i) = CategoryTheory.CategoryStruct.id (SimplexCategory.mk n)

theorem SimplexCategory.δ_comp_σ_of_gt_assoc {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.succ i)) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.castSucc j)) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) h)

theorem SimplexCategory.δ_comp_σ_of_gt {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.succ i)) (SimplexCategory.σ (Fin.castSucc j)) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ i)

The fourth simplicial identity

theorem SimplexCategory.δ_comp_σ_of_gt'_assoc {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : Fin.succ j < i) {Z : SimplexCategory} (h : SimplexCategory.mk (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False))) h)

theorem SimplexCategory.δ_comp_σ_of_gt' {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : Fin.succ j < i) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.σ j) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))) (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False)))

theorem SimplexCategory.σ_comp_σ_assoc {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i ≤ j) {Z : SimplexCategory} (h : SimplexCategory.mk n ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.succ j)) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) h)

theorem SimplexCategory.σ_comp_σ {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.castSucc i)) (SimplexCategory.σ j) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ (Fin.succ j)) (SimplexCategory.σ i)

The fifth simplicial identity

@[simp]

theorem SimplexCategory.skeletalFunctor_obj (a : SimplexCategory) : SimplexCategory.skeletalFunctor.obj a = NonemptyFinLinOrd.of (ULift.{v, 0} (Fin (SimplexCategory.len a + 1)))

@[simp]

theorem SimplexCategory.skeletalFunctor_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.skeletalFunctor.map f = { toFun := fun i => { down := ↑(SimplexCategory.Hom.toOrderHom f) i.down }, monotone' := (_ : ∀ (i j : ↑((fun a => NonemptyFinLinOrd.of (ULift.{v, 0} (Fin (SimplexCategory.len a + 1)))) X)), i ≤ j → ↑(SimplexCategory.Hom.toOrderHom f) i.down ≤ ↑(SimplexCategory.Hom.toOrderHom f) j.down) }

def SimplexCategory.skeletalFunctor : CategoryTheory.Functor SimplexCategory NonemptyFinLinOrd

The functor that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

theorem SimplexCategory.skeletalFunctor.coe_map {Δ₁ : SimplexCategory} {Δ₂ : SimplexCategory} (f : Δ₁ ⟶ Δ₂) : ↑(SimplexCategory.skeletalFunctor.map f) = ULift.up ∘ ↑(SimplexCategory.Hom.toOrderHom f) ∘ ULift.down

theorem SimplexCategory.skeletal : CategoryTheory.Skeletal SimplexCategory

instance SimplexCategory.SkeletalFunctor.instFullSimplexCategorySmallCategoryNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategorySkeletalFunctor : CategoryTheory.Full SimplexCategory.skeletalFunctor

instance SimplexCategory.SkeletalFunctor.instFaithfulSimplexCategorySmallCategoryNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategorySkeletalFunctor : CategoryTheory.Faithful SimplexCategory.skeletalFunctor

instance SimplexCategory.SkeletalFunctor.instEssSurjSimplexCategoryNonemptyFinLinOrdSmallCategoryInstNonemptyFinLinOrdLargeCategorySkeletalFunctor : CategoryTheory.EssSurj SimplexCategory.skeletalFunctor

noncomputable instance SimplexCategory.SkeletalFunctor.isEquivalence : CategoryTheory.IsEquivalence SimplexCategory.skeletalFunctor

noncomputable def SimplexCategory.skeletalEquivalence : SimplexCategory ≌ NonemptyFinLinOrd

The equivalence that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

noncomputable def SimplexCategory.isSkeletonOf : CategoryTheory.IsSkeletonOf NonemptyFinLinOrd SimplexCategory SimplexCategory.skeletalFunctor

SimplexCategory is a skeleton of NonemptyFinLinOrd.

def SimplexCategory.Truncated (n : ℕ) : Type

The truncated simplex category.

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

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

def SimplexCategory.Truncated.inclusion {n : ℕ} : CategoryTheory.Functor (SimplexCategory.Truncated n) SimplexCategory

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

instance SimplexCategory.Truncated.instFullTruncatedInstSmallCategoryTruncatedSimplexCategorySmallCategoryInclusion (n : ℕ) : CategoryTheory.Full SimplexCategory.Truncated.inclusion

instance SimplexCategory.Truncated.instFaithfulTruncatedInstSmallCategoryTruncatedSimplexCategorySmallCategoryInclusion (n : ℕ) : CategoryTheory.Faithful SimplexCategory.Truncated.inclusion

instance SimplexCategory.instConcreteCategorySimplexCategorySmallCategory : CategoryTheory.ConcreteCategory SimplexCategory

theorem SimplexCategory.mono_iff_injective {n : SimplexCategory} {m : SimplexCategory} {f : n ⟶ m} : CategoryTheory.Mono f ↔ Function.Injective ↑(SimplexCategory.Hom.toOrderHom f)

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

theorem SimplexCategory.epi_iff_surjective {n : SimplexCategory} {m : SimplexCategory} {f : n ⟶ m} : CategoryTheory.Epi f ↔ Function.Surjective ↑(SimplexCategory.Hom.toOrderHom f)

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} : CategoryTheory.Mono f → SimplexCategory.len x ≤ SimplexCategory.len y

A monomorphism in SimplexCategory must increase lengths

theorem SimplexCategory.le_of_mono {n : ℕ} {m : ℕ} {f : SimplexCategory.mk n ⟶ SimplexCategory.mk m} : CategoryTheory.Mono f → n ≤ m

theorem SimplexCategory.len_le_of_epi {x : SimplexCategory} {y : SimplexCategory} {f : x ⟶ y} : CategoryTheory.Epi f → SimplexCategory.len y ≤ SimplexCategory.len x

An epimorphism in SimplexCategory must decrease lengths

theorem SimplexCategory.le_of_epi {n : ℕ} {m : ℕ} {f : SimplexCategory.mk n ⟶ SimplexCategory.mk m} : CategoryTheory.Epi f → m ≤ n

instance SimplexCategory.instMonoSimplexCategorySmallCategoryMkHAddNatInstHAddInstAddNatOfNatInstOfNatNatδ {n : ℕ} {i : Fin (n + 2)} : CategoryTheory.Mono (SimplexCategory.δ i)

instance SimplexCategory.instEpiSimplexCategorySmallCategoryMkHAddNatInstHAddInstAddNatOfNatInstOfNatNatσ {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.Epi (SimplexCategory.σ i)

instance SimplexCategory.instReflectsIsomorphismsSimplexCategorySmallCategoryTypeTypesForgetInstConcreteCategorySimplexCategorySmallCategory : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget SimplexCategory)

theorem SimplexCategory.isIso_of_bijective {x : SimplexCategory} {y : SimplexCategory} {f : x ⟶ y} (hf : Function.Bijective (SimplexCategory.Hom.toOrderHom f).toFun) : CategoryTheory.IsIso f

def SimplexCategory.orderIsoOfIso {x : SimplexCategory} {y : SimplexCategory} (e : x ≅ y) : Fin (SimplexCategory.len x + 1) ≃o Fin (SimplexCategory.len y + 1)

An isomorphism in SimplexCategory induces an OrderIso.

theorem SimplexCategory.iso_eq_iso_refl {x : SimplexCategory} (e : x ≅ x) : e = CategoryTheory.Iso.refl x

theorem SimplexCategory.eq_id_of_isIso {x : SimplexCategory} (f : x ⟶ x) [CategoryTheory.IsIso f] : f = CategoryTheory.CategoryStruct.id x

theorem SimplexCategory.eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : SimplexCategory.mk (n + 1) ⟶ Δ') (i : Fin (n + 1)) (hi : ↑(SimplexCategory.Hom.toOrderHom θ) (Fin.castSucc i) = ↑(SimplexCategory.Hom.toOrderHom θ) (Fin.succ i)) : ∃ θ', θ = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) θ'

theorem SimplexCategory.eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : SimplexCategory.mk (n + 1) ⟶ Δ') (hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)) : ∃ i θ', θ = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) θ'

theorem SimplexCategory.eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ SimplexCategory.mk (n + 1)) (i : Fin (n + 2)) (hi : ∀ (x : Fin (SimplexCategory.len Δ + 1)), ↑(SimplexCategory.Hom.toOrderHom θ) x ≠ i) : ∃ θ', θ = CategoryTheory.CategoryStruct.comp θ' (SimplexCategory.δ i)

theorem SimplexCategory.eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ SimplexCategory.mk (n + 1)) (hθ : ¬Function.Surjective ↑(SimplexCategory.Hom.toOrderHom θ)) : ∃ i θ', θ = CategoryTheory.CategoryStruct.comp θ' (SimplexCategory.δ i)

theorem SimplexCategory.eq_id_of_mono {x : SimplexCategory} (i : x ⟶ x) [CategoryTheory.Mono i] : i = CategoryTheory.CategoryStruct.id x

theorem SimplexCategory.eq_id_of_epi {x : SimplexCategory} (i : x ⟶ x) [CategoryTheory.Epi i] : i = CategoryTheory.CategoryStruct.id x

theorem SimplexCategory.eq_σ_of_epi {n : ℕ} (θ : SimplexCategory.mk (n + 1) ⟶ SimplexCategory.mk n) [CategoryTheory.Epi θ] : ∃ i, θ = SimplexCategory.σ i

theorem SimplexCategory.eq_δ_of_mono {n : ℕ} (θ : SimplexCategory.mk n ⟶ SimplexCategory.mk (n + 1)) [CategoryTheory.Mono θ] : ∃ i, θ = SimplexCategory.δ i

theorem SimplexCategory.len_lt_of_mono {Δ' : SimplexCategory} {Δ : SimplexCategory} (i : Δ' ⟶ Δ) [hi : CategoryTheory.Mono i] (hi' : Δ ≠ Δ') : SimplexCategory.len Δ' < SimplexCategory.len Δ

noncomputable instance SimplexCategory.instSplitEpiCategorySimplexCategorySmallCategory : CategoryTheory.SplitEpiCategory SimplexCategory

instance SimplexCategory.instHasStrongEpiMonoFactorisationsSimplexCategorySmallCategory : CategoryTheory.Limits.HasStrongEpiMonoFactorisations SimplexCategory

instance SimplexCategory.instHasStrongEpiImagesSimplexCategorySmallCategoryHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisationsSimplexCategorySmallCategory : CategoryTheory.Limits.HasStrongEpiImages SimplexCategory

instance SimplexCategory.instEpiSimplexCategorySmallCategoryImageHas_imageHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisationsSimplexCategorySmallCategoryFactorThruImage (Δ : SimplexCategory) (Δ' : SimplexCategory) (θ : Δ ⟶ Δ') : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage θ)

theorem SimplexCategory.image_eq {Δ : SimplexCategory} {Δ' : SimplexCategory} {Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ Δ'} [CategoryTheory.Epi e] {i : Δ' ⟶ Δ''} [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = φ) : CategoryTheory.Limits.image φ = Δ'

theorem SimplexCategory.image_ι_eq {Δ : SimplexCategory} {Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e] {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = φ) : CategoryTheory.Limits.image.ι φ = i

theorem SimplexCategory.factorThruImage_eq {Δ : SimplexCategory} {Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e] {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = φ) : CategoryTheory.Limits.factorThruImage φ = e

@[simp]

theorem SimplexCategory.toCat_obj (X : SimplexCategory) : SimplexCategory.toCat.obj X = CategoryTheory.Cat.of ↑((CategoryTheory.forget₂ PartOrd Preord).obj ((CategoryTheory.forget₂ Lat PartOrd).obj ((CategoryTheory.forget₂ LinOrd Lat).obj ((CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).obj (NonemptyFinLinOrd.of (ULift.{0, 0} (Fin (SimplexCategory.len X + 1))))))))

@[simp]

theorem SimplexCategory.toCat_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.toCat.map f = Monotone.functor (_ : Monotone ↑((CategoryTheory.forget₂ PartOrd Preord).map ((CategoryTheory.forget₂ Lat PartOrd).map ((CategoryTheory.forget₂ LinOrd Lat).map ((CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).map { toFun := fun i => { down := ↑(SimplexCategory.Hom.toOrderHom f) i.down }, monotone' := (_ : ∀ (i j : ↑((fun a => NonemptyFinLinOrd.of (ULift.{0, 0} (Fin (SimplexCategory.len a + 1)))) X)), i ≤ j → ↑(SimplexCategory.Hom.toOrderHom f) i.down ≤ ↑(SimplexCategory.Hom.toOrderHom f) j.down) })))))

def SimplexCategory.toCat : CategoryTheory.Functor SimplexCategory CategoryTheory.Cat

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