feat(ring_theory/ideal/over): S/p is noetherian over R/p if S i…

…s over `R` (#12183)

src/ring_theory/ideal/over.lean

@@ -166,6 +166,12 @@ is_scalar_tower.of_algebra_map_eq $ λ x,
 by rw [quotient.algebra_map_eq, quotient.algebra_map_quotient_map_quotient,
        quotient.mk_algebra_map]
 
+instance quotient_map_quotient.is_noetherian [algebra R S] [is_noetherian R S] (I : ideal R) :
+  is_noetherian (R ⧸ I) (S ⧸ ideal.map (algebra_map R S) I) :=
+is_noetherian_of_tower R $
+is_noetherian_of_surjective S (ideal.quotient.mkₐ R _).to_linear_map $
+linear_map.range_eq_top.mpr ideal.quotient.mk_surjective
+
 end comm_ring
 
 section is_domain

src/ring_theory/ideal/quotient.lean

@@ -107,6 +107,13 @@ not_congr zero_eq_one_iff
 protected theorem nontrivial {I : ideal R} (hI : I ≠ ⊤) : nontrivial (R ⧸ I) :=
 ⟨⟨0, 1, zero_ne_one_iff.2 hI⟩⟩
 
+lemma subsingleton_iff {I : ideal R} : subsingleton (R ⧸ I) ↔ I = ⊤ :=
+by rw [eq_top_iff_one, ← subsingleton_iff_zero_eq_one, eq_comm,
+       ← I^.quotient.mk^.map_one, quotient.eq_zero_iff_mem]
+
+instance : unique (R ⧸ (⊤ : ideal R)) :=
+⟨⟨0⟩, by rintro ⟨x⟩; exact quotient.eq_zero_iff_mem.mpr submodule.mem_top⟩
+
 lemma mk_surjective : function.surjective (mk I) :=
 λ y, quotient.induction_on' y (λ x, exists.intro x rfl)