Descent of Noetherianity along faithfully flat algebras #
A ring is Noetherian as soon as some faithfully flat algebra over it is Noetherian: extension of scalars embeds the ideals of the base into the submodules of the base change, which is the algebra itself.
Main results #
IsNoetherianRing.of_faithfullyFlat: Noetherianity descends along a faithfully flat algebra.
theorem
IsNoetherianRing.of_faithfullyFlat
{A : Type u_1}
(B : Type u_2)
[CommRing A]
[CommRing B]
[Algebra A B]
[Module.FaithfullyFlat A B]
[IsNoetherianRing B]
:
A ring is Noetherian if some faithfully flat algebra over it is Noetherian.