Normal forms for morphisms in SimplexCategoryGenRel.

In this file, we establish that P_δ and P_σ morphisms in SimplexCategoryGenRel each admits a normal form.

In both cases, the normal forms are encoded as an integer m, and a strictly increasing list of integers [i₀,…,iₙ] such that iₖ ≤ m + k for all k. We define a predicate isAdmissible m : List ℕ → Prop encoding this property. And provide some lemmas to help work with such lists.

Normal forms for P_σ morphisms are encoded by m-admissible lists, in which case the list [i₀,…,iₙ] represents the morphism σ iₙ ≫ ⋯ ≫ σ i₀ : .mk (m + n) ⟶ .mk n.

Normal forms for P_δ morphisms are encoded by (m + 1)-admissible lists, in which case the list [i₀,…,iₙ] represents the morphism δ i₀ ≫ ⋯ ≫ δ iₙ : .mk n ⟶ .mk (m + n).

The results in this file are to be treated as implementation-only, and they only serve as stepping stones towards proving that the canonical functor toSimplexCategory : SimplexCategoryGenRel ⥤ SimplexCategory is an equivalence.

References:

• Kerodon Tag 04FQ
• Kerodon Tag 04FT

TODOs:

• Show that every P_δ admits a unique normal form.

inductive SimplexCategoryGenRel.IsAdmissible (m : ℕ) (L : List ℕ) : Prop

A list of natural numbers [i₀, ⋯, iₙ] is said to be m-admissible (for m : ℕ) if i₀ < ⋯ < iₙ and iₖ ≤ m + k for all k. This would suggest the definition L.IsChain (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k. However, we instead define IsAdmissible inductively and show, in isAdmissible_iff_isChain_and_le, that this is equivalent to the non-inductive definition.

• nil (m : ℕ) : IsAdmissible m []
• singleton {m a : ℕ} (ha : a ≤ m) : IsAdmissible m [a]
• cons_cons {m a b : ℕ} {L' : List ℕ} (hab : a < b) (hbL : IsAdmissible (m + 1) (b :: L')) (ha : a ≤ m) : IsAdmissible m (a :: b :: L')

theorem SimplexCategoryGenRel.isAdmissible_iff (m : ℕ) (L : List ℕ) : IsAdmissible m L ↔ L = [] ∨ (∃ a ≤ m, L = [a]) ∨ ∃ (a : ℕ) (b : ℕ) (L' : List ℕ), a < b ∧ IsAdmissible (m + 1) (b :: L') ∧ a ≤ m ∧ L = a :: b :: L'

@[simp]

theorem SimplexCategoryGenRel.isAdmissible_singleton_iff {m a : ℕ} : IsAdmissible m [a] ↔ a ≤ m

@[simp]

theorem SimplexCategoryGenRel.isAdmissible_cons_cons_iff {m a b : ℕ} {L : List ℕ} : IsAdmissible m (a :: b :: L) ↔ a < b ∧ IsAdmissible (m + 1) (b :: L) ∧ a ≤ m

theorem SimplexCategoryGenRel.isAdmissible_cons_iff {m a : ℕ} {L : List ℕ} : IsAdmissible m (a :: L) ↔ a ≤ m ∧ (∀ (x : 0 < L.length), a < L[0]) ∧ IsAdmissible (m + 1) L

theorem SimplexCategoryGenRel.isAdmissible_iff_isChain_and_le {m : ℕ} {L : List ℕ} : IsAdmissible m L ↔ List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k

theorem SimplexCategoryGenRel.isAdmissible_iff_pairwise_and_le {m : ℕ} {L : List ℕ} : IsAdmissible m L ↔ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k

theorem SimplexCategoryGenRel.isAdmissible_of_isChain_of_forall_getElem_le {m : ℕ} {L : List ℕ} (hL : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) L) (hL₂ : ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k) : IsAdmissible m L

theorem SimplexCategoryGenRel.IsAdmissible.isChain {m : ℕ} {L : List ℕ} (hL : IsAdmissible m L) : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) L

theorem SimplexCategoryGenRel.IsAdmissible.le {m : ℕ} {L : List ℕ} (hL : IsAdmissible m L) (k : ℕ) (h : k < L.length) : L[k] ≤ m + k

theorem SimplexCategoryGenRel.IsAdmissible.of_cons {m a : ℕ} {L : List ℕ} (h : IsAdmissible m (a :: L)) : IsAdmissible (m + 1) L

The tail of an m-admissible list is (m+1)-admissible.

@[deprecated SimplexCategoryGenRel.IsAdmissible.of_cons (since := "2025-10-15")]

theorem SimplexCategoryGenRel.IsAdmissible.tail {m a : ℕ} {L : List ℕ} (h : IsAdmissible m (a :: L)) : IsAdmissible (m + 1) L

Alias of SimplexCategoryGenRel.IsAdmissible.of_cons.

---

