Finiteness from a monic annihilator

A finite polynomial-ring module annihilated by a monic polynomial is finite over the coefficient ring. This is the algebraic finiteness step for the normal covariable; no characteristic-support assertion is assumed.

theorem AlgebraicAnalysis.MonicAnnihilatorFinite.finite_of_monic_annihilator {R : Type u_1} {E : Type u_2} [CommRing R] [AddCommGroup E] [Module R E] [Module (Polynomial R) E] [IsScalarTower R (Polynomial R) E] [Module.Finite (Polynomial R) E] (g : Polynomial R) (hg : g.Monic) (hkill : ∀ (z : E), g • z = 0) : Module.Finite R E

theorem AlgebraicAnalysis.MonicAnnihilatorFinite.finite_of_variable_annihilates {R : Type u_1} {E : Type u_2} [CommRing R] [AddCommGroup E] [Module R E] [Module (Polynomial R) E] [IsScalarTower R (Polynomial R) E] [Module.Finite (Polynomial R) E] (hkill : ∀ (z : E), Polynomial.X • z = 0) : Module.Finite R E

A finite module killed by the polynomial variable is finite over the coefficient ring.

theorem AlgebraicAnalysis.MonicAnnihilatorFinite.finite_kernel_and_cokernel_variable {R : Type u_1} {E : Type u_2} [CommRing R] [IsNoetherianRing R] [AddCommGroup E] [Module R E] [Module (Polynomial R) E] [IsScalarTower R (Polynomial R) E] [Module.Finite (Polynomial R) E] : Module.Finite R ↥((LinearMap.lsmul (Polynomial R) E) Polynomial.X).ker ∧ Module.Finite R (E ⧸ ((LinearMap.lsmul (Polynomial R) E) Polynomial.X).range)

Both terms of the principal Koszul homology are finite over the coefficient ring, although the ambient module need not be.