English
An algebra A over R is finitely generated if and only if it is a quotient of a free algebra on a finite set of generators.
Русский
Алгебра A над R имеет конечную порождающую набор, если и только если она является квартивентом свободной алгебры на конечном множестве генераторов.
LaTeX
$$FiniteType\\ R\\ A \\iff\\ ∃ s\\ (s\\text{ Finset A})\\ (f : FreeAlgebra\\ R\\ s \\to[R] A), Surjective f$$
Lean4
/-- An algebra is finitely generated if and only if it is a quotient
of a free algebra whose variables are indexed by a finset. -/
theorem iff_quotient_freeAlgebra : FiniteType R A ↔ ∃ (s : Finset A) (f : FreeAlgebra R s →ₐ[R] A), Surjective f :=
by
constructor
· rintro ⟨s, hs⟩
refine ⟨s, FreeAlgebra.lift _ (↑), ?_⟩
rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe_subtype,
Finset.setOf_mem, hs, coe_top]
· rintro ⟨s, f, hsur⟩
exact .of_surjective f hsur
