English
Equality of two constructions of the homology iso: mapHomologyIso' F equals mapHomologyIso F.
Русский
Равенство двух конструкций гомологического изоморфизма: mapHomologyIso' F равен mapHomologyIso F.
LaTeX
$$$S.mapHomologyIso' F = S.mapHomologyIso F$$$
Lean4
theorem mapHomologyIso'_eq_mapHomologyIso [S.HasHomology] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :
S.mapHomologyIso' F = S.mapHomologyIso F := by
ext
rw [S.homologyData.left.mapHomologyIso_eq F, S.homologyData.right.mapHomologyIso'_eq F]
dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, RightHomologyData.homologyIso, rightHomologyIso,
RightHomologyData.rightHomologyIso, LeftHomologyData.homologyIso, leftHomologyIso, LeftHomologyData.leftHomologyIso]
simp only [RightHomologyData.map_H, rightHomologyMapIso'_inv, rightHomologyMapIso'_hom, assoc, Functor.map_comp,
RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj, Functor.map_id, LeftHomologyData.map_H,
leftHomologyMapIso'_inv, leftHomologyMapIso'_hom, LeftHomologyData.map_leftHomologyMap',
← rightHomologyMap'_comp_assoc, ← leftHomologyMap'_comp, id_comp]
have γ : HomologyMapData (𝟙 (S.map F)) (map S F).homologyData (S.homologyData.map F) := default
have eq := γ.comm
rw [← γ.left.leftHomologyMap'_eq, ← γ.right.rightHomologyMap'_eq] at eq
dsimp at eq
simp only [← reassoc_of% eq, ← F.map_comp, Iso.hom_inv_id, F.map_id, comp_id]
