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)

Equations

• SimplexCategory = ℕ

def SimplexCategory.mk (n : ℕ) : SimplexCategory

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

Equations

• SimplexCategory.mk n = n

def Simplicial.«term[_]» : Lean.ParserDescr

the n-dimensional simplex can be denoted [n]

Equations

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

def SimplexCategory.len (n : SimplexCategory) : ℕ

The length of an object of SimplexCategory.

Equations

• SimplexCategory.len n = n

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.

Equations

• SimplexCategory.rec h n = h (SimplexCategory.len n)

@[irreducible]

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

Morphisms in the SimplexCategory.

Equations

• SimplexCategory.Hom a b = (Fin (SimplexCategory.len a + 1) →o Fin (SimplexCategory.len b + 1))

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 morphism in SimplexCategory from a monotone map of Fin's.

Equations

• SimplexCategory.Hom.mk f = f

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.

Equations

• SimplexCategory.Hom.toOrderHom f = f

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.

Equations

• SimplexCategory.Hom.id a = SimplexCategory.Hom.mk OrderHom.id

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.

Equations

• SimplexCategory.Hom.comp f g = SimplexCategory.Hom.mk (OrderHom.comp (SimplexCategory.Hom.toOrderHom f) (SimplexCategory.Hom.toOrderHom g))

instance SimplexCategory.smallCategory : CategoryTheory.SmallCategory SimplexCategory

Equations

• SimplexCategory.smallCategory = CategoryTheory.Category.mk @SimplexCategory.smallCategory.proof_1 @SimplexCategory.smallCategory.proof_2 @SimplexCategory.smallCategory.proof_3

@[simp]

theorem SimplexCategory.id_toOrderHom (a : SimplexCategory) : SimplexCategory.Hom.toOrderHom (CategoryTheory.CategoryStruct.id a) = OrderHom.id

@[simp]

theorem SimplexCategory.comp_toOrderHom {a : SimplexCategory} {b : SimplexCategory} {c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c) : SimplexCategory.Hom.toOrderHom (CategoryTheory.CategoryStruct.comp f g) = OrderHom.comp (SimplexCategory.Hom.toOrderHom g) (SimplexCategory.Hom.toOrderHom f)

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) (y : SimplexCategory) (i : Fin (SimplexCategory.len y + 1)) : x ⟶ y

The constant morphism from [0].

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem SimplexCategory.const_comp (x : SimplexCategory) {y : SimplexCategory} {z : SimplexCategory} (f : y ⟶ z) (i : Fin (SimplexCategory.len y + 1)) : CategoryTheory.CategoryStruct.comp (SimplexCategory.const x y i) f = SimplexCategory.const x z ((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.

Equations

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

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]

Equations

• SimplexCategory.δ i = SimplexCategory.mkHom (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))

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

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

Equations

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

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 ⋯)) (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 ⋯)) (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 ⋯)) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.pred i ⋯)) 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 ⋯)) (SimplexCategory.δ (Fin.pred i ⋯))

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

def SimplexCategory.factor_δ {m : ℕ} {n : ℕ} (f : SimplexCategory.mk m ⟶ SimplexCategory.mk (n + 1)) (j : Fin (n + 2)) : SimplexCategory.mk m ⟶ SimplexCategory.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 : SimplexCategory.mk m ⟶ SimplexCategory.mk (n + 1)) (j : Fin (n + 2)) (hj : ∀ (k : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f) k ≠ j) : CategoryTheory.CategoryStruct.comp (SimplexCategory.factor_δ f j) (SimplexCategory.δ j) = f

@[simp]

theorem SimplexCategory.skeletalFunctor_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.skeletalFunctor.map f = SimplexCategory.Hom.toOrderHom f

@[simp]

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

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.

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

theorem SimplexCategory.skeletal : CategoryTheory.Skeletal SimplexCategory

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

Equations

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

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

Equations

• SimplexCategory.SkeletalFunctor.instFaithfulSimplexCategorySmallCategoryNonemptyFinLinOrdInstNonemptyFinLinOrdLargeCategorySkeletalFunctor = ⋯

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

