English
A FinitePresentation R A holds iff there exist a finite type index ι, a surjective algebra hom f from a polynomial algebra to A, and the kernel is FG.
Русский
Существует эквивалентность: FinitePresentation R A эквивалентно существованию индекса ι с конечным числом элементов, сюръективного гомоморфаFrom полиномы в A, и 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
theorem iff : FinitePresentation R A ↔ ∃ (n : _) (I : Ideal (MvPolynomial (Fin n) R)) (_ : (_ ⧸ I) ≃ₐ[R] A), I.FG :=
by
constructor
· rintro ⟨n, f, hf⟩
exact ⟨n, RingHom.ker f.toRingHom, Ideal.quotientKerAlgEquivOfSurjective hf.1, hf.2⟩
· rintro ⟨n, I, e, hfg⟩
letI := (FinitePresentation.mvPolynomial_aux R _).quotient hfg
exact equiv e
