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.

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

[Merged by Bors] - feat: the derived category of an abelian category #11806

Closed
wants to merge 136 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Mar 31, 2024

The derived category of an abelian category is defined and it is shown that it is a triangulated category.


Open in Gitpod

joelriou and others added 30 commits March 27, 2024 10:52
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 6, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

@@ -230,7 +230,7 @@ lemma mem_homologicalKernel_W_iff {X Y : C} (f : X ⟶ Y) :
simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]
constructor
· intro h n
obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by omega
obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

(Note: with omega, irrelevant unnecessary variables were added to the lemma. Using simp solves this issue.)

Copy link

github-actions bot commented Jun 7, 2024

PR summary

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.CategoryTheory.Triangulated.Subcategory 958 999 +41 (+4.28%)
Mathlib.CategoryTheory.Triangulated.HomologicalFunctor 1048 1055 +7 (+0.67%)

Diff of declarations

+ DerivedCategory
+ HasDerivedCategory.standard
+ Q
+ Qh
+ instance (n : ℤ) : (shiftFunctor (DerivedCategory C) n).Additive
+ instance : Category.{w} (DerivedCategory C)
+ instance : ClosedUnderIsomorphisms (subcategoryAcyclic C).P
+ instance : HasShift (DerivedCategory C) ℤ
+ instance : HasZeroObject (DerivedCategory C)
+ instance : IsTriangulated (DerivedCategory C)
+ instance : Preadditive (DerivedCategory C)
+ instance : Pretriangulated (DerivedCategory C)
+ instance : Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))
+ instance : Qh.IsLocalization (HomotopyCategory.subcategoryAcyclic C).W
+ instance : S.W.IsCompatibleWithShift ℤ
+ instance [IsTriangulated C] : S.W.IsCompatibleWithTriangulation
+ mem_subcategoryAcyclic_iff
+ on
+ quasiIso_eq_subcategoryAcyclic_W
+ quotientCompQhIso
+ quotient_obj_mem_subcategoryAcyclic_iff_exactAt
+ should
+ subcategoryAcyclic
++ instance : (Q (C
+++ instance : (Qh (C

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>

@erdOne
Copy link
Member

erdOne commented Jun 7, 2024

Thanks!
maintainer merge

Copy link

github-actions bot commented Jun 7, 2024

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

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 🎉 This is a massive milestone! Huge kudos!

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 Jun 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 8, 2024
The derived category of an abelian category is defined and it is shown that it is a triangulated category.



Co-authored-by: Joël Riou <[email protected]>
@mathlib-bors
Copy link
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 derived category of an abelian category [Merged by Bors] - feat: the derived category of an abelian category Jun 8, 2024
@mathlib-bors mathlib-bors bot closed this Jun 8, 2024
@mathlib-bors mathlib-bors bot deleted the derived-category branch June 8, 2024 04:57
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
The derived category of an abelian category is defined and it is shown that it is a triangulated category.



Co-authored-by: Joël Riou <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-category-theory Category theory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants