liftCycles_comp_cyclesIso_hom — Mathlib

English

The equality liftCycles k hk ≫ cyclesIso.hom equals liftK k hk.

Русский

Справедливо равенство liftCycles k hk ≫ cyclesIso.hom = liftK k hk.

LaTeX

$$$S.liftCycles\,k\,hk \;\circ\; h.cyclesIso.hom = h.liftK\,k\,hk$$$

Lean4

@[reassoc (attr := simp)]
theorem liftCycles_comp_cyclesIso_hom : S.liftCycles k hk ≫ h.cyclesIso.hom = h.liftK k hk := by
  simp only [← cancel_mono h.i, assoc, LeftHomologyData.cyclesIso_hom_comp_i, liftCycles_i, LeftHomologyData.liftK_i]

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