English
Let A be a finitely generated algebra over a field k. Then there exists a natural number s and an injective k-algebra homomorphism from the polynomial ring in s variables into A such that A is finite as a module over the image of that polynomial ring.
Русский
Пусть A — конечно порожденная алгебра над полем k. Тогда существует натуральное число s и инъекционное алгебро-мополчение из многочленовой кольца k[X0, X1, ..., Xs−1] в A так, что A конечна как модуль над образцом этого кольцевого подалгебра.
LaTeX
$$$\exists s \in \mathbb{N},\; \exists \phi: k[X_0,\dots,X_{s-1}] \to_k\text{A},\; \phi \text{ injective},\; \text{A is finite as a }\phi(k[X_0,\dots,X_{s-1}])\text{-module}$$$
Lean4
/-- For a finitely generated algebra `A` over a field `k`,
there exists a natural number `s` and an injective homomorphism
from `k[X_0, X_1, ..., X_(s-1)]` to `A` such that `A` is finite over `k[X_0, X_1, ..., X_(s-1)]`. -/
theorem exists_finite_inj_algHom_of_fg : ∃ s, ∃ g : (MvPolynomial (Fin s) k) →ₐ[k] R, Function.Injective g ∧ g.Finite :=
by
obtain ⟨s, g, ⟨inj, int⟩⟩ := exists_integral_inj_algHom_of_fg k R
have h : algebraMap k R = g.toRingHom.comp (algebraMap k (MvPolynomial (Fin s) k)) :=
by
algebraize [g.toRingHom]
rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']
exact ⟨s, g, inj, int.to_finite (h ▸ RingHom.finiteType_algebraMap.mpr fin).of_comp_finiteType⟩