The tail of an m-admissible list is (m+1)-admissible.

theorem SimplexCategoryGenRel.IsAdmissible.cons {m a : ℕ} {L : List ℕ} (hL : IsAdmissible (m + 1) L) (ha : a ≤ m) (ha' : ∀ (x : 0 < L.length), a < L[0]) : IsAdmissible m (a :: L)

theorem SimplexCategoryGenRel.IsAdmissible.pairwise {m : ℕ} {L : List ℕ} (hL : IsAdmissible m L) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) L

@[deprecated SimplexCategoryGenRel.IsAdmissible.pairwise (since := "2025-10-16")]

theorem SimplexCategoryGenRel.IsAdmissible.sorted {m : ℕ} {L : List ℕ} (hL : IsAdmissible m L) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) L

Alias of SimplexCategoryGenRel.IsAdmissible.pairwise.

theorem SimplexCategoryGenRel.IsAdmissible.head_lt {m a : ℕ} {L : List ℕ} (hL : IsAdmissible m (a :: L)) (a' : ℕ) : a' ∈ L → a < a'

If (a :: l) is m-admissible then a is less than all elements of l

theorem SimplexCategoryGenRel.IsAdmissible.getElem_lt {m : ℕ} {L : List ℕ} (hL : IsAdmissible m L) {k : ℕ} {hk : k < L.length} : L[k] < m + L.length

def SimplexCategoryGenRel.IsAdmissible.getElemAsFin {m : ℕ} {L : List ℕ} (hl : IsAdmissible m L) (k : ℕ) (hK : k < L.length) : Fin (m + k + 1)

An element of a m-admissible list, as an element of the appropriate Fin

Equations

• hl.getElemAsFin k hK = ⟨L[k], ⋯⟩

@[simp]

theorem SimplexCategoryGenRel.IsAdmissible.getElemAsFin_val {m : ℕ} {L : List ℕ} (hl : IsAdmissible m L) (k : ℕ) (hK : k < L.length) : ↑(hl.getElemAsFin k hK) = L[k]

def SimplexCategoryGenRel.IsAdmissible.head {m a : ℕ} {L : List ℕ} (hl : IsAdmissible m (a :: L)) : Fin (m + 1)

The head of an m-admissible list.

Equations

• hl.head = hl.getElemAsFin 0 ⋯

@[simp]

theorem SimplexCategoryGenRel.IsAdmissible.head_val {m a : ℕ} {L : List ℕ} (hl : IsAdmissible m (a :: L)) : ↑hl.head = a

theorem SimplexCategoryGenRel.IsAdmissible.mono {m : ℕ} {L : List ℕ} {n : ℕ} (hmn : m ≤ n) (hL : IsAdmissible m L) : IsAdmissible n L

def SimplexCategoryGenRel.simplicialInsert (a : ℕ) : List ℕ → List ℕ

The construction simplicialInsert describes inserting an element in a list of integer and moving it to its "right place" according to the simplicial relations. Somewhat miraculously, the algorithm is the same for the first or the fifth simplicial relations, making it "valid" when we treat the list as a normal form for a morphism satisfying P_δ, or for a morphism satisfying P_σ!

This is similar in nature to List.orderedInsert, but note that we increment one of the element every time we perform an exchange, making it a different construction.

Equations

• SimplexCategoryGenRel.simplicialInsert a [] = [a]
• SimplexCategoryGenRel.simplicialInsert a (b :: l) = if a < b then a :: b :: l else b :: SimplexCategoryGenRel.simplicialInsert (a + 1) l

theorem SimplexCategoryGenRel.simplicialInsert_length (a : ℕ) (L : List ℕ) : (simplicialInsert a L).length = L.length + 1

simplicialInsert just adds one to the length.

theorem SimplexCategoryGenRel.simplicialInsert_isAdmissible (m : ℕ) (L : List ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j ≤ m) : IsAdmissible m (simplicialInsert j L)

simplicialInsert preserves admissibility

def SimplexCategoryGenRel.standardσ (L : List ℕ) {m₁ m₂ : ℕ} (h : m₂ + L.length = m₁) : mk m₁ ⟶ mk m₂

Given a sequence L = [ i 0, ..., i b ], standardσ m L i is the morphism σ (i b) ≫ … ≫ σ (i 0). The construction is provided for any list of natural numbers, but it is intended to behave well only when the list is admissible.

Equations

• SimplexCategoryGenRel.standardσ [] h_2 = CategoryTheory.eqToHom ⋯
• SimplexCategoryGenRel.standardσ (a :: t) h_2 = CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ t ⋯) (SimplexCategoryGenRel.σ (Fin.ofNat (m₂ + 1) a))

@[simp]

theorem SimplexCategoryGenRel.standardσ_nil (m : ℕ) : standardσ [] ⋯ = CategoryTheory.CategoryStruct.id (mk m)

@[simp]

