English
Let F and G be cochain complexes in an additive category. There is a natural additive correspondence between morphisms φ: F → G and 0-cocycles in the Hom-complex CochainComplex.HomComplex.Cocycle F G 0, given by φ ↦ ofHom φ and its inverse z ↦ homOf z; in particular, applying the inverse to the image of φ yields φ again: homOf(ofHom φ) = φ.
Русский
Пусть F и G — цепочно-коцепные комплексы в абелевой (или аддитивной) категории. Существует естественная аддитивная эквивалентность между морфизмами φ: F → G и 0-коциклами в Hom-комплексе CochainComplex.HomComplex.Cocycle F G 0, задаваемая φ ↦ ofHom φ и обратная карта z ↦ homOf z; следовательно, применение обратной карты к образу φ возвращает φ: homOf(ofHom φ) = φ.
LaTeX
$$$\\forall F,G\\,\\forall \\phi: F \\to G,\\quad \\mathrm{homOf}(\\mathrm{ofHom}(\\phi)) = \\phi.$$$
Lean4
@[simp]
theorem homOf_ofHom_eq_self (φ : F ⟶ G) : homOf (ofHom φ) = φ := by cat_disch
