map_homologyMap' — Mathlib

English

If S1, S2 have homology data and F preserves left and right homology for S1 and S2, then the map between them preserves the homology iso up to F.mapIso and the corresponding maps.

Русский

Если S1, S2 имеют гомологические данные и F сохраняет левую и правую гомологию для S1 и S2, то отображение между ними сохраняет гомологическое изоморфство с учётом F.mapIso и соответствующих отображений.

LaTeX

$$$S_1.HasHomology \land S_2.HasHomology \land F.PreservesLeftHomologyOf S_1 \land F.PreservesLeftHomologyOf S_2 \Rightarrow (F.mapShortComplex.map φ)\text{...}$$$

Lean4

theorem map_homologyMap' [h₁.left.IsPreservedBy F] [h₁.right.IsPreservedBy F] [h₂.left.IsPreservedBy F]
    [h₂.right.IsPreservedBy F] :
    F.map (ShortComplex.homologyMap' φ h₁ h₂) =
      ShortComplex.homologyMap' (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F) :=
  LeftHomologyData.map_leftHomologyMap' _ _ _ _

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