homologyπ_extendHomologyIso_hom — Mathlib

English

Relates inverse of extendHomologyIso with homologyι under extension, mirroring the dual compatibility of inertial objects.

Русский

Связь обратного extendHomologyIso с homologyι при расширении, отображающая двойственную совместимость гомологий.

LaTeX

$$(K.extendHomologyIso e hj').inv ≫ (K.extend e).homologyι j' = K.homologyι j ≫ (K.extendOpcyclesIso e hj').inv$$

Lean4

@[reassoc (attr := simp)]
theorem homologyπ_extendHomologyIso_hom :
    (K.extend e).homologyπ j' ≫ (K.extendHomologyIso e hj').hom = (K.extendCyclesIso e hj').hom ≫ K.homologyπ j :=
  by
  dsimp [extendHomologyIso, homologyπ]
  rw [ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc, ←
    cancel_mono (K.sc j).homologyData.left.homologyIso.hom, assoc, assoc, assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom]
  dsimp [extendCyclesIso]
  simp only [assoc, Iso.inv_hom_id_assoc]

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