English
There exists a canonical additive equivalence between morphisms F ⟶ G and 0-cocycles Cocycle F G 0, given by toFun = ofHom and inverse = homOf, with left and right inverses provided by the two inverse lemmas.
Русский
Существует каноническая аддитивная эквивалентность между морфизмами F ⟶ G и 0-коциклами Cocycle F G 0, заданная через отображение toFun = ofHom и обратное = homOf, с левой и правой обратностью, обеспечиваемой вспомогательными леммами.
LaTeX
$$$\\text{equivHom} : (F \\to G) \\simeq_+ \\mathrm{Cocycle}(F,G,0)$ with\\ toFun = \\mathrm{ofHom},\\ invFun = \\mathrm{homOf},\\ left\\_inv = \\mathrm{homOf\\_ofHom\\_eq\\_self},\\ right\\_inv = \\mathrm{ofHom\\_homOf\\_eq\\_self}.$$$
Lean4
/-- The additive equivalence between morphisms in `CochainComplex C ℤ` and `0`-cocycles. -/
@[simps]
def equivHom : (F ⟶ G) ≃+ Cocycle F G 0 where
toFun := ofHom
invFun := homOf
left_inv := homOf_ofHom_eq_self
right_inv := ofHom_homOf_eq_self
map_add' := by cat_disch
