toCycles_cyclesIsoSc'_hom — Mathlib

English

Naturality of the map on homology with respect to the iso between π and cycles.

Русский

Естественность отображения на гомологии по отношению к изоморфизму между π и циклами.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem toCycles_cyclesIsoSc'_hom : K.toCycles i j ≫ (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles := by
  simp only [← cancel_mono (K.sc' i j k).iCycles, assoc, cyclesIsoSc'_hom_iCycles, toCycles_i, ShortComplex.toCycles_i,
    shortComplexFunctor'_obj_f]

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