chore(algebra/group_with_zero): weaken assumptions in some lemmas (#3630

)

src/algebra/field.lean

@@ -174,27 +174,28 @@ namespace ring_hom
 
 section
 
-variables {R K : Type*} [semiring R] [field K] (f : R →+* K)
+variables {R K : Type*} [semiring R] [division_ring K] (f : R →+* K)
 
 @[simp] lemma map_units_inv (u : units R) :
   f ↑u⁻¹ = (f ↑u)⁻¹ :=
-monoid_hom.map_units_inv f.to_monoid_hom u
+(f : R →* K).map_units_inv u
 
 end
 
 section
 
-variables {β : Type*} [division_ring α] [division_ring β] (f : α →+* β) {x y : α}
+variables {β γ : Type*} [division_ring α] [semiring β] [nontrivial β] [division_ring γ]
+  (f : α →+* β) (g : α →+* γ) {x y : α}
 
 lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 := (f : α →* β).map_ne_zero f.map_zero
 
 lemma map_eq_zero : f x = 0 ↔ x = 0 := (f : α →* β).map_eq_zero f.map_zero
 
 variables (x y)
 
-lemma map_inv : f x⁻¹ = (f x)⁻¹ := (f : α →* β).map_inv' f.map_zero x
+lemma map_inv : g x⁻¹ = (g x)⁻¹ := (g : α →* γ).map_inv' g.map_zero x
 
-lemma map_div : f (x / y) = f x / f y := (f : α →* β).map_div f.map_zero x y
+lemma map_div : g (x / y) = g x / g y := (g : α →* γ).map_div g.map_zero x y
 
 protected lemma injective : function.injective f := f.injective_iff.2 $ λ x, f.map_eq_zero.1
 

src/algebra/group/hom.lean

@@ -254,14 +254,16 @@ eq_inv_of_mul_eq_one $ f.map_mul_eq_one $ inv_mul_self g
 theorem map_mul_inv {G H} [group G] [group H] (f : G →* H) (g h : G) :
   f (g * h⁻¹) = (f g) * (f h)⁻¹ := by rw [f.map_mul, f.map_inv]
 
-/-- A group homomorphism is injective iff its kernel is trivial. -/
+/-- A homomorphism from a group to a monoid is injective iff its kernel is trivial. -/
 @[to_additive]
-lemma injective_iff {G H} [group G] [group H] (f : G →* H) :
+lemma injective_iff {G H} [group G] [monoid H] (f : G →* H) :
   function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
-⟨λ h _, by rw ← f.map_one; exact @h _ _,
-  λ h x y hxy, by rw [← inv_inv (f x), inv_eq_iff_mul_eq_one, ← f.map_inv,
-      ← f.map_mul] at hxy;
-    simpa using inv_eq_of_mul_eq_one (h _ hxy)⟩
+begin
+  refine ⟨λ h a, (h.eq_iff' f.map_one).1, λ H x y hxy, _⟩,
+  rw [← mul_inv_eq_one],
+  apply H,
+  rw [map_mul, hxy, ← map_mul, mul_inv_self, map_one]
+end
 
 include mM
 /-- Makes a group homomomorphism from a proof that the map preserves multiplication. -/

src/algebra/group_with_zero.lean

@@ -920,10 +920,11 @@ end commute
 
 namespace monoid_hom
 
-section group_with_zero
+variables [group_with_zero G₀] [group_with_zero G₀'] [monoid_with_zero M₀] [nontrivial M₀]
+
+section monoid_with_zero
 
-variables [group_with_zero G₀] [group_with_zero G₀'] (f : G₀ →* G₀') (h0 : f 0 = 0)
-  {a : G₀}
+variables (f : G₀ →* M₀) (h0 : f 0 = 0) {a : G₀}
 
 include h0
 
@@ -933,7 +934,13 @@ lemma map_ne_zero : f a ≠ 0 ↔ a ≠ 0 :=
 lemma map_eq_zero : f a = 0 ↔ a = 0 :=
 by { classical, exact not_iff_not.1 (f.map_ne_zero h0) }
 
-variables (a) (b : G₀)
+end monoid_with_zero
+
+section group_with_zero
+
+variables (f : G₀ →* G₀') (h0 : f 0 = 0) (a b : G₀)
+
+include h0
 
 /-- A monoid homomorphism between groups with zeros sending `0` to `0` sends `a⁻¹` to `(f a)⁻¹`. -/
 lemma map_inv' : f a⁻¹ = (f a)⁻¹ :=
@@ -945,16 +952,12 @@ end
 
 lemma map_div : f (a / b) = f a / f b := (f.map_mul _ _).trans $ congr_arg _ $ f.map_inv' h0 b
 
-end group_with_zero
+omit h0
 
-section comm_group_with_zero
-
-@[simp] lemma map_units_inv {M G₀ : Type*} [monoid M] [comm_group_with_zero G₀]
+@[simp] lemma map_units_inv {M G₀ : Type*} [monoid M] [group_with_zero G₀]
   (f : M →* G₀) (u : units M) : f ↑u⁻¹ = (f u)⁻¹ :=
-have f (u * ↑u⁻¹) = 1 := by rw [←units.coe_mul, mul_inv_self, units.coe_one, f.map_one],
-inv_unique (trans (f.map_mul _ _).symm this)
-  (mul_inv_cancel (λ hu, zero_ne_one (trans (by rw [f.map_mul, hu, zero_mul]) this)))
+by rw [← units.coe_map, ← units.coe_map, ← units.coe_inv', map_inv]
 
-end comm_group_with_zero
+end group_with_zero
 
 end monoid_hom

src/algebra/ring/basic.lean

@@ -594,7 +594,7 @@ namespace ring_hom
   f (x - y) = (f x) - (f y) := (f : α →+ β).map_sub x y
 
 /-- A ring homomorphism is injective iff its kernel is trivial. -/
-theorem injective_iff {α β} [ring α] [ring β] (f : α →+* β) :
+theorem injective_iff {α β} [ring α] [semiring β] (f : α →+* β) :
   function.injective f ↔ (∀ a, f a = 0 → a = 0) :=
 (f : α →+ β).injective_iff