Long exact sequences of Ext-groups #
In this file, we obtain the covariant long exact sequence of Ext when n₀ + 1 = 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₁ → Ext X S.X₃ n₁
when S is a short exact short complex in an abelian category C, n₀ + 1 = n₁ and X : C.
Similarly, if Y : C, there is a contravariant long exact sequence :
Ext S.X₃ Y n₀ → Ext S.X₂ Y n₀ → Ext S.X₁ Y n₀ → Ext S.X₃ Y n₁ → Ext S.X₂ Y n₁ → Ext S.X₁ Y n₁.
We first phrase these exact sequences by using the pre- or post-composition with
the class in Ext S.X₃ S.X₁ 1 attached to the short exact sequence.
Our understanding is that for the covariant exact long exact sequence,
the morphism Ext X S.X₃ n₀ → Ext X S.X₁ n₁ we obtain in this way is the connecting
homomorphism from [Con00]. However, for the contravariant
long exact sequence, the precomposition Ext S.X₁ Y n₀ → Ext S.X₃ Y n₁ with the class
in Ext S.X₃ S.X₁ 1 is the standard connecting homomorphism only up to the multiplication
with the sign (-1) ^ n₁. This is the reason why we introduce a definition Ext.δ
which is the "correct" connecting homomorphism, and the exactness properties are
also restated using Ext.δ instead of the pre-composition with the class in Ext S.X₃ S.X₁ 1.
References #
Alternative formulation of covariant_sequence_exact₂
Alternative formulation of covariant_sequence_exact₃
Alternative formulation of covariant_sequence_exact₁
Given a short exact short complex S in an abelian category C and an object X : C,
this is the long exact sequence
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₁
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alternative formulation of contravariant_sequence_exact₂
Alternative formulation of contravariant_sequence_exact₁
Alternative formulation of contravariant_sequence_exact₃
Given a short exact short complex S in an abelian category C and an object Y : C,
this is the long exact sequence
Ext S.X₃ Y n₀ → Ext S.X₂ Y n₀ → Ext S.X₁ Y n₀ → Ext S.X₃ Y n₁ → Ext S.X₂ Y n₁ → Ext S.X₁ Y n₁
when 1 + n₀ = n₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The standard connecting homomorphism Ext S.X₁ Y n₀ →+ Ext S.X₃ Y n₁
for the contravariant long sequence of Ext when n₀ + 1 = n₁ and S is a
short exact sequence. This definition should be consistent with [Con00].
It is obtained by multiplying by (-1) ^ n₁ the precomposition
with hS.extClass : Ext S.X₃ X₁ 1.
Equations
- CategoryTheory.Abelian.Ext.δ hS n₀ n₁ h = { toFun := fun (e : CategoryTheory.Abelian.Ext S.X₁ Y n₀) => (↑n₁).negOnePow • hS.extClass.comp e ⋯, map_zero' := ⋯, map_add' := ⋯ }