Finiteness from a radical quotient

A quotient algebra is module-finite if its reduced quotient is module-finite and the radical of the defining ideal is finitely generated. This is useful for passing from finite residue fields to finite infinitesimal neighbourhoods, without assuming that the algebra itself is finite over the coefficient ring.

The descent step is Mathlib's Module.finite_of_surjective_of_ker_le_nilradical.

theorem Ideal.moduleFinite_quotient_of_radical {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (I : Ideal A) (hI : I.radical.FG) [Module.Finite R (A ⧸ I.radical)] : Module.Finite R (A ⧸ I)

Finiteness of the quotient by the radical descends to the original quotient when the radical is finitely generated.