English
Let f be a family of isomorphisms f_i: C1.X_i ≅ C2.X_i between the corresponding components of two HomologicalComplexs with the usual compatibility condition hf ensuring the differentials commute up to these isomorphisms. Then the i-th component of the assembled isomorphism equals f_i: isoApp (isoOfComponents f hf) i = f_i.
Русский
Пусть f—семейство изоморфизмов f_i: C1.X_i ≅ C2.X_i между компонентами двух гомологоподобных комплексов, удовлетворяющее обычному условию совместимости hf. Тогда i-й компонент собранного изоморфизма равен f_i: isoApp (isoOfComponents f hf) i = f_i.
LaTeX
$$$\\text{isoApp}(\\text{isoOfComponents } f\ufeff hf)\n i = f i$$$
Lean4
@[simp]
theorem isoOfComponents_app (f : ∀ i, C₁.X i ≅ C₂.X i)
(hf : ∀ i j, c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) (i : ι) :
isoApp (isoOfComponents f hf) i = f i := by
ext
simp
