Finiteness of modules of linear maps over a base ring

Let A be a ring and R a commutative Noetherian ring acting on an A-module M through A-linear maps. If P is finitely generated over A and M is finitely generated over R, then the R-module Hom_A(P, M) is finitely generated: a surjection A ^ n → P embeds it in M ^ n. For example, for a finite group G the ℤ_p-module of ℤ_p[G]-linear maps between finitely generated ℤ_p[G]-modules is finitely generated. No freeness or projectivity is assumed, unlike Mathlib's Module.Finite.linearMap.

Main results

• Module.Finite.linearMap_of_isNoetherianRing: Hom_A(P, M) is finite over R.

theorem Module.Finite.linearMap_of_isNoetherianRing {R : Type u_1} {A : Type u_2} {P : Type u_3} {M : Type u_4} [CommRing R] [IsNoetherianRing R] [Ring A] [AddCommGroup P] [Module A P] [AddCommGroup M] [Module A M] [Module R M] [SMulCommClass A R M] [Module.Finite A P] [Module.Finite R M] : Module.Finite R (P →ₗ[A] M)

Linear maps into a finite module over a Noetherian base. For P finitely generated over A and M finitely generated over the commutative Noetherian ring R, whose action on M commutes with A, the R-module of A-linear maps P → M is finitely generated.