Commit 2025-04-21 14:54 d61e6da5

feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): admissible lists and simplicial insertion (#21744) We introduce the notion of an m-admissible list of natural number: a list [i₀,…,iₙ] is said to be m-admissible if iₖ ≤ m + k for all valid index k. These lists are intended to uniquely represents either P_σ or P_δ morphisms in SimplexCategoryGenRel. We prove basic stability of such lists under some lists operation such as the tail. We also introduce the notion of simplicial insertion, which is intended to be the algorithm on such normal forms representing composition on the right (for P_σ morphisms) or on the left (for P_δ morphisms) by a single morphism, and we prove that this preserves admissibility. Part of a series of PR formalising that SimplexCategoryGenRel is equivalent to SimplexCategory.