feat(AlgebraicTopology): delaborators for truncated simplicial notations#20719
Open
feat(AlgebraicTopology): delaborators for truncated simplicial notations#20719
Conversation
Collaborator
Author
|
The following test, taken from I'm not aware of a fix for this that would still allow pretty-printing things like import Mathlib.AlgebraicTopology.SimplexCategory
open SimplexCategory.Truncated
variable (n : ℕ) (m : ℕ) (h : m ≤ n) (x) (hx : x = [m]ₙ) (n : True)
/- The delaborator should ideally not fire here because the truncation level is now `n✝`,
which cannot be subscripted. -/
/-- info: hx : x = [m]n✝ -/
#guard_msgs in #check hx |
PR summary 99427a7c6c
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.AlgebraicTopology.SimplexCategory.Defs | 385 | 384 | -1 (-0.26%) |
| Mathlib.Tactic | 2702 | 2704 | +2 (+0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.AlgebraicTopology.SimplexCategory.Defs |
-1 |
61 filesMathlib.Algebra.Homology.AlternatingConst Mathlib.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.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.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.Degenerate 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.SimplicialSet.Subcomplex 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 |
Mathlib.Tactic |
2 |
Mathlib.Tactic.SimplexCategory (new file) |
386 |
Declarations diff
+ Nat'
+ Nat'.γ
+ delabSubscript
+ delabSuperscript
+++ delabMkNotation
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).
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>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Collaborator
|
This PR/issue depends on: |
Collaborator
|
This pull request has conflicts, please merge |
joneugster
approved these changes
Jan 16, 2026
Contributor
joneugster
left a comment
There was a problem hiding this comment.
Hi @gio256! Sorry this PR was lying around for quite a while!
I think this is useful for subscripting ⦋m⦌ₙ and ⦋m⦌ₙ₊₁ which seem to be the main intended use cases.
As far as I can see the main blocker of the PR was that @kim-em commented, that the tests are covering cases outside of the intended usage. I think this is fine as is.
Could you please resolve merge conflicts, so we can get this merged afterwards?
Contributor
|
I've asked on Zulip in #Infinity-Cosmos > truncated simplicial notations if anybody is still interested in getting this merged with no reaction. Therefore I am going to mark this ass Please feel free to reassign me if there are any changes :) |
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
10 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 add delaborators for the following notations, introduced in #20688:
⦋m⦌ₙ, which denotes them-dimensional simplex in then-truncated simplex category.X _⦋m⦌ₙ, which denotes them-th term of ann-truncated simplicial objectX.X ^⦋m⦌ₙ, which denotes them-th term of ann-truncated cosimplicial objectX.If
pp.proofsis set totrue, we also pretty-print the proofp : m ≤ nfor all three notations as⦋m, p⦌ₙ,X _⦋m, p⦌ₙ, andX ^⦋m, p⦌ₙ, respectively.Credit to @kmill for one piece of code and much metaprogramming inspiration.