chore(group_theory/free_group): clean up unnecessary lemmas (#6200)

This removes:

* `free_abelian_group.lift.{add,sub,neg,zero}` as these exist already as `(free_abelian_group.lift _).map_{add,sub,neg,zero}` 
* `free_group.to_group.{mul,one,inv}` as these exist already as `(free_group.to_group _).map_{mul,one,inv}`
* `free_group.map.{mul,one,inv}` as these exist already as `(free_group.map _).map_{mul,one,inv}`
* `free_group.prod.{mul,one,inv}` as these exist already as `free_group.prod.map_{mul,one,inv}`
* `to_group.is_group_hom` as this is provided automatically for `monoid_hom`s

and renames

* `free_group.sum.{mul,one,inv}` to `free_group.sum.map_{mul,one,inv}`

These lemmas are already simp lemmas thanks to the functions they relate to being bundled homs.
While the new spelling is slightly longer, it makes it clear that the entire set of `monoid_hom` lemmas apply, not just the three that were copied across.

This also wraps some lines to make the linter happier about these files.

src/group_theory/free_abelian_group.lean

@@ -38,20 +38,6 @@ namespace lift
 variables {β : Type v} [add_comm_group β] (f : α → β)
 open free_abelian_group
 
-@[simp] protected lemma add (x y : free_abelian_group α) :
-  lift f (x + y) = lift f x + lift f y :=
-is_add_hom.map_add _ _ _
-
-@[simp] protected lemma neg (x : free_abelian_group α) : lift f (-x) = -lift f x :=
-is_add_group_hom.map_neg _ _
-
-@[simp] protected lemma sub (x y : free_abelian_group α) :
-  lift f (x - y) = lift f x - lift f y :=
-by simp [sub_eq_add_neg]
-
-@[simp] protected lemma zero : lift f 0 = 0 :=
-is_add_group_hom.map_zero _
-
 @[simp] protected lemma of (x : α) : lift f (of x) = f x :=
 begin
   convert @abelianization.lift.of (free_group α) _ (multiplicative β) _ _ _,
@@ -62,7 +48,7 @@ protected theorem unique (g : free_abelian_group α →+ β)
   (hg : ∀ x, g (of x) = f x) {x} :
   g x = lift f x :=
 @abelianization.lift.unique (free_group α) _ (multiplicative β) _
-  (monoid_hom.of (@free_group.to_group _ (multiplicative β) _ f)) g.to_multiplicative
+  (@free_group.to_group _ (multiplicative β) _ f) g.to_multiplicative
   (λ x, @free_group.to_group.unique α (multiplicative β) _ _
     ((add_monoid_hom.to_multiplicative' g).comp abelianization.of)
     hg x) _
@@ -108,7 +94,7 @@ variables (X : Type*) (G : Type*) [add_comm_group G]
 /-- The bijection underlying the free-forgetful adjunction for abelian groups.-/
 def hom_equiv : (free_abelian_group X →+ G) ≃ (X → G) :=
 { to_fun := λ f, f.1 ∘ of,
-  inv_fun := λ f, add_monoid_hom.of (lift f),
+  inv_fun := λ f, lift f,
   left_inv := λ f, begin ext, simp end,
   right_inv := λ f, funext $ λ x, lift.of f x }
 
@@ -137,13 +123,13 @@ theorem lift.add' {α β} [add_comm_group β] (a : free_abelian_group α) (f g :
   lift (f + g) a = lift f a + lift g a :=
 begin
   refine free_abelian_group.induction_on a _ _ _ _,
-  { simp only [lift.zero, zero_add] },
+  { simp only [(lift _).map_zero, zero_add] },
   { assume x,
     simp only [lift.of, pi.add_apply] },
   { assume x h,
-    simp only [lift.neg, lift.of, pi.add_apply, neg_add] },
+    simp only [(lift _).map_neg, lift.of, pi.add_apply, neg_add] },
   { assume x y hx hy,
-    simp only [lift.add, hx, hy],
+    simp only [(lift _).map_add, hx, hy],
     ac_refl }
 end
 
@@ -171,18 +157,18 @@ free_abelian_group.induction_on z C0 C1 Cn Cp
 lift.of _ _
 
 @[simp] lemma map_zero (f : α → β) : f <$> (0 : free_abelian_group α) = 0 :=
-lift.zero (of ∘ f)
+(lift (of ∘ f)).map_zero
 
 @[simp] lemma map_add (f : α → β) (x y : free_abelian_group α) :
   f <$> (x + y) = f <$> x + f <$> y :=
-lift.add _ _ _
+(lift _).map_add _ _
 
 @[simp] lemma map_neg (f : α → β) (x : free_abelian_group α) : f <$> (-x) = -(f <$> x) :=
-lift.neg _ _
+(lift _).map_neg _
 
 @[simp] lemma map_sub (f : α → β) (x y : free_abelian_group α) :
   f <$> (x - y) = f <$> x - f <$> y :=
-lift.sub _ _ _
+(lift _).map_sub _ _
 
 @[simp] lemma map_of (f : α → β) (y : α) : f <$> of y = of (f y) := rfl
 
@@ -196,29 +182,29 @@ lemma lift_comp {α} {β} {γ} [add_comm_group γ]
   lift (g ∘ f) x = lift g (f <$> x) :=
 begin
   apply free_abelian_group.induction_on x,
-  { simp only [lift.zero, map_zero], },
+  { simp only [(lift _).map_zero, map_zero], },
   { intro y, simp [lift.of, map_of, function.comp_app], },
-  { intros x w, simp only [w, neg_inj, lift.neg, map_neg], },
-  { intros x y w₁ w₂, simp only [w₁, w₂, lift.add, add_right_inj, map_add], },
+  { intros x w, simp only [w, neg_inj, (lift _).map_neg, map_neg], },
+  { intros x y w₁ w₂, simp only [w₁, w₂, (lift _).map_add, add_right_inj, map_add], },
 end
 
 @[simp] lemma pure_bind (f : α → free_abelian_group β) (x) : pure x >>= f = f x :=
 lift.of _ _
 
 @[simp] lemma zero_bind (f : α → free_abelian_group β) : 0 >>= f = 0 :=
-lift.zero f
+(lift f).map_zero
 
 @[simp] lemma add_bind (f : α → free_abelian_group β) (x y : free_abelian_group α) :
   x + y >>= f = (x >>= f) + (y >>= f) :=
-lift.add _ _ _
+(lift _).map_add _ _
 
 @[simp] lemma neg_bind (f : α → free_abelian_group β) (x : free_abelian_group α) :
   -x >>= f = -(x >>= f) :=
-lift.neg _ _
+(lift _).map_neg _
 
 @[simp] lemma sub_bind (f : α → free_abelian_group β) (x y : free_abelian_group α) :
   x - y >>= f = (x >>= f) - (y >>= f) :=
-lift.sub _ _ _
+(lift _).map_sub _ _
 
 @[simp] lemma pure_seq (f : α → β) (x : free_abelian_group α) : pure f <*> x = f <$> x :=
 pure_bind _ _
@@ -289,12 +275,13 @@ instance [monoid α] : semigroup (free_abelian_group α) :=
       { intros L2, iterate 3 { rw lift.of },
         refine free_abelian_group.induction_on x (by simp) _ _ _,
         { intros L1, iterate 3 { rw lift.of }, congr' 1, exact mul_assoc _ _ _ },
-        { intros L1 ih, iterate 3 { rw lift.neg }, rw ih },
-        { intros x1 x2 ih1 ih2, iterate 3 { rw lift.add }, rw [ih1, ih2] } },
-      { intros L2 ih, iterate 4 { rw lift.neg }, rw ih },
-      { intros y1 y2 ih1 ih2, iterate 4 { rw lift.add }, rw [ih1, ih2] } },
-    { intros L3 ih, iterate 3 { rw lift.neg }, rw ih },
-    { intros z1 z2 ih1 ih2, iterate 2 { rw lift.add }, rw [ih1, ih2], exact (lift.add _ _ _).symm }
+        { intros L1 ih, iterate 3 { rw (lift _).map_neg }, rw ih },
+        { intros x1 x2 ih1 ih2, iterate 3 { rw (lift _).map_add }, rw [ih1, ih2] } },
+      { intros L2 ih, iterate 4 { rw (lift _).map_neg }, rw ih },
+      { intros y1 y2 ih1 ih2, iterate 4 { rw (lift _).map_add }, rw [ih1, ih2] } },
+    { intros L3 ih, iterate 3 { rw (lift _).map_neg }, rw ih },
+    { intros z1 z2 ih1 ih2, iterate 2 { rw (lift _).map_add }, rw [ih1, ih2],
+      exact ((lift _).map_add _ _).symm }
   end }
 
 lemma mul_def [monoid α] (x y : free_abelian_group α) :
