Finite power torsion for a principal Koszul endomorphism

This file isolates the reusable algebra needed after tangential localization. The ambient module need not be finite over the ring in which lengths are measured. It is enough that the first kernel has finite length: all finite power kernels then have finite length by devissage.

The final theorem deliberately assumes that the actual residual quotient is nonzero. It proves only the strict length inequality and makes no noncharacteristic-support or geometric nonvanishing claim.

theorem AlgebraicAnalysis.PrincipalKoszulFiniteTorsion.isNoetherian_kernel_power {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] (f : Module.End R E) [IsNoetherian R ↥(LinearMap.ker f)] (n : ℕ) : IsNoetherian R ↥(LinearMap.ker (f ^ n))

If the first kernel of an endomorphism is Noetherian, then so is the kernel of every finite power. No finiteness hypothesis is imposed on the ambient module.

theorem AlgebraicAnalysis.PrincipalKoszulFiniteTorsion.isFiniteLength_kernel_power {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] (f : Module.End R E) (hfinite : IsFiniteLength R ↥(LinearMap.ker f)) (n : ℕ) : IsFiniteLength R ↥(LinearMap.ker (f ^ n))

Finite length of the first kernel propagates to every finite power kernel, even when the ambient module is not finite over R.

theorem AlgebraicAnalysis.PrincipalKoszulFiniteTorsion.length_cokernel_gt_kernel_of_stable_power_and_nonzero {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] (f : Module.End R E) (n : ℕ) (hfinite : IsFiniteLength R ↥(LinearMap.ker f)) (hstable : LinearMap.ker (f ^ n) = LinearMap.ker (f ^ (n + 1))) (hnonzero : Nontrivial (E ⧸ LinearMap.ker (f ^ n) ⊔ LinearMap.range f)) : Module.length R (E ⧸ LinearMap.range f) > Module.length R ↥(LinearMap.ker f)

A stable finite power kernel contributes the same length to the kernel and cokernel. If the actual quotient left after removing that torsion and the range is nonzero, the principal Koszul Euler length is strictly positive.

The nonzero quotient is an explicit input; this theorem does not manufacture it from a support or noncharacteristic hypothesis.