[Merged by Bors] - feat(AlgebraicTopology): truncated simplicial notations#20688
Closed
[Merged by Bors] - feat(AlgebraicTopology): truncated simplicial notations#20688
Conversation
gio256
commented
Jan 12, 2025
2 tasks
1 task
PR summary 3c99f2b9ab
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.AlgebraicTopology.SimplexCategory.Defs | 381 | 382 | +1 (+0.26%) |
| Mathlib.AlgebraicTopology.SimplicialObject.Basic | 862 | 863 | +1 (+0.12%) |
| Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal | 880 | 881 | +1 (+0.11%) |
| Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat | 886 | 887 | +1 (+0.11%) |
Import changes for all files
| Files | Import difference |
|---|---|
58 filesMathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplexCategory.Basic Mathlib.AlgebraicTopology.SimplexCategory.Defs Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicTopology.SimplicialObject.Split Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution |
1 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
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).
gio256
commented
Jan 18, 2025
kim-em
reviewed
Jan 28, 2025
Contributor
|
This seems good to me, but some expert in meta code should also have a look. |
eric-wieser
reviewed
Feb 25, 2025
digama0
reviewed
Mar 2, 2025
digama0
approved these changes
Mar 2, 2025
Member
digama0
left a comment
There was a problem hiding this comment.
The meta code looks fine to me.
YaelDillies
approved these changes
Mar 3, 2025
Contributor
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 10, 2025
We provide macros for the following notations: - `⦋m⦌ₙ` denotes the `m`-dimensional simplex in the `n`-truncated simplex category. - `X _⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated simplicial object `X`. - `X ^⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated cosimplicial object `X`. For all of these notations, the truncation proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`, `X _⦋m, p⦌ₙ`, and `X ^⦋m, p⦌ₙ`, respectively. These notations generalize those already in use in `HomotopyCat.lean` and `Coskeletal.lean`. Delaborators for these notations are added in #20719. See #17732 and #20355 to understand the reason for the use of `subscriptTerm`. Co-authored-by: gio256 <gio256@protonmail.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
tukamilano
pushed a commit
that referenced
this pull request
Mar 20, 2025
We provide macros for the following notations: - `⦋m⦌ₙ` denotes the `m`-dimensional simplex in the `n`-truncated simplex category. - `X _⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated simplicial object `X`. - `X ^⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated cosimplicial object `X`. For all of these notations, the truncation proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`, `X _⦋m, p⦌ₙ`, and `X ^⦋m, p⦌ₙ`, respectively. These notations generalize those already in use in `HomotopyCat.lean` and `Coskeletal.lean`. Delaborators for these notations are added in #20719. See #17732 and #20355 to understand the reason for the use of `subscriptTerm`. Co-authored-by: gio256 <gio256@protonmail.com>
idontgetoutmuch
pushed a commit
to idontgetoutmuch/mathlib4
that referenced
this pull request
Apr 7, 2025
…ommunity#20688) We provide macros for the following notations: - `⦋m⦌ₙ` denotes the `m`-dimensional simplex in the `n`-truncated simplex category. - `X _⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated simplicial object `X`. - `X ^⦋m⦌ₙ` denotes the `m`-th term of an `n`-truncated cosimplicial object `X`. For all of these notations, the truncation proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`, `X _⦋m, p⦌ₙ`, and `X ^⦋m, p⦌ₙ`, respectively. These notations generalize those already in use in `HomotopyCat.lean` and `Coskeletal.lean`. Delaborators for these notations are added in leanprover-community#20719. See leanprover-community#17732 and leanprover-community#20355 to understand the reason for the use of `subscriptTerm`. Co-authored-by: gio256 <gio256@protonmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
8 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
We provide macros for the following notations:
⦋m⦌ₙdenotes them-dimensional simplex in then-truncated simplex category.X _⦋m⦌ₙdenotes them-th term of ann-truncated simplicial objectX.X ^⦋m⦌ₙdenotes them-th term of ann-truncated cosimplicial objectX.For all of these notations, the truncation proof
p : m ≤ ncan also be provided using the syntax⦋m, p⦌ₙ,X _⦋m, p⦌ₙ, andX ^⦋m, p⦌ₙ, respectively.These notations generalize those already in use in
HomotopyCat.leanandCoskeletal.lean.Delaborators for these notations are added in #20719.
See #17732 and #20355 to understand the reason for the use of
subscriptTerm.