@@ -310,23 +297,23 @@ instance [monoid α] : ring (free_abelian_group α) :=
     rw lift.of,
     refine free_abelian_group.induction_on x rfl _ _ _,
     { intros L, erw [lift.of], congr' 1, exact mul_one L },
-    { intros L ih, rw [lift.neg, ih] },
-    { intros x1 x2 ih1 ih2, rw [lift.add, ih1, ih2] }
+    { intros L ih, rw [(lift _).map_neg, ih] },
+    { intros x1 x2 ih1 ih2, rw [(lift _).map_add, ih1, ih2] }
   end,
   one_mul := λ x, begin
     unfold has_mul.mul semigroup.mul has_one.one,
     refine free_abelian_group.induction_on x rfl _ _ _,
     { intros L, rw [lift.of, lift.of], congr' 1, exact one_mul L },
-    { intros L ih, rw [lift.neg, ih] },
-    { intros x1 x2 ih1 ih2, rw [lift.add, ih1, ih2] }
+    { intros L ih, rw [(lift _).map_neg, ih] },
+    { intros x1 x2 ih1 ih2, rw [(lift _).map_add, ih1, ih2] }
   end,
-  left_distrib := λ x y z, lift.add _ _ _,
+  left_distrib := λ x y z, (lift _).map_add _ _,
   right_distrib := λ x y z, begin
     unfold has_mul.mul semigroup.mul,
     refine free_abelian_group.induction_on z rfl _ _ _,
-    { intros L, iterate 3 { rw lift.of }, rw lift.add, refl },
-    { intros L ih, iterate 3 { rw lift.neg }, rw [ih, neg_add], refl },
-    { intros z1 z2 ih1 ih2, iterate 3 { rw lift.add }, rw [ih1, ih2],
+    { intros L, iterate 3 { rw lift.of }, rw (lift _).map_add, refl },
+    { intros L ih, iterate 3 { rw (lift _).map_neg }, rw [ih, neg_add], refl },
+    { intros z1 z2 ih1 ih2, iterate 3 { rw (lift _).map_add }, rw [ih1, ih2],
       rw [add_assoc, add_assoc], congr' 1, apply add_left_comm }
   end,
   .. free_abelian_group.add_comm_group α,

src/group_theory/free_group.lean

@@ -401,28 +401,14 @@ rfl
 @[simp] lemma to_group.of {x} : to_group f (of x) = f x :=
 one_mul _
 
-instance to_group.is_group_hom : is_group_hom (to_group f) :=
-{ map_mul := by rintros ⟨L₁⟩ ⟨L₂⟩; simp }
-
-@[simp] lemma to_group.mul : to_group f (x * y) = to_group f x * to_group f y :=
-is_mul_hom.map_mul _ _ _
-
-@[simp] lemma to_group.one : to_group f 1 = 1 :=
-is_group_hom.map_one _
-
-@[simp] lemma to_group.inv : to_group f x⁻¹ = (to_group f x)⁻¹ :=
-is_group_hom.map_inv _ _
-
 theorem to_group.unique (g : free_group α →* β)
   (hg : ∀ x, g (of x) = f x) : ∀{x}, g x = to_group f x :=
 by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.map_one g)
 (λ ⟨x, b⟩ t (ih : g (mk t) = _), bool.rec_on b
   (show g ((of x)⁻¹ * mk t) = to_group f (mk ((x, ff) :: t)),
-     by simp [monoid_hom.map_mul g, monoid_hom.map_inv g, hg, ih,
-       to_group.to_fun, to_group.aux])
+     by simp [g.map_mul, g.map_inv, hg, ih, to_group.to_fun, to_group.aux])
   (show g (of x * mk t) = to_group f (mk ((x, tt) :: t)),
-     by simp [monoid_hom.map_mul g, monoid_hom.map_inv g, hg, ih,
-       to_group.to_fun, to_group.aux]))
+     by simp [g.map_mul, g.map_inv, hg, ih, to_group.to_fun, to_group.aux]))
 
 /-- Two homomorphisms out of a free group are equal if they are equal on generators.
 
