English
Same Noetherian property transfer: a Noetherian base ring implies Noetherian target under finite type.
Русский
То же свойство Ноether переносится под основание и целевой кольца через конечную порождаемость.
LaTeX
$$IsNoetherianRing\\ R\\Rightarrow IsNoetherianRing\\ S$$
Lean4
theorem isNoetherianRing (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] [h : Algebra.FiniteType R S]
[IsNoetherianRing R] : IsNoetherianRing S := by
obtain ⟨s, hs⟩ := h.1
apply
isNoetherianRing_of_surjective (MvPolynomial s R) S (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom
rw [← Set.range_eq_univ, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, ← AlgHom.coe_range, ←
Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Finset.setOf_mem, hs]
rfl
