Skip to content

[Merged by Bors] - feat(CategoryTheory/Triangulated/TStucture): induced t-structures#35367

Closed
joelriou wants to merge 12 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-1-induced
Closed

[Merged by Bors] - feat(CategoryTheory/Triangulated/TStucture): induced t-structures#35367
joelriou wants to merge 12 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-1-induced

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Feb 15, 2026 •
edited
Loading

This PR introduces a typeclass P.HasInducedTStructure t when P is a triangulated subcategory of a (pre)triangulated category C and t a t-structure on C. This essentially says that P is stable by the truncations. In this situation, we define the induced t-structure on the full subcategory defined by P. In particular, this applies to bounded above/bounded below/bounded objects for a given t-structure.

Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Feb 15, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 15, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 15, 2026 •
edited
Loading

PR summary b9242563f9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Triangulated.TStructure.Induced (new file) 1166

Declarations diff

+ HasInducedTStructure
+ HasInducedTStructure.mk'
+ instance (P P' : ObjectProperty C) [P.IsTriangulated] [P'.IsTriangulated] (t : TStructure C)
+ instance : t.bounded.HasInducedTStructure t := by
+ instance : t.minus.HasInducedTStructure t
+ instance : t.plus.HasInducedTStructure t
+ mem_of_hasInductedTStructure
+ onBounded
+ onMinus
+ onPlus
+ tStructure
+ tStructure_isGE_iff
+ tStructure_isLE_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.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type
9986 1 backward.isDefEq

Current commit 1244fec5bc
Reference commit b9242563f9

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

@joelriou joelriou mentioned this pull request Feb 15, 2026
Open
43 tasks
@mathlib-dependent-issues 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 Feb 15, 2026
@mathlib-merge-conflicts 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 Feb 21, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Feb 21, 2026

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

@joelriou joelriou removed WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 3, 2026
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 3, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 3, 2026

This PR/issue depends on:

robin-carlier
robin-carlier reviewed Mar 3, 2026
View reviewed changes
@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 3, 2026
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 3, 2026
robin-carlier
robin-carlier reviewed Mar 3, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 3, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 3, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Mar 3, 2026

Thanks!

bors merge

@mathlib-triage 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 Mar 3, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 3, 2026
@joelriou
feat(CategoryTheory/Triangulated/TStucture): induced t-structures (#3…
6a27318 
…5367)

This PR introduces a typeclass `P.HasInducedTStructure t` when `P` is a triangulated subcategory of a (pre)triangulated category `C` and `t` a t-structure on `C`. This essentially says that `P` is stable by the truncations. In this situation, we define the induced t-structure on the full subcategory defined by `P`. In particular, this applies to bounded above/bounded below/bounded objects for a given t-structure.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 3, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Triangulated/TStucture): induced t-structures [Merged by Bors] - feat(CategoryTheory/Triangulated/TStucture): induced t-structures Mar 3, 2026
@mathlib-bors mathlib-bors bot closed this Mar 3, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@joelriou @xroblot
feat(CategoryTheory/Triangulated/TStucture): induced t-structures (le…
fbcd680 
…anprover-community#35367)

This PR introduces a typeclass `P.HasInducedTStructure t` when `P` is a triangulated subcategory of a (pre)triangulated category `C` and `t` a t-structure on `C`. This essentially says that `P` is stable by the truncations. In this situation, we define the induced t-structure on the full subcategory defined by `P`. In particular, this applies to bounded above/bounded below/bounded objects for a given t-structure.
pevogam pushed a commit to pevogam/mathlib4 that referenced this pull request Mar 19, 2026
@joelriou @pevogam
feat(CategoryTheory/Triangulated/TStucture): induced t-structures (le…
eece4ce 
…anprover-community#35367)

This PR introduces a typeclass `P.HasInducedTStructure t` when `P` is a triangulated subcategory of a (pre)triangulated category `C` and `t` a t-structure on `C`. This essentially says that `P` is stable by the truncations. In this situation, we define the induced t-structure on the full subcategory defined by `P`. In particular, this applies to bounded above/bounded below/bounded objects for a given t-structure.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@robin-carlier robin-carlier robin-carlier left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @riccardobrasca @robin-carlier