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: the abelian group structure on Ext-groups in abelian categories #14496

Closed
wants to merge 101 commits into from
Closed

[Merged by Bors] - feat: the abelian group structure on Ext-groups in abelian categories #14496

wants to merge 101 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Jul 7, 2024

In this PR, we construct the abelian group structure on Ext-groups.

Open in Gitpod

joelriou and others added 30 commits June 8, 2024 15:25
@joelriou
feat: small types of morphisms in the localized category
dcad359
@joelriou
added compatibilities
9d5cdc1
@joelriou
fixed imports
08077d0
@joelriou
Merge remote-tracking branch 'origin' into has-small-localized-hom
75e6713
@joelriou
added note
88d42d8
@joelriou
feat: the mapping cone of a monomorphism, up to a quasi-isomorphism
aa484c1
@joelriou
updated Mathlib.lean
467fa14
@joelriou
wip
b2f24ea
@joelriou @github-actions
Update Mathlib/Algebra/Homology/Refinements.lean
18af13e 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou
removed a sorry
fab421a
@joelriou
removed a sorry
3b5de64
@joelriou
removed sorries
89fe3b0
@joelriou
added docstring
a0d590b
@joelriou
fixed def/lemma
872879a
@joelriou
s/refine'/refine/
16e77b9
@joelriou
feat: the distinguished triangle attached to a short exact sequence o…
683b743 
…f complexes
@joelriou
Merge remote-tracking branch 'origin' into dist-triangle-ses2
b7d1af2
@joelriou
feat: more API for commutation of functors with shifts
42f76c1
@joelriou
Merge remote-tracking branch 'origin/commshift-comp' into dist-triang…
495efc6 
…le-ses2
@joelriou
feat(Algebra/Homology) the single complex functor preserves (co)limits
127ca96
@joelriou
Merge remote-tracking branch 'origin' into single-triangle
cd70471
@joelriou
Merge remote-tracking branch 'origin/single-preserves-limits' into si…
d60e280 
…ngle-triangle
@joelriou
feat: the distinguished triangle attached to a short exact sequence
365b9df
@joelriou
Merge remote-tracking branch 'origin' into has-small-localized-hom
3d361e0
@joelriou
added docstring
285e3e7
@joelriou
more API
e119185
@joelriou
wip
7ebda0b
@joelriou
Merge remote-tracking branch 'origin/commshift-comp' into has-small-l…
40b7ed7 
…ocalized-shifted-hom
@joelriou
wip
bcdfe45
@joelriou
removed a sorry
95c8bdf
@joelriou joelriou added the t-category-theory Category theory label Jul 7, 2024
@github-actions GitHub Actions
Copy link

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

PR summary ef3ae7270a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ add_comp
+ add_hom
+ biprod_ext
+ comp_add
+ comp_mk₀_id
+ comp_zero
+ equiv_mk₀
+ ext_iff
+ homAddEquiv
+ homAddEquiv_apply
+ instance : AddCommGroup (Ext X Y n)
+ mk₀_hom
+ mk₀_id_comp
+ neg_hom
+ zero_comp
+ zero_hom
++ comp_neg
++ mk₀
++ mk₀_comp_mk₀
++ mk₀_comp_mk₀_assoc
++ mk₀_zero
++ neg_comp

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 and others added 2 commits July 7, 2024 20:42
@joelriou @github-actions
Update Mathlib/Algebra/Homology/DerivedCategory/Ext.lean
deefeb7 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou
added docstring
c684ad6
@joelriou joelriou mentioned this pull request Jul 7, 2024
Closed
7 tasks
@joelriou joelriou mentioned this pull request Jul 8, 2024
Closed
3 tasks
@joelriou joelriou changed the title feat: abelian group structure on Ext-groups in abelian categories feat: the abelian group structure on Ext-groups in abelian categories Jul 8, 2024
@kim-em
Copy link
Contributor

kim-em commented Jul 15, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 15, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 15, 2024
@joelriou
feat: the abelian group structure on Ext-groups in abelian categories (…
f972435 
…#14496)

In this PR, we construct the abelian group structure on `Ext`-groups.



Co-authored-by: Joël Riou <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: the abelian group structure on Ext-groups in abelian categories [Merged by Bors] - feat: the abelian group structure on Ext-groups in abelian categories Jul 15, 2024
@mathlib-bors mathlib-bors bot closed this Jul 15, 2024
@mathlib-bors mathlib-bors bot deleted the small-ext-derived-category-addcommgroup branch July 15, 2024 22:23
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Julian-Kuelshammer Julian-Kuelshammer Julian-Kuelshammer 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.
3 participants
@joelriou @kim-em @Julian-Kuelshammer