cyclesMap_comp_isoCycles₁_hom — Mathlib

English

The morphisms isoCycles₁ and mapCycles₁ satisfy a similar coherence with cycles maps, ensuring functoriality at the level of left homology data.

Русский

Морфизмы isoCycles и mapCycles₁ удовлетворяют аналогичную когерентность с отображениями циклов, обеспечивая функториальность на уровне левого гомологического звена.

LaTeX

$$$ (isoCycles_1 B).hom \circ mapCycles_1(f, \varphi) = cyclesMap_1(f, \varphi, 1) \circ (isoCycles_1 A).hom $$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem cyclesMap_comp_isoCycles₁_hom : cyclesMap f φ 1 ≫ (isoCycles₁ B).hom = (isoCycles₁ A).hom ≫ mapCycles₁ f φ := by
  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, mapShortComplexH1,
    chainsMap_f_1_comp_chainsIso₁ f]

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