map_distinguished_op_exact — Mathlib

English

For an abelian target category A and a homological functor F from Opposite(C) to A, the short complex attached to a distinguished triangle T in C, when mapped oppositely, becomes an exact complex in A.

Русский

Для абелевой целевой категории A и гомологического функторa F: Opposite(C) → A, образ короткого комплекса, связанный с выделенным треугольником T в C, после отображения противоположного направления является точным комплексом в A.

LaTeX

$$(((shortComplexOfDistTriangle T hT).op.map F)).Exact$$

Lean4

theorem map_distinguished_op_exact {A : Type*} [Category A] [Abelian A] (F : Cᵒᵖ ⥤ A) [F.IsHomological] (T : Triangle C)
    (hT : T ∈ distTriang C) : ((shortComplexOfDistTriangle T hT).op.map F).Exact :=
  F.map_distinguished_exact _ (op_distinguished T hT)

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