Skip to content

[Merged by Bors] - feat(CategoryTheory/Adjunction/Additive): adjunctions between additive functors #20083

Closed
smorel394 wants to merge 24 commits intomasterfrom
SM.adjunctionAdditive
Closed

[Merged by Bors] - feat(CategoryTheory/Adjunction/Additive): adjunctions between additive functors #20083
smorel394 wants to merge 24 commits intomasterfrom
SM.adjunctionAdditive

Conversation

@smorel394
Copy link
Copy Markdown
Collaborator

@smorel394 smorel394 commented Dec 19, 2024 •
edited
Loading

This provides some results and constructions for adjunctions between functors on preadditive categories:

  • If one of the adjoint functors is additive, so is the other.
  • If one of the adjoint functors is additive, the equivalence Adjunction.homEquiv lifts to
    an additive equivalence Adjunction.homAddEquiv.
  • We also give a version of this additive equivalence as an isomorphism of preadditiveYoneda
    functors (analogous to Adjunction.compYonedaIso), in
    Adjunction.compPreadditiveYonedaIso.

Open in Gitpod

@smorel394 smorel394 added the t-category-theory Category theory label Dec 19, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 19, 2024 •
edited
Loading

PR summary 6d70f2e362

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Adjunction.Additive (new file) 808

Declarations diff

+ compPreadditiveYonedaIso
+ compPreadditiveYonedaIso_hom_app_app_apply
+ compPreadditiveYonedaIso_inv_app_app_apply
+ homAddEquiv
+ homAddEquiv_add
+ homAddEquiv_apply
+ homAddEquiv_neg
+ homAddEquiv_sub
+ homAddEquiv_symm_add
+ homAddEquiv_symm_apply
+ homAddEquiv_symm_neg
+ homAddEquiv_symm_sub
+ homAddEquiv_symm_zero
+ homAddEquiv_zero
+ left_adjoint_additive
+ right_adjoint_additive

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

joelriou
joelriou reviewed Dec 19, 2024
View reviewed changes
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 19, 2024
@smorel394 smorel394 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 25, 2024
@smorel394 smorel394 mentioned this pull request Dec 26, 2024
Closed
2 tasks
joelriou
joelriou reviewed Dec 26, 2024
View reviewed changes
joelriou
joelriou reviewed Dec 26, 2024
View reviewed changes
joelriou
joelriou reviewed Dec 26, 2024
View reviewed changes
joelriou
joelriou reviewed Dec 26, 2024
View reviewed changes
joelriou
joelriou reviewed Dec 26, 2024
View reviewed changes
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 26, 2024
@smorel394 @joelriou
Update Mathlib/CategoryTheory/Adjunction/Additive.lean
36a89ac 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
smorel394 and others added 4 commits December 26, 2024 19:49
@smorel394 @joelriou
Update Mathlib/CategoryTheory/Adjunction/Additive.lean
8fabfcc 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@smorel394 @joelriou
Update Mathlib/CategoryTheory/Adjunction/Additive.lean
dc2e483 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@smorel394 @joelriou
Update Mathlib/CategoryTheory/Adjunction/Additive.lean
c6ef2da 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
shorten proofs
4da4bab
@smorel394 smorel394 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 26, 2024
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 27, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Dec 27, 2024

Could you also edit the PR description so as to take into account the changes.

@smorel394 smorel394 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 27, 2024
@smorel394
Copy link
Copy Markdown
Collaborator Author

smorel394 commented Dec 27, 2024

Could you also edit the PR description so as to take into account the changes.

Done.

@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Dec 27, 2024

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 27, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 27, 2024
@smorel394
feat(CategoryTheory/Adjunction/Additive): adjunctions between additiv…
cdf32a0 
…e functors (#20083)

This provides some results and constructions for adjunctions between functors on preadditive categories:
* If one of the adjoint functors is additive, so is the other.
* If one of the adjoint functors is additive, the equivalence `Adjunction.homEquiv` lifts to
an additive equivalence `Adjunction.homAddEquiv`.
* We also give a version of this additive equivalence as an isomorphism of `preadditiveYoneda`
functors (analogous to `Adjunction.compYonedaIso`), in
`Adjunction.compPreadditiveYonedaIso`.



Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Adjunction/Additive): adjunctions between additive functors [Merged by Bors] - feat(CategoryTheory/Adjunction/Additive): adjunctions between additive functors Dec 27, 2024
@mathlib-bors mathlib-bors bot closed this Dec 27, 2024
@mathlib-bors mathlib-bors bot deleted the SM.adjunctionAdditive branch December 27, 2024 13:10
mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025
@smorel394
feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a …
9f47fc5 
…triangulated functor is triangulated (#20255)

If a functor `F : C ⥤ D` between pretriangulated categories is triangulated, and if we
have an adjunction `F ⊣ G`, then `G` is also a triangulated functor.

We deduce that, if `E : C ≌ D` is an equivalence of pretriangulated categories, then
`E.functor` is triangulated if and only if `E.inverse` is triangulated.

TODO: The case of left adjoints.

- [x] depends on: #20083 [the adjoint of an additive functor is additive]
- [ ] depends on: #20337



Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou 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.

2 participants

@smorel394 @joelriou