Basic properties of the simplex category

In Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean, we define the simplex category with objects ℕ and morphisms n ⟶ m the monotone maps from Fin (n + 1) to Fin (m + 1).

In this file, we define the generating maps for the simplex category, show that this category is equivalent to NonemptyFinLinOrd, and establish basic properties of its epimorphisms and monomorphisms.

instance SimplexCategory.instFiniteHom {a b : SimplexCategory} : Finite (a ⟶ b)

@[implicit_reducible]

instance SimplexCategory.instDecidableEqHom {n m : SimplexCategory} : DecidableEq (n ⟶ m)

theorem SimplexCategory.congr_toOrderHom_apply {a b : SimplexCategory} {f g : a ⟶ b} (h : f = g) (x : Fin (a.len + 1)) : (Hom.toOrderHom f) x = (Hom.toOrderHom g) x

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

The constant morphism from ⦋0⦌.

@[simp]

theorem SimplexCategory.const_eq_id : (mk 0).const (mk 0) 0 = CategoryTheory.CategoryStruct.id (mk 0)

@[simp]

theorem SimplexCategory.const_apply (x y : SimplexCategory) (i : Fin (y.len + 1)) (a : Fin (x.len + 1)) : (Hom.toOrderHom (x.const y i)) a = i

@[simp]

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

theorem SimplexCategory.const_fac_thru_zero (n m : SimplexCategory) (i : Fin (m.len + 1)) : n.const m i = CategoryTheory.CategoryStruct.comp (n.const (mk 0) 0) ((mk 0).const m i)

theorem SimplexCategory.Hom.ext_zero_left {n : SimplexCategory} (f g : SimplexCategory.mk 0 ⟶ n) (h0 : (toOrderHom f) 0 = (toOrderHom g) 0 := by rfl) : f = g

theorem SimplexCategory.eq_const_of_zero {n : SimplexCategory} (f : mk 0 ⟶ n) : f = (mk 0).const n ((Hom.toOrderHom f) 0)

theorem SimplexCategory.exists_eq_const_of_zero {n : SimplexCategory} (f : mk 0 ⟶ n) : ∃ (a : Fin (n.len + 1)), f = (mk 0).const n a

theorem SimplexCategory.eq_const_to_zero {n : SimplexCategory} (f : n ⟶ mk 0) : f = n.const (mk 0) 0

theorem SimplexCategory.Hom.ext_one_left {n : SimplexCategory} (f g : SimplexCategory.mk 1 ⟶ n) (h0 : (toOrderHom f) 0 = (toOrderHom g) 0 := by rfl) (h1 : (toOrderHom f) 1 = (toOrderHom g) 1 := by rfl) : f = g

theorem SimplexCategory.eq_of_one_to_one (f : mk 1 ⟶ mk 1) : (∃ (a : Fin ((mk 1).len + 1)), f = (mk 1).const (mk 1) a) ∨ f = CategoryTheory.CategoryStruct.id (mk 1)

def SimplexCategory.mkHom {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) : mk n ⟶ 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.

def SimplexCategory.mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) : mk 1 ⟶ mk n

The morphism ⦋1⦌ ⟶ ⦋n⦌ that picks out a specified h : i ≤ j in Fin (n+1).

@[simp]

theorem SimplexCategory.mkOfLe_refl {n : ℕ} (j : Fin (n + 1)) : mkOfLe j j ⋯ = (mk 1).const (mk n) j

def SimplexCategory.diag (n : ℕ) : mk 1 ⟶ mk n

The morphism ⦋1⦌ ⟶ ⦋n⦌ that picks out the "diagonal composite" edge

def SimplexCategory.intervalEdge {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) : mk 1 ⟶ mk n

The morphism ⦋1⦌ ⟶ ⦋n⦌ that picks out the edge spanning the interval from j to j + l.

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

The morphism ⦋1⦌ ⟶ ⦋n⦌ that picks out the arrow i ⟶ i+1 in Fin (n+1).

@[simp]

theorem SimplexCategory.mkOfSucc_homToOrderHom_zero {n : ℕ} (i : Fin n) : (Hom.toOrderHom (mkOfSucc i)) 0 = i.castSucc

@[simp]

