feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for P_σs

[robin-carlier]

We prove that admissible lists indeed provide a normal form for morphisms of satisfying P_σ.
To this end, we introduce standardσ, a construction that takes a list and turn it into a composition of σ is in SimplexCategoryGenRel. We then prove that, thangs to the fifth simplicial identity, composition on the right corresponds to simplicial insertion in the list. This gives existence of a normal form for every morphism satisfying P_σ.

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.

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

---

• depends on: feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): admissible lists and simplicial insertion #21744

[github-actions]

PR summary 0e442a8564

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic (new file)	830
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (new file)	831
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (new file)	832

---

Declarations diff

+ FreeSimplexQuiver
+ FreeSimplexQuiver.len
+ FreeSimplexQuiver.mk
+ Hom
+ P_δ
+ P_δ'
+ P_δ'_comp
+ P_δ_comp
+ P_δ_eqToHom
+ P_δ_eq_P_δ'
+ P_σ
+ P_σ'
+ P_σ'_comp
+ P_σ_comp
+ P_σ_eqToHom
+ P_σ_eq_P_σ'
+ Quiv
+ SimplexCategoryGenRel
+ SimplexCategoryGenRel.mk
+ SplitEpiσ
+ SplitMonoδ
+ eq_or_len_le_of_P_δ
+ exists_P_σ_P_δ_factorisation
+ exists_normal_form_P_σ
+ ext
+ homRel
+ hom_induction
+ hom_induction'
+ hom_induction_eq_top'
+ instance {n : ℕ} {i : Fin (n + 1)} : IsSplitEpi (σ i) := .mk' SplitEpiσ
+ instance {n : ℕ} {i : Fin (n + 2)} : IsSplitMono (δ i) := .mk' SplitMonoδ
+ isAdmissible
+ isAdmissibleGetElemAsFin
+ isAdmissibleHead
+ isAdmissible_cons
+ isAdmissible_ext
+ isAdmissible_head_lt
+ isAdmissible_nil
+ isAdmissible_tail
+ isSplitEpi_P_σ
+ isSplitEpi_P_σ_toSimplexCategory
+ isSplitMono_P_δ
+ isSplitMono_P_δ_toSimplexCategory
+ len
+ lt_and_eval_eq_eval_succ_of_mem_isAdmissible
+ mem_isAdmissible_iff
+ mem_isAdmissible_of_lt_and_eval_eq_eval_succ
+ mk_len
+ morphismProperty_eq_top
+ rec
+ simplicialEvalσ
+ simplicialEvalσ_monotone
+ simplicialEvalσ_of_isAdmissible
+ simplicialEvalσ_of_lt_mem
+ simplicialInsert
+ simplicialInsert_isAdmissible
+ simplicialInsert_length
+ standardσ
+ standardσ_heq
+ standardσ_simplicialInsert
+ toSimplexCategory
+ toSimplexCategory_len
+ toSimplexCategory_map_δ
+ toSimplexCategory_map_σ
+ toSimplexCategory_obj_mk
+ δ_comp_δ
+ δ_comp_δ_nat
+ δ_comp_σ_of_gt
+ δ_comp_σ_of_le
+ δ_comp_σ_self
+ δ_comp_σ_succ
+ σ_comp_σ
+ σ_comp_σ_nat
++ δ
++ σ

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): admissible lists and simplicial insertion #21744
  By Dependent Issues (🤖). Happy coding!