Documentation

Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Long exact sequences of Ext-groups #

In this file, we obtain the covariant long exact sequence of Ext: 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.

source
theorem CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] [HasDerivedCategory C] {X : C} {Y : C} {Z : C} {n : ℕ} (x : CategoryTheory.Abelian.Ext X Y n) (f : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp x.hom ((CategoryTheory.shiftFunctor (DerivedCategory C) ↑n).map ((DerivedCategory.singleFunctor C 0).map f)) = (x.comp (CategoryTheory.Abelian.Ext.mk₀ f) ⋯).hom
source
theorem CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [HasDerivedCategory C] {X : C} {n₀ : ℕ} (x : CategoryTheory.Abelian.Ext X S.X₃ n₀) {n₁ : ℕ} (h : n₀ + 1 = n₁) :
((CategoryTheory.preadditiveCoyoneda.obj (Opposite.op ((DerivedCategory.singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯) x.hom = (x.comp hS.extClass h).hom
source
theorem CategoryTheory.Abelian.Ext.covariant_sequence_exact₂' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n : ℕ) :
(CategoryTheory.ShortComplex.mk (AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).postcomp X ⋯)) ⋯).Exact

Alternative formulation of covariant_sequence_exact₂

source
theorem CategoryTheory.Abelian.Ext.covariant_sequence_exact₃' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n₀ : ℕ) (n₁ : ℕ) (h : n₀ + 1 = n₁) :
(CategoryTheory.ShortComplex.mk (AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).postcomp X ⋯)) (AddCommGrp.ofHom (hS.extClass.postcomp X h)) ⋯).Exact

Alternative formulation of covariant_sequence_exact₃

source
theorem CategoryTheory.Abelian.Ext.covariant_sequence_exact₁' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n₀ : ℕ) (n₁ : ℕ) (h : n₀ + 1 = n₁) :
(CategoryTheory.ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X h)) (AddCommGrp.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.f).postcomp X ⋯)) ⋯).Exact

Alternative formulation of covariant_sequence_exact₁

source
noncomputable def CategoryTheory.Abelian.Ext.covariantSequence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n₀ : ℕ) (n₁ : ℕ) (h : n₀ + 1 = n₁) :
CategoryTheory.ComposableArrows AddCommGrp 5

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
    source
    theorem CategoryTheory.Abelian.Ext.covariantSequence_exact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n₀ : ℕ) (n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (CategoryTheory.Abelian.Ext.covariantSequence X hS n₀ n₁ h).Exact
    source
    theorem CategoryTheory.Abelian.Ext.covariant_sequence_exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {n₁ : ℕ} (x₁ : CategoryTheory.Abelian.Ext X S.X₁ n₁) (hx₁ : x₁.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) ⋯ = 0) {n₀ : ℕ} (hn₀ : n₀ + 1 = n₁) :
    ∃ (x₃ : CategoryTheory.Abelian.Ext X S.X₃ n₀), x₃.comp hS.extClass hn₀ = x₁
    source
    theorem CategoryTheory.Abelian.Ext.covariant_sequence_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {n : ℕ} (x₂ : CategoryTheory.Abelian.Ext X S.X₂ n) (hx₂ : x₂.comp (CategoryTheory.Abelian.Ext.mk₀ S.g) ⋯ = 0) :
    ∃ (x₁ : CategoryTheory.Abelian.Ext X S.X₁ n), x₁.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) ⋯ = x₂
    source
    theorem CategoryTheory.Abelian.Ext.covariant_sequence_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {n₀ : ℕ} (x₃ : CategoryTheory.Abelian.Ext X S.X₃ n₀) {n₁ : ℕ} (hn₁ : n₀ + 1 = n₁) (hx₃ : x₃.comp hS.extClass hn₁ = 0) :
    ∃ (x₂ : CategoryTheory.Abelian.Ext X S.X₂ n₀), x₂.comp (CategoryTheory.Abelian.Ext.mk₀ S.g) ⋯ = x₃