[Merged by Bors] - feat: the (covariant) long exact sequence of Ext#14515
[Merged by Bors] - feat: the (covariant) long exact sequence of Ext#14515
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…ocalized-shifted-hom
|
This PR/issue depends on: |
|
As I understand it, the lemmas |
I considers these as alternative formulations: I would keep both in the same namespace, as it is. |
|
Sorry for the delay! maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by dagurtomas. |
|
This is great, thanks! bors merge |
We obtain the long exact sequence of `Ext`-groups `Ext X S.X₁ n₀ → Ext X S.X₂ n₀ → Ext X S.X₃ n₀ → Ext X S.X₁ n₁ → Ext X S.X₂ n₁ → Ext X S.X₃ n₁` when `n₀ + 1 = n₁` and `S` is a short exact short complex in an abelian category. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Build failed: |
|
It was the linter for primed lemma names complaining. I've merged master and added docstrings "alternative formulation of ..." to them, are you happy with this @joelriou? Are these docstrings good enough to justify the primed names? |
Thanks! This is good to me. |
|
bors merge |
We obtain the long exact sequence of `Ext`-groups `Ext X S.X₁ n₀ → Ext X S.X₂ n₀ → Ext X S.X₃ n₀ → Ext X S.X₁ n₁ → Ext X S.X₂ n₁ → Ext X S.X₃ n₁` when `n₀ + 1 = n₁` and `S` is a short exact short complex in an abelian category. Co-authored-by: dagurtomas <dagurtomas@gmail.com> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
We obtain the long exact sequence of `Ext`-groups `Ext X S.X₁ n₀ → Ext X S.X₂ n₀ → Ext X S.X₃ n₀ → Ext X S.X₁ n₁ → Ext X S.X₂ n₁ → Ext X S.X₃ n₁` when `n₀ + 1 = n₁` and `S` is a short exact short complex in an abelian category. Co-authored-by: dagurtomas <dagurtomas@gmail.com> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
We obtain the long exact sequence of
Ext-groupsExt X S.X₁ n₀ → Ext X S.X₂ n₀ → Ext X S.X₃ n₀ → Ext X S.X₁ n₁ → Ext X S.X₂ n₁ → Ext X S.X₃ n₁whenn₀ + 1 = n₁andSis a short exact short complex in an abelian category.