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

feat: the (contravariant) long exact sequence of Ext #15092

Open
wants to merge 169 commits into
base: master
Choose a base branch
from
Open

feat: the (contravariant) long exact sequence of Ext #15092

wants to merge 169 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Jul 24, 2024 •
edited
Loading

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
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 13, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 23, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 30, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Sep 26, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

mathlib4-dependent-issues-bot commented Sep 26, 2024 •
edited
Loading

This PR/issue depends on:

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 8, 2024
@joelriou joelriou mentioned this pull request Oct 8, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-category-theory Category theory WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@joelriou @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot @dagurtomas