refactor(*): bundle is_field_hom

src/algebra/char_zero.lean

@@ -85,4 +85,4 @@ by rw [sub_eq_iff_eq_add, add_halves']
 lemma half_sub (a : α) : a / 2 - a = - (a / 2) :=
 by rw [← neg_sub, sub_half]
 
-end
+end

src/algebra/field.lean

@@ -174,14 +174,24 @@ field.div_div_cancel ha b0
 
 end
 
-@[reducible] def is_field_hom {α β} [division_ring α] [division_ring β] (f : α → β) := is_ring_hom f
+@[reducible] def field_hom (α β) [division_ring α] [division_ring β] :=
+{ f : α → β // is_ring_hom f }
 
-namespace is_field_hom
+infixr ` →f `:25 := field_hom
+
+namespace field_hom
 open is_ring_hom
 
 section
 variables {β : Type*} [division_ring α] [division_ring β]
-variables (f : α → β) [is_field_hom f] {x y : α}
+
+instance : has_coe_to_fun (α →f β) :=
+⟨_, subtype.val⟩
+
+instance (f : α →f β) : is_ring_hom f :=
+f.property
+
+variables (f : α →f β) {x y : α}
 
 lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 :=
 ⟨mt $ λ h, h.symm ▸ map_zero f,
@@ -190,33 +200,44 @@ lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 :=
   ... = 0 : by rw [map_mul f, h, zero_mul]⟩
 
 lemma map_eq_zero : f x = 0 ↔ x = 0 :=
-by haveI := classical.dec; exact not_iff_not.1 (map_ne_zero f)
+by haveI := classical.dec; exact not_iff_not.1 f.map_ne_zero
 
 lemma map_inv' (h : x ≠ 0) : f x⁻¹ = (f x)⁻¹ :=
-(domain.mul_left_inj ((map_ne_zero f).2 h)).1 $
-by rw [mul_inv_cancel ((map_ne_zero f).2 h), ← map_mul f, mul_inv_cancel h, map_one f]
+(domain.mul_left_inj (f.map_ne_zero.2 h)).1 $
+by rw [mul_inv_cancel (f.map_ne_zero.2 h), ← map_mul f, mul_inv_cancel h, map_one f]
 
 lemma map_div' (h : y ≠ 0) : f (x / y) = f x / f y :=
-(map_mul f).trans $ congr_arg _ $ map_inv' f h
+(map_mul f).trans $ congr_arg _ $ f.map_inv' h
 
 lemma injective : function.injective f :=
 (is_add_group_hom.injective_iff _).2
   (λ a ha, classical.by_contradiction $ λ ha0,
     by simpa [ha, is_ring_hom.map_mul f, is_ring_hom.map_one f, zero_ne_one]
         using congr_arg f (mul_inv_cancel ha0))
 
+variables (α)
+protected def id : α →f α :=
+⟨id, by apply_instance⟩
+
+variables {α} {γ : Type*} [division_ring γ]
+def comp (g : α →f β) (f : β →f γ) : α →f γ :=
+⟨f ∘ g, by apply_instance⟩
+
+@[simp] lemma coe_fun_id : (field_hom.id α : α → α) = id := rfl
+@[simp] lemma coe_fun_comp (g : α →f β) (f : β →f γ) : (g.comp f : α → γ) = f ∘ g := rfl
+
 end
 
 section
 variables {β : Type*} [discrete_field α] [discrete_field β]
-variables (f : α → β) [is_field_hom f] {x y : α}
+variables (f : α →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)
+classical.by_cases (by rintro rfl; simp only [map_zero f, inv_zero]) f.map_inv'
 
 lemma map_div : f (x / y) = f x / f y :=
-(map_mul f).trans $ congr_arg _ $ map_inv f
+(map_mul f).trans $ congr_arg _ $ f.map_inv
 
 end
 
-end is_field_hom
+end field_hom

src/algebra/field_power.lean

@@ -6,7 +6,7 @@ Authors: Robert Y. Lewis
 Integer power operation on fields.
 -/
 
-import algebra.group_power tactic.wlog
+import algebra.ordered_field algebra.group_power tactic.wlog
 
 universe u
 
@@ -51,14 +51,14 @@ begin simp only [fpow_eq_gpow ha], rw ← units.coe_mul, congr, apply gpow_add e
 
 end field_power
 
-namespace is_field_hom
+namespace field_hom
 
-lemma map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α → β) [is_field_hom f]
+lemma map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α →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, f.map_inv]
 
