refactor(algebra/field): partially migrate to bundled homs

src/algebra/field.lean

@@ -214,46 +214,73 @@ end
 
 end
 
-namespace is_ring_hom
-open is_ring_hom
+namespace ring_hom
 
 section
-variables {β : Type*} [division_ring α] [division_ring β]
-variables (f : α → β) [is_ring_hom f] {x y : α}
+
+variables {β : Type*} [division_ring α] [division_ring β] (f : α →+* β) {x y : α}
 
 lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 :=
-⟨mt $ λ h, h.symm ▸ map_zero f,
- λ x0 h, one_ne_zero $ calc
-    1 = f (x * x⁻¹) : by rw [mul_inv_cancel x0, map_one f]
-  ... = 0 : by rw [map_mul f, h, zero_mul]⟩
+⟨mt $ λ h, h.symm ▸ f.map_zero,
+ λ x0 h, one_ne_zero $ by rw [← f.map_one, ← mul_inv_cancel x0, f.map_mul, 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), ← f.map_mul, mul_inv_cancel h, f.map_one]
 
 lemma map_div' (h : y ≠ 0) : f (x / y) = f x / f y :=
-(map_mul f).trans $ congr_arg _ $ map_inv' f h
+(f.map_mul _ _).trans $ congr_arg _ $ f.map_inv' h
 
 lemma injective : function.injective f :=
-(is_add_group_hom.injective_iff _).2
+f.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]
+    by simpa [ha, f.map_mul, f.map_one, zero_ne_one]
         using congr_arg f (mul_inv_cancel ha0))
 
 end
 
 section
-variables {β : Type*} [discrete_field α] [discrete_field β]
-variables (f : α → β) [is_ring_hom f] {x y : α}
+
+variables {β : Type*} [discrete_field α] [discrete_field β] (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)
 
 lemma map_div : f (x / y) = f x / f y :=
-(map_mul f).trans $ congr_arg _ $ map_inv f
+(f.map_mul _ _).trans $ congr_arg _ $ map_inv f
+
+end
+end ring_hom
+
+namespace is_ring_hom
+open ring_hom (of)
+
+section
+variables {β : Type*} [division_ring α] [division_ring β]
+variables (f : α → β) [is_ring_hom f] {x y : α}
+
+@[simp] lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 := (of f).map_ne_zero
+
+@[simp] lemma map_eq_zero : f x = 0 ↔ x = 0 := (of f).map_eq_zero
+
+lemma map_inv' (h : x ≠ 0) : f x⁻¹ = (f x)⁻¹ := (of f).map_inv' h
+
+lemma map_div' (h : y ≠ 0) : f (x / y) = f x / f y := (of f).map_div' h
+
+lemma injective : function.injective f := (of f).injective
+
+end
+
+section
+variables {β : Type*} [discrete_field α] [discrete_field β]
+variables (f : α → β) [is_ring_hom f] {x y : α}
+
+@[simp] lemma map_inv : f x⁻¹ = (f x)⁻¹ := (of f).map_inv
+
+@[simp] lemma map_div : f (x / y) = f x / f y := (of f).map_div
 
 end
 

src/algebra/field_power.lean

@@ -60,22 +60,30 @@ pow_one a
 
 end field_power
 
-namespace is_ring_hom
-
-lemma map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α → β) [is_ring_hom f]
+@[simp] lemma ring_hom.map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (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_ring_hom.map_inv f]
+| (n : ℕ) := f.map_pow a n
+| -[1+n] := by simp [fpow_neg_succ_of_nat, f.map_pow, f.map_inv]
 
-lemma map_fpow' {K L : Type*} [division_ring K] [division_ring L] (f : K → L) [is_ring_hom f]
+lemma ring_hom.map_fpow' {K L : Type*} [division_ring K] [division_ring L] (f : K →+* L)
   (a : K) (ha : a ≠ 0) : ∀ (n : ℤ), f (a ^ n) = f a ^ n