@@ -511,23 +497,14 @@ by rcases x with ⟨L⟩; simp
 
 @[simp] lemma map.of {x} : map f (of x) = of (f x) := rfl
 
-@[simp] lemma map.mul : map f (x * y) = map f x * map f y :=
-is_mul_hom.map_mul _ x y
-
-@[simp] lemma map.one : map f 1 = 1 :=
-is_group_hom.map_one _
-
-@[simp] lemma map.inv : map f x⁻¹ = (map f x)⁻¹ :=
-is_group_hom.map_inv _ x
-
-theorem map.unique (g : free_group α → free_group β) [is_group_hom g]
+theorem map.unique (g : free_group α →* free_group β)
   (hg : ∀ x, g (of x) = of (f x)) : ∀{x}, g x = map f x :=
-by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.map_one g)
+by rintros ⟨L⟩; exact list.rec_on L g.map_one
 (λ ⟨x, b⟩ t (ih : g (mk t) = map f (mk t)), bool.rec_on b
   (show g ((of x)⁻¹ * mk t) = map f ((of x)⁻¹ * mk t),
-     by simp [is_mul_hom.map_mul g, is_group_hom.map_inv g, hg, ih])
+     by simp [g.map_mul, g.map_inv, hg, ih])
   (show g (of x * mk t) = map f (of x * mk t),
-     by simp [is_mul_hom.map_mul g, hg, ih]))
+     by simp [g.map_mul, hg, ih]))
 
 /-- Equivalent types give rise to equivalent free groups. -/
 def free_group_congr {α β} (e : α ≃ β) : free_group α ≃ free_group β :=
