Commit 2025-10-04 08:50 5903e2ba

feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for P_σs (#25736) We prove that admissible lists introduced in #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 σ is 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.