feat(AlgebraicTopology): weakly polyhedral like simplicial sets

[joelriou]

In this file, we introduce a typeclass SSet.IsWeaklyPolyhedralLike for a simplicial set X : SSet: it says that for any non-degenerate simplex x : X _⦋n⦌, the corresponding morphism Δ[n] ⟶ X is a monomorphism.

---

(I would welcome any better name than IsWeaklyPolyhedralLike.)

[github-actions]

PR summary e8bf6cc224

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.WeaklyPolyhedralLike (new file)	985

---

Declarations diff

+ IsWeaklyPolyhedralLike
+ IsWeaklyPolyhedralLike.mono'
+ IsWeaklyPolyhedralLike.of_iso
+ IsWeaklyPolyhedralLike.of_mono
+ IsWeaklyPolyhedralLike.δ_injective
+ instance (A : X.Subcomplex) [X.IsWeaklyPolyhedralLike] :
+ instance (T : Type*) [PartialOrder T] : (nerve T).IsWeaklyPolyhedralLike
+ instance (n : SimplexCategory) : (stdSimplex.{u}.obj n).IsWeaklyPolyhedralLike
+ instance (n m : SimplexCategory) :
+ nonDegenerate_δ

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.