leftRightHomologyComparison'_eq_liftH

English

Let S be a short complex with left and right homology data h1 and h2. The canonical morphism comparing the two homologies is expressible via a lift constructed from h1 and h2; this expresses the compatibility of the left and right homology data within the short complex.

Русский

Пусть S — короткий комплекс с данными левой и правой гомологий h1 и h2. Каноничное отображение, сопоставляющее две гомологии, задаётся через подъём, сконструированный из h1 и h2, что выражает совместимость левой и правой гомологии в коротком комплексе.

LaTeX

$$$\\text{leftRightHomologyComparison}'(h_1,h_2) = h_2.\\mathrm{liftH}(h_1.\\mathrm{descH}(h_1. i \\circ h_2. p))$$$

Lean4

theorem leftRightHomologyComparison'_eq_liftH :
    leftRightHomologyComparison' h₁ h₂ =
      h₂.liftH (h₁.descH (h₁.i ≫ h₂.p) (by simp))
        (by
          rw [← cancel_epi h₁.π, LeftHomologyData.π_descH_assoc, assoc, RightHomologyData.p_g', LeftHomologyData.wi,
            comp_zero]) :=
  rfl

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