iff_quotient_mvPolynomial'' — Mathlib

English

If R is Noetherian and S is a finitely generated R-algebra, then S is Noetherian.

Русский

Если R является кольцом Ноether, и S — конечно порождаемая над R алгебра, то S также Ноether.

LaTeX

$$IsNoetherianRing\\ R\\Rightarrow IsNoetherianRing\\ S$$

Lean4

/-- A commutative algebra is finitely generated if and only if it is a quotient of a polynomial ring
in `n` variables. -/
theorem iff_quotient_mvPolynomial'' : FiniteType R S ↔ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S), Surjective f :=
  by
  constructor
  · rw [iff_quotient_mvPolynomial']
    rintro ⟨ι, hfintype, f, hsur⟩
    have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
    exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩
  · rintro ⟨n, f, hsur⟩
    exact .of_surjective f hsur

Похожие утверждения