Tracking issue: definition of simplicial objects by generators and relations.

[robin-carlier]

This is a tracking issue for my series of PR formalising the fact that the simplex category is equivalent to the category
presented by generators and relations via the simplicial identities.

The proof that I adapt is mostly the one present in Kerodon. The global strategy is the following:

• Define a category SimplexCategoryGenRel by generators and relations, with generating morphisms representing faces and degeneracies map, and relations the simplicial relations.
• Define a functor toSimplexCategory out of this category to the usual simplex category: such a functor exists as the simplicial relations hold in the ssimplex category. This functor is essentially surjective (in fact, even bijective on objects).
• Show that every morphism in that category admits a decomposition as a composition of degeneracies, followed by a composition of faces. In practice, this means doing some sorting using the simplicial identities.
• Show that compositions of faces can be put in a normal form which is entirely determined by the realisation of the morphism in SimplexCategory (see Kerodon 04FQ for the precise statement).
• Show the same for composition of degeneracies.
• From the previous two points, obtain that for any monomorphism in SimplexCategory, there is a unique composition of faces in SimplexCategoryGenRel that lifts it. Same for epimorphisms in SimplexCategory and composition of degeneracies.
• Using the epi-mono factorisation in SimplexCategory, conclude that toSimplexCategory is fully faithful

The formalisation is of course way more technical (since, in the end it involves a lot of sorting...), and so I split the proof over several files and pull requests, they are organized as follows.

• Pull request [Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): the category SimplexCategoryGenRel #21741 introduces the file AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean, which defines SimplexCategoryGenRel, records that it satisfies the simplicial identities, and define its canonical functor to SimplexCategory, as well as a few induction principles that will help working with this category.
• Pull request [Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): Morphism properties in SimplexCategoryGenRel #21742 introduces the file AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean, which inductively defines predicates P_σ and P_δ asserting that a morphism in SimplexCategoryGenRel is a composition of degeneracies (resp. faces). I also prove that one can define these predicates either by composition on the left, or on the right (both will be needed).
• Pull request [Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in SimplexCategoryGenRel #21743 continues the previous PR, and shows that every morphisms admits a decomposition as a P_σ followed by a P_δ, essentially showing that SimplexCategoryGenRel has epi-mono factorisations. Only existence is needed for the proof that toSimplexCategory is an equivalence, so I did not include unicity.
• Pull request [Merged by Bors] - feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): admissible lists and simplicial insertion #21744 introduces the file AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean. This will be the file where I will prove that P_σ and P_δ can be uniquely represented as some lists of natural numbers satisfying some inequalities. This PR introduce said lists and call them admissible. I also prove a few technical lemmas about those lists that will be used extensively in the later proofs. Finally, the file introduces a List construction called simplicialInsert which describes inserting an element into an admissible list while keeping admissibility. The simplicial insertion of an element j reflects on morphism either composition on the left by δ i (when the list represents a normal form of a P_δ morphism) or composition on the right by σ j (when the list represents a normal form of a P_σ morphism).
• Pull request feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for P_σs #21745 carries out this program for P_σ morphisms. It introduces a construction standard_σ which turns an integer m and a list L into a morphism mk m + L.length ⟶ mk m in SimplexCategoryGenRel. The PR also introduce a helper construction simplicialEvalσ which is a bare hand definition of what (toSimplexCategory.map standardσ _).toOrderHom is supposed to be. This helper construction is nicer to work with than the former, and the PR prove they are indeed equal (up to a lift to the naturals). Finally, the PR shows that every P_σ is indeed equal to some standardσ m L for some admissible list, and that this admissible list only depends on simplicialEvalσ, so that with the previous facts, it only depends on the realisation in SimplexCategory of the morphism.
• Pull request feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for P_δs #21746 is the mirror of the previous PR but for P_δ morphisms, again, it defines standardδ and simplicialEvalδ, prove how they relate both to simplicial insertion and to toSimplexCategory, and finally prove that any morphism satisfying P_δ is a standardδ for some admissible list that is entirely determined by simplicialEvalδ.
• Pull request feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): SimplexCategoryGenRel.toSimplexCategory is an equivalence #21747 introduces a new file AlgebraicTopology/SimplexCategory/GeneratorsRelations/Equivalence.lean which uses the previous results to establish that the canonical functor toSimplexCategory is an equivalence. The file first show that every monomorphism in SimplexCategory can be uniquely lifted along toSimplexCategory to a morphism satisfying P_δ, then something similar for epimorphisms, and finally, using existence and unicity of epi-mono factorisations in SimplexCategory, the functor is fully faithful, and essential surjectivity is free here, so the functor is an equivalence.
• Pull request feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation #21748 provides the API to use this equivalence in the (new) file AlgebraicTopology/SimplicialObject/GeneratorsRelations.lean, in the form of new constructors for (co)simplicial objects and natural transformations of such. The results in this PR should be the only ones one should use in practice, all of the results in the previous PR being essentially a big black box to obtains the one in this PR.