English
A module that satisfies a universal lifting property is projective; more precisely, if every surjection f: M → N admits liftings for maps from P, then P is projective.
Русский
Модуль, удовлетворяющий универсальному признаку подъёмов, является проективным; точнее, если каждый сюръективный отображение f: M → N допускает поднятие для отображений из P, то P — проективен.
LaTeX
$$$$ \\text{(lifting property)} \\Rightarrow \\text{Projective}(R,P). $$$$
Lean4
instance [Projective R P] [Projective R Q] : Projective R (P × Q) :=
by
refine .of_lifting_property'' fun f hf ↦ ?_
rcases projective_lifting_property f (.inl _ _ _) hf with ⟨g₁, hg₁⟩
rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩
refine ⟨coprod g₁ g₂, ?_⟩
rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
