preservesLeftHomology_of_zero_f — Mathlib

English

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

Русский

Пусть φ: S1 → S2 и φ': S2 → S3—морфизмы, для которых φ квазиизоморфизм, и если состав φ ≫ φ' также квазиизоморфизм, тогда φ' — квазиизоморфизм.

LaTeX

$$$\text{QuasiIso}(\phi')$ given $\text{QuasiIso}(\phi)$ and $\text{QuasiIso}(\phi \!\gg\! \phi')$$$

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 left homology of `S`. -/
theorem preservesLeftHomology_of_zero_f (hf : S.f = 0) [PreservesLimit (parallelPair S.g 0) F] :
    F.PreservesLeftHomologyOf S :=
  ⟨fun h =>
    { g := by infer_instance
      f' := Limits.preservesCokernel_zero' _ _ (by rw [← cancel_mono h.i, h.f'_i, zero_comp, hf]) }⟩

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