chore: make a few lemmas using in RingHomClass definitions take in a concrete morphism

Mathlib/RingTheory/DedekindDomain/Basic.lean

@@ -99,7 +99,8 @@ theorem of_ringEquiv [hA : Ring.DimensionLEOne A] (e : R ≃+* A) : Ring.Dimensi
     rw [← Ideal.map_comap_eq_self_of_equiv e.symm P,
       Ideal.isMaximal_map_iff_of_bijective _ e.symm.bijective]
     apply Ring.DimensionLEOne.maximalOfPrime ?_ (P.comap_isPrime e.symm)
-    simp [Ideal.map_eq_bot_iff_of_injective e.injective, hP_ne]
+    simp --[Ideal.map_eq_bot_iff_of_injective (f := e.toRingHom) e.injective, hP_ne]
+    sorry
 
 -- TODO: replace `Ring.DimensionLEOne` with `Ring.KrullDimLE`.
 instance (priority := low) {R : Type*} [CommRing R] [Ring.DimensionLEOne R] : Ring.KrullDimLE 1 R :=

Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

@@ -465,8 +465,11 @@ theorem eq_prime_pow_mul_coprime {I : Ideal T} (hI : I ≠ ⊥)
 theorem map_prime_of_equiv {R : Type*} [CommRing R] [IsDedekindDomain R]
     (f : T ≃+* R) {I : Ideal T} (hI : Prime I) (h : I ≠ ⊥) : Prime (I.map f) := by
   rw [prime_iff_isPrime h] at hI
-  exact (prime_iff_isPrime <| (I.map_eq_bot_iff_of_injective f.injective).not.2 h).2
-    (map_isPrime_of_equiv _)
+  refine (prime_iff_isPrime ?_).2 (map_isPrime_of_equiv _)
+  -- TODO: simplify this once Ideal.map takes a concrete ring homomorphism
+  suffices map f.toRingHom I ≠ ⊥ from this
+  have aux := I.map_eq_bot_iff_of_injective (f := f.toRingHom) f.injective
+  simp_all
 
 @[deprecated (since := "2026-04-16")] alias _root_.map_prime_of_equiv := map_prime_of_equiv
 

Mathlib/RingTheory/Extension/Presentation/Basic.lean

@@ -439,10 +439,15 @@ lemma span_range_relation_eq_ker_comp : Ideal.span
     (Set.range (Sum.elim (Algebra.Presentation.compRelationAux Q P)
       fun rp ↦ (rename Sum.inr) (P.relation rp))) = (Q.comp P.toGenerators).ker := by
   rw [Generators.ker_eq_ker_aeval_val, Q.aeval_comp_val_eq, ← AlgHom.comap_ker]
