English
If P and Q are projective R-modules, then their product P × Q is projective over R.
Русский
Если P и Q — проективные модули над R, то их произведение P × Q также проективно над R.
LaTeX
$$$$ \\text{If } P,Q \\text{ are projective over } R, \\; P \\times Q \\text{ is projective over } R. $$$$
Lean4
/-- A module which satisfies the universal property is projective: If all surjections of
`R`-modules `(P →₀ R) →ₗ[R] P` have `R`-linear left inverse maps, then `P` is
projective. -/
theorem of_lifting_property'' {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P]
(huniv : ∀ (f : (P →₀ R) →ₗ[R] P), Function.Surjective f → ∃ h : P →ₗ[R] (P →₀ R), f.comp h = .id) :
Projective R P :=
projective_def'.2 <|
huniv (Finsupp.linearCombination R (id : P → P)) (linearCombination_surjective _ Function.surjective_id)
