mk' — Mathlib

English

If F preserves left homology of S, then h is preserved by F.

Русский

Если F сохраняет левую гомологию S, то h сохраняется F.

LaTeX

$$$h_1.IsPreservedBy F$$$

Lean4

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

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