preservesHomology_preadditiveYonedaObj_of_injective

English

The preadditive Yoneda functor on an object J preserves homology when J is injective.

Русский

Предобу́дованный функтор Йонеда на объекте J сохраняет гомологию, когда J инъективен.

LaTeX

$$$\text{PreadditiveYonedaObj}(J) \;\text{preserves Homology}$$$

Lean4

/-- The preadditive Yoneda functor on `J` preserves homology if `J` is injective. -/
instance preservesHomology_preadditiveYonedaObj_of_injective (J : C) [hJ : Injective J] :
    (preadditiveYonedaObj J).PreservesHomology :=
  by
  letI := (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J).mp hJ
  apply Functor.preservesHomology_of_preservesEpis_and_kernels

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