English
A module P is projective iff there exists a linear map s: P →ₗ[R] P →₀ R such that the composition with the linear combination map equals the identity on P; an equivalent formulation to the previous definition.
Русский
Модуль P проективен тогда и только тогда, когда существует линейное отображение s: P →ₗ[R] P →₀ R и композиция с отображением линейной комбинации даёт идентичность на P; эквивалентно предыдущему определению.
LaTeX
$$$$ \\exists s: P \\to P \\to_0 R,\; (Finsupp.linearCombination R id) \\circ s = \\mathrm{id}_P. $$$$
Lean4
theorem projective_def' : Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.linearCombination R id ∘ₗ s = .id := by
simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]
