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