English
The localization functor Qh cohesively interacts with singleFunctors to realize a coherent family of derived functors parameterized by ℤ, preserving shift compatibility.
Русский
Локализующий функтор Q_h согласован с family-ами singleFunctors, образуя когерентную семью производных функторов, параметризованных ℤ, сохраняющую совместимость со сдвигами.
LaTeX
$$$\text{Qh} \text{ coherently interacts with } \text{singleFunctors}$$$
Lean4
theorem mem_distTriang_iff (T : Triangle (DerivedCategory C)) :
(T ∈ distTriang (DerivedCategory C)) ↔
∃ (X Y : CochainComplex C ℤ) (f : X ⟶ Y),
Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f)) :=
by
constructor
· rintro ⟨T', e, ⟨X, Y, f, ⟨e'⟩⟩⟩
refine ⟨_, _, f, ⟨?_⟩⟩
exact
e ≪≫
Qh.mapTriangle.mapIso e' ≪≫
(Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).symm.app _ ≪≫
(Functor.mapTriangleIso (quotientCompQhIso C)).app _
· rintro ⟨X, Y, f, ⟨e⟩⟩
refine
isomorphic_distinguished _ (Qh.map_distinguished _ ?_) _
(e ≪≫
(Functor.mapTriangleIso (quotientCompQhIso C)).symm.app _ ≪≫
(Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).app _)
exact ⟨_, _, f, ⟨Iso.refl _⟩⟩
