triangleOfSESIso — Mathlib

English

The triangle attached to a short exact sequence SESδ is isomorphic to the standard triangle obtained from the corresponding short exact sequence of cochain complexes after applying the single functor.

Русский

К треугольник, связанный с SESδ, изоморфен стандартному треугольнику, получаемому из соответствующей короткой точной последовательности коchain-комплекс после применения единичного функторa.

LaTeX

$$$$ hS.singleTriangle \cong \mathrm{Q.mapTriangle}.obj (\mathrm{CochainComplex.mappingCone.triangle} S.f) $$$$

Lean4

/-- 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`. -/
noncomputable def triangleOfSESIso : triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f) :=
  by
  have := CochainComplex.mappingCone.quasiIso_descShortComplex hS
  refine
    Iso.symm
      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))) ?_
        ?_ ?_)
  · dsimp [triangleOfSES]
    simp only [comp_id, id_comp]
  · dsimp
    simp only [← Q.map_comp, CochainComplex.mappingCone.inr_descShortComplex, id_comp]
  · dsimp [triangleOfSESδ]
    rw [CategoryTheory.Functor.map_id, comp_id, IsIso.hom_inv_id_assoc]

Похожие утверждения