leftRightHomologyComparison'_compatibility

English

The left-right homology comparison is compatible with both left- and right-maps when adjusting the data by identity on the ambient short complex; this expresses a bidirectional coherence.

Русский

Сопоставление лево-правой гомологии совместимо как с левыми, так и с правыми отображениями при учёте тождественных изменений во внешнем коротком комплексе; это выражает двунаправленную когерентность.

LaTeX

$$$\\text{leftRightHomologyComparison}'(h_1,h_2) = \\text{leftHomologyMap}'(\\mathrm{Id}_S)\\; h_1 \\; \\cdot \\; \\text{rightHomologyMap}'(\\mathrm{Id}_S)\\, _ _$$$

Lean4

theorem leftRightHomologyComparison'_compatibility (h₁ h₁' : S.LeftHomologyData) (h₂ h₂' : S.RightHomologyData) :
    leftRightHomologyComparison' h₁ h₂ =
      leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) _ _ :=
  by
  rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂', ← rightHomologyMap'_comp, comp_id,
    rightHomologyMap'_id, comp_id]

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