injective_of_preservesFiniteColimits_preadditiveYonedaObj

English

If the preadditive Yoneda functor preserves finite colimits, then J is injective.

Русский

Если предаддитивный Yoneda-функтор сохраняет конечные колимиты, тогда J инъективен.

LaTeX

$$$\text{Injective } J$$$

Lean4

/-- An object is injective if its preadditive Yoneda functor preserves finite colimits. -/
theorem injective_of_preservesFiniteColimits_preadditiveYonedaObj (J : C)
    [hP : PreservesFiniteColimits (preadditiveYonedaObj J)] : Injective J :=
  by
  rw [injective_iff_preservesEpimorphisms_preadditive_yoneda_obj']
  have := Functor.preservesHomologyOfExact (preadditiveYonedaObj J)
  infer_instance

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