Principal Koszul positivity from minimal support

The support primes used by the strict length argument are produced from the finite C-module itself. In particular, no finiteness of E over the base ring R is needed.

theorem AlgebraicAnalysis.PrincipalKoszulMinimalSupportPositivity.length_cokernel_gt_kernel_of_minimal_support {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) (hmin : ∀ p ∈ (Module.annihilator C E).minimalPrimes, x ∉ p) (hnonzero : Nontrivial (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

Minimal support primes of E produce the ordered support pair needed by the principal Koszul positivity argument.