feat(ring_theory): the surjective image of a PID is a PID (#9069)

If the preimage of an ideal/submodule under a surjective map is principal, so is the original ideal. Therefore, the image of a principal ideal domain under a surjective ring hom is again a PID.

src/ring_theory/principal_ideal_domain.lean

@@ -75,6 +75,10 @@ classical.some (principal S)
 lemma span_singleton_generator (S : submodule R M) [S.is_principal] : span R {generator S} = S :=
 eq.symm (classical.some_spec (principal S))
 
+lemma _root_.ideal.span_singleton_generator (I : ideal R) [I.is_principal] :
+  ideal.span ({generator I} : set R) = I :=
+eq.symm (classical.some_spec (principal I))
+
 @[simp] lemma generator_mem (S : submodule R M) [S.is_principal] : generator S ∈ S :=
 by { conv_rhs { rw ← span_singleton_generator S }, exact subset_span (mem_singleton _) }
 
@@ -118,7 +122,7 @@ is_maximal_iff.2 ⟨(ne_top_iff_one S).1 hpi.1, begin
   assume T x hST hxS hxT,
   cases (mem_iff_generator_dvd _).1 (hST $ generator_mem S) with z hz,
   cases hpi.mem_or_mem (show generator T * z ∈ S, from hz ▸ generator_mem S),
-  { have hTS : T ≤ S, rwa [← span_singleton_generator T, submodule.span_le, singleton_subset_iff],
+  { have hTS : T ≤ S, rwa [← T.span_singleton_generator, ideal.span_le, singleton_subset_iff],
     exact (hxS $ hTS hxT).elim },
   cases (mem_iff_generator_dvd _).1 h with y hy,
   have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS,
@@ -242,3 +246,32 @@ instance to_unique_factorization_monoid : unique_factorization_monoid R :=
 end
 
 end principal_ideal_ring
+
+section surjective
+
+open submodule
+
+variables {S N : Type*} [ring R] [add_comm_group M] [add_comm_group N] [ring S]
+variables [module R M] [module R N]
+
+lemma submodule.is_principal.of_comap (f : M →ₗ[R] N) (hf : function.surjective f)
+  (S : submodule R N) [hI : is_principal (S.comap f)] :
+  is_principal S :=
+⟨⟨f (is_principal.generator (S.comap f)),
+  by rw [← set.image_singleton, ← submodule.map_span,
+      is_principal.span_singleton_generator, submodule.map_comap_eq_of_surjective hf]⟩⟩
+
+lemma ideal.is_principal.of_comap (f : R →+* S) (hf : function.surjective f)
+  (I : ideal S) [hI : is_principal (I.comap f)] :
+  is_principal I :=
+⟨⟨f (is_principal.generator (I.comap f)),
+  by rw [ideal.submodule_span_eq, ← set.image_singleton, ← ideal.map_span,
+    ideal.span_singleton_generator, ideal.map_comap_of_surjective f hf]⟩⟩
+
+/-- The surjective image of a principal ideal ring is again a principal ideal ring. -/
+lemma is_principal_ideal_ring.of_surjective [is_principal_ideal_ring R]
+  (f : R →+* S) (hf : function.surjective f) :
+  is_principal_ideal_ring S :=
+⟨λ I, ideal.is_principal.of_comap f hf I⟩
+
+end surjective