Skip to content

[Merged by Bors] - feat: the single functors from the homotopy category#13600

Closed
joelriou wants to merge 6 commits intomasterfrom
single-functors-homotopy-category
Closed

[Merged by Bors] - feat: the single functors from the homotopy category#13600
joelriou wants to merge 6 commits intomasterfrom
single-functors-homotopy-category

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jun 7, 2024 •
edited
Loading

In this PR, we define the single functors from a preadditive category (with a zero object) to its homotopy category of cochain complexes and show they behave well with respect to shift functors.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Jun 7, 2024
@joelriou joelriou mentioned this pull request Jun 7, 2024
Closed
3 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

No significant changes to the import graph

@erdOne erdOne added the WIP Work in progress label Jun 7, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 7, 2024

Judging by the comments in the code, I have marked this WIP.

@joelriou joelriou added awaiting-review and removed WIP Work in progress labels Jun 7, 2024
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jun 7, 2024

Now this is ready for review.

erdOne
erdOne reviewed Jun 7, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

I think simps can generate some useful lemmas?

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jun 7, 2024

I think simps can generate some useful lemmas?

Actually, in most (future) situations, we do not want these definitions to be unfolded. These are almost like blackboxes which give an additional structure on these categories.

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 7, 2024

Gotcha. Can you record this in the docstring?

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jun 7, 2024

I have just added a comment.

erdOne
erdOne reviewed Jun 7, 2024
View reviewed changes
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024 •
edited
Loading

PR summary

Import changes

No significant changes to the import graph

Declarations diff

+ instance (W : Type*) [Category W] [Preadditive W] [HasZeroObject W] [DecidableEq ι] (j : ι) :
+ instance (j : ι) : (single V c j).PreservesZeroMorphisms
+ instance (n : ℤ) : ((singleFunctors C).functor n).Additive
+ instance (n : ℤ) : (singleFunctor C n).Additive
+ singleFunctorPostcompQuotientIso
+ singleFunctorsPostcompQuotientIso
++ singleFunctors

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 8, 2024
@joelriou joelriou added awaiting-review 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 Jun 8, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 8, 2024

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 8, 2024

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

@github-actions github-actions bot added maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. and removed awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 8, 2024
jcommelin
jcommelin reviewed Jun 8, 2024
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 awaiting-review labels Jun 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 8, 2024
@joelriou
feat: the single functors from the homotopy category (#13600)
d498432 
In this PR, we define the single functors from a preadditive category (with a zero object) to its homotopy category of cochain complexes and show they behave well with respect to shift functors.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: the single functors from the homotopy category [Merged by Bors] - feat: the single functors from the homotopy category Jun 8, 2024
@mathlib-bors mathlib-bors bot closed this Jun 8, 2024
@mathlib-bors mathlib-bors bot deleted the single-functors-homotopy-category branch June 8, 2024 19:30
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@joelriou @AntoineChambert-Loir
feat: the single functors from the homotopy category (#13600)
eddc419 
In this PR, we define the single functors from a preadditive category (with a zero object) to its homotopy category of cochain complexes and show they behave well with respect to shift functors.
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

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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 @erdOne @jcommelin