English
Let C be a preadditive category and J an object. Then J is injective iff the variant preadditive Yoneda object at J preserves epimorphisms.
Русский
Пусть C — предадмитивная категория и J — объект. Тогда J является инъекционным тогда и только тогда, когда вариант предадмитивного Yoneda объекта в J сохраняет эпиморфизмы.
LaTeX
$$$\text{Injective}(J) \iff (\text{preadditiveYonedaObj } J).\text{PreservesEpimorphisms}$$$
Lean4
theorem injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' (J : C) :
Injective J ↔ (preadditiveYonedaObj J).PreservesEpimorphisms :=
by
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
refine ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms => ?_, ?_⟩
· exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)
· intro
exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)
