feat(algebra/group): make map_[z]pow generic in monoid_hom_class (#10749)

This PR makes `map_pow` take a `monoid_hom_class` instead of specifically a `monoid_hom`.

Author: Vierkantor

src/algebra/group/hom.lean

@@ -281,6 +281,25 @@ by rw [map_mul, map_inv]
   (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]
 
+@[simp, to_additive map_nsmul] theorem map_pow [monoid G] [monoid H] [monoid_hom_class F G H]
+  (f : F) (a : G) :
+  ∀ (n : ℕ), f (a ^ n) = (f a) ^ n
+| 0     := by rw [pow_zero, pow_zero, map_one]
+| (n+1) := by rw [pow_succ, pow_succ, map_mul, map_pow]
+
+@[to_additive]
+theorem map_zpow' [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H]
+  (f : F) (hf : ∀ (x : G), f (x⁻¹) = (f x)⁻¹) (a : G) :
+  ∀ n : ℤ, f (a ^ n) = (f a) ^ n
+| (n : ℕ) := by rw [zpow_coe_nat, map_pow, zpow_coe_nat]
+| -[1+n]  := by rw [zpow_neg_succ_of_nat, hf, map_pow, ← zpow_neg_succ_of_nat]
+
+/-- Group homomorphisms preserve integer power. -/
+@[simp, to_additive /-" Additive group homomorphisms preserve integer scaling. "-/]
+theorem map_zpow [group G] [group 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
+
 end mul_one
 
 section mul_zero_one
@@ -760,18 +779,16 @@ monoid_with_zero_hom.ext $ λ x, rfl
   (f : monoid_with_zero_hom M N) : (monoid_with_zero_hom.id N).comp f = f :=
 monoid_with_zero_hom.ext $ λ x, rfl
 
-@[simp, to_additive add_monoid_hom.map_nsmul]
-theorem monoid_hom.map_pow [monoid M] [monoid N] (f : M →* N) (a : M) :
-  ∀(n : ℕ), f (a ^ n) = (f a) ^ n
-| 0     := by rw [pow_zero, pow_zero, f.map_one]
-| (n+1) := by rw [pow_succ, pow_succ, f.map_mul, monoid_hom.map_pow]
+@[to_additive add_monoid_hom.map_nsmul]
+protected theorem monoid_hom.map_pow [monoid M] [monoid N] (f : M →* N) (a : M) (n : ℕ) :
+  f (a ^ n) = (f a) ^ n :=
+map_pow f a n
 
 @[to_additive]
-theorem monoid_hom.map_zpow' [div_inv_monoid M] [div_inv_monoid N] (f : M →* N)
-  (hf : ∀ x, f (x⁻¹) = (f x)⁻¹) (a : M) :
-  ∀ n : ℤ, f (a ^ n) = (f a) ^ n
-| (n : ℕ) := by rw [zpow_coe_nat, f.map_pow, zpow_coe_nat]
-| -[1+n]  := by rw [zpow_neg_succ_of_nat, hf, f.map_pow, ← zpow_neg_succ_of_nat]
+protected theorem monoid_hom.map_zpow' [div_inv_monoid M] [div_inv_monoid N] (f : M →* N)
+  (hf : ∀ x, f (x⁻¹) = (f x)⁻¹) (a : M) (n : ℤ) :
+  f (a ^ n) = (f a) ^ n :=
+map_zpow' f hf a n
 
 @[to_additive]
 theorem monoid_hom.map_div' [div_inv_monoid M] [div_inv_monoid N] (f : M →* N)
@@ -926,9 +943,10 @@ protected theorem map_inv {G H} [group G] [group H] (f : G →* H) (g : G) : f g
 map_inv f g
 
 /-- Group homomorphisms preserve integer power. -/
-@[simp, to_additive /-" Additive group homomorphisms preserve integer scaling. "-/]
-theorem map_zpow {G H} [group G] [group H] (f : G →* H) (g : G) (n : ℤ) : f (g ^ n) = (f g) ^ n :=
-f.map_zpow' f.map_inv g n
+@[to_additive /-" Additive group homomorphisms preserve integer scaling. "-/]
+protected theorem map_zpow {G H} [group G] [group H] (f : G →* H) (g : G) (n : ℤ) :
+  f (g ^ n) = (f g) ^ n :=
+map_zpow f g n
 
 /-- Group homomorphisms preserve division. -/
 @[to_additive /-" Additive group homomorphisms preserve subtraction. "-/]

src/algebra/group_power/basic.lean

@@ -286,9 +286,9 @@ namespace ring_hom
 
 variables [semiring R] [semiring S]
 
-@[simp] lemma map_pow (f : R →+* S) (a) :
+protected lemma map_pow (f : R →+* S) (a) :
   ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
-f.to_monoid_hom.map_pow a
+map_pow f a
 
 end ring_hom
 

src/category_theory/preadditive/default.lean

@@ -133,16 +133,16 @@ map_neg (left_comp R f) g
 by simp
 
 lemma nsmul_comp (n : ℕ) : (n • f) ≫ g = n • (f ≫ g) :=
-map_nsmul (right_comp _ _) _ _
+map_nsmul (right_comp P g) f n
 
 lemma comp_nsmul (n : ℕ) : f ≫ (n • g) = n • (f ≫ g) :=
-map_nsmul (left_comp _ _) _ _
+map_nsmul (left_comp R f) g n
 
 lemma zsmul_comp (n : ℤ) : (n • f) ≫ g = n • (f ≫ g) :=
-map_zsmul (right_comp _ _) _ _
+map_zsmul (right_comp P g) f n
 
 lemma comp_zsmul (n : ℤ) : f ≫ (n • g) = n • (f ≫ g) :=
-map_zsmul (left_comp _ _) _ _
+map_zsmul (left_comp R f) g n
 
 @[reassoc] lemma comp_sum {P Q R : C} {J : Type*} (s : finset J) (f : P ⟶ Q) (g : J → (Q ⟶ R)) :
   f ≫ ∑ j in s, g j = ∑ j in s, f ≫ g j :=

src/data/polynomial/derivative.lean

@@ -214,10 +214,10 @@ theorem derivative_map [comm_semiring S] (p : polynomial R) (f : R →+* S) :
 polynomial.induction_on p
   (λ r, by rw [map_C, derivative_C, derivative_C, map_zero])
   (λ p q ihp ihq, by rw [map_add, derivative_add, ihp, ihq, derivative_add, map_add])
-  (λ n r ih, by rw [map_mul, map_C, map_pow, map_X,
+  (λ n r ih, by rw [map_mul, map_C, polynomial.map_pow, map_X,
       derivative_mul, derivative_pow_succ, derivative_C, zero_mul, zero_add, derivative_X, mul_one,
       derivative_mul, derivative_pow_succ, derivative_C, zero_mul, zero_add, derivative_X, mul_one,
-      map_mul, map_C, map_mul, map_pow, map_add, map_nat_cast, map_one, map_X])
+      map_mul, map_C, map_mul, polynomial.map_pow, map_add, map_nat_cast, map_one, map_X])
 
 @[simp]
 theorem iterate_derivative_map [comm_semiring S] (p : polynomial R) (f : R →+* S) (k : ℕ):

src/data/polynomial/eval.lean

@@ -594,7 +594,8 @@ ring_hom.ext $ map_map g f
 lemma map_list_prod (L : list (polynomial R)) : L.prod.map f = (L.map $ map f).prod :=
 eq.symm $ list.prod_hom _ (map_ring_hom f).to_monoid_hom
 
-@[simp] lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n := (map_ring_hom f).map_pow _ _
+@[simp] protected lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n :=
+(map_ring_hom f).map_pow _ _
 
 lemma mem_map_srange {p : polynomial S} :
   p ∈ (map_ring_hom f).srange ↔ ∀ n, p.coeff n ∈ f.srange :=
@@ -606,7 +607,7 @@ begin
     intros i hi,
     rcases h i with ⟨c, hc⟩,
     use [C c * X^i],
-    rw [coe_map_ring_hom, map_mul, map_C, hc, map_pow, map_X] }
+    rw [coe_map_ring_hom, map_mul, map_C, hc, polynomial.map_pow, map_X] }
 end
 
 lemma mem_map_range {R S : Type*} [ring R] [ring S] (f : R →+* S)

