projective_iff_llp_epimorphisms_of_isZero

English

In a category with zero morphisms, a object P is projective iff the LLP (left lifting property) with respect to epimorphisms from 0 to P holds.

Русский

В категории с нулевыми морфизмами объект P проективен тогда и только тогда, когда выполняется левые свойства подъёма относительно эпиморфизмов.

LaTeX

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

Lean4

theorem projective_iff_llp_epimorphisms_of_isZero [HasZeroMorphisms C] {P Z : C} (i : Z ⟶ P) (hZ : IsZero Z) :
    Projective P ↔ (MorphismProperty.epimorphisms C).llp i :=
  by
  obtain rfl := hZ.eq_of_src i 0
  constructor
  · intro _ X Y p (_ : Epi p)
    exact Projective.hasLiftingProperty_of_isZero 0 p hZ
  · intro h
    constructor
    intro X Y f p hp
    have := h _ hp
    have sq : CommSq 0 (0 : Z ⟶ P) p f := ⟨by simp⟩
    exact ⟨sq.lift, by simp⟩

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