Projectivity along a tower of scalars #
If S is a projective R-module and M is a projective S-module, compatibly with the
R-actions, then M is a projective R-module: M is a direct summand of a free S-module,
which is a direct sum of copies of the projective R-module S.
No commutativity is assumed, and S need not be an R-algebra: it suffices that R acts on S
compatibly with multiplication on the left. This is the situation of a subring that is not central,
for instance the group algebra A[H] of a subgroup acting on A[G] by left multiplication, and is
how a projective A[G]-module is restricted to a projective A[H]-module.
Main results #
Module.Projective.trans: projectivity is transitive along a scalar tower.
theorem
Module.Projective.trans
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
[Semiring R]
[Semiring S]
[Module R S]
[IsScalarTower R S S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
[Projective R S]
[Projective S M]
:
Projective R M
Projectivity is transitive along a scalar tower. A projective module over a ring S that is
itself projective as a left R-module is projective over R.