Equations

• SimplexCategory.SkeletalFunctor.instEssSurjSimplexCategoryNonemptyFinLinOrdSmallCategoryInstNonemptyFinLinOrdLargeCategorySkeletalFunctor = ⋯

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

Equations

• SimplexCategory.SkeletalFunctor.isEquivalence = CategoryTheory.Functor.IsEquivalence.ofFullyFaithfullyEssSurj SimplexCategory.skeletalFunctor

noncomputable def SimplexCategory.skeletalEquivalence : SimplexCategory ≌ NonemptyFinLinOrd

The equivalence that exhibits SimplexCategory as skeleton of NonemptyFinLinOrd

Equations

• SimplexCategory.skeletalEquivalence = CategoryTheory.Functor.asEquivalence SimplexCategory.skeletalFunctor

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

SimplexCategory is a skeleton of NonemptyFinLinOrd.

Equations

• SimplexCategory.isSkeletonOf = { skel := SimplexCategory.skeletal, eqv := SimplexCategory.SkeletalFunctor.isEquivalence }

def SimplexCategory.Truncated (n : ℕ) : Type

The truncated simplex category.

Equations

• SimplexCategory.Truncated n = CategoryTheory.FullSubcategory fun (a : SimplexCategory) => SimplexCategory.len a ≤ n

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

Equations

• SimplexCategory.instSmallCategoryTruncated n = CategoryTheory.FullSubcategory.category fun (a : SimplexCategory) => SimplexCategory.len a ≤ n

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

Equations

• SimplexCategory.Truncated.instInhabitedTruncated = { default := { obj := SimplexCategory.mk 0, property := ⋯ } }

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.

Equations

• SimplexCategory.Truncated.inclusion = CategoryTheory.fullSubcategoryInclusion fun (a : SimplexCategory) => SimplexCategory.len a ≤ n

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

Equations

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

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

Equations

• ⋯ = ⋯

instance SimplexCategory.instConcreteCategorySimplexCategorySmallCategory : CategoryTheory.ConcreteCategory SimplexCategory

Equations

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

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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• SimplexCategory.instReflectsIsomorphismsSimplexCategorySmallCategoryTypeTypesForgetInstConcreteCategorySimplexCategorySmallCategory = ⋯

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.

Equations

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

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)) : ∃ (θ' : SimplexCategory.mk n ⟶ Δ'), θ = 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 : Fin (n + 1)) (θ' : SimplexCategory.mk n ⟶ Δ'), θ = 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) : ∃ (θ' : Δ ⟶ SimplexCategory.mk n), θ = 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 : Fin (n + 2)) (θ' : Δ ⟶ SimplexCategory.mk n), θ = 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 : Fin (n + 1)), θ = SimplexCategory.σ i

theorem SimplexCategory.eq_δ_of_mono {n : ℕ} (θ : SimplexCategory.mk n ⟶ SimplexCategory.mk (n + 1)) [CategoryTheory.Mono θ] : ∃ (i : Fin (n + 2)), θ = 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

Equations

• SimplexCategory.instSplitEpiCategorySimplexCategorySmallCategory = ⋯

instance SimplexCategory.instHasStrongEpiMonoFactorisationsSimplexCategorySmallCategory : CategoryTheory.Limits.HasStrongEpiMonoFactorisations SimplexCategory

Equations

• SimplexCategory.instHasStrongEpiMonoFactorisationsSimplexCategorySmallCategory = ⋯

instance SimplexCategory.instHasStrongEpiImagesSimplexCategorySmallCategoryHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisationsSimplexCategorySmallCategory : CategoryTheory.Limits.HasStrongEpiImages SimplexCategory

Equations

• SimplexCategory.instHasStrongEpiImagesSimplexCategorySmallCategoryHasImages_of_hasStrongEpiMonoFactorisationsInstHasStrongEpiMonoFactorisationsSimplexCategorySmallCategory = ⋯

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

Equations

• ⋯ = ⋯

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_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.toCat.map f = Monotone.functor ⋯

@[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 (Fin (SimplexCategory.len X + 1)))))))

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.