theorem SimplexCategory.mkOfSucc_homToOrderHom_one {n : ℕ} (i : Fin n) : (Hom.toOrderHom (mkOfSucc i)) 1 = i.succ

@[simp]

theorem SimplexCategory.mkOfSucc_eq_id : mkOfSucc 0 = CategoryTheory.CategoryStruct.id (mk 1)

def SimplexCategory.mkOfLeComp {n : ℕ} (i j k : Fin (n + 1)) (h₁ : i ≤ j) (h₂ : j ≤ k) : mk 2 ⟶ mk n

The morphism ⦋2⦌ ⟶ ⦋n⦌ that picks out a specified composite of morphisms in Fin (n+1).

def SimplexCategory.subinterval {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) : mk l ⟶ mk n

The "inert" morphism associated to a subinterval j ≤ i ≤ j + l of Fin (n + 1).

theorem SimplexCategory.const_subinterval_eq {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin (l + 1)) : CategoryTheory.CategoryStruct.comp ((mk 0).const (mk l) i) (subinterval j l hjl) = (mk 0).const (mk n) ⟨j + ↑i, ⋯⟩

@[simp]

theorem SimplexCategory.mkOfSucc_subinterval_eq {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin l) : CategoryTheory.CategoryStruct.comp (mkOfSucc i) (subinterval j l hjl) = mkOfSucc ⟨j + ↑i, ⋯⟩

@[simp]

theorem SimplexCategory.diag_subinterval_eq {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) : CategoryTheory.CategoryStruct.comp (diag l) (subinterval j l hjl) = intervalEdge j l hjl

instance SimplexCategory.instSubsingletonHomMkOfNatNat (Δ : SimplexCategory) : Subsingleton (Δ ⟶ mk 0)

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

@[simp]

theorem SimplexCategory.eqToHom_toOrderHom {x y : SimplexCategory} (h : x = y) : Hom.toOrderHom (CategoryTheory.eqToHom h) = (Fin.castOrderIso ⋯).toOrderEmbedding.toOrderHom

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

The i-th face map from ⦋n⦌ to ⦋n+1⦌

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

The i-th degeneracy map from ⦋n+1⦌ to ⦋n⦌

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

The generic case of the first simplicial identity

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

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

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

The special case of the first simplicial identity

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

The special case of the first simplicial identity

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

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

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

The second simplicial identity

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

The second simplicial identity

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

The first part of the third simplicial identity

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

The first part of the third simplicial identity

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

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

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

The second part of the third simplicial identity

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

The second part of the third simplicial identity

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

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

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

The fourth simplicial identity

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

The fourth simplicial identity

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

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

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

The fifth simplicial identity

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

The fifth simplicial identity

theorem SimplexCategory.δ_zero_eq_const : δ 0 = (mk 0).const (mk (0 + 1)) 1

theorem SimplexCategory.δ_one_eq_const : δ 1 = (mk 0).const (mk (0 + 1)) 0

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

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

theorem SimplexCategory.factor_δ_spec {m n : ℕ} (f : mk m ⟶ mk (n + 1)) (j : Fin (n + 2)) (hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ j) : CategoryTheory.CategoryStruct.comp (factor_δ f j) (δ j) = f

@[simp]

theorem SimplexCategory.δ_zero_mkOfSucc {n : ℕ} (i : Fin n) : CategoryTheory.CategoryStruct.comp (δ 0) (mkOfSucc i) = (mk 0).const (mk n) i.succ

@[simp]

theorem SimplexCategory.δ_one_mkOfSucc {n : ℕ} (i : Fin n) : CategoryTheory.CategoryStruct.comp (δ 1) (mkOfSucc i) = (mk 0).const (mk n) i.castSucc

theorem SimplexCategory.mkOfSucc_δ_lt {n : ℕ} {i : Fin n} {j : Fin (n + 2)} (h : i.succ.castSucc < j) : CategoryTheory.CategoryStruct.comp (mkOfSucc i) (δ j) = mkOfSucc i.castSucc

If i + 1 < j, mkOfSucc i ≫ δ j is the morphism ⦋1⦌ ⟶ ⦋n⦌ that sends 0 and 1 to i and i + 1, respectively.

