[Merged by Bors] - refactor(AlgebraicTopology/SimplicialSet): use the Subpresheaf API#21090
[Merged by Bors] - refactor(AlgebraicTopology/SimplicialSet): use the Subpresheaf API#21090
Conversation
…redef-horn-boundary
…to sset-redef-horn-boundary
PR summary e025886861
|
| 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 filesMathlib.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 filesMathlib.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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
…jriou-sset-subcomplex' into sset-redef-horn-boundary
This PR introduces `SSet.Subcomplex` as an abbreviation for `Subpresheaf`. (This is needed because `SSet` is defined as a category of presheaves, but not reducibly so.) (Part of the purpose of this PR is to shorten the diff of the refactor PR #21090.) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
This PR introduces constant morphisms `X ⟶ Y` of simplicial sets that are given by a `0`-simplex of `Y`. (This is to make the diff shorter for the refactor PR #21090.)
|
What explains the reason you need to annotate various simplicial sets as belonging to the type |
Yes, this is to coerce subcomplexes to simplicial sets. (In some cases, the |
| intro hj | ||
| exact Set.range_comp_subset_range _ _ hj⟩ | ||
| @[simps (config := .lemmasOnly)] | ||
| def subcomplexHorn (n : ℕ) (i : Fin (n + 1)) : (Δ[n] : SSet.{u}).Subcomplex where |
There was a problem hiding this comment.
How about keeping the old name horn?
Anyway, if you decide to stick with the new name, then please update it in the docstring.
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks! bors merge |
…21090) 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. - [x] depends on: #21543 - [x] depends on: #21540 - [x] depends on: #21542 - [x] depends on: #21303 - [x] depends on: #21047 - [x] depends on: #20840 - [x] depends on: #21096 Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
…21090) 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. - [x] depends on: #21543 - [x] depends on: #21540 - [x] depends on: #21542 - [x] depends on: #21303 - [x] depends on: #21047 - [x] depends on: #20840 - [x] depends on: #21096 Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Some new API is introduced for subcomplexes of the standard simplex: any
S : Finset (Fin (n + 1))defines a subcomplexface SofΔ[n], and this face is isomorphic toΔ[m]whenFin (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.