Finiteness of quotient modules

instance module_finite_of_liesOver {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [Module.Finite A B] : Module.Finite (A ⧸ p) (B ⧸ P)

B ⧸ P is a finite A ⧸ p-module if B is a finite A-module.

instance algebra_finiteType_of_liesOver {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [Algebra.FiniteType A B] : Algebra.FiniteType (A ⧸ p) (B ⧸ P)

B ⧸ P is a finitely generated A ⧸ p-algebra if B is a finitely generated A-algebra.

instance isNoetherian_of_liesOver {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [IsNoetherian A B] : IsNoetherian (A ⧸ p) (B ⧸ P)

B ⧸ P is a Noetherian A ⧸ p-module if B is a Noetherian A-module.

instance QuotientMapQuotient.isNoetherian {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [IsNoetherian A B] : IsNoetherian (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)