opcyclesIsoSc'_inv_fromOpcycles — Mathlib

English

Naturality of the inverse homology iso with respect to φ in the i-j-k arrangement.

Русский

Естественность обратного гомологии-изоморфизма по отношению к φ для конфигурации i-j-k.

LaTeX

$$$ (K.sc' i j k).homologyπ \circ (K.homologyIsoSc' i j k hi hk).inv = (K.cyclesIsoSc' i j k hi hk).inv \circ K.homologyπ j $$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesIsoSc'_inv_fromOpcycles :
    (K.opcyclesIsoSc' i j k hi hk).inv ≫ K.fromOpcycles j k = (K.sc' i j k).fromOpcycles := by
  simp only [← cancel_epi (K.sc' i j k).pOpcycles, pOpcycles_opcyclesIsoSc'_inv_assoc, p_fromOpcycles,
    ShortComplex.p_fromOpcycles, shortComplexFunctor'_obj_g]

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