English
A finite presentation is equivalent to having a quotient of a mvPolynomial by a finitely generated ideal with a surjective map.
Русский
Финитная презентация эквивалентна тому, что A является фактор-млаим mvPolynomial по FG-идеалу через сюръективное отображение.
LaTeX
$$$\\text{FinitePresentation } R A \\iff \\exists ι (\\text{Fintype } ι) (f : \\mathrm{MvPolynomial } ι R \\to_A A), \\; \\text{Surjective } f \\wedge (\\ker f).FG$$$
Lean4
/-- An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose
variables are indexed by a fintype by a finitely generated ideal. -/
theorem iff_quotient_mvPolynomial' :
FinitePresentation R A ↔
∃ (ι : Type*) (_ : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A), Surjective f ∧ (RingHom.ker f.toRingHom).FG :=
by
constructor
· rintro ⟨n, f, hfs, hfk⟩
set ulift_var := MvPolynomial.renameEquiv R Equiv.ulift
refine
⟨ULift (Fin n), inferInstance, f.comp ulift_var.toAlgHom, hfs.comp ulift_var.surjective,
Ideal.fg_ker_comp _ _ ?_ hfk ulift_var.surjective⟩
simpa using Submodule.fg_bot
· rintro ⟨ι, hfintype, f, hf⟩
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
use Fintype.card ι, f.comp equiv.symm, hf.1.comp (AlgEquiv.symm equiv).surjective
refine Ideal.fg_ker_comp (S := MvPolynomial ι R) (A := A) _ f ?_ hf.2 equiv.symm.surjective
simpa using Submodule.fg_bot
