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

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) : Q.obj S.X₃ ⟶ (CategoryTheory.shiftFunctor (DerivedCategory C) 1).obj (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.

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

• DerivedCategory.triangleOfSES hS = CategoryTheory.Pretriangulated.Triangle.mk (DerivedCategory.Q.map S.f) (DerivedCategory.Q.map S.g) (DerivedCategory.triangleOfSESδ hS)

@[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) : (triangleOfSES hS).obj₁ = Q.obj S.X₁

@[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) : (triangleOfSES hS).mor₃ = triangleOfSESδ hS

@[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) : (triangleOfSES hS).mor₁ = Q.map S.f

@[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) : (triangleOfSES hS).obj₂ = Q.obj S.X₂

@[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) : (triangleOfSES hS).obj₃ = Q.obj S.X₃

@[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) : (triangleOfSES hS).mor₂ = Q.map S.g

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) : triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)

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

Equations

• One or more equations did not get rendered due to their size.

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) : triangleOfSES hS ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

noncomputable def DerivedCategory.triangleOfSES.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) : triangleOfSES h₁ ⟶ triangleOfSES h₂

The morphism triangleOfSES h₁ ⟶ triangleOfSES h₂ that is induced by a morphism of short exact sequences of cochain complexes.

Equations

• DerivedCategory.triangleOfSES.map h₁ h₂ f = { hom₁ := DerivedCategory.Q.map f.τ₁, hom₂ := DerivedCategory.Q.map f.τ₂, hom₃ := DerivedCategory.Q.map f.τ₃, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

theorem DerivedCategory.triangleOfSES.map_hom₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) : (map h₁ h₂ f).hom₃ = Q.map f.τ₃

@[simp]

theorem DerivedCategory.triangleOfSES.map_hom₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) : (map h₁ h₂ f).hom₁ = Q.map f.τ₁

@[simp]

theorem DerivedCategory.triangleOfSES.map_hom₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) : (map h₁ h₂ f).hom₂ = Q.map f.τ₂