Presentation of the simplex category by generators and relations.

We introduce SimplexCategoryGenRel as the category presented by generating morphisms δ i : [n] ⟶ [n + 1] and σ i : [n + 1] ⟶ [n] and subject to the simplicial identities, and we provide induction principles for reasoning about objects and morphisms in this category.

This category admits a canonical functor toSimplexCategory to the usual simplex category. The fact that this functor is an equivalence will be recorded in a separate file.

def FreeSimplexQuiver : Type

The objects of the free simplex quiver are the natural numbers.

Equations

• FreeSimplexQuiver = ℕ

def FreeSimplexQuiver.mk (n : ℕ) : FreeSimplexQuiver

Making an object of FreeSimplexQuiver out of a natural number.

Equations

• FreeSimplexQuiver.mk n = n

def FreeSimplexQuiver.len (x : FreeSimplexQuiver) : ℕ

Getting back the natural number from the objects.

Equations

• x.len = x

inductive FreeSimplexQuiver.Hom : FreeSimplexQuiver → FreeSimplexQuiver → Type

A morphism in FreeSimplexQuiver is either a face map (δ) or a degeneracy map (σ).

• δ {n : ℕ} (i : Fin (n + 2)) : (mk n).Hom (mk (n + 1))
• σ {n : ℕ} (i : Fin (n + 1)) : (mk (n + 1)).Hom (mk n)

instance FreeSimplexQuiver.quiv : Quiver FreeSimplexQuiver

Equations

• FreeSimplexQuiver.quiv = { Hom := FreeSimplexQuiver.Hom }

@[reducible, inline]

abbrev FreeSimplexQuiver.δ {n : ℕ} (i : Fin (n + 2)) : mk n ⟶ mk (n + 1)

FreeSimplexQuiver.δ i represents the i-th face map .mk n ⟶ .mk (n + 1).

Equations

• FreeSimplexQuiver.δ i = FreeSimplexQuiver.Hom.δ i

@[reducible, inline]

abbrev FreeSimplexQuiver.σ {n : ℕ} (i : Fin (n + 1)) : mk (n + 1) ⟶ mk n

FreeSimplexQuiver.σ i represents i-th degeneracy map .mk (n + 1) ⟶ .mk n.

Equations

• FreeSimplexQuiver.σ i = FreeSimplexQuiver.Hom.σ i

inductive FreeSimplexQuiver.homRel : HomRel (CategoryTheory.Paths FreeSimplexQuiver)

FreeSimplexQuiver.homRel is the relation on morphisms freely generated on the five simplicial identities.

• δ_comp_δ {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) : homRel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (δ i)) (CategoryTheory.Paths.of.map (δ j.succ))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (δ j)) (CategoryTheory.Paths.of.map (δ i.castSucc)))
• δ_comp_σ_of_le {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) : homRel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (δ i.castSucc)) (CategoryTheory.Paths.of.map (σ j.succ))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (σ j)) (CategoryTheory.Paths.of.map (δ i)))
• δ_comp_σ_self {n : ℕ} {i : Fin (n + 1)} : homRel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (δ i.castSucc)) (CategoryTheory.Paths.of.map (σ i))) (CategoryTheory.CategoryStruct.id (CategoryTheory.Paths.of.obj (mk n)))
• δ_comp_σ_succ {n : ℕ} {i : Fin (n + 1)} : homRel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (δ i.succ)) (CategoryTheory.Paths.of.map (σ i))) (CategoryTheory.CategoryStruct.id (CategoryTheory.Paths.of.obj (mk n)))
• δ_comp_σ_of_gt {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) : homRel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (δ i.succ)) (CategoryTheory.Paths.of.map (σ j.castSucc))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (σ j)) (CategoryTheory.Paths.of.map (δ i)))
• σ_comp_σ {n : ℕ} {i j : Fin (n + 1)} (H : i ≤ j) : homRel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (σ i.castSucc)) (CategoryTheory.Paths.of.map (σ j))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Paths.of.map (σ j.succ)) (CategoryTheory.Paths.of.map (σ i)))

