feat(ring_theory/noetherian): is_noetherian_ring_range

Author: kckennylau

src/ring_theory/noetherian.lean

@@ -8,6 +8,7 @@ import data.equiv.algebra
 import data.polynomial
 import linear_algebra.linear_combination
 import ring_theory.ideal_operations
+import ring_theory.subring
 
 open set lattice
 
@@ -305,6 +306,12 @@ begin
   convert order_embedding.well_founded (order_embedding.rsymm (ideal.lt_order_embedding_of_surjective f hf)) H
 end
 
+theorem is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R → S) (hf : is_ring_hom f)
+  (h : is_noetherian_ring R) : is_noetherian_ring (set.range f) :=
+is_noetherian_ring_of_surjective _ _ (λ r, ⟨f r, r, rfl⟩)
+  ⟨subtype.eq $ is_ring_hom.map_one f, λ x y, subtype.eq $ is_ring_hom.map_mul f, λ x y, subtype.eq $ is_ring_hom.map_add f⟩
+  (λ ⟨y, r, h⟩, ⟨r, subtype.eq h⟩) h
+
 theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
   (f : R ≃r S) (H : is_noetherian_ring R) : is_noetherian_ring S :=
 is_noetherian_ring_of_surjective R S f.1 f.2 f.1.bijective.2 H