leftRightHomologyComparison'_eq_descH

English

The left-right homology comparison equals the description morphism built by applying a left-descending construction followed by a lifting from the right, under suitable conditions.

Русский

Сопоставление левой и правой гомологий равно описывающему отображению, получаемому последовательностью конструкций слева и подъёма справа при подходящих условиях.

LaTeX

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

Lean4

theorem leftRightHomologyComparison'_eq_descH :
    leftRightHomologyComparison' h₁ h₂ =
      h₁.descH (h₂.liftH (h₁.i ≫ h₂.p) (by simp))
        (by
          rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι, LeftHomologyData.f'_i_assoc, RightHomologyData.wp,
            zero_comp]) :=
  by
  simp only [← cancel_mono h₂.ι, ← cancel_epi h₁.π, π_leftRightHomologyComparison'_ι, LeftHomologyData.π_descH_assoc,
    RightHomologyData.liftH_ι]

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