English
A finite type over R is equivalent to the existence of a finitely generated presentation of S via a polynomial algebra with variables indexed by a finite type.
Русский
С точки зрения порождения над R, конечная порождаемость эквивалентна существованиюresentation через полиномиальную алгебру с переменными, индексированными конечным множеством.
LaTeX
$$FiniteType\\ R\\ S \\iff\\ ∃ ι\\ (Fintype\\ ι)\\ (f : MvPolynomial\\ { x // x∈ι }\\ R →ₐ[R] S), Surjective f$$
Lean4
/-- An 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_freeAlgebra' :
FiniteType R A ↔ ∃ (ι : Type uA) (_ : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A), Surjective f :=
by
constructor
· rw [iff_quotient_freeAlgebra]
rintro ⟨s, f, hsur⟩
use { x : A // x ∈ s }, inferInstance, f
· rintro ⟨ι, hfintype, f, hsur⟩
letI : Fintype ι := hfintype
exact .of_surjective f hsur
