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)
:
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
@[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₁
@[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₂
@[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
@[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
@[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₃
@[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
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)
:
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)
Instances For
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
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