Skip to content

[Merged by Bors] - feat(CategoryTheory/Triangulated): fully faithful triangulated functors#33887

Closed
joelriou wants to merge 4 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-3-triangulated-functor
Closed

[Merged by Bors] - feat(CategoryTheory/Triangulated): fully faithful triangulated functors#33887
joelriou wants to merge 4 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-3-triangulated-functor

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jan 12, 2026 •
edited
Loading

A fully faithful triangulated functor preserves and reflects distinguished triangles. If the target category satisfies the octahedron axiom (i.e. the category is triangulated), then the source category also does.
This is part of the formalization of spectral sequences #33842.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Jan 12, 2026
@joelriou joelriou mentioned this pull request Jan 12, 2026
Closed
43 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 12, 2026 •
edited
Loading

PR summary 8127997b11

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsTriangulated.of_fully_faithful_triangulated_functor
+ isTriangulated_iff_comp_right
+ map_distinguished_iff

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

robin-carlier
robin-carlier reviewed Jan 22, 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 Jan 22, 2026

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 22, 2026
jcommelin
jcommelin reviewed Jan 23, 2026
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost 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 Jan 23, 2026
mathlib-bors bot pushed a commit that referenced this pull request Jan 23, 2026
@joelriou
feat(CategoryTheory/Triangulated): fully faithful triangulated functo…
b59214f 
…rs (#33887)

A fully faithful triangulated functor preserves and reflects distinguished triangles. If the target category satisfies the octahedron axiom (i.e. the category is triangulated), then the source category also does.
This is part of the formalization of spectral sequences #33842.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 23, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Triangulated): fully faithful triangulated functors [Merged by Bors] - feat(CategoryTheory/Triangulated): fully faithful triangulated functors Jan 23, 2026
@mathlib-bors mathlib-bors bot closed this Jan 23, 2026
goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026
@joelriou @goliath-klein
feat(CategoryTheory/Triangulated): fully faithful triangulated functo…
626f191 
…rs (leanprover-community#33887)

A fully faithful triangulated functor preserves and reflects distinguished triangles. If the target category satisfies the octahedron axiom (i.e. the category is triangulated), then the source category also does.
This is part of the formalization of spectral sequences leanprover-community#33842.
YellPika pushed a commit to YellPika/mathlib4 that referenced this pull request Feb 3, 2026
@joelriou @YellPika
feat(CategoryTheory/Triangulated): fully faithful triangulated functo…
a875acf 
…rs (leanprover-community#33887)

A fully faithful triangulated functor preserves and reflects distinguished triangles. If the target category satisfies the octahedron axiom (i.e. the category is triangulated), then the source category also does.
This is part of the formalization of spectral sequences leanprover-community#33842.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

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

Assignees

@adamtopaz adamtopaz

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.

4 participants

@joelriou @jcommelin @robin-carlier @adamtopaz