English
The connecting morphism δ in DerivedCategory attached to a short exact sequence S of cochain complexes is defined by the morphisms coming from the mapping cone of S and the standard triangle δ_T.
Русский
Соединяющее отображение δ, соответствующее короткой точной последовательности SES коchain-комплекс, определяется из отображения конуса отображений SES и стандартного треугольника δ_T.
LaTeX
$$$$ \delta_T(n_0,n_1,h) : (\text{object}_1) \to (\text{object}_2) $$$$
Lean4
/-- 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. -/
noncomputable def triangleOfSESδ : Q.obj (S.X₃) ⟶ (Q.obj S.X₁)⟦(1 : ℤ)⟧ :=
have := CochainComplex.mappingCone.quasiIso_descShortComplex hS
inv (Q.map (CochainComplex.mappingCone.descShortComplex S)) ≫
Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Q.commShiftIso (1 : ℤ)).hom.app S.X₁
