preservesRightHomology_of_zero_f — Mathlib

English

If φ: S1 → S2 and φ': S2 → S3 are quasi-iso, then φ ≫ φ' is also a quasi-iso.

Русский

Если φ: S1 → S2 и φ': S2 → S3 — квазиизоморфизмы, то их композиция φ ≫ φ' — тоже квазиизоморфизм.

LaTeX

$$$\text{QuasiIso}(φ) \land \text{QuasiIso}(φ') \Rightarrow \text{QuasiIso}(φ \gg φ')$$$

Lean4

/-- If a short complex `S` is such that `S.f = 0` and that the kernel of `S.g` is preserved
by a functor `F`, then `F` preserves the right homology of `S`. -/
theorem preservesRightHomology_of_zero_f (hf : S.f = 0) [PreservesLimit (parallelPair S.g 0) F] :
    F.PreservesRightHomologyOf S :=
  ⟨fun h =>
    { f := by
        rw [hf]
        infer_instance
      g' := by
        have := h.isIso_p hf
        let e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
          parallelPair.ext (asIso h.p) (Iso.refl _) (by simp) (by simp)
        exact Limits.preservesLimit_of_iso_diagram F e }⟩

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