mapHomologyIso_inv_naturality — Mathlib

English

Under the usual assumptions, the inverse of the homology isomorphism commutes with the functorial homology map in the natural way.

Русский

При обычных предпосылках обратный гомологический изоморфизм коммутирует с отображением гомологий, согласованно через функцию-функтор.

LaTeX

$$$F(\mathrm{homologyMap}(\phi)) \;\circ\; (S_2.mapHomologyIso\,F)^{-1} \\= (S_1.mapHomologyIso\,F)^{-1} \circ \mathrm{homologyMap}(F.mapShortComplex.map\,\phi)$$$

Lean4

@[reassoc]
theorem mapHomologyIso_inv_naturality [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology]
    [(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
    F.map (homologyMap φ) ≫ (S₂.mapHomologyIso F).inv =
      (S₁.mapHomologyIso F).inv ≫ @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ :=
  by
  rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id,
    Iso.hom_inv_id_assoc]

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