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 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₁.

source
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
source
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
source
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 : ℕ) :
(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) ⋯).Exact

Alternative formulation of covariant_sequence_exact₂

source
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₁) :
(ShortComplex.mk (AddCommGrp.ofHom ((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} [Category.{v, u} C] [Abelian C] [HasExt C] (X : C) {S : ShortComplex C} (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
(ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.postcomp X h)) (AddCommGrp.ofHom ((mk₀ S.f).postcomp X ⋯)) ⋯).Exact

Alternative formulation of covariant_sequence_exact₁

source
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₁) :
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} [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
    source
    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₁) :
    ∃ (x₃ : Ext X S.X₃ n₀), x₃.comp hS.extClass hn₀ = x₁
    source
    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.g) ⋯ = 0) :
    ∃ (x₁ : Ext X S.X₁ n), x₁.comp (mk₀ S.f) ⋯ = x₂
    source
    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) :
    ∃ (x₂ : Ext X S.X₂ n₀), x₂.comp (mk₀ S.g) ⋯ = x₃
    source
    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) :
    CategoryStruct.comp ((DerivedCategory.singleFunctor C 0).map f) x.hom = ((mk₀ f).comp x ⋯).hom
    source
    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
    source
    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 : ℕ) :
    (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).Exact

    Alternative formulation of contravariant_sequence_exact₂

    source
    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₁) :
    (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) (AddCommGrp.ofHom (hS.extClass.precomp Y h)) ⋯).Exact

    Alternative formulation of contravariant_sequence_exact₁

    source
    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₁) :
    (ShortComplex.mk (AddCommGrp.ofHom (hS.extClass.precomp Y h)) (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) ⋯).Exact

    Alternative formulation of contravariant_sequence_exact₃

    source
    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₁) :
    ComposableArrows AddCommGrp 5

    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
      source
      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
      source
      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) :
      ∃ (x₂ : Ext S.X₂ Y n₀), (mk₀ S.f).comp x₂ ⋯ = x₁
      source
      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.f).comp x₂ ⋯ = 0) :
      ∃ (x₁ : Ext S.X₃ Y n), (mk₀ S.g).comp x₁ ⋯ = x₂
      source
      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₁) :
      ∃ (x₁ : Ext S.X₁ Y n₀), hS.extClass.comp x₁ hn₀ = x₃