English
If M is a finitely generated projective R-module, there exist n, a surjective f: R^n → M and a g: M → R^n with f ∘ g = id_M and g is injective on M.
Русский
Пусть M — конечнопорождённый проективный модуль над R. Тогда существует n и линейные отображения f: R^n → M, g: M → R^n такие, что f сюръективно, g инъективно, и f ∘ g = id_M.
LaTeX
$$$\\exists n, f: R^{n} \\to M, g: M \\to R^{n},\\ f \\text{ surjective},\\ g \\text{ injective},\\ f \\circ g = \\mathrm{id}_M$$$
Lean4
theorem exists_comp_eq_id_of_projective [Module.Finite R M] [Projective R M] :
∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M) (g : M →ₗ[R] Fin n → R),
Function.Surjective f ∧ Function.Injective g ∧ f ∘ₗ g = .id :=
have ⟨n, f, surj⟩ := exists_fin' R M
have ⟨g, hfg⟩ := Module.projective_lifting_property f .id surj
⟨n, f, g, surj, LinearMap.injective_of_comp_eq_id _ _ hfg, hfg⟩