-end is_field_hom
+end field_hom
 
 section discrete_field_power
 open int nat

src/algebra/group_power.lean

@@ -11,7 +11,7 @@ a^n is used for the first, but users can locally redefine it to gpow when needed
 
 Note: power adopts the convention that 0^0=1.
 -/
-import algebra.char_zero algebra.group algebra.ordered_field
+import algebra.group
 import data.int.basic data.list.basic
 
 universes u v

src/data/complex/basic.lean

@@ -247,10 +247,10 @@ instance of_real.is_ring_hom : is_ring_hom (coe : ℝ → ℂ) :=
 by refine_struct {..}; simp
 
 @[simp] lemma of_real_div (r s : ℝ) : ((r / s : ℝ) : ℂ) = r / s :=
-is_field_hom.map_div coe
+field_hom.map_div ⟨coe, of_real.is_ring_hom⟩
 
 @[simp] lemma of_real_fpow (r : ℝ) (n : ℤ) : ((r ^ n : ℝ) : ℂ) = (r : ℂ) ^ n :=
-is_field_hom.map_fpow of_real r n
+field_hom.map_fpow ⟨coe, of_real.is_ring_hom⟩ r n
 
 @[simp] theorem of_real_int_cast : ∀ n : ℤ, ((n : ℝ) : ℂ) = n :=
 int.eq_cast (λ n, ((n : ℝ) : ℂ))

src/data/polynomial.lean

@@ -1831,34 +1831,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 : α →f β) :
   degree (p.map f) = degree p :=
-degree_map_eq_of_injective _ (is_field_hom.injective f)
+degree_map_eq_of_injective _ f.injective
 
