feat(algebra/field): remove is_field_hom (#1777)

* feat(algebra/field): remove is_field_hom

A field homomorphism is just a ring homomorphism.
This is one trivial tiny step in moving over to bundled homs.

* Fix up nolints.txt

* Remove duplicate instances

scripts/nolints.txt

@@ -1390,7 +1390,6 @@ is_comm_applicative
 is_conj
 is_cyclic
 is_cyclic.comm_group
-is_field_hom
 is_group_hom.ker
 is_integral
 is_lawful_bifunctor

src/algebra/direct_limit.lean

@@ -480,7 +480,7 @@ end ring
 namespace field
 
 variables [Π i, field (G i)]
-variables (f : Π i j, i ≤ j → G i → G j) [Π i j hij, is_field_hom (f i j hij)]
+variables (f : Π i j, i ≤ j → G i → G j) [Π i j hij, is_ring_hom (f i j hij)]
 variables [directed_system G f]
 
 namespace direct_limit

src/algebra/field.lean

@@ -200,14 +200,12 @@ end
 
 end
 
-@[reducible] def is_field_hom {α β} [division_ring α] [division_ring β] (f : α → β) := is_ring_hom f
-
-namespace is_field_hom
+namespace is_ring_hom
 open is_ring_hom
 
 section
 variables {β : Type*} [division_ring α] [division_ring β]
-variables (f : α → β) [is_field_hom f] {x y : α}
+variables (f : α → β) [is_ring_hom f] {x y : α}
 
 lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 :=
 ⟨mt $ λ h, h.symm ▸ map_zero f,
@@ -235,7 +233,7 @@ end
 
 section
 variables {β : Type*} [discrete_field α] [discrete_field β]
-variables (f : α → β) [is_field_hom f] {x y : α}
+variables (f : α → β) [is_ring_hom f] {x y : α}
 
 lemma map_inv : f x⁻¹ = (f x)⁻¹ :=
 classical.by_cases (by rintro rfl; simp only [map_zero f, inv_zero]) (map_inv' f)
@@ -245,4 +243,4 @@ lemma map_div : f (x / y) = f x / f y :=
 
 end
 
-end is_field_hom
+end is_ring_hom

src/algebra/field_power.lean

@@ -58,14 +58,14 @@ pow_one a
 
 end field_power
 
-namespace is_field_hom
+namespace is_ring_hom
 
-lemma map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α → β) [is_field_hom f]
+lemma map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α → β) [is_ring_hom f]
   (a : α) : ∀ (n : ℤ), f (a ^ n) = f a ^ n
 | (n : ℕ) := is_semiring_hom.map_pow f a n
-| -[1+ n] := by simp [fpow_neg_succ_of_nat, is_semiring_hom.map_pow f, is_field_hom.map_inv f]
+| -[1+ n] := by simp [fpow_neg_succ_of_nat, is_semiring_hom.map_pow f, is_ring_hom.map_inv f]
 
-end is_field_hom
+end is_ring_hom
 
 section discrete_field_power
 open int

src/data/complex/basic.lean

@@ -261,10 +261,10 @@ lemma div_im (z w : ℂ) : (z / w).im = z.im * w.re / norm_sq w - z.re * w.im /
 by simp [div_eq_mul_inv, mul_assoc]
 
 @[simp, move_cast] lemma of_real_div (r s : ℝ) : ((r / s : ℝ) : ℂ) = r / s :=
-is_field_hom.map_div coe
+is_ring_hom.map_div coe
 
 @[simp, move_cast] lemma of_real_fpow (r : ℝ) (n : ℤ) : ((r ^ n : ℝ) : ℂ) = (r : ℂ) ^ n :=
-is_field_hom.map_fpow of_real r n
+is_ring_hom.map_fpow of_real r n
 
 @[simp, squash_cast] theorem of_real_int_cast : ∀ n : ℤ, ((n : ℝ) : ℂ) = n :=
 int.eq_cast (λ n, ((n : ℝ) : ℂ))

src/data/polynomial.lean

@@ -2174,34 +2174,34 @@ by rw [div_def, mul_comm, degree_mul_leading_coeff_inv _ hq0];
   exact degree_div_by_monic_lt _ (monic_mul_leading_coeff_inv hq0) hp
     (by rw degree_mul_leading_coeff_inv _ hq0; exact hq)
 
-@[simp] lemma degree_map [discrete_field β] (p : polynomial α) (f : α → β) [is_field_hom f] :
+@[simp] lemma degree_map [discrete_field β] (p : polynomial α) (f : α → β) [is_ring_hom f] :
   degree (p.map f) = degree p :=
