map_leftRightHomologyComparison' — Mathlib

English

Under a homotopy h, the map leftRightHomologyComparison' commutes with F.

Русский

При гомотопии h карта leftRightHomologyComparison' commute с F.

LaTeX

$$$F.map\\left(\\text{leftRightHomologyComparison}'(h_l,h_r)\\right) = \\text{leftRightHomologyComparison}'\\left( h_l.map F, h_r.map F\\right)$$$

Lean4

theorem map_leftRightHomologyComparison' (F : C ⥤ D) [F.PreservesZeroMorphisms] (hₗ : S.LeftHomologyData)
    (hᵣ : S.RightHomologyData) [hₗ.IsPreservedBy F] [hᵣ.IsPreservedBy F] :
    F.map (leftRightHomologyComparison' hₗ hᵣ) = leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) :=
  by
  apply Cofork.IsColimit.hom_ext (hₗ.map F).hπ
  apply Fork.IsLimit.hom_ext (hᵣ.map F).hι
  trans F.map (hₗ.i ≫ hᵣ.p)
  · simp [← Functor.map_comp]
  trans (hₗ.map F).π ≫ ShortComplex.leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι
  · rw [ShortComplex.π_leftRightHomologyComparison'_ι]; simp
  · simp

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