feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by an homotopy

[joelriou]

In this PR, we show that a homotopy between morphisms of simplicial sets (given as a morphism X ⊗ Δ[1] ⟶ Y) induces a "combinatorial" simplicial homotopy.

WIP

---

[github-actions]

PR summary a637594054

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialObject.SimplicialHomotopy (new file)	543
Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne (new file)	578
Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (new file)	618
Mathlib.AlgebraicTopology.SimplicialSet.SimplicialHomotopy (new file)	621

---

Declarations diff

+ Fin.eq_id_of_strictMono
+ Fin.orderHom_ext_of_injective
+ Fin.orderHom_ext_of_injective_aux
+ Homotopy
+ SimplicialHomotopy
+ _root_.Fin.eq_iff_eq_zero_iff
+ botEquiv
+ h₀
+ h₁
+ instance : SymmetricCategory SSet.{u}
+ le_orderHomOfSimplex
+ nonDegenerateEquiv₁
+ nonDegenerateEquiv₁_fst
+ nonDegenerateEquiv₁_snd
+ nonDegenerate_ext₁
+ nonDegenerate_ext₂
+ nonDegenerate_max_dim_iff
+ objMk_bijective
+ objMk₁
+ objMk₁_apply_eq_one_iff
+ objMk₁_apply_eq_zero_iff
+ objMk₁_bijective
+ objMk₁_injective
+ objMk₁_of_castSucc_lt
+ objMk₁_of_le_castSucc
+ objMk₁_surjective
+ prod_map_fst
+ prod_map_snd
+ prod_δ_fst
+ prod_δ_snd
+ prod_σ_fst
+ prod_σ_snd
+ refl
+ strictMono_orderHomOfSimplex
+ toFun
+ toSimplicialHomotopy
+ whiskerRight
+ yonedaEquiv_symm_app_objEquiv_symm
+ δ_objEquiv_symm_apply
+ δ_objMk₁_of_le
+ δ_objMk₁_of_lt
+ σ_objEquiv_symm_apply
+ σ_objMk₁_of_le
+ σ_objMk₁_of_lt

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.

---

Increase in tech debt: (relative, absolute) = (4.00, 0.01)

Current number	Change	Type
640	4	erw

Current commit 435d5214f6
Reference commit a637594054

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).