-@[simp] lemma nat_degree_map [discrete_field β] (f : α → β) [is_field_hom f] :
+@[simp] lemma nat_degree_map [discrete_field β] (f : α →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 : α →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 : α →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 [f.map_inv, leading_coeff, coeff_map f]
 
-lemma map_mod [discrete_field β] (f : α → β) [is_field_hom f] :
+lemma map_mod [discrete_field β] (f : α →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, ← f.map_inv, ← 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 : α →f β) :
   p.map f = 0 ↔ p = 0 :=
-by simp [polynomial.ext, is_field_hom.map_eq_zero f, coeff_map]
+by simp [polynomial.ext, f.map_eq_zero, 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/splitting_field.lean

@@ -21,7 +21,7 @@ open polynomial adjoin_root
 
 section splits
 
-variables (i : α → β) [is_field_hom i]
+variables (i : α →f β)
 
 /-- a polynomial `splits` iff it is zero or all of its irreducible factors have `degree` 1 -/
 def splits (f : polynomial α) : Prop :=
@@ -32,8 +32,7 @@ f = 0 ∨ ∀ {g : polynomial β}, irreducible g → g ∣ f.map i → degree g
 @[simp] lemma splits_C (a : α) : splits i (C a) :=
 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,
+have hia : i a ≠ 0, from mt ((is_add_group_hom.injective_iff i).1 i.injective _) 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,
@@ -71,8 +70,8 @@ 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 α} :
-  splits j (f.map i) ↔ splits (λ x, j (i x)) f :=
+lemma splits_map_iff (j : β →f γ) {f : polynomial α} :
+  splits j (f.map i) ↔ splits (i.comp j) f :=
 by simp [splits, polynomial.map_map]
 
 lemma exists_root_of_splits {f : polynomial α} (hs : splits i f) (hf0 : degree f ≠ 0) :
@@ -86,10 +85,11 @@ else
   let ⟨i, hi⟩ := hg.2 in
   ⟨x, by rw [← eval_map, hi, eval_mul, show _ = _, from hx, zero_mul]⟩
 
+set_option class.instance_max_depth 100
 lemma exists_multiset_of_splits {f : polynomial α} : splits i f →
   ∃ (s : multiset β), f.map i = C (i f.leading_coeff) *
   (s.map (λ a : β, (X : polynomial β) - C a)).prod :=
-suffices splits id (f.map i) → ∃ s : multiset β, f.map i =
+suffices splits (field_hom.id _) (f.map i) → ∃ s : multiset β, f.map i =
   (C (f.map i).leading_coeff) * (s.map (λ a : β, (X : polynomial β) - C a)).prod,
 by rwa [splits_map_iff, leading_coeff_map i] at this,
 is_noetherian_ring.irreducible_induction_on (f.map i)
@@ -142,14 +142,14 @@ else
   by rw [← degree_X_sub_C a, ha.2];
     exact degree_eq_degree_of_associated (hpq.trans hqq')
 
-lemma splits_of_splits_id {f : polynomial α} : splits id f → splits i f :=
+lemma splits_of_splits_id {f : polynomial α} : splits (field_hom.id _) f → splits i f :=
 unique_factorization_domain.induction_on_prime f (λ _, splits_zero _)
   (λ _ hu _, splits_of_degree_le_one _
     ((is_unit_iff_degree_eq_zero.1 hu).symm ▸ dec_trivial))
   (λ a p ha0 hp ih hfi, splits_mul _
     (splits_of_degree_eq_one _
       ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.resolve_left
-        hp.1 (irreducible_of_prime hp) (by rw map_id)))
+        hp.1 (irreducible_of_prime hp) (by rw [coe_fun_id, map_id])))
     (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2))
 
 end UFD
@@ -159,12 +159,12 @@ 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 α}
-  (h : splits i f) : splits (λ x, j (i x)) f :=
+lemma splits_comp_of_splits (j : β →f γ) {f : polynomial α}
+  (h : splits i f) : splits (i.comp j) f :=
 begin
-  change i with (λ x, id (i x)) at h,
+  change i with i.comp (field_hom.id _) at h,
   rw [← splits_map_iff],
-  rw [← splits_map_iff i id] at h,
+  rw [← splits_map_iff i (field_hom.id _)] at h,
   exact splits_of_splits_id _ h
 end
 

src/ring_theory/adjoin_root.lean

@@ -96,13 +96,19 @@ noncomputable instance field : discrete_field (adjoin_root f) :=
   ..adjoin_root.comm_ring f,
   ..ideal.quotient.field (span {f} : ideal (polynomial α)) }
 
-instance : is_field_hom (coe : α → adjoin_root f) := by apply_instance
+variables (α f)
+def fof : α →f adjoin_root f :=
+⟨coe, by apply_instance⟩
 
-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
+def flift [field β] (i : α → β) [is_ring_hom i] (a : β)
+  (h : f.eval₂ i a = 0) : adjoin_root f →f β :=
+⟨lift i a h, by apply_instance⟩
 
-lemma coe_injective : function.injective (coe : α → adjoin_root f) :=
-is_field_hom.injective _
+variables {α f}
+
+@[simp] lemma fof_apply {x : α} : fof α f x = ↑x := rfl
+@[simp] lemma flift_apply [field β] {i : α → β} [is_ring_hom i] {a : β} {h x} :
+  flift α f i a h x = lift i a h x := rfl
 
 lemma mul_div_root_cancel (f : polynomial α) [irreducible f] :
   (X - C (root : adjoin_root f)) * (f.map coe / (X - C root)) = f.map coe :=