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₁.
theorem
CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
[HasDerivedCategory C]
{X Y Z : C}
{n : ℕ}
(x : Ext X Y n)
(f : Y ⟶ Z)
:
CategoryStruct.comp x.hom ((shiftFunctor (DerivedCategory C) ↑n).map ((DerivedCategory.singleFunctor C 0).map f)) = (x.comp (mk₀ f) ⋯).hom
theorem
CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
[HasDerivedCategory C]
{X : C}
{n₀ : ℕ}
(x : Ext X S.X₃ n₀)
{n₁ : ℕ}
(h : n₀ + 1 = n₁)
:
(ConcreteCategory.hom
((preadditiveCoyoneda.obj (Opposite.op ((DerivedCategory.singleFunctor C 0).obj X))).homologySequenceδ
hS.singleTriangle ↑n₀ ↑n₁ ⋯))
x.hom = (x.comp hS.extClass h).hom
theorem
CategoryTheory.Abelian.Ext.covariant_sequence_exact₂'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(X : C)
{S : ShortComplex C}
(hS : S.ShortExact)
(n : ℕ)
:
{ X₁ := AddCommGrp.of (Ext X S.X₁ n), X₂ := AddCommGrp.of (Ext X S.X₂ n), X₃ := AddCommGrp.of (Ext X S.X₃ n),
f := AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯), g := AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯), zero := ⋯ }.Exact
Alternative formulation of covariant_sequence_exact₂
theorem
CategoryTheory.Abelian.Ext.covariant_sequence_exact₃'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(X : C)
{S : ShortComplex C}
(hS : S.ShortExact)
(n₀ n₁ : ℕ)
(h : n₀ + 1 = n₁)
:
{ X₁ := AddCommGrp.of (Ext X S.X₂ n₀), X₂ := AddCommGrp.of (Ext X S.X₃ n₀), X₃ := AddCommGrp.of (Ext X S.X₁ n₁),
f := AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯), g := AddCommGrp.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.Exact
Alternative formulation of covariant_sequence_exact₃
theorem
CategoryTheory.Abelian.Ext.covariant_sequence_exact₁'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(X : C)
{S : ShortComplex C}
(hS : S.ShortExact)
(n₀ n₁ : ℕ)
(h : n₀ + 1 = n₁)
:
{ X₁ := AddCommGrp.of (Ext X S.X₃ n₀), X₂ := AddCommGrp.of (Ext X S.X₁ n₁), X₃ := AddCommGrp.of (Ext X S.X₂ n₁),
f := AddCommGrp.ofHom (hS.extClass.postcomp X h), g := AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.Exact
Alternative formulation of covariant_sequence_exact₁
noncomputable def
CategoryTheory.Abelian.Ext.covariantSequence
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(X : C)
{S : ShortComplex C}
(hS : S.ShortExact)
(n₀ n₁ : ℕ)
(h : n₀ + 1 = n₁)
:
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
theorem
CategoryTheory.Abelian.Ext.covariantSequence_exact
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(X : C)
{S : ShortComplex C}
(hS : S.ShortExact)
(n₀ n₁ : ℕ)
(h : n₀ + 1 = n₁)
:
(covariantSequence X hS n₀ n₁ h).Exact
theorem
CategoryTheory.Abelian.Ext.covariant_sequence_exact₁
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(X : C)
{S : ShortComplex C}
(hS : S.ShortExact)
{n₁ : ℕ}
(x₁ : Ext X S.X₁ n₁)
(hx₁ : x₁.comp (mk₀ S.f) ⋯ = 0)
{n₀ : ℕ}
(hn₀ : n₀ + 1 = n₁)
:
theorem
CategoryTheory.Abelian.Ext.covariant_sequence_exact₃
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
(X : C)
{S : ShortComplex C}
(hS : S.ShortExact)
{n₀ : ℕ}
(x₃ : Ext X S.X₃ n₀)
{n₁ : ℕ}
(hn₁ : n₀ + 1 = n₁)
(hx₃ : x₃.comp hS.extClass hn₁ = 0)
:
theorem
CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
[HasDerivedCategory C]
{X Y Z : C}
(f : X ⟶ Y)
{n : ℕ}
(x : Ext Y Z n)
:
theorem
CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
[HasDerivedCategory C]
{Y : C}
{n₀ : ℕ}
(x : Ext S.X₁ Y n₀)
{n₁ : ℕ}
(h : 1 + n₀ = n₁)
:
(ConcreteCategory.hom
((preadditiveYoneda.obj ((DerivedCategory.singleFunctor C 0).obj Y)).homologySequenceδ
((Pretriangulated.triangleOpEquivalence (DerivedCategory C)).functor.obj (Opposite.op hS.singleTriangle)) ↑n₀
↑n₁ ⋯))
x.hom = (hS.extClass.comp x h).hom
theorem
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
(Y : C)
(n : ℕ)
:
{ X₁ := AddCommGrp.of (Ext S.X₃ Y n), X₂ := AddCommGrp.of (Ext S.X₂ Y n), X₃ := AddCommGrp.of (Ext S.X₁ Y n),
f := AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯), g := AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.Exact
Alternative formulation of contravariant_sequence_exact₂
theorem
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
(Y : C)
(n₀ n₁ : ℕ)
(h : 1 + n₀ = n₁)
:
{ X₁ := AddCommGrp.of (Ext S.X₂ Y n₀), X₂ := AddCommGrp.of (Ext S.X₁ Y n₀), X₃ := AddCommGrp.of (Ext S.X₃ Y n₁),
f := AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯), g := AddCommGrp.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact
Alternative formulation of contravariant_sequence_exact₁
theorem
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃'
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
(Y : C)
(n₀ n₁ : ℕ)
(h : 1 + n₀ = n₁)
:
{ X₁ := AddCommGrp.of (Ext S.X₁ Y n₀), X₂ := AddCommGrp.of (Ext S.X₃ Y n₁), X₃ := AddCommGrp.of (Ext S.X₂ Y n₁),
f := AddCommGrp.ofHom (hS.extClass.precomp Y h), g := AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact
Alternative formulation of contravariant_sequence_exact₃
noncomputable def
CategoryTheory.Abelian.Ext.contravariantSequence
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
(Y : C)
(n₀ n₁ : ℕ)
(h : 1 + n₀ = n₁)
:
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
theorem
CategoryTheory.Abelian.Ext.contravariantSequence_exact
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
(Y : C)
(n₀ n₁ : ℕ)
(h : 1 + n₀ = n₁)
:
(contravariantSequence hS Y n₀ n₁ h).Exact
theorem
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
(Y : C)
{n₀ : ℕ}
(x₁ : Ext S.X₁ Y n₀)
{n₁ : ℕ}
(hn₁ : 1 + n₀ = n₁)
(hx₁ : hS.extClass.comp x₁ hn₁ = 0)
:
theorem
CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃
{C : Type u}
[Category.{v, u} C]
[Abelian C]
[HasExt C]
{S : ShortComplex C}
(hS : S.ShortExact)
(Y : C)
{n₁ : ℕ}
(x₃ : Ext S.X₃ Y n₁)
(hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0)
{n₀ : ℕ}
(hn₀ : 1 + n₀ = n₁)
: