mapCyclesIso_hom_naturality — Mathlib

English

For the primed version, S.mapHomologyIso' F equals the trans of (hr.map F).homologyIso with F.mapIso hr.homologyIso.symm.

Русский

Для обобщённой версии S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm.

LaTeX

$$$S.mapHomologyIso' F = (hr.map F).homologyIso \;\circ\; F.mapIso hr.homologyIso.symm$$

Lean4

@[reassoc]
theorem mapCyclesIso_hom_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomology] [F.PreservesLeftHomologyOf S₁]
    [F.PreservesLeftHomologyOf S₂] :
    cyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapCyclesIso F).hom = (S₁.mapCyclesIso F).hom ≫ F.map (cyclesMap φ) :=
  by
  dsimp only [cyclesMap, mapCyclesIso, LeftHomologyData.cyclesIso, cyclesMapIso', Iso.refl]
  simp only [LeftHomologyData.map_cyclesMap', Functor.mapShortComplex_obj, ← cyclesMap'_comp, comp_id, id_comp]

Похожие утверждения