projective_iff_llp_epimorphisms_zero

English

Specialization: In presence of a zero morphism, Projective P is equivalent to LLP with epimorphisms from the zero object to P.

Русский

Специализация: при наличии нулевого объекта и LLP относительно эпиморфизмов, связанных с нулём, проективность P эквивалентна LLP.

LaTeX

$$$ \\mathrm{Projective}(P) \\iff (\\mathrm{MorphismProperty.epimorphisms\\, C}).llp(0) $$

Lean4

theorem projective_iff_llp_epimorphisms_zero [HasZeroMorphisms C] [HasZeroObject C] (P : C) :
    Projective P ↔ (MorphismProperty.epimorphisms C).llp (0 : 0 ⟶ P) :=
  projective_iff_llp_epimorphisms_of_isZero _ (isZero_zero C)

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