English
The Noether normalization asserts the existence of an integral injective algebra map from a polynomial ring to the finitely generated algebra, making the latter integral over the image.
Русский
Нормализация Ноэта утверждает существование интегрального инъективного алгебра-гомоморфизма из многочленовой алгебры в конечносгенерируемую алгебру, над образцом интегрально.
LaTeX
$$Exists s, Exists g, Injective g ∧ g.IsIntegral$$
Lean4
/-- **Noether normalization lemma**
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 integral over `k[X_0, X_1, ..., X_(s-1)]`.
-/
@[stacks 00OW]
theorem exists_integral_inj_algHom_of_fg :
∃ s, ∃ g : (MvPolynomial (Fin s) k) →ₐ[k] R, Function.Injective g ∧ g.IsIntegral :=
by
obtain ⟨n, f, fsurj⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp fin
set ϕ := quotientKerAlgEquivOfSurjective fsurj
obtain ⟨s, _, g, injg, intg⟩ := exists_integral_inj_algHom_of_quotient (ker f) (ker_ne_top _)
use s, ϕ.toAlgHom.comp g
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, EmbeddingLike.comp_injective,
AlgHom.toRingHom_eq_coe]
exact ⟨injg, intg.trans _ _ (isIntegral_of_surjective _ ϕ.surjective)⟩
