[Merged by Bors] - refactor(AlgebraicTopology/SimplicialSet): use the Subpresheaf API

[joelriou]

Some new API is introduced for subcomplexes of the standard simplex: any S : Finset (Fin (n + 1)) defines a subcomplex face S of Δ[n], and this face is isomorphic to Δ[m] when Fin (m + 1) ≃o S. Then, boundaries and horns are redefined as subcomplexes of the standard simplex and it is shown that they are unions of certain codimension one faces of the standard simplex.

• depends on: [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): constant morphisms #21543
• depends on: [Merged by Bors] - chore(CategoryTheory/Sites): fix names #21540
• depends on: [Merged by Bors] - feat(AlgebraicTopology): subcomplexes of simplicial sets #21542
• depends on: [Merged by Bors] - feat(Order): Fin.succAboveOrderIso #21303
• depends on: [Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves #21047
• depends on: [Merged by Bors] - feat(CategoryTheory): Subpresheaf is a complete lattice #20840
• depends on: [Merged by Bors] - feat(CategoryTheory/Subpresheaf): equalizer #21096

---

[github-actions]

PR summary e025886861

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicTopology.SimplicialSet.Horn	869	876	+7 (+0.81%)
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex	870	877	+7 (+0.80%)
Mathlib.AlgebraicTopology.SimplicialSet.Path	870	877	+7 (+0.80%)
Mathlib.AlgebraicTopology.Quasicategory.Basic	871	878	+7 (+0.80%)
Mathlib.AlgebraicTopology.Quasicategory.StrictSegal	879	886	+7 (+0.80%)
Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex	868	874	+6 (+0.69%)
Mathlib.AlgebraicTopology.SimplicialSet.Boundary	869	875	+6 (+0.69%)
Mathlib.AlgebraicTopology.ExtraDegeneracy	1114	1120	+6 (+0.54%)

Import changes for all files

Files	Import difference
10 files Mathlib.Algebra.Homology.AlternatingConst Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution	6
11 files Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.CategoryTheory.Category.Cat.Colimit	7

---

Declarations diff

+ Subcomplex.liftPath
+ Subcomplex.map_ι_liftPath
+ asOrderHom
+ boundary_eq_iSup
+ const_val_apply
+ ext
+ faceRepresentableBy
+ face_eq_ofSimplex
+ face_inter_face
+ face_le_horn
+ horn_eq_iSup
+ horn_obj_zero
+ instance (n i : ℕ) : DFunLike (Δ[n] _⦋i⦌) (Fin (i + 1)) (fun _ ↦ Fin (n + 1))
+ isoOfRepresentableBy
+ mem_face_iff
+ mem_ofSimplex_obj
+ objEquiv_symm_apply
+ objEquiv_symm_comp
+ objEquiv_toOrderHom_apply
+ objMk_apply
+ obj₀Equiv
+ ofSimplex
+ ofSimplex_le_iff
+ ofSimplex_yonedaEquiv_δ
+ range_eq_ofSimplex
+ range_δ
+ stdSimplex.spineId_arrow_apply_one
+ stdSimplex.spineId_arrow_apply_zero
+ stdSimplex.spineId_vertex
+ yonedaEquiv_coe
+ yonedaEquiv_comp
+ yonedaEquiv_map
++- face
- id
- id_eq_objEquiv_symm
- objEquiv_id

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:

• [Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): constant morphisms #21543
• [Merged by Bors] - chore(CategoryTheory/Sites): fix names #21540
• [Merged by Bors] - feat(AlgebraicTopology): subcomplexes of simplicial sets #21542
• [Merged by Bors] - feat(Order): Fin.succAboveOrderIso #21303
• [Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves #21047
• [Merged by Bors] - feat(CategoryTheory): Subpresheaf is a complete lattice #20840
• [Merged by Bors] - feat(CategoryTheory/Subpresheaf): equalizer #21096
  By Dependent Issues (🤖). Happy coding!

[emilyriehl]

What explains the reason you need to annotate various simplicial sets as belonging to the type SSet.{u}? Is this to coerce a subcomplex of a simplex to a standard simplicial set?

[joelriou]

What explains the reason you need to annotate various simplicial sets as belonging to the type SSet.{u}? Is this to coerce a subcomplex of a simplex to a standard simplicial set?

Yes, this is to coerce subcomplexes to simplicial sets. (In some cases, the (_ : SSet.{u}) syntax may not have been absolutely necesary, but this was also a way to clarify in which universe it was.)

[jcommelin]

bors d+

[jcommelin]

How about keeping the old name horn?
Anyway, if you decide to stick with the new name, then please update it in the docstring.

[mathlib-bors]

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style