-p.degree_map_eq_of_injective (is_field_hom.injective f)
+p.degree_map_eq_of_injective (is_ring_hom.injective f)
 
-@[simp] lemma nat_degree_map [discrete_field β] (f : α → β) [is_field_hom f] :
+@[simp] lemma nat_degree_map [discrete_field β] (f : α → β) [is_ring_hom f] :
   nat_degree (p.map f) = nat_degree p :=
 nat_degree_eq_of_degree_eq (degree_map _ f)
 
-@[simp] lemma leading_coeff_map [discrete_field β] (f : α → β) [is_field_hom f] :
+@[simp] lemma leading_coeff_map [discrete_field β] (f : α → β) [is_ring_hom f] :
   leading_coeff (p.map f) = f (leading_coeff p) :=
 by simp [leading_coeff, coeff_map f]
 
-lemma map_div [discrete_field β] (f : α → β) [is_field_hom f] :
+lemma map_div [discrete_field β] (f : α → β) [is_ring_hom f] :
   (p / q).map f = p.map f / q.map f :=
 if hq0 : q = 0 then by simp [hq0]
 else
 by rw [div_def, div_def, map_mul, map_div_by_monic f (monic_mul_leading_coeff_inv hq0)];
-  simp [is_field_hom.map_inv f, leading_coeff, coeff_map f]
+  simp [is_ring_hom.map_inv f, leading_coeff, coeff_map f]
 
-lemma map_mod [discrete_field β] (f : α → β) [is_field_hom f] :
+lemma map_mod [discrete_field β] (f : α → β) [is_ring_hom f] :
   (p % q).map f = p.map f % q.map f :=
 if hq0 : q = 0 then by simp [hq0]
-else by rw [mod_def, mod_def, leading_coeff_map f, ← is_field_hom.map_inv f, ← map_C f,
+else by rw [mod_def, mod_def, leading_coeff_map f, ← is_ring_hom.map_inv f, ← map_C f,
   ← map_mul f, map_mod_by_monic f (monic_mul_leading_coeff_inv hq0)]
 
-@[simp] lemma map_eq_zero [discrete_field β] (f : α → β) [is_field_hom f] :
+@[simp] lemma map_eq_zero [discrete_field β] (f : α → β) [is_ring_hom f] :
   p.map f = 0 ↔ p = 0 :=
-by simp [polynomial.ext_iff, is_field_hom.map_eq_zero f, coeff_map]
+by simp [polynomial.ext_iff, is_ring_hom.map_eq_zero f, coeff_map]
 
 lemma exists_root_of_degree_eq_one (h : degree p = 1) : ∃ x, is_root p x :=
 ⟨-(p.coeff 0 / p.coeff 1),

src/field_theory/minimal_polynomial.lean

@@ -155,7 +155,7 @@ begin
     rwa [← with_bot.coe_one, with_bot.coe_le_coe], },
   apply degree_pos_of_root (ne_zero_of_monic hq),
   show is_root q a,
-  apply is_field_hom.injective (algebra_map β : α → β),
+  apply is_ring_hom.injective (algebra_map β : α → β),
   rw [is_ring_hom.map_zero (algebra_map β : α → β), ← H],
   convert polynomial.hom_eval₂ _ _ _ _,
   { exact is_semiring_hom.id },

src/field_theory/splitting_field.lean

@@ -25,7 +25,7 @@ open polynomial
 
 section splits
 
-variables (i : α → β) [is_field_hom i]
+variables (i : α → β) [is_ring_hom i]
 
 /-- a polynomial `splits` iff it is zero or all of its irreducible factors have `degree` 1 -/
 def splits (f : polynomial α) : Prop :=
@@ -37,7 +37,7 @@ f = 0 ∨ ∀ {g : polynomial β}, irreducible g → g ∣ f.map i → degree g
 if ha : a = 0 then ha.symm ▸ (@C_0 α _).symm ▸ splits_zero i
 else
 have hia : i a ≠ 0, from mt ((is_add_group_hom.injective_iff i).1
-  (is_field_hom.injective i) _) ha,
+  (is_ring_hom.injective i) _) ha,
 or.inr $ λ g hg ⟨p, hp⟩, absurd hg.1 (classical.not_not.2 (is_unit_iff_degree_eq_zero.2 $
   by have := congr_arg degree hp;
     simp [degree_C hia, @eq_comm (with_bot ℕ) 0,
@@ -75,7 +75,7 @@ lemma splits_of_splits_mul {f g : polynomial α} (hfg : f * g ≠ 0) (h : splits
 ⟨or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_right _ _)),
  or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_left _ _))⟩
 
