Principal Koszul positivity after restriction of scalars

Support and torsion are computed over the coefficient algebra C; the resulting length inequality is measured over the base ring R. No finite generation of E over R is needed: only the first R-kernel has finite length.

theorem AlgebraicAnalysis.PrincipalKoszulSupportOverBase.length_cokernel_gt_kernel_of_support_over_base {R : Type u} {C : Type v} {E : Type w} [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] (x : C) (p q : PrimeSpectrum C) (hp : p ∈ Module.support C E) (hpq : p ≤ q) (hxp : x ∉ p.asIdeal) (hq : q ∈ Module.support C (QuotSMulTop x E)) (hfinite : IsFiniteLength R ↥(↑R ((LinearMap.lsmul C E) x)).ker) : Module.length R (E ⧸ (↑R ((LinearMap.lsmul C E) x)).range) > Module.length R ↥(↑R ((LinearMap.lsmul C E) x)).ker