Skip to content

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

Closed
joelriou wants to merge 101 commits intomasterfrom
small-ext-derived-category-addcommgroup
Closed

[Merged by Bors] - feat: the abelian group structure on Ext-groups in abelian categories#14496
joelriou wants to merge 101 commits intomasterfrom
small-ext-derived-category-addcommgroup

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@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
Copy link
Copy Markdown

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
Julian-Kuelshammer
Julian-Kuelshammer reviewed Jul 8, 2024
View reviewed changes
@joelriou @Julian-Kuelshammer
Update Mathlib/Algebra/Homology/DerivedCategory/Ext.lean
69ce8aa 
Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
@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
Copy Markdown
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 <37772949+joelriou@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
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

1 more reviewer

@Julian-Kuelshammer Julian-Kuelshammer Julian-Kuelshammer left review comments

Reviewers whose approvals may not affect merge requirements

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