English
If RingHom f is finite-type, then its induced polynomial ring is manageable (finite type).
Русский
Если гомоморфизм f имеет конечный тип, то индуцированный многочленовый кольцо тоже конечного типа.
LaTeX
$$IsJacobsonRing B$$
Lean4
@[stacks 0CY7 "See also https://en.wikipedia.org/wiki/Zariski%27s_lemma."]
theorem finite_of_finite_type_of_isJacobsonRing (R S : Type*) [CommRing R] [Field S] [Algebra R S] [IsJacobsonRing R]
[Algebra.FiniteType R S] : Module.Finite R S :=
by
obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›
have : (algebraMap R S).IsIntegral :=
by
rw [← f.comp_algebraMap]
-- We need to write `f.toRingHom` instead of just `f`, to avoid unification issues.
exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf
have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this
exact Algebra.IsIntegral.finite