-| (n : ℕ) := is_semiring_hom.map_pow f a n
+| (n : ℕ) := f.map_pow a n
 | -[1+ n] :=
 begin
   have : a^(n+1) ≠ 0 := mt pow_eq_zero ha,
-  simp [fpow_neg_succ_of_nat, is_semiring_hom.map_pow f, is_ring_hom.map_inv' f this],
+  simp [fpow_neg_succ_of_nat, f.map_pow, f.map_inv' this],
 end
 
+namespace is_ring_hom
+
+lemma map_fpow {α β : Type*} [discrete_field α] [discrete_field β] (f : α → β) [is_ring_hom f]
+  (a : α) : ∀ (n : ℤ), f (a ^ n) = f a ^ n :=
+(ring_hom.of f).map_fpow a
+
+lemma map_fpow' {K L : Type*} [division_ring K] [division_ring L] (f : K → L) [is_ring_hom f]
+  (a : K) (ha : a ≠ 0) : ∀ (n : ℤ), f (a ^ n) = f a ^ n :=
+(ring_hom.of f).map_fpow' a ha
+
 end is_ring_hom
 
 section discrete_field_power
@@ -246,19 +254,9 @@ end
 
 @[simp, move_cast] theorem cast_fpow [char_zero K] (q : ℚ) (n : ℤ) :
   ((q ^ n : ℚ) : K) = q ^ n :=
-@is_ring_hom.map_fpow _ _ _ _ _ (rat.is_ring_hom_cast) q n
+(ring_hom.of rat.cast).map_fpow q n
 
 lemma fpow_eq_zero {x : K} {n : ℤ} (h : x^n = 0) : x = 0 :=
-begin
-  by_cases hn : 0 ≤ n,
-  { lift n to ℕ using hn, rw fpow_of_nat at h, exact pow_eq_zero h, },
-  { by_cases hx : x = 0, { exact hx },
-    push_neg at hn, rw ← neg_pos at hn, replace hn := le_of_lt hn,
-    lift (-n) to ℕ using hn with m hm,
-    rw [← neg_neg n, fpow_neg, ← hm, fpow_of_nat] at h,
-    rw ← inv_eq_zero,
-    apply pow_eq_zero (_ : _^m = _),
-    rwa [inv_eq_one_div, one_div_pow hx], }
-end
+classical.by_contradiction $ λ hx, fpow_ne_zero_of_ne_zero hx n h
 
 end

src/field_theory/subfield.lean

@@ -35,23 +35,23 @@ instance univ.is_subfield : is_subfield (@set.univ F) :=
   `is_add_subgroup _` and `is_submonoid _` are chosen (which are not the default ones).
   If we specify it explicitly, then it doesn't complain. -/
 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) :=
+  (f : F →+* K) (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_ring_hom.map_inv' f ha0],
-         exact is_subfield.inv_mem ((is_ring_hom.map_ne_zero f).2 ha0) ha },
+    by { rw [f.map_inv' ha0],
+         exact is_subfield.inv_mem (f.map_ne_zero.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) :=
+  (f : F →+* K) (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),
+    have hx0 : x ≠ 0, from λ hx0, ha0 (hx.2 ▸ hx0.symm ▸ f.map_zero),
     ⟨x⁻¹, is_subfield.inv_mem hx0 hx.1,
-    by { rw [← hx.2, is_ring_hom.map_inv' f hx0], refl }⟩,
+    by { rw [← hx.2, f.map_inv' hx0], refl }⟩,
   ..is_ring_hom.is_subring_image f s }
 
 instance range.is_subfield {K : Type*} [discrete_field K]
-  (f : F → K) [is_ring_hom f] : is_subfield (set.range f) :=
-by rw ← set.image_univ; apply_instance
+  (f : F →+* K) : is_subfield (set.range f) :=
+by { rw ← set.image_univ, apply_instance }
 
 namespace field