English
If cycles maps φ has left-isomorphism data, and φ.τ₃ is mono, then the homology map φ is itself an isomorphism. This connects mono properties of mid-level cycles data to isomorphism of the induced homology map.
Русский
Если для маппинга φ данные левой циклической части образуют изоморфизм, а φ.τ₃ моно, тогда отображение гомологии φ является изоморфизмом.
LaTeX
$$IsIso (homologyMap φ)$$
Lean4
theorem homologyMap_op [HasHomology S₁] [HasHomology S₂] :
(homologyMap φ).op = (S₂.homologyOpIso).inv ≫ homologyMap (opMap φ) ≫ (S₁.homologyOpIso).hom :=
by
dsimp only [homologyMap, homologyOpIso]
rw [homologyMap'_op]
dsimp only [Iso.symm, Iso.trans, Iso.op, Iso.refl, rightHomologyIso, leftHomologyIso, leftHomologyOpIso,
leftHomologyMapIso', rightHomologyMapIso', LeftHomologyData.leftHomologyIso, homologyMap']
simp only [assoc, rightHomologyMap'_op, op_comp, ← leftHomologyMap'_comp_assoc, id_comp, opMap_id, comp_id,
HomologyData.op_left]
