refactor(algebra/hom/group): Generalize map_inv to division monoids (…

…#14134)

A minor change with unexpected instance synthesis breakage. A good deal of dot notation on `monoid_hom.map_inv` breaks, along with a few uses of `map_inv`. Expliciting the type fixes them all, but this is still quite concerning.

src/algebra/group/ext.lean

@@ -125,7 +125,7 @@ begin
   set f := @monoid_hom.mk' G G (by letI := g₁; apply_instance) g₂ id
     (λ a b, congr_fun (congr_fun h_mul a) b),
   exact group.to_div_inv_monoid_injective (div_inv_monoid.ext h_mul
-    (funext $ @monoid_hom.map_inv G G g₁ g₂ f))
+    (funext $ @monoid_hom.map_inv G G g₁ (@group.to_division_monoid _ g₂) f))
 end
 
 @[ext, to_additive]

src/algebra/hom/equiv.lean

@@ -459,12 +459,13 @@ def Pi_subsingleton
 
 /-- A multiplicative equivalence of groups preserves inversion. -/
 @[to_additive "An additive equivalence of additive groups preserves negation."]
-protected lemma map_inv [group G] [group H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹ :=
+protected lemma map_inv [group G] [division_monoid H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹ :=
 map_inv h x
 
 /-- A multiplicative equivalence of groups preserves division. -/
 @[to_additive "An additive equivalence of additive groups preserves subtractions."]
-protected lemma map_div [group G] [group H] (h : G ≃* H) (x y : G) : h (x / y) = h x / h y :=
+protected lemma map_div [group G] [division_monoid H] (h : G ≃* H) (x y : G) :
+  h (x / y) = h x / h y :=
 map_div h x y
 
 end mul_equiv
@@ -502,10 +503,6 @@ protected lemma group.is_unit {G} [group G] (x : G) : is_unit x := (to_units x).
 
 namespace units
 
-@[simp, to_additive] lemma coe_inv [group G] (u : Gˣ) :
-  ↑u⁻¹ = (u⁻¹ : G) :=
-to_units.symm.map_inv u
-
 variables [monoid M] [monoid N] [monoid P]
 
 /-- A multiplicative equivalence of monoids defines a multiplicative equivalence

src/algebra/hom/group.lean

@@ -58,7 +58,7 @@ monoid_hom, add_monoid_hom
 
 -/
 
-variables {M : Type*} {N : Type*} {P : Type*} -- monoids
+variables {α β M N P : Type*} -- monoids
 variables {G : Type*} {H : Type*} -- groups
 variables {F : Type*} -- homs
 
@@ -294,28 +294,28 @@ lemma map_mul_eq_one [monoid_hom_class F M N] (f : F) {a b : M} (h : a * b = 1)
   f a * f b = 1 :=
 by rw [← map_mul, h, map_one]
 
+@[to_additive]
+lemma map_div' [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H] (f : F)
+  (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (a b : G) : f (a / b) = f a / f b :=
+by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]
+
 /-- Group homomorphisms preserve inverse. -/
 @[simp, to_additive "Additive group homomorphisms preserve negation."]
-theorem map_inv [group G] [group H] [monoid_hom_class F G H]
-  (f : F) (g : G) : f g⁻¹ = (f g)⁻¹ :=
-eq_inv_of_mul_eq_one_left $ map_mul_eq_one f $ inv_mul_self g
+lemma map_inv [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (a : G) :
+  f a⁻¹ = (f a)⁻¹ :=
+eq_inv_of_mul_eq_one_left $ map_mul_eq_one f $ inv_mul_self _
 
 /-- Group homomorphisms preserve division. -/
 @[simp, to_additive "Additive group homomorphisms preserve subtraction."]
-theorem map_mul_inv [group G] [group H] [monoid_hom_class F G H]
-  (f : F) (g h : G) : f (g * h⁻¹) = f g * (f h)⁻¹ :=
+lemma map_mul_inv [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (a b : G) :
+  f (a * b⁻¹) = f a * (f b)⁻¹ :=
 by rw [map_mul, map_inv]
 
 /-- Group homomorphisms preserve division. -/
 @[simp, to_additive "Additive group homomorphisms preserve subtraction."]
-lemma map_div [group G] [group H] [monoid_hom_class F G H]
-  (f : F) (x y : G) : f (x / y) = f x / f y :=
-by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul_inv]
-
-@[to_additive]
-theorem map_div' [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H] (f : F)
-  (hf : ∀ x, f (x⁻¹) = (f x)⁻¹) (a b : G) : f (a / b) = f a / f b :=
-by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]
+lemma map_div [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) :
+  ∀ a b, f (a / b) = f a / f b :=
+map_div' _ $ map_inv f
 
 -- to_additive puts the arguments in the wrong order, so generate an auxiliary lemma, then
 -- swap its arguments.
@@ -342,12 +342,13 @@ theorem map_zpow' [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H]
 -- swap its arguments.
 /-- Group homomorphisms preserve integer power. -/
 @[to_additive map_zsmul.aux, simp]
-theorem map_zpow [group G] [group H] [monoid_hom_class F G H] (f : F) (g : G) (n : ℤ) :
+theorem map_zpow [group G] [division_monoid H] [monoid_hom_class F G H] (f : F) (g : G) (n : ℤ) :
   f (g ^ n) = (f g) ^ n :=
 map_zpow' f (map_inv f) g n
 
 /-- Additive group homomorphisms preserve integer scaling. -/
-theorem map_zsmul [add_group G] [add_group H] [add_monoid_hom_class F G H] (f : F) (n : ℤ) (g : G) :
+theorem map_zsmul [add_group G] [subtraction_monoid H] [add_monoid_hom_class F G H] (f : F)
+  (n : ℤ) (g : G) :
   f (n • g) = n • f g :=
 map_zsmul.aux f g n
 
@@ -1062,25 +1063,25 @@ left_inv_eq_right_inv (map_mul_eq_one f $ inv_mul_self x) $
   h.symm ▸ map_mul_eq_one g $ mul_inv_self x
 
 /-- Group homomorphisms preserve inverse. -/
-@[to_additive]
-protected theorem map_inv {G H} [group G] [group H] (f : G →* H) (g : G) : f g⁻¹ = (f g)⁻¹ :=
-map_inv f g
+@[to_additive "Additive group homomorphisms preserve negation."]
+protected lemma map_inv [group α] [division_monoid β] (f : α →* β) (a : α) : f a⁻¹ = (f a)⁻¹ :=
+map_inv f _
 
 /-- Group homomorphisms preserve integer power. -/
 @[to_additive "Additive group homomorphisms preserve integer scaling."]
-protected theorem map_zpow {G H} [group G] [group H] (f : G →* H) (g : G) (n : ℤ) :
+protected theorem map_zpow [group α] [division_monoid β] (f : α →* β) (g : α) (n : ℤ) :
   f (g ^ n) = (f g) ^ n :=
 map_zpow f g n
 
 /-- Group homomorphisms preserve division. -/
 @[to_additive "Additive group homomorphisms preserve subtraction."]
-protected theorem map_div {G H} [group G] [group H] (f : G →* H) (g h : G) :
+protected theorem map_div [group α] [division_monoid β] (f : α →* β) (g h : α) :
   f (g / h) = f g / f h :=
 map_div f g h
 
 /-- Group homomorphisms preserve division. -/
-@[to_additive]
-protected theorem map_mul_inv {G H} [group G] [group H] (f : G →* H) (g h : G) :
+@[to_additive "Additive group homomorphisms preserve subtraction."]
+protected theorem map_mul_inv [group α] [division_monoid β] (f : α →* β) (g h : α) :
   f (g * h⁻¹) = (f g) * (f h)⁻¹ :=
 map_mul_inv f g h
 

src/algebra/hom/units.lean

@@ -12,7 +12,7 @@ import algebra.hom.group
 universes u v w
 
 namespace units
-variables {M : Type u} {N : Type v} {P : Type w} [monoid M] [monoid N] [monoid P]
+variables {α : Type*} {M : Type u} {N : Type v} {P : Type w} [monoid M] [monoid N] [monoid P]
 
 /-- The group homomorphism on units induced by a `monoid_hom`. -/
 @[to_additive "The `add_group` homomorphism on `add_unit`s induced by an `add_monoid_hom`."]
@@ -48,9 +48,16 @@ variable {M}
 lemma coe_pow (u : Mˣ) (n : ℕ) : ((u ^ n : Mˣ) : M) = u ^ n :=
 (units.coe_hom M).map_pow u n
 
-@[simp, norm_cast, to_additive]
-lemma coe_zpow {G} [group G] (u : Gˣ) (n : ℤ) : ((u ^ n : Gˣ) : G) = u ^ n :=
-(units.coe_hom G).map_zpow u n
+section division_monoid
+variables [division_monoid α]
+
+@[simp, norm_cast, to_additive] lemma coe_inv : ∀ u : αˣ, ↑u⁻¹ = (u⁻¹ : α) :=
+(units.coe_hom α).map_inv
+
+@[simp, norm_cast, to_additive] lemma coe_zpow : ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) = u ^ n :=
+(units.coe_hom α).map_zpow
+
+end division_monoid
 
 /-- If a map `g : M → Nˣ` agrees with a homomorphism `f : M →* N`, then
 this map is a monoid homomorphism too. -/

src/analysis/normed/group/hom_completion.lean

@@ -121,15 +121,15 @@ end
 
 lemma normed_group_hom.completion_neg (f : normed_group_hom G H) :
   (-f).completion = -f.completion :=
-normed_group_hom_completion_hom.map_neg f
+map_neg (normed_group_hom_completion_hom : normed_group_hom G H →+ _) f
 
 lemma normed_group_hom.completion_add (f g : normed_group_hom G H) :
   (f + g).completion = f.completion + g.completion :=
 normed_group_hom_completion_hom.map_add f g
 
 lemma normed_group_hom.completion_sub (f g : normed_group_hom G H) :
   (f - g).completion = f.completion - g.completion :=
-normed_group_hom_completion_hom.map_sub f g
+map_sub (normed_group_hom_completion_hom : normed_group_hom G H →+ _) f g
 
 @[simp]
 lemma normed_group_hom.zero_completion : (0 : normed_group_hom G H).completion = 0 :=

src/category_theory/linear/linear_functor.lean

@@ -81,7 +81,7 @@ instance nat_linear : F.linear ℕ :=
 { map_smul' := λ X Y f r, F.map_add_hom.map_nsmul f r, }
 
 instance int_linear : F.linear ℤ :=
-{ map_smul' := λ X Y f r, F.map_add_hom.map_zsmul f r, }
+{ map_smul' := λ X Y f r, (F.map_add_hom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_zsmul f r, }
 
 variables [category_theory.linear ℚ C] [category_theory.linear ℚ D]
 

src/category_theory/preadditive/additive_functor.lean

@@ -65,15 +65,15 @@ instance {E : Type*} [category E] [preadditive E] (G : D ⥤ E) [functor.additiv
 
 @[simp]
 lemma map_neg {X Y : C} {f : X ⟶ Y} : F.map (-f) = - F.map f :=
-F.map_add_hom.map_neg _
+(F.map_add_hom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_neg _
 
 @[simp]
 lemma map_sub {X Y : C} {f g : X ⟶ Y} : F.map (f - g) = F.map f - F.map g :=
-F.map_add_hom.map_sub _ _
+(F.map_add_hom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_sub _ _
 
 -- You can alternatively just use `functor.map_smul` here, with an explicit `(r : ℤ)` argument.
 lemma map_zsmul {X Y : C} {f : X ⟶ Y} {r : ℤ} : F.map (r • f) = r • F.map f :=
-F.map_add_hom.map_zsmul _ _
+(F.map_add_hom : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)).map_zsmul _ _
 
 open_locale big_operators
 

src/category_theory/preadditive/functor_category.lean

@@ -65,7 +65,7 @@ as group homomorphism -/
 (app_hom X).map_nsmul α n
 
 @[simp] lemma app_zsmul (X : C) (α : F ⟶ G) (n : ℤ) : (n • α).app X = n • α.app X :=
-(app_hom X).map_zsmul α n
+(app_hom X : (F ⟶ G) →+ (F.obj X ⟶ G.obj X)).map_zsmul α n
 
 @[simp] lemma app_sum {ι : Type*} (s : finset ι) (X : C) (α : ι → (F ⟶ G)) :
   (∑ i in s, α i).app X = ∑ i in s, ((α i).app X) :=

src/group_theory/free_abelian_group.lean

@@ -164,7 +164,7 @@ begin
   { assume x,
     simp only [lift.of, pi.add_apply] },
   { assume x h,
-    simp only [(lift _).map_neg, lift.of, pi.add_apply, neg_add] },
+    simp only [map_neg, lift.of, pi.add_apply, neg_add] },
   { assume x y hx hy,
     simp only [(lift _).map_add, hx, hy, add_add_add_comm] }
 end
@@ -208,11 +208,11 @@ rfl
 (lift _).map_add _ _
 
 @[simp] protected lemma map_neg (f : α → β) (x : free_abelian_group α) : f <$> (-x) = -(f <$> x) :=
-(lift _).map_neg _
+map_neg (lift $ of ∘ f) _
 
 @[simp] protected lemma map_sub (f : α → β) (x y : free_abelian_group α) :
   f <$> (x - y) = f <$> x - f <$> y :=
-(lift _).map_sub _ _
+map_sub (lift $ of ∘ f) _ _
 
 @[simp] lemma map_of (f : α → β) (y : α) : f <$> of y = of (f y) := rfl
 
@@ -228,11 +228,11 @@ lift.of _ _
 
 @[simp] lemma neg_bind (f : α → free_abelian_group β) (x : free_abelian_group α) :
   -x >>= f = -(x >>= f) :=
-(lift _).map_neg _
+map_neg (lift f) _
 
 @[simp] lemma sub_bind (f : α → free_abelian_group β) (x y : free_abelian_group α) :
   x - y >>= f = (x >>= f) - (y >>= f) :=
-(lift _).map_sub _ _
+map_sub (lift f) _ _
 
 @[simp] lemma pure_seq (f : α → β) (x : free_abelian_group α) : pure f <*> x = f <$> x :=
 pure_bind _ _
@@ -423,19 +423,17 @@ def lift_monoid : (α →* R) ≃ (free_abelian_group α →+* R) :=
     map_one' := (lift.of f _).trans f.map_one,
     map_mul' := λ x y,
     begin
-      refine free_abelian_group.induction_on y (mul_zero _).symm (λ L2, _) _ _,
+      refine free_abelian_group.induction_on y (mul_zero _).symm (λ L2, _) (λ L2 ih, _) _,
       { refine free_abelian_group.induction_on x (zero_mul _).symm (λ L1, _) (λ L1 ih, _) _,
         { simp_rw [of_mul_of, lift.of],
           exact f.map_mul _ _ },
-        { simp_rw [neg_mul, (lift f).map_neg, neg_mul],
+        { simp_rw [neg_mul, map_neg, neg_mul],
           exact congr_arg has_neg.neg ih },
         { intros x1 x2 ih1 ih2,
           simp only [add_mul, map_add, ih1, ih2] } },
-      { intros L2 ih,
-        rw [mul_neg, add_monoid_hom.map_neg, add_monoid_hom.map_neg,
-          mul_neg, ih] },
+      { rw [mul_neg, map_neg, map_neg, mul_neg, ih] },
       { intros y1 y2 ih1 ih2,
-        rw [mul_add, add_monoid_hom.map_add, add_monoid_hom.map_add, mul_add, ih1, ih2] },
+        rw [mul_add, map_add, map_add, mul_add, ih1, ih2] },
     end,
     .. lift f },
   inv_fun := λ F, monoid_hom.comp ↑F of_mul_hom,

src/group_theory/free_group.lean

@@ -603,7 +603,7 @@ prod.of
 (@prod (multiplicative _) _).map_one
 
 @[simp] lemma sum.map_inv : sum x⁻¹ = -sum x :=
-(@prod (multiplicative _) _).map_inv _
+(prod : free_group (multiplicative α) →* multiplicative α).map_inv _
 
 end sum