instIsIsoAppFromLeftDerivedZeroOfProjective

English

Let F be an additive functor C → D between abelian categories with HasProjectiveResolutions. Then for every object X in C, the morphism F.fromLeftDerivedZero.app X is an isomorphism.

Русский

Пусть F будет аддитивным функтором между абелевыми категориями и сохраняет проективные разрешения; тогда для каждого объекта X из C отображение F.fromLeftDerivedZero.app X является изоморфизмом.

LaTeX

$$$\\forall X,\\ \\operatorname{IsIso}(F.fromLeftDerivedZero.app X)$$$

Lean4

instance (F : C ⥤ D) [F.Additive] (X : C) [Projective X] : IsIso (F.fromLeftDerivedZero.app X) :=
  by
  rw [(ProjectiveResolution.self X).fromLeftDerivedZero_eq F]
  infer_instance

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