def SimplexCategoryGenRel : Type

SimplexCategory is the category presented by generators and relation by the simplicial identities.

Equations

• SimplexCategoryGenRel = CategoryTheory.Quotient FreeSimplexQuiver.homRel

instance instSimplexCategoryGenRelCategory : CategoryTheory.Category.{0, 0} SimplexCategoryGenRel

Equations

• instSimplexCategoryGenRelCategory = CategoryTheory.Quotient.category FreeSimplexQuiver.homRel

def SimplexCategoryGenRel.mk (n : ℕ) : SimplexCategoryGenRel

SimplexCategoryGenRel.mk is the main constructor for objects of SimplexCategoryGenRel.

Equations

• SimplexCategoryGenRel.mk n = { as := CategoryTheory.Paths.of.obj n }

@[reducible, inline]

abbrev SimplexCategoryGenRel.δ {n : ℕ} (i : Fin (n + 2)) : mk n ⟶ mk (n + 1)

SimplexCategoryGenRel.δ i is the i-th face map .mk n ⟶ .mk (n + 1).

Equations

• SimplexCategoryGenRel.δ i = (CategoryTheory.Quotient.functor FreeSimplexQuiver.homRel).map (CategoryTheory.Paths.of.map (FreeSimplexQuiver.Hom.δ i))

@[reducible, inline]

abbrev SimplexCategoryGenRel.σ {n : ℕ} (i : Fin (n + 1)) : mk (n + 1) ⟶ mk n

SimplexCategoryGenRel.σ i is the i-th degeneracy map .mk (n + 1) ⟶ .mk n.

Equations

• SimplexCategoryGenRel.σ i = (CategoryTheory.Quotient.functor FreeSimplexQuiver.homRel).map (CategoryTheory.Paths.of.map (FreeSimplexQuiver.Hom.σ i))

def SimplexCategoryGenRel.len (x : SimplexCategoryGenRel) : ℕ

The length of an object of SimplexCategoryGenRel.

Equations

• x.len = CategoryTheory.Quotient.casesOn x fun (n : CategoryTheory.Paths FreeSimplexQuiver) => n

@[simp]

theorem SimplexCategoryGenRel.mk_len (n : ℕ) : (mk n).len = n

inductive SimplexCategoryGenRel.faces : CategoryTheory.MorphismProperty SimplexCategoryGenRel

A morphism is called a face if it is a δ i for some i : Fin (n + 2).

• δ {n : ℕ} (i : Fin (n + 2)) : faces (SimplexCategoryGenRel.δ i)

inductive SimplexCategoryGenRel.degeneracies : CategoryTheory.MorphismProperty SimplexCategoryGenRel

A morphism is called a degeneracy if it is a σ i for some i : Fin (n + 1).

• σ {n : ℕ} (i : Fin (n + 1)) : degeneracies (SimplexCategoryGenRel.σ i)

@[reducible, inline]

abbrev SimplexCategoryGenRel.generators : CategoryTheory.MorphismProperty SimplexCategoryGenRel

A morphism is a generator if it is either a face or a degeneracy.

Equations

• SimplexCategoryGenRel.generators = SimplexCategoryGenRel.faces ⊔ SimplexCategoryGenRel.degeneracies

theorem SimplexCategoryGenRel.generators.δ {n : ℕ} (i : Fin (n + 2)) : generators (SimplexCategoryGenRel.δ i)

theorem SimplexCategoryGenRel.generators.σ {n : ℕ} (i : Fin (n + 1)) : generators (SimplexCategoryGenRel.σ i)

theorem SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top : generators.multiplicativeClosure = ⊤

A property is true for every morphism iff it holds for generators and is multiplicative.

