English
If M is projective and M ≃ₗ[R] P, then P is projective; projectivity is preserved under linear isomorphisms.
Русский
Если M проективен и M эквивалентен P линейно, то P также проективен; проективность сохраняется под линейными изоморфизмами.
LaTeX
$$$$ \\text{If } M \\cong P \\text{ and } M \\text{ is projective, then } P \\text{ is projective}. $$$$
Lean4
/-- A direct summand of a projective module is projective. -/
theorem of_split [Module.Projective R M] (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s.comp i = LinearMap.id) :
Module.Projective R P :=
by
obtain ⟨g, hg⟩ :=
projective_lifting_property (Finsupp.linearCombination R id) s (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)
refine ⟨g.comp i, fun x ↦ ?_⟩
rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg, ← LinearMap.comp_apply, H, LinearMap.id_apply]