-lemma splits_map_iff (j : β → γ) [is_field_hom j] {f : polynomial α} :
+lemma splits_map_iff (j : β → γ) [is_ring_hom j] {f : polynomial α} :
   splits j (f.map i) ↔ splits (λ x, j (i x)) f :=
 by simp [splits, polynomial.map_map]
 
@@ -163,7 +163,7 @@ lemma splits_iff_exists_multiset {f : polynomial α} : splits i f ↔
   (s.map (λ a : β, (X : polynomial β) - C a)).prod :=
 ⟨exists_multiset_of_splits i, λ ⟨s, hs⟩, splits_of_exists_multiset i hs⟩
 
-lemma splits_comp_of_splits (j : β → γ) [is_field_hom j] {f : polynomial α}
+lemma splits_comp_of_splits (j : β → γ) [is_ring_hom j] {f : polynomial α}
   (h : splits i f) : splits (λ x, j (i x)) f :=
 begin
   change i with (λ x, id (i x)) at h,

src/field_theory/subfield.lean

@@ -37,16 +37,16 @@ instance univ.is_subfield : is_subfield (@set.univ F) :=
 instance preimage.is_subfield {K : Type*} [discrete_field K]
   (f : F → K) [is_ring_hom f] (s : set K) [is_subfield s] : is_subfield (f ⁻¹' s) :=
 { inv_mem := λ a ha0 (ha : f a ∈ s), show f a⁻¹ ∈ s,
-    by { rw [is_field_hom.map_inv' f ha0],
-         exact is_subfield.inv_mem ((is_field_hom.map_ne_zero f).2 ha0) ha },
+    by { rw [is_ring_hom.map_inv' f ha0],
+         exact is_subfield.inv_mem ((is_ring_hom.map_ne_zero f).2 ha0) ha },
   ..is_ring_hom.is_subring_preimage f s }
 
 instance image.is_subfield {K : Type*} [discrete_field K]
   (f : F → K) [is_ring_hom f] (s : set F) [is_subfield s] : is_subfield (f '' s) :=
 { inv_mem := λ a ha0 ⟨x, hx⟩,
     have hx0 : x ≠ 0, from λ hx0, ha0 (hx.2 ▸ hx0.symm ▸ is_ring_hom.map_zero f),
     ⟨x⁻¹, is_subfield.inv_mem hx0 hx.1,
-    by { rw [← hx.2, is_field_hom.map_inv' f hx0], refl }⟩,
+    by { rw [← hx.2, is_ring_hom.map_inv' f hx0], refl }⟩,
   ..is_ring_hom.is_subring_image f s }
 
 instance range.is_subfield {K : Type*} [discrete_field K]

src/ring_theory/adjoin_root.lean

@@ -95,14 +95,8 @@ principal_ideal_domain.is_maximal_of_irreducible ‹irreducible f›
 noncomputable instance field : discrete_field (adjoin_root f) :=
 ideal.quotient.field (span {f} : ideal (polynomial α))
 
- -- short-circuit type class inference
-instance : is_field_hom (coe : α → adjoin_root f) := by apply_instance
- -- short-circuit type class inference
-instance lift_is_field_hom [field β] {i : α → β} [is_ring_hom i] {a : β}
-  {h : f.eval₂ i a = 0} : is_field_hom (lift i a h) := by apply_instance
-
 lemma coe_injective : function.injective (coe : α → adjoin_root f) :=
-is_field_hom.injective _
+is_ring_hom.injective _
 
 lemma mul_div_root_cancel (f : polynomial α) [irreducible f] :
   (X - C (root : adjoin_root f)) * (f.map coe / (X - C root)) = f.map coe :=

src/ring_theory/ideals.lean

@@ -498,8 +498,8 @@ begin
   exact map_nonunit f a ha
 end
 
-instance map.is_field_hom (f : α → β) [is_local_ring_hom f] :
-  is_field_hom (map f) :=
+instance map.is_ring_hom (f : α → β) [is_local_ring_hom f] :
+  is_ring_hom (map f) :=
 ideal.quotient.is_ring_hom
 
 end residue_field

src/ring_theory/localization.lean

@@ -547,7 +547,7 @@ localization.map_coe _ _ _
   map f hf ∘ (of : A → fraction_ring A) = (of : B → fraction_ring B) ∘ f :=
 localization.map_comp_of _ _
 
-instance map.is_field_hom (hf : injective f) : is_field_hom (map f hf) :=
+instance map.is_ring_hom (hf : injective f) : is_ring_hom (map f hf) :=
 localization.map.is_ring_hom _ _
 
 def equiv_of_equiv (h : A ≃+* B) : fraction_ring A ≃+* fraction_ring B :=