feat(AlgebraicTopology/SimplicialSet): the relative cell complex of a monomorphism

[joelriou]

In this PR, we show that any monomorphism of simplicial sets is a relative cell complex with basic cells given by boundary inclusions.

---

Note: I think we can ignore the large-import label here, because this is a leaf file, and the relative cell complex that is constructed here is a basic fact about the skeleton filtration.

[github-actions]

PR summary d480e9ea56

Import changes exceeding 2%

%	File
+18.23%	Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.Skeleton	883	1044	+161 (+18.23%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.Skeleton	161

---

Declarations diff

+ Cell
+ b
+ b_app_ι_app_objEquiv_symm_val
+ eq_boundary_iff
+ instance (J : Type*) [(monomorphisms C).IsStableUnderCoproductsOfShape J]
+ instance (j : ι) : Mono (f.m j) := by dsimp [m]; infer_instance
+ isPullback
+ isPushout
+ isPushout_aux
+ l
+ map
+ map_app_objEquiv_symm
+ map_app_objEquiv_symm_id
+ max_range_r_range_b
+ mem_skeletonOfMono_obj_iff
+ preimage_map
+ r
+ range_map_le
+ range_r_app_union_range_b_app
+ relativeCellComplex
+ relativeCellComplexCellsEquiv
+ relativeCellComplexOfMono
+ sigmaBoundary
+ sigmaStdSimplex
+ t
+ w
+ ιSigmaBoundary
+ ιSigmaStdSimplex
+ ιSigmaStdSimplex_jointly_surjective
+ ι_b_ι
+ ι_l
+ ι_t_ι_eq_ι_l_b_ι
- instance (j : ι) : Mono (f.m j)

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).