refactor(ring_theory/non_zero_divisors): use fun_like (#11764)

src/field_theory/ratfunc.lean

@@ -467,8 +467,8 @@ def lift_monoid_with_zero_hom (φ : polynomial K →*₀ G₀) (hφ : function.i
 { to_fun := λ f, ratfunc.lift_on f (λ p q, φ p / (φ q)) $ λ p q p' q' hq hq' h, begin
     casesI subsingleton_or_nontrivial K,
     { rw [subsingleton.elim p q, subsingleton.elim p' q, subsingleton.elim q' q] },
-    rw [div_eq_div_iff (φ.map_ne_zero_of_mem_non_zero_divisors hφ hq)
-        (φ.map_ne_zero_of_mem_non_zero_divisors hφ hq'), ←map_mul, h, map_mul]
+    rw [div_eq_div_iff (map_ne_zero_of_mem_non_zero_divisors _ hφ hq)
+        (map_ne_zero_of_mem_non_zero_divisors _ hφ hq'), ←map_mul, h, map_mul]
   end,
   map_one' := by { rw [←of_fraction_ring_one, ←localization.mk_one, lift_on_of_fraction_ring_mk],
                    simp only [map_one, submonoid.coe_one, div_one] },
@@ -497,7 +497,7 @@ begin
     intro h,
     refine localization.r_of_eq _,
     simpa only [←hφ.eq_iff, map_mul] using mul_eq_mul_of_div_eq_div _ _ _ _ h.symm;
-    exact (φ.map_ne_zero_of_mem_non_zero_divisors hφ (set_like.coe_mem _)) },
+    exact (map_ne_zero_of_mem_non_zero_divisors _ hφ (set_like.coe_mem _)) },
   { exact λ _, rfl },
   { exact λ _, rfl }
 end
@@ -517,7 +517,7 @@ def lift_ring_hom (φ : polynomial K →+* L) (hφ : function.injective φ) : ra
         simp only [map_add, map_mul, submonoid.coe_mul] },
       all_goals {
         try { simp only [←map_mul, ←submonoid.coe_mul] },
-        exact ring_hom.map_ne_zero_of_mem_non_zero_divisors _ hφ (set_like.coe_mem _) } },
+        exact map_ne_zero_of_mem_non_zero_divisors _ hφ (set_like.coe_mem _) } },
     { refl },
     { refl } },
   ..lift_monoid_with_zero_hom φ.to_monoid_with_zero_hom hφ }

src/number_theory/cyclotomic/basic.lean

