feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` by erdOne · Pull Request #37057 · leanprover-community/mathlib4

erdOne · 2026-03-23T19:59:17Z

github-actions · 2026-03-23T20:00:27Z

PR summary 5289bf289a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.stdSimplex.map_δ_apply
+ castSucc_eq_zero
+ succAbove_eq_iff
+ succAbove_eq_zero
+ toTop_map_δ_apply
+ δ_apply
+ σ_apply

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

github-actions · 2026-03-23T20:00:34Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

mathlib-merge-conflicts · 2026-03-25T09:05:58Z

This pull request has conflicts, please merge master and resolve them.

…lib4 into erd1/toTop_map_δ_apply

Raph-DG · 2026-03-31T13:09:24Z

awaiting-author

…lib4 into erd1/toTop_map_δ_apply :wpecially if it merges an updated upstream into a topic branch.

dagurtomas

Thanks!

maintainer merge

github-actions · 2026-04-02T15:39:08Z

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

joelriou · 2026-04-02T16:28:03Z

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

 lemma concreteCategoryHom_id (n : SimplexCategory) : ConcreteCategory.hom (𝟙 n) = .id := rfl

+@[simp]
+lemma δ_apply {n : ℕ} (i : Fin (n + 2)) (j : Fin (⦋n⦌.len + 1)) : δ i j = i.succAbove j := rfl


This works also fine:

Suggested change

lemma δ_apply {n : ℕ} (i : Fin (n + 2)) (j : Fin (⦋n⦌.len + 1)) : δ i j = i.succAbove j := rfl

lemma δ_apply {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : δ i j = i.succAbove j := rfl

This is not reducibly type correct because currently ⦋n⦌.len is not reducibly defeq to n and it causes troubles especially with the new transparency changes.

I do not understand what you mean:

example (n : ℕ) : ⦋n⦌.len = n := by dsimp

The point I was trying to make is that

example ⦋n⦌.len = n := by with_reducible rfl

fails and this causes much trouble (similar to ones that dsimp% is trying to fix), and especially after the recent changes to transparency handling.

Mathlib/AlgebraicTopology/TopologicalSimplex.lean

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

riccardobrasca · 2026-04-04T14:49:02Z

@joelriou are you happy with this?

Mathlib/Data/Fin/SuccPred.lean

Co-authored-by: Joël Riou <[email protected]>

feat(AlgebraicTopology): SimplexCategory.toTop_map_δ_apply

81865a4

erdOne force-pushed the erd1/toTop_map_δ_apply branch from 454ac5e to 81865a4 Compare March 23, 2026 20:00

erdOne changed the title ~~Erd1/toTop map δ apply~~ feat(AlgebraicTopology): SimplexCategory.toTop_map_δ_apply Mar 23, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 25, 2026

Merge branch 'master' of https://github.com/leanprover-community/math…

fa2cd5e

…lib4 into erd1/toTop_map_δ_apply

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 27, 2026

fix

82ea12d

github-actions bot added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026

erdOne added 2 commits April 1, 2026 11:05

Merge branch 'master' of https://github.com/leanprover-community/math…

0cb8f91

…lib4 into erd1/toTop_map_δ_apply :wpecially if it merges an updated upstream into a topic branch.

add docstring

3697092

erdOne added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebraic-topology Algebraic topology and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 1, 2026

Update Defs.lean

49f704b

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 1, 2026

mathlib-triage bot assigned robin-carlier Apr 2, 2026

dagurtomas self-requested a review April 2, 2026 14:56

dagurtomas reviewed Apr 2, 2026

View reviewed changes

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 2, 2026

joelriou reviewed Apr 2, 2026

View reviewed changes

Mathlib/AlgebraicTopology/TopologicalSimplex.lean Show resolved Hide resolved

joelriou reviewed Apr 2, 2026

View reviewed changes

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2026

fix proof

061322e

erdOne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026

joelriou reviewed Apr 4, 2026

View reviewed changes

Mathlib/Data/Fin/SuccPred.lean Outdated Show resolved Hide resolved

joelriou reviewed Apr 4, 2026

View reviewed changes

Mathlib/Data/Fin/SuccPred.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 4, 2026

Apply suggestions from code review

b02fa85

Co-authored-by: Joël Riou <[email protected]>

erdOne added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 4, 2026

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 4, 2026

	lemma δ_apply {n : ℕ} (i : Fin (n + 2)) (j : Fin (⦋n⦌.len + 1)) : δ i j = i.succAbove j := rfl
	lemma δ_apply {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : δ i j = i.succAbove j := rfl

Conversation

erdOne commented Mar 23, 2026

Uh oh!

github-actions bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5289bf289a

Import changes for modified files

Declarations diff

Uh oh!

github-actions bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

mathlib-merge-conflicts bot commented Mar 25, 2026

Uh oh!

Raph-DG commented Mar 31, 2026

Uh oh!

dagurtomas left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Apr 2, 2026

Uh oh!

joelriou Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

erdOne Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

joelriou Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

erdOne Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Apr 4, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Mar 23, 2026 •

edited

Loading

github-actions bot commented Mar 23, 2026 •

edited

Loading