English
A commutative algebra is finitely generated over R if and only if it is a quotient of a polynomial ring in finitely many variables over R.
Русский
Коммутативная алгебра над R конечна по порождению тогда и только тогда, когда она является фактор-алгеброй полинномного кольца в конечном числе переменных над R.
LaTeX
$$FiniteType\\ R\\ S\\iff\\ ∃ s\\ (Finset\\ S)\\ (f : MvPolynomial\\ { x\\;\\vert\\; x∈s }\\ R →ₐ[R] S), Surjective f$$
Lean4
/-- A commutative algebra is finitely generated if and only if it is a quotient
of a polynomial ring whose variables are indexed by a finset. -/
theorem iff_quotient_mvPolynomial :
FiniteType R S ↔ ∃ (s : Finset S) (f : MvPolynomial { x // x ∈ s } R →ₐ[R] S), Surjective f :=
by
constructor
· rintro ⟨s, hs⟩
use s, MvPolynomial.aeval (↑)
intro x
have hrw : (↑s : Set S) = fun x : S => x ∈ s.val := rfl
rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range]
simp_rw [← hrw, hs]
exact Set.mem_univ x
· rintro ⟨s, f, hsur⟩
exact .of_surjective f hsur
