[Merged by Bors] - feat(CategoryTheory/Triangulated): Generators in triangulated categories by justus-springer · Pull Request #37046 · leanprover-community/mathlib4

justus-springer · 2026-03-23T17:05:28Z

Define strong and classical generators in triangulated categories. See also the zulip thread.

depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty/Shift): Shift closure is iSup of shifts #37080
depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty/Retract): Retracts and biproducts/zeros #37081
depends on: [Merged by Bors] - feat(CategoryTheory/Triangulated/Subcategory): extensionProductIter #37083
depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): binaryProductsClosure #37085
depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): API for bot/top as object properties #37090
depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): add ObjectProperty.Nonempty #37442

github-actions · 2026-03-23T17:06:42Z

PR summary 410d5afde2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.ObjectProperty.ClosureShift` (new file)	882
`Mathlib.CategoryTheory.Triangulated.Generators` (new file)	1190

Declarations diff

+ IsClassicalTriangulatedGenerator
+ IsStrongTriangulatedGenerator
+ IsStrongTriangulatedGenerator.isClassicalTriangulatedGenerator
+ instance : P.triangEnvelope.IsStableUnderRetracts
+ instance : P.triangEnvelope.IsStableUnderShift ℤ
+ instance [IsTriangulated C] : P.triangEnvelope.IsTriangulatedClosed₂ := by
+ instance [P.Nonempty] : P.triangEnvelope.Nonempty
+ instance [P.Nonempty] [IsTriangulated C] : P.triangEnvelope.IsTriangulated
+ instance {A : Type*} [AddGroup A] [HasShift C A] {α : Type*} {J : α → Type*}
+ instance {A : Type*} [AddMonoid A] [HasShift C A] [P.IsStableUnderShift A] :
+ isClassicalTriangulatedGenerator_iff
+ isStrongTriangulatedGenerator_iff
+ le_triangEnvelope
+ le_triangEnvelopeIter
+ monotone'_triangEnvelopeIter
+ monotone_triangEnvelope
+ monotone_triangEnvelopeIter
+ prop_triangEnvelope_iff
+ retractClosure_retractClosure
+ triangEnvelope
+ triangEnvelopeIter
+ triangEnvelopeIter_add
+ triangEnvelopeIter_add'
+ triangEnvelopeIter_le_triangEnvelope
+ triangEnvelopeIter_succ
+ triangEnvelopeIter_succ'
+ triangEnvelopeIter_zero
+ triangEnvelope_le_iff

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).

…zeros (#37081) Bicones and zeros are always retracts, hence if an object property is stable under retracts, it is also is stable under taking summands. This is used in the definition of strong generators in #37046

Define an abbreviation `limitClosure` where you only take limits of one shape. Then this is used to define `binaryProductsClosure` and its dual. This is used in the definition of strong generators in #37046.

…#37083) This PR adds some more API to `extensionProduct` and then defines `extensionProductIter`, the `n`-fold extension product of an object property with itself. Note that there is no "neutral element" for the extension product, hence `extensionProductIter P 0` is `P`, and `extensionProductIter P n` is `P * ... * P` with `n+1` terms. See also `extensionProductIter_add`, where this offset is clearly visible. This is used in the definition of strong generators in #37046.

…ties (#37090) This PR adds some instances and API handling bot and top as object properties. This is used in the definition of strong generators in #37046.

…37442) Adding this typeclass was suggested in the review of #37046. The crucial point where this gets used is in the file `CategoryTheory/ObjectProperty/Retract.lean`. Here, we have the instance `P.IsStableUnderRetracts -> P.Nonempty -> P.ContainsZero`, since a zero object is a retract of *any* object. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-dependent-issues · 2026-04-03T17:11:29Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory/ObjectProperty/Shift): Shift closure is iSup of shifts #37080~~
~~[Merged by Bors] - feat(CategoryTheory/ObjectProperty/Retract): Retracts and biproducts/zeros #37081~~
~~[Merged by Bors] - feat(CategoryTheory/Triangulated/Subcategory): extensionProductIter #37083~~
~~[Merged by Bors] - feat(CategoryTheory/ObjectProperty): binaryProductsClosure #37085~~
~~[Merged by Bors] - feat(CategoryTheory/ObjectProperty): API for bot/top as object properties #37090~~
~~[Merged by Bors] - feat(CategoryTheory/ObjectProperty): add ObjectProperty.Nonempty #37442~~
By Dependent Issues (🤖). Happy coding!

mathlib-merge-conflicts · 2026-04-03T19:50:36Z

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

…eanprover-community#37442) Adding this typeclass was suggested in the review of leanprover-community#37046. The crucial point where this gets used is in the file `CategoryTheory/ObjectProperty/Retract.lean`. Here, we have the instance `P.IsStableUnderRetracts -> P.Nonempty -> P.ContainsZero`, since a zero object is a retract of *any* object. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Co-authored-by: Dagur Asgeirsson <[email protected]>

robin-carlier · 2026-04-13T10:05:28Z

Thanks!

maintainer merge

github-actions · 2026-04-13T10:06:00Z

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

joelriou · 2026-04-13T10:47:42Z

Thanks!

bors merge

…ies (#37046) Define strong and classical generators in triangulated categories. See also the [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Generators.20in.20triangulated.20categories/with/573268390). Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-04-13T11:28:13Z

Pull request successfully merged into master.

Build succeeded:

justus-springer and others added 2 commits March 23, 2026 17:03

triangulated generators

730a5b3

[pre-commit.ci lite] apply automatic fixes

d5a68d6

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 23, 2026

github-actions bot added the t-category-theory Category theory label Mar 23, 2026

small refactor

bbb5a07

This was referenced Mar 24, 2026

[Merged by Bors] - feat(CategoryTheory/Triangulated/Subcategory): extensionProductIter #37083

Closed

[Merged by Bors] - feat(CategoryTheory/ObjectProperty): binaryProductsClosure #37085

Closed

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 24, 2026

justus-springer mentioned this pull request Mar 24, 2026

[Merged by Bors] - feat(CategoryTheory/ObjectProperty): API for bot/top as object properties #37090

Closed

justus-springer marked this pull request as ready for review March 24, 2026 11:02

justus-springer mentioned this pull request Mar 24, 2026

[Merged by Bors] - feat(CategoryTheory/ObjectProperty/Retract): Retracts and biproducts/zeros #37081

Closed

add documentation

e42a8f4

add a todo to docstring

af85c09

justus-springer force-pushed the justus/triangulated_generators branch from b26f803 to af85c09 Compare March 24, 2026 14:27

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 24, 2026

justus-springer added 5 commits March 24, 2026 17:32

Merge branch 'master' into justus/triangulated_generators

d23f020

fix

86e878c

add note in docstring

4976ce1

fix

c0376ff

mk_all

8a6f349

justus-springer added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 24, 2026

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

joelriou reviewed Mar 24, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/ObjectProperty/Shift.lean Outdated

split into new file

52e9ebe

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 25, 2026

justus-springer mentioned this pull request Mar 31, 2026

[Merged by Bors] - feat(CategoryTheory/ObjectProperty): add ObjectProperty.Nonempty #37442

Closed

justus-springer removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026

mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 31, 2026

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 3, 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 Apr 3, 2026

Merge branch 'master' into justus/triangulated_generators

e3692a5

mathlib-merge-conflicts 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 Apr 4, 2026

revert _root_ additions

1f2076d

dagurtomas reviewed Apr 10, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Triangulated/Generators.lean Outdated

Comment thread Mathlib/CategoryTheory/Triangulated/Generators.lean Outdated

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

justus-springer and others added 3 commits April 10, 2026 09:52

Update Mathlib/CategoryTheory/Triangulated/Generators.lean

e025862

Co-authored-by: Dagur Asgeirsson <[email protected]>

Update Mathlib/CategoryTheory/Triangulated/Generators.lean

e051aa4

Co-authored-by: Dagur Asgeirsson <[email protected]>

retractClosure_retractClosure

1ec2ce7

justus-springer removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 10, 2026

Merge branch 'master' into justus/triangulated_generators

ac4ada5

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

mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 13, 2026

mathlib-bors bot changed the title ~~feat(CategoryTheory/Triangulated): Generators in triangulated categories~~ [Merged by Bors] - feat(CategoryTheory/Triangulated): Generators in triangulated categories Apr 13, 2026

mathlib-bors bot closed this Apr 13, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory/Triangulated): Generators in triangulated categories#37046

[Merged by Bors] - feat(CategoryTheory/Triangulated): Generators in triangulated categories#37046
justus-springer wants to merge 26 commits intoleanprover-community:masterfrom
justus-springer:justus/triangulated_generators

justus-springer commented Mar 23, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 23, 2026 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

mathlib-dependent-issues bot commented Apr 3, 2026

Uh oh!

mathlib-merge-conflicts bot commented Apr 3, 2026

Uh oh!

Uh oh!

Uh oh!

robin-carlier commented Apr 13, 2026

Uh oh!

github-actions bot commented Apr 13, 2026

Uh oh!

joelriou commented Apr 13, 2026

Uh oh!

mathlib-bors bot commented Apr 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

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

Uh oh!

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 410d5afde2

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

mathlib-dependent-issues bot commented Apr 3, 2026

Uh oh!

mathlib-merge-conflicts bot commented Apr 3, 2026

Uh oh!

Uh oh!

Uh oh!

robin-carlier commented Apr 13, 2026

Uh oh!

github-actions bot commented Apr 13, 2026

Uh oh!

joelriou commented Apr 13, 2026

Uh oh!

mathlib-bors bot commented Apr 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

justus-springer commented Mar 23, 2026 •

edited

Loading

github-actions bot commented Mar 23, 2026 •

edited

Loading