English
If R and S are commutative rings with S finitely presented over R, then there exist natural numbers n and m such that there is a presentation of S as an R-algebra with Fin(n) generators and Fin(m) relations.
Русский
Если кольца R и S коммутативны и S является конечно presentations над R, то существуют натуральные числа n и m, такие что существует презентация S как A–алгебры над R с Fin(n) генераторами и Fin(m) отношениями.
LaTeX
$$$\\exists n\\,\\exists m\\,\\text{Nonempty} \\bigl(\\mathrm{Presentation}\\; R\\; S\\; (\\mathrm{Fin}\\,n)\\; (\\mathrm{Fin}\\,m)\\bigr)$$$
Lean4
theorem exists_presentation_fin [FinitePresentation R S] : ∃ n m, Nonempty (Presentation R S (Fin n) (Fin m)) :=
letI H := FinitePresentation.out (R := R) (A := S)
letI n : ℕ := H.choose
letI f : MvPolynomial (Fin n) R →ₐ[R] S := H.choose_spec.choose
haveI hf : Function.Surjective f := H.choose_spec.choose_spec.1
haveI hf' : (RingHom.ker f).FG := H.choose_spec.choose_spec.2
letI H' := Submodule.fg_iff_exists_fin_generating_family.mp hf'
let m : ℕ := H'.choose
let v : Fin m → MvPolynomial (Fin n) R := H'.choose_spec.choose
have hv : Ideal.span (Set.range v) = RingHom.ker f := H'.choose_spec.choose_spec
⟨n, m,
⟨{ __ := Generators.ofSurjective (fun x ↦ f (.X x)) (by convert hf; ext; simp)
relation := v
span_range_relation_eq_ker := hv.trans (by congr; ext; simp) }⟩⟩
