feat(AlgebraicTopology/SimplexCategory/SimplicialObject): definitions of simplicial objects by generators and relation

[robin-carlier]

We leverage the equivalence between SimplexCategory and SimplexCategoryGenRel to give new constructors for (co)simplicial objects, as well as constructors for natural transformations (resp. isomorphism) between those.

Final PR in the series of PR formalising the equivalence between SimplexCategory and SimplexCategoryGenRel.

---

• depends on: feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations): SimplexCategoryGenRel.toSimplexCategory is an equivalence #21747

[github-actions]

PR summary e9d9f11b69

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
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Equivalence (new file)	833
Mathlib.AlgebraicTopology.SimplicialObject.GeneratorsRelations (new file)	849

---

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_of_simplicialEvalδ_eq
+ eq_or_len_le_of_P_δ
+ equivSimplexCategory
+ equivSimplexCategory_functor_map_δ
+ equivSimplexCategory_functor_map_σ
+ equivSimplexCategory_functor_obj_mk
+ equivSimplexCategory_inverse_map_σ
+ equivSimplexCategory_inverse_objIsoMk
+ equivSimplexCategory_inverse_δ
+ existsUnique_P_δ_of_mono
+ existsUnique_P_σ_of_epi
+ existsUnique_toSimplexCategory_map
+ exists_P_σ_P_δ_factorisation
+ exists_normal_form_P_δ
+ exists_normal_form_P_σ
+ ext
+ homRel
+ hom_induction
+ hom_induction'
+ hom_induction_eq_top'
+ instance : toSimplexCategory.EssSurj
+ instance : toSimplexCategory.Faithful
+ instance : toSimplexCategory.Full
+ instance : toSimplexCategory.IsEquivalence := by
+ 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
+ le_simplicialEvalδ_self
+ 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δ_eq_self_of_isAdmissible_and_lt
+ simplicialEvalδ_eq_self_of_isAdmissible_cons
+ simplicialEvalδ_monotone
+ simplicialEvalδ_of_isAdmissible
+ simplicialEvalσ
+ simplicialEvalσ_monotone
+ simplicialEvalσ_of_isAdmissible
+ simplicialEvalσ_of_lt_mem
+ simplicialInsert
+ simplicialInsert_isAdmissible
+ simplicialInsert_length
+ standardδ
+ standardδ_heq
+ standardδ_simplicialInsert
+ 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
++ mkNatIso:
++ mkNatIso_hom_app
++ mkNatIso_inv_app
++ mkNatTrans:
++ mkNatTrans_app
++ mkNatTrans_comp
++ mkNatTrans_id
++ ofGeneratorsAndRelations:
++ ofGeneratorsAndRelationsObjMkIso
++ ofGeneratorsAndRelations_map_δ
++ ofGeneratorsAndRelations_map_σ
++ δ
++ σ

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): SimplexCategoryGenRel.toSimplexCategory is an equivalence #21747
  By Dependent Issues (🤖). Happy coding!