@@ -471,7 +471,7 @@ instance is_cyclotomic_extension [ne_zero (n : A)] :
 instance [ne_zero (n : A)] : is_fraction_ring (cyclotomic_ring n A K) (cyclotomic_field n K) :=
 { map_units := λ ⟨x, hx⟩, begin
     rw is_unit_iff_ne_zero,
-    apply ring_hom.map_ne_zero_of_mem_non_zero_divisors,
+    apply map_ne_zero_of_mem_non_zero_divisors,
     apply adjoin_algebra_injective,
     exact hx
   end,
@@ -484,7 +484,7 @@ instance [ne_zero (n : A)] : is_fraction_ring (cyclotomic_ring n A K) (cyclotomi
     { have : is_localization (non_zero_divisors A) K := infer_instance,
       replace := this.surj,
       obtain ⟨⟨z, w⟩, hw⟩ := this k,
-      refine ⟨⟨algebra_map A _ z, algebra_map A _ w, ring_hom.map_mem_non_zero_divisors _
+      refine ⟨⟨algebra_map A _ z, algebra_map A _ w, map_mem_non_zero_divisors _
         (algebra_base_injective n A K) w.2⟩, _⟩,
       letI : is_scalar_tower A K (cyclotomic_field n K) :=
         is_scalar_tower.of_algebra_map_eq (congr_fun rfl),

src/ring_theory/jacobson.lean

@@ -333,7 +333,7 @@ lemma jacobson_bot_of_integral_localization
   (⊥ : ideal S).jacobson = (⊥ : ideal S) :=
 begin
   have hM : ((submonoid.powers x).map φ : submonoid S) ≤ non_zero_divisors S :=
-    φ.map_le_non_zero_divisors_of_injective hφ (powers_le_non_zero_divisors_of_no_zero_divisors hx),
+    map_le_non_zero_divisors_of_injective φ hφ (powers_le_non_zero_divisors_of_no_zero_divisors hx),
   letI : is_domain Sₘ := is_localization.is_domain_of_le_non_zero_divisors _ hM,
   let φ' : Rₘ →+* Sₘ := is_localization.map _ φ (submonoid.powers x).le_comap_map,
   suffices : ∀ I : ideal Sₘ, I.is_maximal → (I.comap (algebra_map S Sₘ)).is_maximal,

src/ring_theory/laurent_series.lean

@@ -149,7 +149,7 @@ rfl
 instance {K : Type u} [field K] : is_fraction_ring (power_series K) (laurent_series K) :=
 is_localization.of_le (submonoid.powers (power_series.X : power_series K)) _
   (powers_le_non_zero_divisors_of_no_zero_divisors power_series.X_ne_zero)
-  (λ f hf, is_unit_of_mem_non_zero_divisors $ ring_hom.map_mem_non_zero_divisors _
+  (λ f hf, is_unit_of_mem_non_zero_divisors $ map_mem_non_zero_divisors _
     hahn_series.of_power_series_injective hf)
 
 end laurent_series

src/ring_theory/localization.lean

@@ -1850,7 +1850,7 @@ end
 protected lemma to_map_ne_zero_of_mem_non_zero_divisors [nontrivial R]
   (hM : M ≤ non_zero_divisors R) {x : R} (hx : x ∈ non_zero_divisors R) : algebra_map R S x ≠ 0 :=
 show (algebra_map R S).to_monoid_with_zero_hom x ≠ 0,
-from (algebra_map R S).map_ne_zero_of_mem_non_zero_divisors (is_localization.injective S hM) hx
+from map_ne_zero_of_mem_non_zero_divisors (algebra_map R S) (is_localization.injective S hM) hx
 
 variables (S Q M)
 
@@ -2217,7 +2217,7 @@ in ⟨x, y, hy, by rwa mk'_eq_div at h⟩
 lemma is_unit_map_of_injective (hg : function.injective g)
   (y : non_zero_divisors A) : is_unit (g y) :=
 is_unit.mk0 (g y) $ show g.to_monoid_with_zero_hom y ≠ 0,
-  from g.map_ne_zero_of_mem_non_zero_divisors hg y.2
+  from map_ne_zero_of_mem_non_zero_divisors g hg y.2
 
 /-- Given an integral domain `A` with field of fractions `K`,
 and an injective ring hom `g : A →+* L` where `L` is a field, we get a
@@ -2246,10 +2246,12 @@ by simp only [mk'_eq_div, ring_hom.map_div, lift_algebra_map]
 and an injective ring hom `j : A →+* B`, we get a field hom
 sending `z : K` to `g (j x) * (g (j y))⁻¹`, where `(x, y) : A × (non_zero_divisors A)` are
 such that `z = f x * (f y)⁻¹`. -/
-noncomputable def map [algebra B L] [is_fraction_ring B L] {j : A →+* B} (hj : injective j) :
+noncomputable def map {A B K L : Type*} [comm_ring A] [comm_ring B] [is_domain B]
+  [comm_ring K] [algebra A K] [is_fraction_ring A K] [comm_ring L] [algebra B L]
+  [is_fraction_ring B L] {j : A →+* B} (hj : injective j) :
   K →+* L :=
 map L j (show non_zero_divisors A ≤ (non_zero_divisors B).comap j,
-         from λ y hy, j.map_mem_non_zero_divisors hj hy)
+         from non_zero_divisors_le_comap_non_zero_divisors_of_injective j hj)
 
 /-- Given integral domains `A, B` and localization maps to their fields of fractions
 `f : A →+* K, g : B →+* L`, an isomorphism `j : A ≃+* B` induces an isomorphism of

src/ring_theory/non_zero_divisors.lean

@@ -32,7 +32,7 @@ def non_zero_divisors (R : Type*) [monoid_with_zero R] : submonoid R :=
 
 localized "notation R`⁰`:9000 := non_zero_divisors R" in non_zero_divisors
 
-variables {M M' M₁ R R' : Type*} [monoid_with_zero M] [monoid_with_zero M']
+variables {M M' M₁ R R' F : Type*} [monoid_with_zero M] [monoid_with_zero M']
   [comm_monoid_with_zero M₁] [ring R] [comm_ring R']
 
 lemma mem_non_zero_divisors_iff {r : M} : r ∈ M⁰ ↔ ∀ x, x * r = 0 → x = 0 := iff.rfl
@@ -105,29 +105,21 @@ lemma eq_zero_of_ne_zero_of_mul_left_eq_zero [no_zero_divisors M]
   {x y : M} (hnx : x ≠ 0) (hxy : x * y = 0) : y = 0 :=
 or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hnx
 
+lemma mem_non_zero_divisors_of_ne_zero [no_zero_divisors M] {x : M} (hx : x ≠ 0) : x ∈ M⁰ :=
+λ _, eq_zero_of_ne_zero_of_mul_right_eq_zero hx
+
 lemma mem_non_zero_divisors_iff_ne_zero [no_zero_divisors M] [nontrivial M] {x : M} :
   x ∈ M⁰ ↔ x ≠ 0 :=
-⟨non_zero_divisors.ne_zero, λ hnx z, eq_zero_of_ne_zero_of_mul_right_eq_zero hnx⟩
-
-lemma monoid_with_zero_hom.map_ne_zero_of_mem_non_zero_divisors [nontrivial M] (g : M →*₀ M')
-  (hg : function.injective g) {x : M} (h : x ∈ M⁰) : g x ≠ 0 :=
-λ h0, one_ne_zero (h 1 ((one_mul x).symm ▸ (hg (trans h0 g.map_zero.symm))))
+⟨non_zero_divisors.ne_zero, mem_non_zero_divisors_of_ne_zero⟩
 
-lemma ring_hom.map_ne_zero_of_mem_non_zero_divisors {R R' : Type*} [semiring R] [semiring R']
-  [nontrivial R] (g : R →+* R') (hg : function.injective g)
-  {x : R} (h : x ∈ R⁰) : g x ≠ 0 :=
-g.to_monoid_with_zero_hom.map_ne_zero_of_mem_non_zero_divisors hg h
+lemma map_ne_zero_of_mem_non_zero_divisors [nontrivial M] [zero_hom_class F M M']
+  (g : F) (hg : function.injective (g : M → M')) {x : M} (h : x ∈ M⁰) : g x ≠ 0 :=
+λ h0, one_ne_zero (h 1 ((one_mul x).symm ▸ (hg (trans h0 (map_zero g).symm))))
 
-lemma monoid_with_zero_hom.map_mem_non_zero_divisors [nontrivial M] [no_zero_divisors M']
-  (g : M →*₀ M') (hg : function.injective g) {x : M} (h : x ∈ M⁰) : g x ∈ M'⁰ :=
+lemma map_mem_non_zero_divisors [nontrivial M] [no_zero_divisors M'] [zero_hom_class F M M']
+  (g : F) (hg : function.injective g) {x : M} (h : x ∈ M⁰) : g x ∈ M'⁰ :=
 λ z hz, eq_zero_of_ne_zero_of_mul_right_eq_zero
-  (g.map_ne_zero_of_mem_non_zero_divisors hg h) hz
-
-lemma ring_hom.map_mem_non_zero_divisors {R R' : Type*} [semiring R] [semiring R']
-  [nontrivial R] [no_zero_divisors R']
-  (g : R →+* R') (hg : function.injective g)
-  {x : R} (h : x ∈ R⁰) : g x ∈ R'⁰ :=
-g.to_monoid_with_zero_hom.map_mem_non_zero_divisors hg h
+  (map_ne_zero_of_mem_non_zero_divisors g hg h) hz
 
 lemma le_non_zero_divisors_of_no_zero_divisors [no_zero_divisors M] {S : submonoid M}
   (hS : (0 : M) ∉ S) : S ≤ M⁰ :=
@@ -138,17 +130,19 @@ lemma powers_le_non_zero_divisors_of_no_zero_divisors [no_zero_divisors M]
   {a : M} (ha : a ≠ 0) : submonoid.powers a ≤ M⁰ :=
 le_non_zero_divisors_of_no_zero_divisors (λ h, absurd (h.rec_on (λ _ hn, pow_eq_zero hn)) ha)
 
-lemma monoid_with_zero_hom.map_le_non_zero_divisors_of_injective [nontrivial M]
-  [no_zero_divisors M'] (f : M →*₀ M') (hf : function.injective f) {S : submonoid M} (hS : S ≤ M⁰) :
-  S.map ↑f ≤ M'⁰ :=
-le_non_zero_divisors_of_no_zero_divisors (λ h, let ⟨x, hx, hx0⟩ := h in
-  zero_ne_one (hS (hf (trans hx0 (f.map_zero.symm)) ▸ hx : 0 ∈ S) 1 (mul_zero 1)).symm)
-
-lemma ring_hom.map_le_non_zero_divisors_of_injective {R R' : Type*} [semiring R] [semiring R']
-  [nontrivial R] [no_zero_divisors R']
-  (f : R →+* R') (hf : function.injective f)
-  {S : submonoid R} (hS : S ≤ R⁰) : S.map ↑f ≤ R'⁰ :=
-f.to_monoid_with_zero_hom.map_le_non_zero_divisors_of_injective hf hS
+lemma map_le_non_zero_divisors_of_injective [no_zero_divisors M']
+  [monoid_with_zero_hom_class F M M'] (f : F) (hf : function.injective f) {S : submonoid M}
+  (hS : S ≤ M⁰) : S.map ↑f ≤ M'⁰ :=
+begin
+  casesI subsingleton_or_nontrivial M,
+  { simp [subsingleton.elim S ⊥] },
+  { exact le_non_zero_divisors_of_no_zero_divisors (λ h, let ⟨x, hx, hx0⟩ := h in
+      zero_ne_one (hS (hf (trans hx0 ((map_zero f).symm)) ▸ hx : 0 ∈ S) 1 (mul_zero 1)).symm) }
+end
+
+lemma non_zero_divisors_le_comap_non_zero_divisors_of_injective [no_zero_divisors M']
+  [monoid_with_zero_hom_class F M M'] (f : F) (hf : function.injective f) : M⁰ ≤ M'⁰.comap f :=
+submonoid.le_comap_of_map_le _ (map_le_non_zero_divisors_of_injective _ hf le_rfl)
 
 lemma prod_zero_iff_exists_zero [no_zero_divisors M₁] [nontrivial M₁]
   {s : multiset M₁} : s.prod = 0 ↔ ∃ (r : M₁) (hr : r ∈ s), r = 0 :=

src/ring_theory/polynomial/scale_roots.lean

@@ -117,7 +117,7 @@ lemma scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero
 begin
   convert scale_roots_eval₂_eq_zero f hr,
   rw [←mul_div_assoc, mul_comm, mul_div_cancel],
-  exact f.map_ne_zero_of_mem_non_zero_divisors hf hs
+  exact map_ne_zero_of_mem_non_zero_divisors _ hf hs
 end
 
 lemma scale_roots_aeval_eq_zero_of_aeval_div_eq_zero [algebra A K]