Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian #12721

Closed
wants to merge 39 commits into from
Closed

[Merged by Bors] - feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian #12721

wants to merge 39 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented May 7, 2024 •
edited
Loading

@joelriou
feat(CategoryTheory): triangulated subcategories
2865b80
@joelriou
feat(CategoryTheory/Triangulated): homological functors
58bd6d3
@joelriou
fixing Mathlib.lean
0fa5280
@joelriou
coding style
05af53c
@joelriou
one more constructor
6da2115
@joelriou
feat: the homological functor on the homotopy category of an abelian …
42656e4 
…category
@joelriou
cleaning up
73051a1
@joelriou
added docstrings
bd494bb
@joelriou
Merge remote-tracking branch 'origin' into triangulated-subcategory
7225e05
@joelriou
followed @TwoFX suggestions
fa0c448
@joelriou
replaces sets by predicates
7e48b5f
@joelriou
fixed coding style
dd4cd80
@joelriou
added isIso variants
f05ab7b
@joelriou
Merge remote-tracking branch 'origin/triangulated-subcategory' into h…
dbde1b9 
…omological-functor
@joelriou
fixed the build
a07dd2f
@joelriou
Merge remote-tracking branch 'origin/homological-functor' into homoto…
7f09d1e 
…py-category-homological-functor
@joelriou
Merge remote-tracking branch 'origin' into homotopy-category-homologi…
280bb5f 
…cal-functor
@joelriou
Merge remote-tracking branch 'origin' into triangulated-subcategory
5de084d
@joelriou
Merge remote-tracking branch 'origin' into triangulated-subcategory
d5c8df7
@joelriou
fixing names
8d93376
@joelriou
fixed def of isoClosure
447e037
@joelriou
fixed names
79edf14
@joelriou
Merge remote-tracking branch 'origin/triangulated-subcategory' into h…
4f5cd42 
…omological-functor
@joelriou
Merge remote-tracking branch 'origin/homological-functor' into homoto…
14e636f 
…py-category-homological-functor
@joelriou
Merge remote-tracking branch 'origin' into homotopy-category-homologi…
73fd877 
…cal-functor
@joelriou
typo
f355a73
@joelriou
feat(Algebra/Category/ModuleCat): the category of preheaves of module…
7c81f56 
…s has colimits
@joelriou
fixes
d60cab1
@joelriou
one sorry left
e7900a9
@joelriou
finished the proof
e22a2e3
@joelriou joelriou added the t-category-theory Category theory label May 7, 2024
@joelriou joelriou mentioned this pull request May 7, 2024
Closed
2 tasks
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (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 May 7, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels May 10, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@erdOne erdOne changed the title feat(Algebra/Homology/ModuleCat): the category of presheaves of modules is abelian feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian May 18, 2024
@erdOne
Copy link
Member

erdOne commented May 18, 2024

Thanks!
maintainer merge

@github-actions GitHub Actions
Copy link

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

jcommelin
jcommelin reviewed May 18, 2024
View reviewed changes
Copy link
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

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 18, 2024
@joelriou
feat(Algebra/Category/ModuleCat): the category of presheaves of modul…
b210748 
…es is abelian (#12721)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian [Merged by Bors] - feat(Algebra/Category/ModuleCat): the category of presheaves of modules is abelian May 18, 2024
@mathlib-bors mathlib-bors bot closed this May 18, 2024
@mathlib-bors mathlib-bors bot deleted the modulecat-presheaf-abelian branch May 18, 2024 09:44
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@joelriou @callesonne
feat(Algebra/Category/ModuleCat): the category of presheaves of modul…
52a9e89 
…es is abelian (#12721)
js2357 pushed a commit that referenced this pull request Jun 18, 2024
@joelriou @js2357
feat(Algebra/Category/ModuleCat): the category of presheaves of modul…
68f8e58 
…es is abelian (#12721)
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

Assignees
No one assigned
Labels
maintainer-merge 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 @leanprover-community-mathlib4-bot @erdOne @jcommelin