cyclesIso_hom_comp_i — Mathlib

English

For a LeftHomologyData h on a short complex S, the hom component of the cycles isomorphism composed with i equals the left cycle map iCycles: h.cyclesIso.hom ≫ h.i = S.iCycles.

Русский

Для данных левой гомологии h на кратком комплексе S, композиция компонент изоморфизма циклов с i равна iCycles: h.cyclesIso.hom ≫ h.i = S.iCycles.

LaTeX

$$$h.cyclesIso.hom\,\circ\, h.i = S.iCycles$$$

Lean4

@[reassoc (attr := simp)]
theorem cyclesIso_hom_comp_i : h.cyclesIso.hom ≫ h.i = S.iCycles :=
  by
  dsimp [iCycles, LeftHomologyData.cyclesIso]
  simp only [cyclesMap'_i, id_τ₂, comp_id]

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