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

• n.len = n

theorem SimplexCategory.ext (a b : SimplexCategory) : a.len = b.len → a = b

@[simp]

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

@[simp]

theorem SimplexCategory.mk_len (n : SimplexCategory) : SimplexCategory.mk n.len = 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 n.len

@[irreducible]

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

Morphisms in the SimplexCategory.

Equations

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

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

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

Equations

• SimplexCategory.Hom.mk f = f

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

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

Equations

• f.toOrderHom = f

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

@[simp]

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

@[simp]

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

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

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

Identity morphisms of SimplexCategory.

Equations

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

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

Composition of morphisms of SimplexCategory.

Equations

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

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 b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c) : SimplexCategory.Hom.toOrderHom (CategoryTheory.CategoryStruct.comp f g) = (SimplexCategory.Hom.toOrderHom g).comp (SimplexCategory.Hom.toOrderHom f)

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

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 : (SimplexCategory.mk 0).const (SimplexCategory.mk 0) 0 = CategoryTheory.CategoryStruct.id (SimplexCategory.mk 0)

@[simp]

theorem SimplexCategory.const_apply (x y : SimplexCategory) (i : Fin (y.len + 1)) (a : Fin (x.len + 1)) : (SimplexCategory.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 ((SimplexCategory.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 (SimplexCategory.mk 0) 0) ((SimplexCategory.mk 0).const m i)

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

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

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

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

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

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

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

def SimplexCategory.mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) : SimplexCategory.mk 1 ⟶ SimplexCategory.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' := ⋯ }

def SimplexCategory.diag (n : ℕ) : SimplexCategory.mk 1 ⟶ SimplexCategory.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) : SimplexCategory.mk 1 ⟶ SimplexCategory.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) : SimplexCategory.mk 1 ⟶ SimplexCategory.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) : (SimplexCategory.Hom.toOrderHom (SimplexCategory.mkOfSucc i)) 0 = i.castSucc

@[simp]

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

def SimplexCategory.mkOfLeComp {n : ℕ} (i j k : Fin (n + 1)) (h₁ : i ≤ j) (h₂ : j ≤ k) : SimplexCategory.mk 2 ⟶ SimplexCategory.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) : SimplexCategory.mk l ⟶ SimplexCategory.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 ((SimplexCategory.mk 0).const (SimplexCategory.mk l) i) (SimplexCategory.subinterval j l hjl) = (SimplexCategory.mk 0).const (SimplexCategory.mk n) ⟨j + ↑i, ⋯⟩

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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 i.succAboveOrderEmb.toOrderHom

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 := i.predAbove, monotone' := ⋯ }

theorem SimplexCategory.δ_comp_δ {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ j.succ) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ j) (SimplexCategory.δ 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 (SimplexCategory.δ i) (SimplexCategory.δ j) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (j.pred ⋯)) (SimplexCategory.δ i.castSucc)

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

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

The special case of the first simplicial identity

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.δ i.castSucc) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) h)

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

theorem SimplexCategory.δ_comp_δ_self'_assoc {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) {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.δ i.succ) h)

theorem SimplexCategory.δ_comp_σ_of_le {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc) (SimplexCategory.σ j.succ) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ 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 : SimplexCategory.mk (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j.succ) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) h)

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

The first part of the third simplicial identity

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

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

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

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

The second part of the third simplicial identity

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

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

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

theorem SimplexCategory.δ_comp_σ_of_gt {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) (SimplexCategory.σ j.castSucc) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (SimplexCategory.δ 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 : SimplexCategory.mk (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.succ) (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j.castSucc) h) = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) h)

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

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

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

The fifth simplicial identity

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

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.δ_zero_mkOfSucc {n : ℕ} (i : Fin n) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0) (SimplexCategory.mkOfSucc i) = (SimplexCategory.mk 0).const (SimplexCategory.mk n) i.succ

@[simp]

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

