Projectivity of a reduction along a surjective ring homomorphism #
Let f : A →+* B be a surjective ring homomorphism and I an ideal of A contained in the kernel
of f. If M is a projective A-module, then its reduction M ⧸ I • M, endowed with any
B-module structure through which A acts via f, is a projective B-module.
No commutativity is assumed. A typical application is reduction of coefficients: a projective
ℤ_p[G]-module reduces modulo p to a projective 𝔽_p[G]-module.
Main results #
Module.Projective.quotient_smul_top: the reduction of a projective module along a surjective ring homomorphism is projective.
theorem
Module.Projective.quotient_smul_top
{A : Type u_1}
{B : Type u_2}
{M : Type u_3}
[Ring A]
[Ring B]
[AddCommGroup M]
[Module A M]
[Projective A M]
(f : A →+* B)
(hf : Function.Surjective ⇑f)
{I : Ideal A}
(hI : I ≤ RingHom.ker f)
[Module B (M ⧸ I • ⊤)]
(hsmul : ∀ (a : A) (q : M ⧸ I • ⊤), f a • q = a • q)
:
Projective B (M ⧸ I • ⊤)
Reduction along a surjective ring homomorphism preserves projectivity. Let
f : A →+* B be surjective and I ≤ ker f. If M is a projective A-module, then
M ⧸ I • M is a projective B-module for any B-module structure through which each a : A acts
as f a.