English
Let R be a ring and P an Additive commutative group with an R-module structure. If for every surjective R-linear map f: M → N between R-modules and every R-linear map g: P → N there exists a lift h: P → M with f ∘ h = g, then P is a projective object in the category of R-modules.
Русский
Пусть R — кольцо, P — добавочная коммутативная группа с R-модульной структурой. Если для любого сюръективного R-линейного отображения f: M → N между R-модулями и любого линейного отображения g: P → N существует подъем h: P → M такой, что f ∘ h = g, тогда P является проективным объектом в категории R-модуляй.
LaTeX
$$$\\Big(\\forall M,N\\,[\\text{AddCommGroup } M]\\,[\\text{AddCommGroup } N]\\,[\\text{Module } R M]\\,[\\text{Module } R N]\\ (f: M \\to_{\\!\\ell[R]} N)\\ (g: P \\to_{\\!\\ell[R]} N), \\text{Surjective } f \\Rightarrow \\exists h: P \\to_{\\!\\ell[R]} M, f \\circ h = g\\Big) \\Rightarrow \\text{Projective } R\,P$$
Lean4
/-- A variant of `of_lifting_property'` when we're working over a `[Ring R]`,
which only requires quantifying over modules with an `AddCommGroup` instance. -/
theorem of_lifting_property {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P]
[Small.{v} R]
-- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
(h :
∀ {M : Type v} {N : Type v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N)
(g : P →ₗ[R] N), Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) :
-- then `P` is projective.
Projective R P := by
refine of_lifting_property'' (fun p hp ↦ ?_)
let e := Finsupp.mapRange.linearEquiv (α := P) (Shrink.linearEquiv R R)
rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩
exact ⟨e.toLinearMap ∘ₗ g, hg⟩
