mk' — Mathlib

English

There exists a construction showing F preservesLeftHomologyOf S when F preservesLeftHomologyOf.

Русский

Существуют конструкция, показывающая, что F сохраняетLeftHomologyOf S.

LaTeX

$$$F\\text{ preservesLeftHomologyOf }S$$$

Lean4

/-- If a functor preserves a certain left homology data of a short complex `S`, then it
preserves the left homology of `S`. -/
theorem mk' (h : S.LeftHomologyData) [h.IsPreservedBy F] : F.PreservesLeftHomologyOf S where
  isPreservedBy
    h' :=
    { g := ShortComplex.LeftHomologyData.IsPreservedBy.hg h F
      f' := by
        have := ShortComplex.LeftHomologyData.IsPreservedBy.hf' h F
        let e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
          parallelPair.ext (Iso.refl _) (ShortComplex.cyclesMapIso' (Iso.refl S) h h') (by simp) (by simp)
        exact preservesColimit_of_iso_diagram F e }

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