chore(RingTheory/PrincipalIdealDomain): factor out IsPrincipal.map, use RingHomClass (#18010)

Author: pechersky

Mathlib/RingTheory/PrincipalIdealDomain.lean

@@ -348,23 +348,32 @@ section Surjective
 
 open Submodule
 
-variable {S N : Type*} [Ring R] [AddCommGroup M] [AddCommGroup N] [Ring S]
-variable [Module R M] [Module R N]
+variable {S N F : Type*} [Ring R] [AddCommGroup M] [AddCommGroup N] [Ring S]
+variable [Module R M] [Module R N] [FunLike F R S] [RingHomClass F R S]
+
+theorem Submodule.IsPrincipal.map (f : M →ₗ[R] N) {S : Submodule R M}
+    (hI : IsPrincipal S) : IsPrincipal (map f S) :=
+  ⟨⟨f (IsPrincipal.generator S), by
+      rw [← Set.image_singleton, ← map_span, span_singleton_generator]⟩⟩
 
 theorem Submodule.IsPrincipal.of_comap (f : M →ₗ[R] N) (hf : Function.Surjective f)
-    (S : Submodule R N) [hI : IsPrincipal (S.comap f)] : IsPrincipal S :=
-  ⟨⟨f (IsPrincipal.generator (S.comap f)), by
-      rw [← Set.image_singleton, ← Submodule.map_span, IsPrincipal.span_singleton_generator,
-        Submodule.map_comap_eq_of_surjective hf]⟩⟩
-
-theorem Ideal.IsPrincipal.of_comap (f : R →+* S) (hf : Function.Surjective f) (I : Ideal S)
-    [hI : IsPrincipal (I.comap f)] : IsPrincipal I :=
-  ⟨⟨f (IsPrincipal.generator (I.comap f)), by
+    (S : Submodule R N) [hI : IsPrincipal (S.comap f)] : IsPrincipal S := by
+  rw [← Submodule.map_comap_eq_of_surjective hf S]
+  exact hI.map f
+
+theorem Submodule.IsPrincipal.map_ringHom (f : F) {I : Ideal R}
+    (hI : IsPrincipal I) : IsPrincipal (Ideal.map f I) :=
+  ⟨⟨f (IsPrincipal.generator I), by
       rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
-        Ideal.span_singleton_generator, Ideal.map_comap_of_surjective f hf]⟩⟩
+      Ideal.span_singleton_generator]⟩⟩
+
+theorem Ideal.IsPrincipal.of_comap (f : F) (hf : Function.Surjective f) (I : Ideal S)
+    [hI : IsPrincipal (I.comap f)] : IsPrincipal I := by
+  rw [← map_comap_of_surjective f hf I]
+  exact hI.map_ringHom f
 
 /-- The surjective image of a principal ideal ring is again a principal ideal ring. -/
-theorem IsPrincipalIdealRing.of_surjective [IsPrincipalIdealRing R] (f : R →+* S)
+theorem IsPrincipalIdealRing.of_surjective [IsPrincipalIdealRing R] (f : F)
     (hf : Function.Surjective f) : IsPrincipalIdealRing S :=
   ⟨fun I => Ideal.IsPrincipal.of_comap f hf I⟩