theorem SimplexCategoryGenRel.standardσ_cons (L : List ℕ) (a : ℕ) {m₁ m₂ : ℕ} (h : m₂ + (a :: L).length = m₁) : standardσ (a :: L) h = CategoryTheory.CategoryStruct.comp (standardσ L ⋯) (σ (Fin.ofNat (m₂ + 1) a))

theorem SimplexCategoryGenRel.standardσ_cons_assoc (L : List ℕ) (a : ℕ) {m₁ m₂ : ℕ} (h : m₂ + (a :: L).length = m₁) {Z : SimplexCategoryGenRel} (h✝ : mk m₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (standardσ (a :: L) h) h✝ = CategoryTheory.CategoryStruct.comp (standardσ L ⋯) (CategoryTheory.CategoryStruct.comp (σ (Fin.ofNat (m₂ + 1) a)) h✝)

theorem SimplexCategoryGenRel.standardσ_comp_standardσ (L₁ L₂ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + L₂.length = m₂) : CategoryTheory.CategoryStruct.comp (standardσ L₁ h) (standardσ L₂ h') = standardσ (L₂ ++ L₁) ⋯

theorem SimplexCategoryGenRel.standardσ_comp_standardσ_assoc (L₁ L₂ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + L₂.length = m₂) {Z : SimplexCategoryGenRel} (h✝ : mk m₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (standardσ L₁ h) (CategoryTheory.CategoryStruct.comp (standardσ L₂ h') h✝) = CategoryTheory.CategoryStruct.comp (standardσ (L₂ ++ L₁) ⋯) h✝

def SimplexCategoryGenRel.simplicialEvalσ (L : List ℕ) : ℕ → ℕ

simplicialEvalσ is a lift to ℕ of (toSimplexCategory.map (standardσ m L _ _)).toOrderHom. Rather than defining it as such, we define it inductively for less painful inductive reasoning, (see simplicialEvalσ_of_isAdmissible). It is expected to produce the correct result only if L is admissible, and values for non-admissible lists should be considered junk values. Similarly, values for out-of-bounds inputs are junk values.

Equations

• One or more equations did not get rendered due to their size.
• SimplexCategoryGenRel.simplicialEvalσ [] j = j

theorem SimplexCategoryGenRel.simplicialEvalσ_of_le_mem (L : List ℕ) (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) : simplicialEvalσ L j = j

@[deprecated SimplexCategoryGenRel.simplicialEvalσ_of_le_mem (since := "2025-10-16")]

theorem SimplexCategoryGenRel.simplicialEvalσ_of_lt_mem (L : List ℕ) (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) : simplicialEvalσ L j = j

Alias of SimplexCategoryGenRel.simplicialEvalσ_of_le_mem.

theorem SimplexCategoryGenRel.simplicialEvalσ_monotone (L : List ℕ) : Monotone (simplicialEvalσ L)

theorem SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible (L : List ℕ) (m₁ m₂ : ℕ) (hL : IsAdmissible m₂ L) (hk : m₂ + L.length = m₁) (j : ℕ) (hj : j < m₁ + 1) : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j

theorem SimplexCategoryGenRel.standardσ_simplicialInsert {m : ℕ} (L : List ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (m₁ : ℕ) (hm₁ : m + L.length + 1 = m₁) : standardσ (simplicialInsert j L) ⋯ = CategoryTheory.CategoryStruct.comp (standardσ L ⋯) (σ (Fin.ofNat (m + 1) j))

Performing a simplicial insertion in a list is the same as composition on the right by the corresponding degeneracy operator.

theorem SimplexCategoryGenRel.exists_normal_form_P_σ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf : P_σ f) : ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ f = standardσ L ⋯

Using standardσ_simplicialInsert, we can prove that every morphism satisfying P_σ is equal to some standardσ for some admissible list of indices.

theorem SimplexCategoryGenRel.IsAdmissible.simplicialEvalσ_succ_getElem {m : ℕ} (L : List ℕ) (hL : IsAdmissible m L) {k : ℕ} {hk : k < L.length} : simplicialEvalσ L L[k] = simplicialEvalσ L (L[k] + 1)

theorem SimplexCategoryGenRel.mem_isAdmissible_of_lt_and_eval_eq_eval_add_one {m : ℕ} (L : List ℕ) (hL : IsAdmissible m L) (j : ℕ) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)) : j ∈ L

theorem SimplexCategoryGenRel.lt_and_eval_eq_eval_add_one_of_mem_isAdmissible {m : ℕ} (L : List ℕ) (hL : IsAdmissible m L) (j : ℕ) (hj : j ∈ L) : j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

theorem SimplexCategoryGenRel.mem_isAdmissible_iff {m : ℕ} (L : List ℕ) (hL : IsAdmissible m L) (j : ℕ) : j ∈ L ↔ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

We can characterize elements in an admissible list as exactly those for which simplicialEvalσ takes the same value twice in a row.