Documentation

Mathlib.Algebra.Homology.DerivedCategory.ShortExact

The distinguished triangle attached to a short exact sequence of cochain complexes #

Given a short exact short complex S in the category CochainComplex C ℤ, we construct a distinguished triangle Q.obj S.X₁ ⟶ Q.obj S.X₂ ⟶ Q.obj S.X₃ ⟶ (Q.obj S.X₃)⟦1⟧ in the derived category of C. (See triangleOfSES and triangleOfSES_distinguished.)

source
noncomputable def DerivedCategory.triangleOfSESδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
DerivedCategory.Q.obj S.X₃ ⟶ (CategoryTheory.shiftFunctor (DerivedCategory C) 1).obj (DerivedCategory.Q.obj S.X₁)

The connecting homomorphism Q.obj (S.X₃) ⟶ (Q.obj S.X₁)⟦(1 : ℤ)⟧ in the derived category when S is a short exact short complex of cochain complexes in an abelian category.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem DerivedCategory.triangleOfSES_obj₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    (DerivedCategory.triangleOfSES hS).obj₂ = DerivedCategory.Q.obj S.X₂
    source
    @[simp]
    theorem DerivedCategory.triangleOfSES_obj₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    (DerivedCategory.triangleOfSES hS).obj₃ = DerivedCategory.Q.obj S.X₃
    source
    @[simp]
    theorem DerivedCategory.triangleOfSES_obj₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    (DerivedCategory.triangleOfSES hS).obj₁ = DerivedCategory.Q.obj S.X₁
    source
    @[simp]
    theorem DerivedCategory.triangleOfSES_mor₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    (DerivedCategory.triangleOfSES hS).mor₃ = DerivedCategory.triangleOfSESδ hS
    source
    @[simp]
    theorem DerivedCategory.triangleOfSES_mor₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    (DerivedCategory.triangleOfSES hS).mor₂ = DerivedCategory.Q.map S.g
    source
    @[simp]
    theorem DerivedCategory.triangleOfSES_mor₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    (DerivedCategory.triangleOfSES hS).mor₁ = DerivedCategory.Q.map S.f
    source
    noncomputable def DerivedCategory.triangleOfSES {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)

    The distinguished triangle in the derived category associated to a short exact sequence of cochain complexes.

    Equations
    Instances For
      source
      noncomputable def DerivedCategory.triangleOfSESIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
      DerivedCategory.triangleOfSES hS ≅ DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)

      The triangle triangleOfSES attached to a short exact sequence S of cochain complexes is isomorphism to the standard distinguished triangle associated to the morphism S.f.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem DerivedCategory.triangleOfSES_distinguished {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
        DerivedCategory.triangleOfSES hS ∈ CategoryTheory.Pretriangulated.distinguishedTriangles