feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for P_σs (leanprover-community#25736)

We prove that admissible lists introduced in leanprover-community#21744  indeed provide a suitable normal form for morphisms of `SimplexCategoryGenRel` satisfying `P_σ` (i.e that are compositions of degeneracies).

To this end, we introduce `standardσ`, a construction that takes a list and turn it into a composition of `σ i`s in `SimplexCategoryGenRel`. We then prove that, thanks to the fifth simplicial identity, composition on the right by some `σ i` corresponds to simplicial insertion of `i` in the list. This gives existence of a normal form for every morphism satisfying `P_σ`, i.e exhibits such morphism as some `standardσ`.

For unicity, we introduce an auxiliary function `simplicialEvalσ : (List ℕ) → ℕ → ℕ` and show that for admissible lists, it lifts to `ℕ` the `orderHom` attached to `toSimplexCategory.map standardσ` and that we can recover elements of the list only by looking at values of this function. Since admissible lists are sorted, this fully characterizes the list, and thus shows that the list only depends on the morphism `standardσ` attached to it.

Part of a series of PR formalising that `SimplexCategoryGenRel` is equivalent to `SimplexCategory`.

Author: robin-carlier

Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

@@ -3,12 +3,7 @@ Copyright (c) 2025 Robin Carlier. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Carlier
 -/
-import Mathlib.Tactic.Zify
-import Mathlib.Data.List.Sort
-import Mathlib.Tactic.Linarith
-import Mathlib.Tactic.NormNum.Ineq
-import Mathlib.Tactic.Ring.Basic
-
+import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
 /-! # Normal forms for morphisms in `SimplexCategoryGenRel`.
 
 In this file, we establish that `P_δ` and `P_σ` morphisms in `SimplexCategoryGenRel`
@@ -34,12 +29,13 @@ stones towards proving that the canonical functor
 * [Kerodon Tag 04FT](https://kerodon.net/tag/04FT)
 
 ## TODOs:
-- Show that every `P_σ` admits a unique normal form.
 - Show that every `P_δ` admits a unique normal form.
 -/
 
 namespace SimplexCategoryGenRel
 
+open CategoryTheory
+
 section AdmissibleLists
 -- Impl. note: We are not bundling admissible lists as a subtype of `List ℕ` so that it remains
 -- easier to perform inductive constructions and proofs on such lists, and we instead bundle
@@ -155,4 +151,191 @@ theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : IsAdmissible (m + 1)
 
 end AdmissibleLists
 
+section NormalFormsP_σ
+
+-- Impl note.: The definition is a bit awkward with the extra parameters, but this
+-- is necessary in order to avoid some type theory hell when proving that `orderedInsert`
+-- behaves as expected...
+
+/-- 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. -/
+def standardσ (L : List ℕ) {m₁ m₂ : ℕ} (h : m₂ + L.length = m₁) : mk m₁ ⟶ mk m₂ :=
+  match L with
+  | .nil => eqToHom (by grind)
+  | .cons a t => standardσ t (by grind) ≫ σ (Fin.ofNat _ a)
+
+@[simp]
+lemma standardσ_nil (m : ℕ) : standardσ .nil (by grind) = 𝟙 (mk m) := rfl
+
+@[simp, reassoc]
+lemma standardσ_cons (L : List ℕ) (a : ℕ) {m₁ m₂ : ℕ} (h : m₂ + (a :: L).length = m₁) :
+    standardσ (L.cons a) h = standardσ L (by grind) ≫ σ (Fin.ofNat _ a) := rfl
+
+@[reassoc]
+lemma standardσ_comp_standardσ (L₁ L₂ : List ℕ) {m₁ m₂ m₃ : ℕ}
+    (h : m₂ + L₁.length = m₁) (h' : m₃ + L₂.length = m₂) :
+    standardσ L₁ h ≫ standardσ L₂ h' = standardσ (L₂ ++ L₁) (by grind) := by
+  induction L₂ generalizing L₁ m₁ m₂ m₃ with
+  | nil =>
+    obtain rfl : m₃ = m₂ := by grind
+    simp
+  | cons a t H =>
+    dsimp at h' ⊢
+    obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind
+    simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1)
+      (by grind) (by grind))]
+
+variable (m : ℕ) (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-bonds inputs
+are junk values. -/
+def simplicialEvalσ (L : List ℕ) : ℕ → ℕ :=
+  fun j ↦ match L with
+  | [] => j
+  | a :: L => if a < simplicialEvalσ L j then simplicialEvalσ L j - 1 else simplicialEvalσ L j
+
+lemma simplicialEvalσ_of_lt_mem (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) : simplicialEvalσ L j = j := by
+  induction L with
+  | nil => grind [simplicialEvalσ]
+  | cons _ _ _ =>
+    simp only [List.mem_cons, forall_eq_or_imp] at hj
+    grind [simplicialEvalσ]
+
+lemma simplicialEvalσ_monotone (L : List ℕ) : Monotone (simplicialEvalσ L) := by
+  intro a b hab
+  induction L generalizing a b with
+  | nil => exact hab
+  | cons head tail h_rec => grind [simplicialEvalσ]
+
+variable {m}
+/- We prove that `simplicialEvalσ` is indeed a lift of
+`(toSimplexCategory.map (standardσ m L _ _)).toOrderHom` when the list is admissible. -/
+lemma simplicialEvalσ_of_isAdmissible
+    (m₁ m₂ : ℕ) (hL : IsAdmissible m₂ L) (hk : m₂ + L.length = m₁)
+    (j : ℕ) (hj : j < m₁ + 1) :
+    (toSimplexCategory.map <| standardσ L hk).toOrderHom ⟨j, hj⟩ =
+    simplicialEvalσ L j := by
+  induction L generalizing m₁ m₂ with
+  | nil =>
+    obtain rfl : m₁ = m₂ := by grind
+    simp [simplicialEvalσ]
+  | cons a L h_rec =>
+    simp only [List.length_cons] at hk
+    subst hk
+    set a₀ := hL.head
+    have aux (t : Fin (m₂ + 2)) :
+        (a₀.predAbove t : ℕ) = if a < ↑t then (t : ℕ) - 1 else ↑t := by
+      simp only [Fin.predAbove, a₀]
+      split_ifs with h₁ h₂ h₂
+      · rfl
+      · simp only [Fin.lt_def, Fin.coe_castSucc, IsAdmissible.head_val] at h₁; grind
+      · simp only [Fin.lt_def, Fin.coe_castSucc, IsAdmissible.head_val, not_lt] at h₁; grind
+      · rfl
+    have := h_rec _ _ hL.tail (by grind) hj
+    have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
+    simpa only [toSimplexCategory_obj_mk, SimplexCategory.len_mk, standardσ_cons, Functor.map_comp,
+      toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategory.mkHom,
+      SimplexCategory.comp_toOrderHom, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe,
+      Function.comp_apply, Fin.predAboveOrderHom_coe, simplicialEvalσ, ha₀, ← this] using aux _
+
+/-- Performing a simplicial insertion in a list is the same as composition on the right by the
+corresponding degeneracy operator. -/
+lemma standardσ_simplicialInsert (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1)
+    (m₁ : ℕ) (hm₁ : m + L.length + 1 = m₁) :
+    standardσ (m₂ := m) (simplicialInsert j L) (m₁ := m₁)
+      (by simpa only [simplicialInsert_length, add_assoc]) =
+    standardσ (m₂ := m + 1) L (by grind) ≫ σ (Fin.ofNat _ j) := by
+  induction L generalizing m j with
+  | nil => simp [standardσ, simplicialInsert]
+  | cons a L h_rec =>
+    simp only [simplicialInsert]
+    split_ifs
+    · simp
+    · have : ∀ (j k : ℕ) (h : j < (k + 1)), Fin.ofNat (k + 1) j = j := by simp -- helps grind below
+      have : a < m + 2 := by grind -- helps grind below
+      have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
+        convert σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind
+      simp only [standardσ_cons, Category.assoc, this,
+        h_rec hL.tail (j + 1) (by grind) (by grind)]
+
+attribute [local grind] simplicialInsert_length simplicialInsert_isAdmissible in
+/-- Using `standardσ_simplicialInsert`, we can prove that every morphism satisfying `P_σ` is equal
+to some `standardσ` for some admissible list of indices. -/
+theorem 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 (by rw [h, h₁.symm, h₂]; rfl) := by
+  induction hf with
+  | id n =>
+    use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _
+    rfl
+  | of f hf =>
+    cases hf with | @σ m k =>
+    use [k.val], m, 1 , rfl, rfl, rfl
+    constructor <;> simp [IsAdmissible, Nat.le_of_lt_add_one k.prop, standardσ]
+  | @comp_of _ j x' g g' hg hg' h_rec =>
+    cases hg' with | @σ m k =>
+    obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
+    obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
+    use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
+    subst_vars
+    have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
+      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
+    simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
+      standardσ_comp_standardσ]
+
+section MemIsAdmissible
+
+lemma mem_isAdmissible_of_lt_and_eval_eq_eval_add_one (hL : IsAdmissible m L)
+    (j : ℕ) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)) :
+    j ∈ L := by
+  induction L generalizing m with
+  | nil => grind [simplicialEvalσ]
+  | cons a L h_rec =>
+    have := h_rec hL.tail (by grind)
+    suffices ¬j = a → (simplicialEvalσ L j = simplicialEvalσ L (j + 1)) by grind
+    intro hja
+    simp only [simplicialEvalσ] at hj₂
+    have : simplicialEvalσ L j ≤ simplicialEvalσ L (j + 1) :=
+      simplicialEvalσ_monotone L (by grind)
+    suffices ¬a < simplicialEvalσ L j → a < simplicialEvalσ L (j + 1) →
+      simplicialEvalσ L j = simplicialEvalσ L (j + 1) - 1 →
+      simplicialEvalσ L j = simplicialEvalσ L (j + 1) by grind
+    intro h₁ h₂ hj₂
+    simp only [IsAdmissible, List.sorted_cons, List.length_cons] at hL
+    obtain h | rfl | h := Nat.lt_trichotomy j a
+    · grind [simplicialEvalσ_monotone, Monotone, simplicialEvalσ_of_lt_mem]
+    · grind
+    · have := simplicialEvalσ_of_lt_mem L (a + 1) <| fun x h ↦ hL.1.1 x h
+      grind [simplicialEvalσ_monotone, Monotone]
+
+lemma lt_and_eval_eq_eval_add_one_of_mem_isAdmissible (hL : IsAdmissible m L) (j : ℕ) (hj : j ∈ L) :
+    j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1) := by
+  induction L generalizing m with
+  | nil => grind
+  | cons a L h_rec =>
+    constructor
+    · grind [List.mem_iff_getElem, IsAdmissible, List.sorted_cons]
+    · obtain rfl | h := List.mem_cons.mp hj
+      · grind [simplicialEvalσ_of_lt_mem, simplicialEvalσ, IsAdmissible, List.sorted_cons]
+      · have := h_rec hL.tail h
+        grind [simplicialEvalσ]
+
+/-- We can characterize elements in an admissible list as exactly those for which
+`simplicialEvalσ` takes the same value twice in a row. -/
+lemma mem_isAdmissible_iff (hL : IsAdmissible m L) (j : ℕ) :
+    j ∈ L ↔ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1) := by
+  grind [lt_and_eval_eq_eval_add_one_of_mem_isAdmissible,
+    mem_isAdmissible_of_lt_and_eval_eq_eval_add_one]
+
+end MemIsAdmissible
+
+end NormalFormsP_σ
+
 end SimplexCategoryGenRel