English
A module is projective iff it is a direct summand of a free module.
Русский
Модуль проективен тогда и только тогда, когда является прямым дополнением свободного модуля.
LaTeX
$$$$ \\text{Projective}(R,P) \\iff \\exists M, \\text{ free over } R, P \\text{ is a direct summand of } M. $$$$
Lean4
theorem of_ringEquiv {R S} [Semiring R] [Semiring S] {M N} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N]
(e₁ : R ≃+* S) (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] N) [Projective R M] : Projective S N :=
by
obtain ⟨f, hf⟩ := ‹Projective R M›
let g : N →ₗ[S] N →₀ S :=
{ toFun := fun x ↦ (equivCongrLeft e₂ (f (e₂.symm x))).mapRange e₁ e₁.map_zero
map_add' := fun x y ↦ by ext; simp
map_smul' := fun r v ↦ by ext i; simp [e₂.symm.map_smulₛₗ] }
refine ⟨⟨g, fun x ↦ ?_⟩⟩
replace hf := congr(e₂ $(hf (e₂.symm x)))
simpa [linearCombination_apply, sum_mapRange_index, g, map_finsuppSum, e₂.map_smulₛₗ] using hf
