injective_iff_preservesEpimorphisms_preadditiveYoneda_obj

English

Let C be a preadditive category and J an object of C. Then J is injective if and only if the preadditive Yoneda object at J preserves epimorphisms.

Русский

Пусть C — предадмитивная категория и J — объект в C. Тогда J является инъективным тогда и только тогда, когда предадмитивный объект Йонеда в J сохраняет эпиморфизмы.

LaTeX

$$$\text{Injective}(J) \iff (\text{preadditive Yoneda.obj } J).\text{PreservesEpimorphisms}$$$

Lean4

theorem injective_iff_preservesEpimorphisms_preadditiveYoneda_obj (J : C) :
    Injective J ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms :=
  by
  rw [injective_iff_preservesEpimorphisms_yoneda_obj]
  refine ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩
  · exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)
  · intro
    exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)

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