-  change _ = Ideal.comap _ (RingHom.ker (aeval Q.val))
+  change _ = Ideal.comap (Q.aux P).toRingHom (RingHom.ker (aeval Q.val))
+  -- TODO: change Ideal.map to take a concrete morphism, then this `have` can be deleted
+  have h (I : Ideal (MvPolynomial (ι' ⊕ ι) R)) :
+      Ideal.map (Q.aux P) I = Ideal.map (Q.aux P).toRingHom I := rfl
+  -- TODO: change RingHom.ker to take a concrete morphism, then this `have` can be deleted
+  have h' : RingHom.ker (Q.aux P).toRingHom = RingHom.ker (Q.aux P) := rfl
   rw [← Q.ker_eq_ker_aeval_val, ← Q.span_range_relation_eq_ker, ← Q.aux_image_relation P,
-    ← Ideal.map_span, Ideal.comap_map_of_surjective' _ (Q.aux_surjective P)]
-  rw [Set.Sum.elim_range, Ideal.span_union, Q.aux_ker, ← P.ker_eq_ker_aeval_val,
+    ← Ideal.map_span, h, Ideal.comap_map_of_surjective' _ (Q.aux_surjective P),
+    Set.Sum.elim_range, Ideal.span_union, h', Q.aux_ker, ← P.ker_eq_ker_aeval_val,
     ← P.span_range_relation_eq_ker, Ideal.map_span]
   congr
   ext

Mathlib/RingTheory/Ideal/Maps.lean

@@ -823,9 +823,10 @@ end Ring
 
 section RingRing
 
-variable {F : Type*} [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S] (f : F)
+variable [Ring R] [Ring S]
 
-theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y := by rw [mem_ker, map_sub, sub_eq_zero]
+theorem sub_mem_ker_iff (f : R →+* S) {x y} : x - y ∈ ker f ↔ f x = f y := by
+  rw [mem_ker, map_sub, sub_eq_zero]
 
 @[simp]
 theorem ker_rangeRestrict (f : R →+* S) : ker f.rangeRestrict = ker f :=
@@ -834,15 +835,13 @@ theorem ker_rangeRestrict (f : R →+* S) : ker f.rangeRestrict = ker f :=
 end RingRing
 
 /-- The kernel of a homomorphism to a domain is a prime ideal. -/
-theorem ker_isPrime {F : Type*} [Semiring R] [Semiring S] [IsDomain S]
-    [FunLike F R S] [RingHomClass F R S] (f : F) :
+theorem ker_isPrime [Semiring R] [Semiring S] [IsDomain S] (f : R →+* S) :
     (ker f).IsPrime :=
   inferInstanceAs (Ideal.comap f ⊥).IsPrime
 
 /-- The kernel of a homomorphism to a division ring is a maximal ideal. -/
-theorem ker_isMaximal_of_surjective {R K F : Type*} [Ring R] [DivisionRing K]
-    [FunLike F R K] [RingHomClass F R K] (f : F)
-    (hf : Function.Surjective f) : (ker f).IsMaximal :=
+theorem ker_isMaximal_of_surjective {R K : Type*} [Ring R] [DivisionRing K]
+    (f : R →+* K) (hf : Function.Surjective f) : (ker f).IsMaximal :=
   have := Ideal.bot_isMaximal (K := K)
   Ideal.comap_isMaximal_of_surjective _ hf
 
@@ -1040,16 +1039,16 @@ end annihilator
 
 namespace Ideal
 
-variable {R : Type*} {S : Type*} {F : Type*}
+variable {R : Type*} {S : Type*}
 
 section Semiring
 
-variable [Semiring R] [Semiring S] [FunLike F R S] [rc : RingHomClass F R S]
+variable [Semiring R] [Semiring S]
 
-theorem map_eq_bot_iff_le_ker {I : Ideal R} (f : F) : I.map f = ⊥ ↔ I ≤ RingHom.ker f := by
+theorem map_eq_bot_iff_le_ker {I : Ideal R} (f : R →+* S) : I.map f = ⊥ ↔ I ≤ RingHom.ker f := by
   rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]
 
-theorem ker_le_comap {K : Ideal S} (f : F) : RingHom.ker f ≤ comap f K := fun _ hx =>
+theorem ker_le_comap {K : Ideal S} (f : R →+* S) : RingHom.ker f ≤ comap f K := fun _ hx =>
   mem_comap.2 (RingHom.mem_ker.1 hx ▸ K.zero_mem)
 
 /-- A ring isomorphism sends a prime ideal to a prime ideal. -/
@@ -1059,7 +1058,7 @@ instance map_isPrime_of_equiv {F' : Type*} [EquivLike F' R S] [RingEquivClass F'
   rw [h, map_comap_of_equiv (RingEquivClass.toRingEquiv f : R ≃+* S)]
   exact Ideal.IsPrime.comap (RingEquivClass.toRingEquiv f : R ≃+* S).symm
 
-theorem map_eq_bot_iff_of_injective {I : Ideal R} {f : F} (hf : Function.Injective f) :
+theorem map_eq_bot_iff_of_injective {I : Ideal R} {f : R →+* S} (hf : Function.Injective f) :
     I.map f = ⊥ ↔ I = ⊥ := by
   simp [map, ← map_zero f, -map_zero, hf.eq_iff, I.eq_bot_iff]
 
@@ -1074,13 +1073,15 @@ lemma map_pointwise_smul {R S : Type*} [CommSemiring R] [CommSemiring S]
 
 section Ring
 
-variable [Ring R] [Ring S] [FunLike F R S] [rc : RingHomClass F R S]
+variable [Ring R] [Ring S]
 
-lemma comap_map_of_surjective' (f : F) (hf : Function.Surjective f) (I : Ideal R) :
+lemma comap_map_of_surjective' (f : R →+* S) (hf : Function.Surjective f) (I : Ideal R) :
     (I.map f).comap f = I ⊔ RingHom.ker f :=
   comap_map_of_surjective f hf I
 
-theorem map_sInf {A : Set (Ideal R)} {f : F} (hf : Function.Surjective f) :
+variable {f : R →+* S}
+
+theorem map_sInf {A : Set (Ideal R)} (hf : Function.Surjective f) :
     (∀ J ∈ A, RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A) := by
   refine fun h => le_antisymm (le_sInf ?_) ?_
   · intro j hj y hy
@@ -1100,7 +1101,7 @@ theorem map_sInf {A : Set (Ideal R)} {f : F} (hf : Function.Surjective f) :
       rw [RingHom.mem_ker, map_sub, hx, sub_self]
     simpa only [sub_add_cancel] using J.add_mem this hx'
 
-theorem map_isPrime_of_surjective {f : F} (hf : Function.Surjective f) {I : Ideal R} [H : IsPrime I]
+theorem map_isPrime_of_surjective (hf : Function.Surjective f) {I : Ideal R} [H : IsPrime I]
     (hk : RingHom.ker f ≤ I) : IsPrime (map f I) := by
   refine ⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩
   · replace h := congr_arg (comap f) h
@@ -1116,7 +1117,7 @@ theorem map_isPrime_of_surjective {f : F} (hf : Function.Surjective f) {I : Idea
     exact
       (H.mem_or_mem this).imp (fun h => ha ▸ mem_map_of_mem f h) fun h => hb ▸ mem_map_of_mem f h
 
-lemma IsMaximal.map_of_surjective_of_ker_le {f : F} (hf : Function.Surjective f) {m : Ideal R}
+lemma IsMaximal.map_of_surjective_of_ker_le (hf : Function.Surjective f) {m : Ideal R}
     [m.IsMaximal] (hk : RingHom.ker f ≤ m) : (m.map f).IsMaximal := by
   refine m.map_eq_top_or_isMaximal_of_surjective f hf ‹_› |>.resolve_left fun h => ?_
   apply congr_arg (comap f) at h

Mathlib/RingTheory/IsAdjoinRoot.lean

@@ -375,12 +375,18 @@ variable (h : IsAdjoinRootMonic S f)
 open IsAdjoinRoot
 
 theorem map_modByMonic (g : R[X]) : h.map (g %ₘ f) = h.map g := by
-  rw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div, sub_right_comm,
+  -- TODO: fix by making RingHom.ker take a concrete morphism instead!
+  erw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div, sub_right_comm,
     sub_self, zero_sub, dvd_neg]
   exact ⟨_, rfl⟩
 
 theorem modByMonic_repr_map (g : R[X]) : h.repr (h.map g) %ₘ f = g %ₘ f :=
-  modByMonic_eq_of_dvd_sub h.monic <| by rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]
+  -- TODO: fix by making RingHom.ker take a concrete morphism instead!
+  modByMonic_eq_of_dvd_sub h.monic <| by
+    --rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]
+    rw [← h.mem_ker_map]
+    erw [RingHom.sub_mem_ker_iff h.map.toRingHom (x := h.repr (h.map g)) (y := g), map_repr]
+    rfl
 
 /-- `IsAdjoinRoot.modByMonicHom` sends the equivalence class of `f` mod `g` to `f %ₘ g`. -/
 def modByMonicHom : S →ₗ[R] R[X] where

Mathlib/RingTheory/Nullstellensatz.lean

@@ -103,11 +103,11 @@ theorem mem_vanishingIdeal_singleton_iff (x : σ → K) (p : MvPolynomial σ k)
   ⟨fun h => h x rfl, fun hpx _ hy => hy.symm ▸ hpx⟩
 
 instance {x : σ → K} : (vanishingIdeal k {x} : Ideal (MvPolynomial σ k)).IsPrime := by
-  convert! RingHom.ker_isPrime (aeval (R := k) x)
+  convert! RingHom.ker_isPrime (aeval (R := k) x).toRingHom
   ext; simp
 
 instance {x : σ → K} : (vanishingIdeal K {x} : Ideal (MvPolynomial σ K)).IsMaximal := by
-  convert! RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_
+  convert! RingHom.ker_isMaximal_of_surjective (aeval (R := K) x).toRingHom ?_
   · ext; simp
   · intro z; use C z; simp