src/data/polynomial/lifts.lean

@@ -199,7 +199,7 @@ begin
   { rw [← erase_lead_add_C_mul_X_pow p, er_zero, zero_add, monic.def.1 hmonic, C_1, one_mul],
     use X ^ p.nat_degree,
     repeat {split},
-    { simp only [map_pow, map_X] },
+    { simp only [polynomial.map_pow, map_X] },
     { rw [@degree_X_pow R _ Rtrivial, degree_X_pow] },
     {exact monic_pow monic_X p.nat_degree } },
   obtain ⟨q, hq⟩ := mem_lifts_and_degree_eq (erase_mem_lifts p.nat_degree hlifts),
@@ -210,7 +210,7 @@ begin
     ← @degree_X_pow R _ Rtrivial p.nat_degree] at deg_er,
   use q + X ^ p.nat_degree,
   repeat {split},
-  { simp only [hq, map_add, map_pow, map_X],
+  { simp only [hq, map_add, polynomial.map_pow, map_X],
     nth_rewrite 3 [← erase_lead_add_C_mul_X_pow p],
     rw [erase_lead, monic.leading_coeff hmonic, C_1, one_mul] },
   { rw [degree_add_eq_right_of_degree_lt deg_er, @degree_X_pow R _ Rtrivial p.nat_degree,

src/field_theory/abel_ruffini.lean

@@ -182,8 +182,9 @@ begin
   have C_mul_C : (C (i a⁻¹)) * (C (i a)) = 1,
   { rw [←C_mul, ←i.map_mul, inv_mul_cancel ha, i.map_one, C_1] },
   have key1 : (X ^ n - 1).map i = C (i a⁻¹) * ((X ^ n - C a).map i).comp (C b * X),
-  { rw [polynomial.map_sub, polynomial.map_sub, map_pow, map_X, map_C, polynomial.map_one, sub_comp,
-        pow_comp, X_comp, C_comp, mul_pow, ←C_pow, hb, mul_sub, ←mul_assoc, C_mul_C, one_mul] },
+  { rw [polynomial.map_sub, polynomial.map_sub, polynomial.map_pow, map_X, map_C,
+        polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ←C_pow, hb, mul_sub,
+        ←mul_assoc, C_mul_C, one_mul] },
   have key2 : (λ q : polynomial E, q.comp (C b * X)) ∘ (λ c : E, X - C c) =
     (λ c : E, C b * (X - C (c / b))),
   { ext1 c,
@@ -202,10 +203,11 @@ begin
   apply gal_is_solvable_tower (X ^ n - 1) (X ^ n - C x),
   { exact splits_X_pow_sub_one_of_X_pow_sub_C _ n hx (splitting_field.splits _) },
   { exact gal_X_pow_sub_one_is_solvable n },
-  { rw [polynomial.map_sub, map_pow, map_X, map_C],
+  { rw [polynomial.map_sub, polynomial.map_pow, map_X, map_C],
     apply gal_X_pow_sub_C_is_solvable_aux,
     have key := splitting_field.splits (X ^ n - 1 : polynomial F),
-    rwa [←splits_id_iff_splits, polynomial.map_sub, map_pow, map_X, polynomial.map_one] at key }
+    rwa [←splits_id_iff_splits, polynomial.map_sub, polynomial.map_pow, map_X, polynomial.map_one]
+      at key }
 end
 
 end gal_X_pow_sub_C
@@ -311,7 +313,7 @@ begin
   { refine gal_is_solvable_tower p (p.comp (X ^ n)) _ hα _,
     { exact gal.splits_in_splitting_field_of_comp _ _ (by rwa [nat_degree_X_pow]) },
     { obtain ⟨s, hs⟩ := exists_multiset_of_splits _ (splitting_field.splits p),
-      rw [map_comp, map_pow, map_X, hs, mul_comp, C_comp],
+      rw [map_comp, polynomial.map_pow, map_X, hs, mul_comp, C_comp],
       apply gal_mul_is_solvable (gal_C_is_solvable _),
       rw prod_comp,
       apply gal_prod_is_solvable,

src/field_theory/finite/basic.lean

@@ -276,14 +276,14 @@ instance : is_splitting_field (zmod p) K (X^q - X) :=
   begin
     have h : (X^q - X : polynomial K).nat_degree = q :=
       X_pow_card_sub_X_nat_degree_eq K fintype.one_lt_card,
-    rw [←splits_id_iff_splits, splits_iff_card_roots, polynomial.map_sub, map_pow, map_X, h,
-      roots_X_pow_card_sub_X K, ←finset.card_def, finset.card_univ],
+    rw [←splits_id_iff_splits, splits_iff_card_roots, polynomial.map_sub, polynomial.map_pow,
+      map_X, h, roots_X_pow_card_sub_X K, ←finset.card_def, finset.card_univ],
   end,
   adjoin_roots :=
   begin
     classical,
     transitivity algebra.adjoin (zmod p) ((roots (X^q - X : polynomial K)).to_finset : set K),
-    { simp only [map_pow, map_X, polynomial.map_sub], convert rfl },
+    { simp only [polynomial.map_pow, map_X, polynomial.map_sub], convert rfl },
     { rw [roots_X_pow_card_sub_X, val_to_finset, coe_univ, algebra.adjoin_univ], }
   end }
 

src/field_theory/finite/galois_field.lean

@@ -93,7 +93,7 @@ begin
   apply subring.closure_induction hx; clear_dependent x; simp_rw mem_root_set aux,
   { rintros x (⟨r, rfl⟩ | hx),
     { simp only [aeval_X_pow, aeval_X, alg_hom.map_sub],
-      rw [← ring_hom.map_pow, zmod.pow_card_pow, sub_self], },
+      rw [← map_pow, zmod.pow_card_pow, sub_self], },
     { dsimp only [galois_field] at hx,
       rwa mem_root_set aux at hx, }, },
   { dsimp only [g_poly],
@@ -144,7 +144,7 @@ by exactI (is_splitting_field.alg_equiv (zmod p) (X ^ (p ^ 1) - X : polynomial (
 variables {K : Type*} [field K] [fintype K] [algebra (zmod p) K]
 
 theorem splits_X_pow_card_sub_X : splits (algebra_map (zmod p) K) (X ^ fintype.card K - X) :=
-by rw [←splits_id_iff_splits, polynomial.map_sub, map_pow, map_X, splits_iff_card_roots,
+by rw [←splits_id_iff_splits, polynomial.map_sub, polynomial.map_pow, map_X, splits_iff_card_roots,
   finite_field.roots_X_pow_card_sub_X, ←finset.card_def, finset.card_univ,
   finite_field.X_pow_card_sub_X_nat_degree_eq]; exact fintype.one_lt_card
 
@@ -157,8 +157,8 @@ lemma is_splitting_field_of_card_eq (h : fintype.card K = p ^ n) :
     { rintro rfl, rw [pow_zero, fintype.card_eq_one_iff_nonempty_unique] at h,
       cases h, resetI, exact false_of_nontrivial_of_subsingleton K },
     refine algebra.eq_top_iff.mpr (λ x, algebra.subset_adjoin _),
-    rw [polynomial.map_sub, map_pow, map_X, finset.mem_coe, multiset.mem_to_finset, mem_roots,
-        is_root.def, eval_sub, eval_pow, eval_X, ← h, finite_field.pow_card, sub_self],
+    rw [polynomial.map_sub, polynomial.map_pow, map_X, finset.mem_coe, multiset.mem_to_finset,
+        mem_roots, is_root.def, eval_sub, eval_pow, eval_X, ← h, finite_field.pow_card, sub_self],
     exact finite_field.X_pow_card_pow_sub_X_ne_zero K hne (fact.out _)
   end }
 

src/linear_algebra/tensor_product.lean

@@ -643,7 +643,7 @@ lemma map_mul (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N) :
   map (f₁ * f₂) (g₁ * g₂) = (map f₁ g₁) * (map f₂ g₂) :=
 map_comp f₁ f₂ g₁ g₂
 
-@[simp] lemma map_pow (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) :
+@[simp] protected lemma map_pow (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) :
   (map f g)^n = map (f^n) (g^n) :=
 begin
   induction n with n ih,
@@ -827,10 +827,10 @@ by simp only [ltensor, rtensor, ← map_comp, id_comp, comp_id]
 variables {M}
 
 @[simp] lemma rtensor_pow (f : M →ₗ[R] M) (n : ℕ) : (f.rtensor N)^n = (f^n).rtensor N :=
-by { have h := map_pow f (id : N →ₗ[R] N) n, rwa id_pow at h, }
+by { have h := tensor_product.map_pow f (id : N →ₗ[R] N) n, rwa id_pow at h, }
 
 @[simp] lemma ltensor_pow (f : N →ₗ[R] N) (n : ℕ) : (f.ltensor M)^n = (f^n).ltensor M :=
-by { have h := map_pow (id : M →ₗ[R] M) f n, rwa id_pow at h, }
+by { have h := tensor_product.map_pow (id : M →ₗ[R] M) f n, rwa id_pow at h, }
 
 end linear_map