English
A module P is projective if for all surjections f: M → N there exists a linear map h: P → M lifting all maps to N; this is the strengthened lifting property version.
Русский
Модуль P проективен, если для всех сюръекций f: M → N существует линейное отображение h: P → M, поднимающее любые отображения P → N.
LaTeX
$$$$ \\text{(lifting property'')}\\Rightarrow \\text{Projective}(R,P). $$$$
Lean4
instance [h : ∀ i : ι, Projective R (A i)] : Projective R (Π₀ i, A i) :=
.of_lifting_property'' fun f hf ↦ by
classical
choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
refine ⟨DFinsupp.coprodMap g, ?_⟩
ext i x j
simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