theorem SimplexCategory.eq_of_one_to_two (f : SimplexCategory.mk 1 ⟶ SimplexCategory.mk 2) : f = SimplexCategory.δ 0 ∨ f = SimplexCategory.δ 1 ∨ f = SimplexCategory.δ 2 ∨ ∃ (a : Fin ((SimplexCategory.mk 2).len + 1)), f = (SimplexCategory.mk 1).const (SimplexCategory.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_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 (a.len + 1))

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

theorem SimplexCategory.skeletal : CategoryTheory.Skeletal SimplexCategory

instance SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor : SimplexCategory.skeletalFunctor.Full

Equations

• SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor = ⋯

instance SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor : SimplexCategory.skeletalFunctor.Faithful

Equations

• SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor = ⋯

instance SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor : SimplexCategory.skeletalFunctor.EssSurj

Equations

• SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor = ⋯

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

Equations

• SimplexCategory.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 SimplexCategory.skeletalFunctor

SimplexCategory is a skeleton of NonemptyFinLinOrd.

def SimplexCategory.Truncated (n : ℕ) : Type

The truncated simplex category.

Equations

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

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

Equations

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

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

Equations

• SimplexCategory.Truncated.instInhabited = { 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) => a.len ≤ n

instance SimplexCategory.Truncated.instFullInclusion (n : ℕ) : SimplexCategory.Truncated.inclusion.Full

Equations

• ⋯ = ⋯

instance SimplexCategory.Truncated.instFaithfulInclusion (n : ℕ) : SimplexCategory.Truncated.inclusion.Faithful

Equations

• ⋯ = ⋯

noncomputable def SimplexCategory.Truncated.inclusion.fullyFaithful (n : ℕ) : SimplexCategory.Truncated.inclusion.op.FullyFaithful

A proof that the full subcategory inclusion is fully faithful.

Equations

• SimplexCategory.Truncated.inclusion.fullyFaithful n = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful SimplexCategory.Truncated.inclusion.op

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

instance SimplexCategory.instConcreteCategory : CategoryTheory.ConcreteCategory SimplexCategory

Equations

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

theorem SimplexCategory.mono_iff_injective {n 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 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 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 : SimplexCategory.mk n ⟶ SimplexCategory.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 : SimplexCategory.mk n ⟶ SimplexCategory.mk m} : CategoryTheory.Epi f → m ≤ n

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• SimplexCategory.instReflectsIsomorphismsForget = ⋯

theorem SimplexCategory.isIso_of_bijective {x y : SimplexCategory} {f : x ⟶ y} (hf : Function.Bijective (SimplexCategory.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} (θ : SimplexCategory.mk (n + 1) ⟶ Δ') (i : Fin (n + 1)) (hi : (SimplexCategory.Hom.toOrderHom θ) i.castSucc = (SimplexCategory.Hom.toOrderHom θ) i.succ) : ∃ (θ' : 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 (Δ.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} (i : Δ' ⟶ Δ) [hi : CategoryTheory.Mono i] (hi' : Δ ≠ Δ') : Δ'.len < Δ.len

noncomputable instance SimplexCategory.instSplitEpiCategory : CategoryTheory.SplitEpiCategory SimplexCategory

Equations

• SimplexCategory.instSplitEpiCategory = ⋯

instance SimplexCategory.instHasStrongEpiMonoFactorisations : CategoryTheory.Limits.HasStrongEpiMonoFactorisations SimplexCategory

Equations

• SimplexCategory.instHasStrongEpiMonoFactorisations = ⋯

instance SimplexCategory.instHasStrongEpiImages : CategoryTheory.Limits.HasStrongEpiImages SimplexCategory

Equations

• SimplexCategory.instHasStrongEpiImages = ⋯

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

Equations

• ⋯ = ⋯

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_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : SimplexCategory.toCat.map f = ⋯.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 (X.len + 1)))))))