English
For any j ∈ ι and any object X in W, the j-th component of the homomorphism in the map of the single-map construction from F to D is given by composing the image under F of the homomorphism of the unit object with the inverse of the unit object under F.
Русский
Пусть j ∈ ι и X ∈ W. Компонента j-ой степени в гомоморфизме отображения в конструкции single-map равна композиции образа под F гомоморфизма единичного объекта с обратным преобразованием единичного объекта под F.
LaTeX
$$$((\mathrm{singleMapHomologicalComplex} F \ c \ j).\mathrm{hom}.\mathrm{app} \, X).f_j = F( (\mathrm{singleObjXSelf} \ c \ j \ X).hom ) \circ (\mathrm{singleObjXSelf} \ c \ j \ (F\,\mathrm{obj}\ X)).inv$$$
Lean4
@[simp]
theorem singleMapHomologicalComplex_hom_app_self (j : ι) (X : W₁) :
((singleMapHomologicalComplex F c j).hom.app X).f j =
F.map (singleObjXSelf c j X).hom ≫ (singleObjXSelf c j (F.obj X)).inv :=
by simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
