English
Over a Noetherian ring R, a finitely generated algebra A is finitely presented iff A is finitely generated and relations are finitely generated, i.e., Noetherian condition ensures equivalence between finite type and finite presentation.
Русский
Над Noetherian кольцом R, алгебра A, являясь конечно порождаемой, эквивалентна конечной презентации; Noetherian условие обеспечивает эквивалентность между конечной порождаемостью и конечной презентацией.
LaTeX
$$$[\\text{IsNoetherianRing } R]\\;:\\; \\text{FiniteType } R A \\iff \\text{FinitePresentation } R A$$$
Lean4
/-- An algebra over a Noetherian ring is finitely generated if and only if it is finitely
presented. -/
theorem of_finiteType [IsNoetherianRing R] : FiniteType R A ↔ FinitePresentation R A :=
by
refine ⟨fun h => ?_, fun hfp => Algebra.FiniteType.of_finitePresentation⟩
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.1 h
refine ⟨n, f, hf, ?_⟩
exact (inferInstance : IsNoetherianRing (MvPolynomial (Fin n) R)).noetherian (RingHom.ker f.toRingHom)