theorem SimplexCategoryGenRel.hom_induction (P : CategoryTheory.MorphismProperty SimplexCategoryGenRel) (id : ∀ {n : ℕ}, P (CategoryTheory.CategoryStruct.id (mk n))) (comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (CategoryTheory.CategoryStruct.comp u (δ i))) (comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (CategoryTheory.CategoryStruct.comp u (σ i))) {a b : SimplexCategoryGenRel} (f : a ⟶ b) : P f

An unrolled version of the induction principle obtained in the previous lemma.

theorem SimplexCategoryGenRel.hom_induction' (P : CategoryTheory.MorphismProperty SimplexCategoryGenRel) (id : ∀ {n : ℕ}, P (CategoryTheory.CategoryStruct.id (mk n))) (δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (CategoryTheory.CategoryStruct.comp (δ i) u)) (σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (CategoryTheory.CategoryStruct.comp (σ i) u)) {a b : SimplexCategoryGenRel} (f : a ⟶ b) : P f

An induction principle for reasonning about morphisms in SimplexCategoryGenRel, where we compose with generators on the right.

def SimplexCategoryGenRel.rec {P : SimplexCategoryGenRel → Sort u_1} (H : (n : ℕ) → P (mk n)) (x : SimplexCategoryGenRel) : P x

An induction principle for reasonning about objects in SimplexCategoryGenRel. This should be used instead of identifying an object with mk of its len.

Equations

• SimplexCategoryGenRel.rec H x = H x.len

theorem SimplexCategoryGenRel.ext {x y : SimplexCategoryGenRel} (h : x.len = y.len) : x = y

A basic ext lemma for objects of SimplexCategoryGenRel.

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

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

theorem SimplexCategoryGenRel.δ_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)

theorem SimplexCategoryGenRel.δ_comp_σ_of_le_assoc {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) {Z : SimplexCategoryGenRel} (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 SimplexCategoryGenRel.δ_comp_σ_self {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.CategoryStruct.comp (δ i.castSucc) (σ i) = CategoryTheory.CategoryStruct.id (mk n)

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

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

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

theorem SimplexCategoryGenRel.δ_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)

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

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

theorem SimplexCategoryGenRel.δ_comp_δ_nat {n : ℕ} (i j : ℕ) (hi : i < n + 2) (hj : j < n + 2) (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (δ ⟨i, hi⟩) (δ ⟨j + 1, ⋯⟩) = CategoryTheory.CategoryStruct.comp (δ ⟨j, hj⟩) (δ ⟨i, ⋯⟩)

A version of δ_comp_δ with indices in ℕ satisfying relevant inequalities.

theorem SimplexCategoryGenRel.σ_comp_σ_nat {n : ℕ} (i j : ℕ) (hi : i < n + 1) (hj : j < n + 1) (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (σ ⟨i, ⋯⟩) (σ ⟨j, hj⟩) = CategoryTheory.CategoryStruct.comp (σ ⟨j + 1, ⋯⟩) (σ ⟨i, hi⟩)

A version of σ_comp_σ with indices in ℕ satisfying relevant inequalities.

def SimplexCategoryGenRel.toSimplexCategory : CategoryTheory.Functor SimplexCategoryGenRel SimplexCategory

The canonical functor from SimplexCategoryGenRel to SimplexCategory, which exists as the simplicial identities hold in SimplexCategory.

Equations

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

@[simp]

theorem SimplexCategoryGenRel.toSimplexCategory_obj_mk (n : ℕ) : toSimplexCategory.obj (mk n) = SimplexCategory.mk n

@[simp]

theorem SimplexCategoryGenRel.toSimplexCategory_map_δ {n : ℕ} (i : Fin (n + 2)) : toSimplexCategory.map (δ i) = SimplexCategory.δ i

@[simp]

theorem SimplexCategoryGenRel.toSimplexCategory_map_σ {n : ℕ} (i : Fin (n + 1)) : toSimplexCategory.map (σ i) = SimplexCategory.σ i

@[simp]

theorem SimplexCategoryGenRel.toSimplexCategory_len {x : SimplexCategoryGenRel} : (toSimplexCategory.obj x).len = x.len