@@ -559,15 +536,6 @@ rfl
 @[simp] lemma prod.of {x : α} : prod (of x) = x :=
 to_group.of
 
-@[simp] lemma prod.mul : prod (x * y) = prod x * prod y :=
-to_group.mul
-
-@[simp] lemma prod.one : prod (1:free_group α) = 1 :=
-to_group.one
-
-@[simp] lemma prod.inv : prod x⁻¹ = (prod x)⁻¹ :=
-to_group.inv
-
 lemma prod.unique (g : free_group α →* α)
   (hg : ∀ x, g (of x) = x) {x} :
   g x = prod x :=
@@ -603,17 +571,16 @@ rfl
 @[simp] lemma sum.of {x : α} : sum (of x) = x :=
 prod.of
 
-instance sum.is_group_hom : is_group_hom (@sum α _) :=
-prod.is_group_hom
-
-@[simp] lemma sum.mul : sum (x * y) = sum x + sum y :=
-prod.mul
+-- note: there are no bundled homs with different notation in the domain and codomain, so we copy
+-- these manually
+@[simp] lemma sum.map_mul : sum (x * y) = sum x + sum y :=
+(@prod (multiplicative _) _).map_mul _ _
 
-@[simp] lemma sum.one : sum (1:free_group α) = 0 :=
-prod.one
+@[simp] lemma sum.map_one : sum (1:free_group α) = 0 :=
+(@prod (multiplicative _) _).map_one
 
-@[simp] lemma sum.inv : sum x⁻¹ = -sum x :=
-prod.inv
+@[simp] lemma sum.map_inv : sum x⁻¹ = -sum x :=
+(@prod (multiplicative _) _).map_inv _
 
 end sum
 
@@ -667,25 +634,25 @@ bool.rec_on b (Cm _ _ (Ci _ $ Cp x) ih) (Cm _ _ (Cp x) ih)
 map.of
 
 @[simp] lemma map_one (f : α → β) : f <$> (1 : free_group α) = 1 :=
-map.one
+(map f).map_one
 
 @[simp] lemma map_mul (f : α → β) (x y : free_group α) : f <$> (x * y) = f <$> x * f <$> y :=
