English
There is a canonical equality statement expressing that the above isomorphism equals the composed postcomp/quotient constructions; i.e., the explicit equality of isomorphisms.
Русский
Существует каноничное равенство, выражающее что указанный выше изоморфизм равен составному посткомпу/квотиционной конструкции; то есть явное равенство изоморфизмов.
LaTeX
$$singleFunctorsPostcompQIso_eq : (singleFunctorsPostcompQIso C) = (((CategoryTheory.SingleFunctors.postcompFunctor C Int DerivedCategory.Qh).mapIso (HomotopyCategory.singleFunctorsPostcompQuotientIso C)).trans ( (CochainComplex.singleFunctors C).postcompPostcompIso (HomotopyCategory.quotient C (ComplexShape.up Int)) DerivedCategory.Qh).trans (SingleFunctors.postcompIsoOfIso (CochainComplex.singleFunctors C) (quotientCompQhIso C)))$$
Lean4
/-- The isomorphism
`DerivedCategory.singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q`. -/
noncomputable def singleFunctorsPostcompQIso : singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q :=
(SingleFunctors.postcompFunctor C ℤ (Qh : _ ⥤ DerivedCategory C)).mapIso
(HomotopyCategory.singleFunctorsPostcompQuotientIso C) ≪≫
(CochainComplex.singleFunctors C).postcompPostcompIso (HomotopyCategory.quotient _ _) Qh ≪≫
SingleFunctors.postcompIsoOfIso (CochainComplex.singleFunctors C) (quotientCompQhIso C)
