English
A finite type over R is equivalent to a surjective homomorphism from mvPolynomial in n variables for some n.
Русский
Конечная порождаемость над R эквивалентна существованию сюръективного гомоморфизма из mvPolynomial в сколь угодно число переменных.
LaTeX
$$FiniteType\\ R\\ S \\iff\\ ∃ n\\ (f : MvPolynomial\\ (Fin n)\\ 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 fintype. -/
theorem iff_quotient_mvPolynomial' :
FiniteType R S ↔ ∃ (ι : Type uS) (_ : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S), Surjective f :=
by
constructor
· rw [iff_quotient_mvPolynomial]
rintro ⟨s, f, hsur⟩
use { x : S // x ∈ s }, inferInstance, f
· rintro ⟨ι, hfintype, f, hsur⟩
letI : Fintype ι := hfintype
exact .of_surjective f hsur