-map.mul
+(map f).map_mul x y
 
 @[simp] lemma map_inv (f : α → β) (x : free_group α) : f <$> (x⁻¹) = (f <$> x)⁻¹ :=
-map.inv
+(map f).map_inv x
 
 @[simp] lemma pure_bind (f : α → free_group β) (x) : pure x >>= f = f x :=
 to_group.of
 
 @[simp] lemma one_bind (f : α → free_group β) : 1 >>= f = 1 :=
-@@to_group.one _ f
+(to_group f).map_one
 
 @[simp] lemma mul_bind (f : α → free_group β) (x y : free_group α) : x * y >>= f = (x >>= f) * (y >>= f) :=
-to_group.mul
+(to_group f).map_mul _ _
 
 @[simp] lemma inv_bind (f : α → free_group β) (x : free_group α) : x⁻¹ >>= f = (x >>= f)⁻¹ :=
-to_group.inv
+(to_group f).map_inv _
 
 instance : is_lawful_monad free_group.{u} :=
 { id_map := λ α x, free_group.induction_on x (map_one id) (λ x, map_pure id x)

src/ring_theory/free_comm_ring.lean

@@ -105,11 +105,14 @@ def lift : free_comm_ring α →+* R :=
         calc _ = multiset.prod ((multiset.map f s1) + (multiset.map f s2)) :
             by {congr' 1, exact multiset.map_add _ _ _}
           ... = _ : multiset.prod_add _ _ },
-      { intros s1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_mul_eq_neg_mul] },
-      { intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2, add_mul] } },
+      { intros s1 ih, iterate 3 { rw (free_abelian_group.lift _).map_neg },
+        rw [ih, neg_mul_eq_neg_mul] },
+      { intros x1 x2 ih1 ih2, iterate 3 { rw (free_abelian_group.lift _).map_add },
+        rw [ih1, ih2, add_mul] } },
     { intros s2 ih,
       simp only [add_monoid_hom.to_fun_eq_coe] at ih ⊢,
-      rw [mul_neg_eq_neg_mul_symm, add_monoid_hom.map_neg, add_monoid_hom.map_neg, mul_neg_eq_neg_mul_symm, ih] },
+      rw [mul_neg_eq_neg_mul_symm, add_monoid_hom.map_neg, add_monoid_hom.map_neg,
+        mul_neg_eq_neg_mul_symm, ih] },
     { intros y1 y2 ih1 ih2,
       simp only [add_monoid_hom.to_fun_eq_coe] at ih1 ih2 ⊢,
       rw [mul_add, add_monoid_hom.map_add, add_monoid_hom.map_add, mul_add, ih1, ih2] },

src/ring_theory/free_ring.lean

@@ -79,11 +79,16 @@ def lift : free_ring α →+* R :=
       refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _,
       { intros L1, iterate 3 { rw free_abelian_group.lift.of },
         show list.prod (list.map f (_ ++ _)) = _, rw [list.map_append, list.prod_append] },
-      { intros L1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_mul_eq_neg_mul] },
-      { intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2, add_mul] } },
+      { intros L1 ih,
+        iterate 3 { rw (free_abelian_group.lift _).map_neg },
+        rw [ih, neg_mul_eq_neg_mul] },
+      { intros x1 x2 ih1 ih2,
+        iterate 3 { rw (free_abelian_group.lift _).map_add },
+        rw [ih1, ih2, add_mul] } },
     { intros L2 ih,
       simp only [add_monoid_hom.to_fun_eq_coe] at ih ⊢,
-      rw [mul_neg_eq_neg_mul_symm, add_monoid_hom.map_neg, add_monoid_hom.map_neg, mul_neg_eq_neg_mul_symm, ih] },
+      rw [mul_neg_eq_neg_mul_symm, add_monoid_hom.map_neg, add_monoid_hom.map_neg,
+        mul_neg_eq_neg_mul_symm, ih] },
     { intros y1 y2 ih1 ih2,
       simp only [add_monoid_hom.to_fun_eq_coe] at ih1 ih2 ⊢,
       rw [mul_add, add_monoid_hom.map_add, add_monoid_hom.map_add, mul_add, ih1, ih2] },