English
If M is projective over R and N is projective over R0, with R0-algebra structure and an IsScalarTower, then their tensor product M ⊗_{R0} N is projective over R.
Русский
Если M проективен над R, а N проективен над R0, при наличии структуры алгебры R0 над R и тензорного расправления IsScalarTower, то их тензорное произведение M ⊗_{R0} N проективно над R.
LaTeX
$$$$ \\text{If } M \\text{ and } N \\text{ are projective with the given scalar-tower data, then } M \\otimes_{R0} N \\text{ is projective over } R. $$$$
Lean4
/-- A module which satisfies the universal property is projective. -/
theorem of_lifting_property' {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P]
[Small.{v} R]
-- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
(h :
∀ {M : Type v} {N : Type v} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N)
(g : P →ₗ[R] N), Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) :
-- then `P` is projective.
Projective R P := by
refine of_lifting_property'' (fun p hp ↦ ?_)
let e := Finsupp.mapRange.linearEquiv (α := P) (Shrink.linearEquiv R R)
rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩
exact ⟨e.toLinearMap ∘ₗ g, hg⟩
