Basic properties of the simplex category

In Mathlib.AlgebraicTopology.SimplexCategory.Defs, 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.

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

The constant morphism from ⦋0⦌.

Equations

• x.const y i = SimplexCategory.Hom.mk { toFun := fun (x : Fin (x.len + 1)) => i, monotone' := ⋯ }

@[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.

Equations

• SimplexCategory.mkHom f = SimplexCategory.Hom.mk f

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

Equations

• SimplexCategory.mkOfLe i j h = SimplexCategory.mkHom { toFun := fun (x : Fin (1 + 1)) => match x with | 0 => i | 1 => j, monotone' := ⋯ }

@[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

Equations

• SimplexCategory.diag n = SimplexCategory.mkOfLe 0 ↑n ⋯

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.

Equations

• SimplexCategory.intervalEdge j l hjl = SimplexCategory.mkOfLe ⟨j, ⋯⟩ ⟨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).

Equations

• SimplexCategory.mkOfSucc i = SimplexCategory.mkHom { toFun := fun (x : Fin (1 + 1)) => match x with | 0 => i.castSucc | 1 => i.succ, monotone' := ⋯ }

@[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

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

Equations

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

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

Equations

• SimplexCategory.subinterval j l hjl = SimplexCategory.mkHom { toFun := fun (i : Fin (l + 1)) => ⟨↑i + j, ⋯⟩, monotone' := ⋯ }

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)

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⦌

Equations

• SimplexCategory.δ i = SimplexCategory.mkHom i.succAboveOrderEmb.toOrderHom

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

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

Equations

• SimplexCategory.σ i = SimplexCategory.mkHom { toFun := i.predAbove, monotone' := ⋯ }

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)

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)

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

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

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)

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)

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

Equations

• SimplexCategory.factor_δ f j = CategoryTheory.CategoryStruct.comp f (SimplexCategory.σ (Fin.predAbove 0 j))

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

Equations

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

@[simp]

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

@[simp]

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

theorem SimplexCategory.skeletalFunctor.coe_map {Δ₁ Δ₂ : SimplexCategory} (f : Δ₁ ⟶ Δ₂) : LinOrd.Hom.hom (skeletalFunctor.map f) = 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

Equations

• SimplexCategory.skeletalEquivalence = SimplexCategory.skeletalFunctor.asEquivalence

theorem SimplexCategory.isSkeletonOf : CategoryTheory.IsSkeletonOf NonemptyFinLinOrd SimplexCategory skeletalFunctor

SimplexCategory is a skeleton of NonemptyFinLinOrd.

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

Equations

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

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

Equations

• x.instFintypeToTypeOrderHomFinHAddNatLenOfNat = inferInstanceAs (Fintype (Fin (x.len + 1)))

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

Equations

• x.instOfNatToTypeOrderHomFinHAddNatLenOfNat n = inferInstanceAs (OfNat (Fin (x.len + 1)) n)

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

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

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

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

instance SimplexCategory.instReflectsIsomorphismsForget : (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

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.

Equations

• SimplexCategory.orderIsoOfIso e = { toFun := ⇑(SimplexCategory.Hom.toOrderHom e.hom), invFun := ⇑(SimplexCategory.Hom.toOrderHom e.inv), left_inv := ⋯, right_inv := ⋯ }.toOrderIso ⋯ ⋯

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 : Δ' ⟶ Δ) [hi : 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}

Equations

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

@[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