π_leftRightHomologyComparison'_ι

English

For left/right homology data h1, h2 and their counterparts in the target complex, the composite through the canonical left-right morphism equals the straightforward iota-p map across the components.

Русский

Для левых/правых данных гомологии h1, h2 и соответствующих данных в целевом комплексе композиция через канонический лево-правой отображает равенство с отображением iota-p между компонентами.

LaTeX

$$$h_1.\\pi \\; \\circ \\text{leftRightHomologyComparison}'(h_1,h_2) \\; \\circ h_2.\\iota = h_1.\\mathrm{i} \\circ h_2.\\mathrm{p}$$$

Lean4

@[reassoc (attr := simp)]
theorem π_leftRightHomologyComparison'_ι : h₁.π ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.ι = h₁.i ≫ h₂.p := by
  simp only [leftRightHomologyComparison'_eq_liftH, RightHomologyData.liftH_ι, LeftHomologyData.π_descH]

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