English
A object P is projective iff the preadditiveCoyoneda.obj (op P) preserves epimorphisms.
Русский
Объект P проективен тогда и только тогда, когда предадмитивный Coyoneda-объект (op P) сохраняет эпиморфизмы.
LaTeX
$$$\text{Projective}(P) \iff (\text{preadditiveCoyoneda.obj } (op P)).\text{PreservesEpimorphisms}$$$
Lean4
theorem projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj (P : C) :
Projective P ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms :=
by
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
refine ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGrpCat).PreservesEpimorphisms => ?_, ?_⟩
· exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P)) (forget _)
· intro
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)
