instIsIsoFromLeftDerivedZero' — Mathlib

English

Let F be additive and preserve finite colimits. For every X and projective resolution P of X, the morphism P.fromLeftDerivedZero' F is an isomorphism.

Русский

Пусть F аддитивен и сохраняет конечные колимиты; для каждого X и проектive разрешения P_X отображение P.fromLeftDerivedZero' F является изоморфизмом.

LaTeX

$$$\\forall X\\, \\forall P : \\mathrm{ProjectiveResolution}\ X,\\ \\operatorname{IsIso}(P.fromLeftDerivedZero'\\, F)$$$

Lean4

instance {X : C} (P : ProjectiveResolution X) : IsIso (P.fromLeftDerivedZero' F) :=
  by
  dsimp [ProjectiveResolution.fromLeftDerivedZero']
  rw [ChainComplex.isIso_descOpcycles_iff, ShortComplex.exact_and_epi_g_iff_g_is_cokernel]
  exact ⟨CokernelCofork.mapIsColimit _ (P.isColimitCokernelCofork) F⟩

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