Finite length of a localized kernel and cokernel

This is the small commutative-algebra adapter needed when the finite module is over a larger coefficient algebra. Finiteness over the base is supplied explicitly; no restriction-of-scalars finiteness of the ambient module is used.

theorem AlgebraicAnalysis.localized_kernel_and_cokernel_isFiniteLength {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 R] [IsNoetherianRing C] [Module.Finite C E] (f : Module.End C E) [Module.Finite R ↥(↑R f).ker] [Module.Finite R (E ⧸ (↑R f).range)] (q : PrimeSpectrum R) (hqmem : q ∈ Module.support R (E ⧸ (↑R f).range)) (hq : ∀ p ∈ Module.support R (E ⧸ (↑R f).range), p.asIdeal ≤ q.asIdeal → q.asIdeal ≤ p.asIdeal) : IsFiniteLength (Localization q.asIdeal.primeCompl) (LocalizedModule q.asIdeal.primeCompl (E ⧸ (↑R f).range)) ∧ IsFiniteLength (Localization q.asIdeal.primeCompl) (LocalizedModule q.asIdeal.primeCompl ↥(↑R f).ker)