Kernel support over a base ring

A finite module over a commutative Noetherian coefficient algebra is Hopfian over that algebra. This gives the kernel--cokernel support inclusion after restriction of scalars, without assuming finite generation over the base.

theorem AlgebraicAnalysis.endomorphism_kernel_support_subset_cokernel_support_over_base {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module C E] [Module R E] [IsScalarTower R C E] [IsNoetherianRing C] [Module.Finite C E] (f : Module.End C E) : Module.support R ↥(↑R f).ker ⊆ Module.support R (E ⧸ (↑R f).range)