theorem SimplexCategory.mkOfSucc_δ_gt {n : ℕ} {i : Fin n} {j : Fin (n + 2)} (h : j < i.succ.castSucc) : CategoryTheory.CategoryStruct.comp (mkOfSucc i) (δ j) = mkOfSucc i.succ

If i + 1 > j, mkOfSucc i ≫ δ j is the morphism ⦋1⦌ ⟶ ⦋n⦌ that sends 0 and 1 to i + 1 and i + 2, respectively.

theorem SimplexCategory.mkOfSucc_δ_eq {n : ℕ} {i : Fin n} {j : Fin (n + 2)} (h : j = i.succ.castSucc) : CategoryTheory.CategoryStruct.comp (mkOfSucc i) (δ j) = intervalEdge (↑i) 2 ⋯

If i + 1 = j, mkOfSucc i ≫ δ j is the morphism ⦋1⦌ ⟶ ⦋n⦌ that sends 0 and 1 to i and i + 2, respectively.

theorem SimplexCategory.mkOfSucc_one_eq_δ : mkOfSucc 1 = δ 0

theorem SimplexCategory.mkOfSucc_zero_eq_δ : mkOfSucc 0 = δ 2

theorem SimplexCategory.eq_of_one_to_two (f : mk 1 ⟶ mk 2) : (∃ (i : Fin (1 + 2)), f = δ i) ∨ ∃ (a : Fin ((mk 2).len + 1)), f = (mk 1).const (mk 2) a

theorem SimplexCategory.eq_of_one_to_two' (f : mk 1 ⟶ mk 2) : f = δ 0 ∨ f = δ 1 ∨ f = δ 2 ∨ ∃ (a : Fin ((mk 2).len + 1)), f = (mk 1).const (mk 2) a

def SimplexCategory.skeletalFunctor : CategoryTheory.Functor SimplexCategory NonemptyFinLinOrd

The functor that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

@[simp]

theorem SimplexCategory.skeletalFunctor_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : skeletalFunctor.map f = NonemptyFinLinOrd.ofHom (Hom.toOrderHom f)

@[simp]

theorem SimplexCategory.skeletalFunctor_obj (a : SimplexCategory) : skeletalFunctor.obj a = NonemptyFinLinOrd.of (Fin (a.len + 1))

theorem SimplexCategory.skeletalFunctor.coe_map {Δ₁ Δ₂ : SimplexCategory} (f : Δ₁ ⟶ Δ₂) : LinOrd.Hom.hom (skeletalFunctor.map f).hom = Hom.toOrderHom f

theorem SimplexCategory.skeletal : CategoryTheory.Skeletal SimplexCategory

instance SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor : skeletalFunctor.Full

instance SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor : skeletalFunctor.Faithful

instance SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor : skeletalFunctor.EssSurj

instance SimplexCategory.SkeletalFunctor.isEquivalence : skeletalFunctor.IsEquivalence

noncomputable def SimplexCategory.skeletalEquivalence : SimplexCategory ≌ NonemptyFinLinOrd

The equivalence that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

theorem SimplexCategory.isSkeletonOf : CategoryTheory.IsSkeletonOf NonemptyFinLinOrd SimplexCategory skeletalFunctor

SimplexCategory is a skeleton of NonemptyFinLinOrd.

@[implicit_reducible]

instance SimplexCategory.instConcreteCategoryOrderHomFinHAddNatLenOfNat : CategoryTheory.ConcreteCategory SimplexCategory fun (i j : SimplexCategory) => Fin (i.len + 1) →o Fin (j.len + 1)

@[implicit_reducible]

instance SimplexCategory.instFintypeToTypeOrderHomFinHAddNatLenOfNat (x : SimplexCategory) : Fintype (CategoryTheory.ToType x)

@[implicit_reducible]

instance SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat (x : SimplexCategory) (n : ℕ) : OfNat (CategoryTheory.ToType x) n

theorem SimplexCategory.toType_apply (x : SimplexCategory) : CategoryTheory.ToType x = Fin (x.len + 1)

@[simp]

theorem SimplexCategory.concreteCategoryHom_id (n : SimplexCategory) : CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id n) = OrderHom.id

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

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

theorem SimplexCategory.epi_iff_surjective {n m : SimplexCategory} {f : n ⟶ m} : CategoryTheory.Epi f ↔ Function.Surjective ⇑(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 y : SimplexCategory} (f : x ⟶ y) [CategoryTheory.Mono f] : x.len ≤ y.len

A monomorphism in SimplexCategory must increase lengths

theorem SimplexCategory.le_of_mono {n m : ℕ} (f : mk n ⟶ mk m) [CategoryTheory.Mono f] : n ≤ m

theorem SimplexCategory.len_le_of_epi {x y : SimplexCategory} (f : x ⟶ y) [CategoryTheory.Epi f] : y.len ≤ x.len

An epimorphism in SimplexCategory must decrease lengths

theorem SimplexCategory.le_of_epi {n m : ℕ} (f : mk n ⟶ mk m) [CategoryTheory.Epi f] : m ≤ n

theorem SimplexCategory.len_eq_of_isIso {x y : SimplexCategory} (f : x ⟶ y) [CategoryTheory.IsIso f] : x.len = y.len

theorem SimplexCategory.eq_of_isIso {n m : ℕ} (f : mk n ⟶ mk m) [CategoryTheory.IsIso f] : n = m

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

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

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

theorem SimplexCategory.isIso_iff_of_mono {n m : SimplexCategory} (f : n ⟶ m) [hf : CategoryTheory.Mono f] : CategoryTheory.IsIso f ↔ n.len = m.len

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

theorem SimplexCategory.isIso_iff_of_epi {n m : SimplexCategory} (f : n ⟶ m) [hf : CategoryTheory.Epi f] : CategoryTheory.IsIso f ↔ n.len = m.len

instance SimplexCategory.instBalanced : CategoryTheory.Balanced SimplexCategory

def SimplexCategory.orderIsoOfIso {x y : SimplexCategory} (e : x ≅ y) : Fin (x.len + 1) ≃o Fin (y.len + 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} (θ : mk (n + 1) ⟶ Δ') (i : Fin (n + 1)) (hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ) : ∃ (θ' : mk n ⟶ Δ'), θ = CategoryTheory.CategoryStruct.comp (σ i) θ'

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

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

theorem SimplexCategory.eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1)) (hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)) : ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ mk n), θ = CategoryTheory.CategoryStruct.comp θ' (δ 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 : ℕ} (θ : mk (n + 1) ⟶ mk n) [CategoryTheory.Epi θ] : ∃ (i : Fin (n + 1)), θ = σ i

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

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

instance SimplexCategory.instSplitEpiCategory : CategoryTheory.SplitEpiCategory SimplexCategory

instance SimplexCategory.instHasStrongEpiMonoFactorisations : CategoryTheory.Limits.HasStrongEpiMonoFactorisations SimplexCategory

instance SimplexCategory.instHasStrongEpiImages : CategoryTheory.Limits.HasStrongEpiImages SimplexCategory

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

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

theorem SimplexCategory.image_ι_eq {Δ Δ'' : 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} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e] {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = φ) : CategoryTheory.Limits.factorThruImage φ = e

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}

@[simp]

theorem SimplexCategory.toCat_obj (X : 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 (Fin (X.len + 1)))))))

@[simp]

theorem SimplexCategory.toCat_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : toCat.map f = ⋯.functor.toCatHom

theorem SimplexCategory.toCat.obj_eq_Fin (n : ℕ) : ↑(toCat.obj (mk n)) = Fin (n + 1)

@[implicit_reducible]

instance SimplexCategory.uniqueHomToZero {Δ : SimplexCategory} : Unique (Δ ⟶ mk 0)

def SimplexCategory.isTerminalZero : CategoryTheory.Limits.IsTerminal (mk 0)

The object ⦋0⦌ is terminal in SimplexCategory.

instance SimplexCategory.instHasTerminal : CategoryTheory.Limits.HasTerminal SimplexCategory

noncomputable def SimplexCategory.topIsoZero : ⊤_ SimplexCategory ≅ mk 0

The isomorphism between the terminal object in SimplexCategory and ⦋0⦌.

theorem SimplexCategory.δ_injective {n : ℕ} : Function.Injective δ

theorem SimplexCategory.σ_injective {n : ℕ} : Function.Injective σ