chore(algebra/module/basic): generalize to add_monoid_hom_class (#13346)

eric-wieser · eric-wieser · commit bf1b813e20e1 · 2022-04-12T03:21:17.000Z
I need some of these lemmas for `ring_hom`.

Additionally, this:
* removes `map_nat_module_smul` (duplicate of `map_nsmul`) and `map_int_module_smul` (duplicate of `map_zsmul`)
* renames `map_rat_module_smul` to `map_rat_smul` for brevity.
* adds the lemmas `inv_nat_cast_smul_comm` and `inv_int_cast_smul_comm`.
* Swaps the order of the arguments to `map_zsmul` and `map_nsmul` to align with the usual rules (`to_additive` emitted them in the wrong order)
diff --git a/src/algebra/category/Group/Z_Module_equivalence.lean b/src/algebra/category/Group/Z_Module_equivalence.lean
@@ -24,10 +24,12 @@ namespace Module
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is full. -/
 instance forget₂_AddCommGroup_full : full (forget₂ (Module ℤ) AddCommGroup.{u}) :=
 { preimage := λ A B f,
-  -- TODO: why `add_monoid_hom.to_int_linear_map` doesn't work here?
+  -- `add_monoid_hom.to_int_linear_map` doesn't work here because `A` and `B` are not definitionally
+  -- equal to the canonical `add_comm_group.int_module` module instances it expects.
   { to_fun := f,
     map_add' := add_monoid_hom.map_add f,
-    map_smul' := λ n x, by simp [int_smul_eq_zsmul] } }
+    map_smul' := λ n x, by rw [int_smul_eq_zsmul, int_smul_eq_zsmul, map_zsmul,
+                               ring_hom.id_apply] } }
 
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
 instance forget₂_AddCommGroup_ess_surj : ess_surj (forget₂ (Module ℤ) AddCommGroup.{u}) :=
diff --git a/src/algebra/hom/group.lean b/src/algebra/hom/group.lean
@@ -307,25 +307,42 @@ 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]
 
-@[simp, to_additive] theorem map_pow [monoid G] [monoid H] [monoid_hom_class F G H]
+-- to_additive puts the arguments in the wrong order, so generate an auxiliary lemma, then
+-- swap its arguments.
+@[to_additive map_nsmul.aux, simp] 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]
 
+@[simp] theorem map_nsmul [add_monoid G] [add_monoid H] [add_monoid_hom_class F G H]
+  (f : F) (n : ℕ) (a : G) : f (n • a) = n • (f a) :=
+map_nsmul.aux f a n
+
+attribute [to_additive_reorder 8, to_additive] 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]
 
+-- to_additive puts the arguments in the wrong order, so generate an auxiliary lemma, then
+-- swap its arguments.
 /-- Group homomorphisms preserve integer power. -/
-@[simp, to_additive "Additive group homomorphisms preserve integer scaling."]
+@[to_additive map_zsmul.aux, simp]
 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
 
+/-- 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) :
+  f (n • g) = n • f g :=
+map_zsmul.aux f g n
+
+attribute [to_additive_reorder 8, to_additive] map_zpow
+
 end mul_one
 
 section mul_zero_one
diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean
@@ -360,29 +360,21 @@ def add_comm_group.int_module.unique : unique (module ℤ M) :=
 
 end add_comm_group
 
-namespace add_monoid_hom
-
-lemma map_nat_module_smul [add_monoid M] [add_monoid M₂]
-  (f : M →+ M₂) (x : ℕ) (a : M) : f (x • a) = x • f a :=
-f.map_nsmul a x
-
-lemma map_int_module_smul [add_group M] [add_group M₂]
-  (f : M →+ M₂) (x : ℤ) (a : M) : f (x • a) = x • f a :=
-f.map_zsmul a x
-
-lemma map_int_cast_smul [add_comm_group M] [add_comm_group M₂]
-  (f : M →+ M₂) (R S : Type*) [ring R] [ring S] [module R M] [module S M₂]
+lemma map_int_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
+  [add_monoid_hom_class F M M₂] (f : F) (R S : Type*) [ring R] [ring S] [module R M] [module S M₂]
   (x : ℤ) (a : M) : f ((x : R) • a) = (x : S) • f a :=
-by simp only [←zsmul_eq_smul_cast, f.map_zsmul]
+by simp only [←zsmul_eq_smul_cast, map_zsmul]
 
-lemma map_nat_cast_smul [add_comm_monoid M] [add_comm_monoid M₂] (f : M →+ M₂)
+lemma map_nat_cast_smul [add_comm_monoid M] [add_comm_monoid M₂] {F : Type*}
+  [add_monoid_hom_class F M M₂] (f : F)
   (R S : Type*) [semiring R] [semiring S] [module R M] [module S M₂] (x : ℕ) (a : M) :
   f ((x : R) • a) = (x : S) • f a :=
-by simp only [←nsmul_eq_smul_cast, f.map_nsmul]
+by simp only [←nsmul_eq_smul_cast, map_nsmul]
 
-lemma map_inv_int_cast_smul {E F : Type*} [add_comm_group E] [add_comm_group F] (f : E →+ F)
-  (R S : Type*) [division_ring R] [division_ring S] [module R E] [module S F]
-  (n : ℤ) (x : E) :
+lemma map_inv_int_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
+  [add_monoid_hom_class F M M₂] (f : F)
+  (R S : Type*) [division_ring R] [division_ring S] [module R M] [module S M₂]
+  (n : ℤ) (x : M) :
   f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x :=
 begin
   by_cases hR : (n : R) = 0; by_cases hS : (n : S) = 0,
@@ -394,65 +386,79 @@ begin
   { rw [← inv_smul_smul₀ hS (f _), ← map_int_cast_smul f R S, smul_inv_smul₀ hR] }
 end
 
-lemma map_inv_nat_cast_smul {E F : Type*} [add_comm_group E] [add_comm_group F] (f : E →+ F)
-  (R S : Type*) [division_ring R] [division_ring S] [module R E] [module S F]
-  (n : ℕ) (x : E) :
+lemma map_inv_nat_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
+  [add_monoid_hom_class F M M₂] (f : F)
+  (R S : Type*) [division_ring R] [division_ring S] [module R M] [module S M₂]
+  (n : ℕ) (x : M) :
   f ((n⁻¹ : R) • x) = (n⁻¹ : S) • f x :=
-f.map_inv_int_cast_smul R S n x
+map_inv_int_cast_smul f R S n x
 
-lemma map_rat_cast_smul {E F : Type*} [add_comm_group E] [add_comm_group F] (f : E →+ F)
-  (R S : Type*) [division_ring R] [division_ring S] [module R E] [module S F]
-  (c : ℚ) (x : E) :
+lemma map_rat_cast_smul [add_comm_group M] [add_comm_group M₂] {F : Type*}
+  [add_monoid_hom_class F M M₂] (f : F)
+  (R S : Type*) [division_ring R] [division_ring S] [module R M] [module S M₂]
+  (c : ℚ) (x : M) :
   f ((c : R) • x) = (c : S) • f x :=
 by rw [rat.cast_def, rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
   map_int_cast_smul f R S, map_inv_nat_cast_smul f R S]
 
-lemma map_rat_module_smul {E : Type*} [add_comm_group E] [module ℚ E]
-  {F : Type*} [add_comm_group F] [module ℚ F] (f : E →+ F) (c : ℚ) (x : E) :
+lemma map_rat_smul [add_comm_group M] [add_comm_group M₂] [module ℚ M] [module ℚ M₂] {F : Type*}
+  [add_monoid_hom_class F M M₂] (f : F) (c : ℚ) (x : M) :
   f (c • x) = c • f x :=
-rat.cast_id c ▸ f.map_rat_cast_smul ℚ ℚ c x
-
-end add_monoid_hom
+rat.cast_id c ▸ map_rat_cast_smul f ℚ ℚ c x
 
 /-- There can be at most one `module ℚ E` structure on an additive commutative group. This is not
 an instance because `simp` becomes very slow if we have many `subsingleton` instances,
 see [gh-6025]. -/
 lemma subsingleton_rat_module (E : Type*) [add_comm_group E] : subsingleton (module ℚ E) :=
 ⟨λ P Q, module.ext' P Q $ λ r x,
-  @add_monoid_hom.map_rat_module_smul E ‹_› P E ‹_› Q (add_monoid_hom.id _) r x⟩
+  @map_rat_smul _ _ _ _ P Q _ _ (add_monoid_hom.id E) r x⟩
 
 /-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
 agree on inverses of integer numbers in `R` and `S`. -/
 lemma inv_int_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]
   [division_ring S] [module R E] [module S E] (n : ℤ) (x : E) :
   (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
-(add_monoid_hom.id E).map_inv_int_cast_smul R S n x
+map_inv_int_cast_smul (add_monoid_hom.id E) R S n x
 
 /-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
 agree on inverses of natural numbers in `R` and `S`. -/
 lemma inv_nat_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]
   [division_ring S] [module R E] [module S E] (n : ℕ) (x : E) :
   (n⁻¹ : R) • x = (n⁻¹ : S) • x :=
-(add_monoid_hom.id E).map_inv_nat_cast_smul R S n x
+map_inv_nat_cast_smul (add_monoid_hom.id E) R S n x
+
+/-- If `E` is a vector space over a division rings `R` and has a monoid action by `α`, then that
+action commutes by scalar multiplication of inverses of integers in `R` -/
+lemma inv_int_cast_smul_comm {α E : Type*} (R : Type*) [add_comm_group E] [division_ring R]
+  [monoid α] [module R E] [distrib_mul_action α E] (n : ℤ) (s : α) (x : E) :
+  (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
+(map_inv_int_cast_smul (distrib_mul_action.to_add_monoid_hom E s) R R n x).symm
+
+/-- If `E` is a vector space over a division rings `R` and has a monoid action by `α`, then that
+action commutes by scalar multiplication of inverses of natural numbers in `R`. -/
+lemma inv_nat_cast_smul_comm {α E : Type*} (R : Type*) [add_comm_group E] [division_ring R]
+  [monoid α] [module R E] [distrib_mul_action α E] (n : ℕ) (s : α) (x : E) :
+  (n⁻¹ : R) • s • x = s • (n⁻¹ : R) • x :=
+(map_inv_nat_cast_smul (distrib_mul_action.to_add_monoid_hom E s) R R n x).symm
 
 /-- If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications
 agree on rational numbers in `R` and `S`. -/
 lemma rat_cast_smul_eq {E : Type*} (R S : Type*) [add_comm_group E] [division_ring R]
   [division_ring S] [module R E] [module S E] (r : ℚ) (x : E) :
   (r : R) • x = (r : S) • x :=
-(add_monoid_hom.id E).map_rat_cast_smul R S r x
+map_rat_cast_smul (add_monoid_hom.id E) R S r x
 
 instance add_comm_group.int_is_scalar_tower {R : Type u} {M : Type v} [ring R] [add_comm_group M]
   [module R M]: is_scalar_tower ℤ R M :=
-{ smul_assoc := λ n x y, ((smul_add_hom R M).flip y).map_int_module_smul n x }
+{ smul_assoc := λ n x y, ((smul_add_hom R M).flip y).map_zsmul x n }
 
 instance is_scalar_tower.rat {R : Type u} {M : Type v} [ring R] [add_comm_group M]
   [module R M] [module ℚ R] [module ℚ M] : is_scalar_tower ℚ R M :=
-{ smul_assoc := λ r x y, ((smul_add_hom R M).flip y).map_rat_module_smul r x }
+{ smul_assoc := λ r x y, map_rat_smul ((smul_add_hom R M).flip y) r x }
 
 instance smul_comm_class.rat {R : Type u} {M : Type v} [semiring R] [add_comm_group M]
   [module R M] [module ℚ M] : smul_comm_class ℚ R M :=
-{ smul_comm := λ r x y, ((smul_add_hom R M x).map_rat_module_smul r y).symm }
+{ smul_comm := λ r x y, (map_rat_smul (smul_add_hom R M x) r y).symm }
 
 instance smul_comm_class.rat' {R : Type u} {M : Type v} [semiring R] [add_comm_group M]
   [module R M] [module ℚ M] : smul_comm_class R ℚ M :=
diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
@@ -500,7 +500,7 @@ abbreviation module.End (R : Type u) (M : Type v)
 /-- Reinterpret an additive homomorphism as a `ℕ`-linear map. -/
 def add_monoid_hom.to_nat_linear_map [add_comm_monoid M] [add_comm_monoid M₂] (f : M →+ M₂) :
   M →ₗ[ℕ] M₂ :=
-{ to_fun := f, map_add' := f.map_add, map_smul' := f.map_nat_module_smul }
+{ to_fun := f, map_add' := f.map_add, map_smul' := map_nsmul f }
 
 lemma add_monoid_hom.to_nat_linear_map_injective [add_comm_monoid M] [add_comm_monoid M₂] :
   function.injective (@add_monoid_hom.to_nat_linear_map M M₂ _ _) :=
@@ -509,7 +509,7 @@ by { intros f g h, ext, exact linear_map.congr_fun h x }
 /-- Reinterpret an additive homomorphism as a `ℤ`-linear map. -/
 def add_monoid_hom.to_int_linear_map [add_comm_group M] [add_comm_group M₂] (f : M →+ M₂) :
   M →ₗ[ℤ] M₂ :=
-{ to_fun := f, map_add' := f.map_add, map_smul' := f.map_int_module_smul }
+{ to_fun := f, map_add' := f.map_add, map_smul' := map_zsmul f }
 
 lemma add_monoid_hom.to_int_linear_map_injective [add_comm_group M] [add_comm_group M₂] :
   function.injective (@add_monoid_hom.to_int_linear_map M M₂ _ _) :=
@@ -523,7 +523,7 @@ by { intros f g h, ext, exact linear_map.congr_fun h x }
 def add_monoid_hom.to_rat_linear_map [add_comm_group M] [module ℚ M]
   [add_comm_group M₂] [module ℚ M₂] (f : M →+ M₂) :
   M →ₗ[ℚ] M₂ :=
-{ map_smul' := f.map_rat_module_smul, ..f }
+{ map_smul' := map_rat_smul f, ..f }
 
 lemma add_monoid_hom.to_rat_linear_map_injective
   [add_comm_group M] [module ℚ M] [add_comm_group M₂] [module ℚ M₂] :
diff --git a/src/category_theory/preadditive/default.lean b/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 P g) f n
+map_nsmul (right_comp P g) n f
 
 lemma comp_nsmul (n : ℕ) : f ≫ (n • g) = n • (f ≫ g) :=
-map_nsmul (left_comp R f) g n
+map_nsmul (left_comp R f) n g
 
 lemma zsmul_comp (n : ℤ) : (n • f) ≫ g = n • (f ≫ g) :=
-map_zsmul (right_comp P g) f n
+map_zsmul (right_comp P g) n f
 
 lemma comp_zsmul (n : ℤ) : f ≫ (n • g) = n • (f ≫ g) :=
-map_zsmul (left_comp R f) g n
+map_zsmul (left_comp R f) n g
 
 @[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 :=
diff --git a/src/group_theory/free_abelian_group.lean b/src/group_theory/free_abelian_group.lean
@@ -481,7 +481,7 @@ def punit_equiv (T : Type*) [unique T] : free_abelian_group T ≃+ ℤ :=
     (λ x y hx hy, by { simp only [add_monoid_hom.map_add, add_smul] at *, rw [hx, hy]}),
   right_inv := λ n,
   begin
-    rw [add_monoid_hom.map_int_module_smul, lift.of],
+    rw [add_monoid_hom.map_zsmul, lift.of],
     exact zsmul_int_one n
   end,
   map_add' := add_monoid_hom.map_add _ }
diff --git a/src/topology/instances/real_vector_space.lean b/src/topology/instances/real_vector_space.lean
@@ -27,7 +27,7 @@ suffices (λ c : ℝ, f (c • x)) = λ c : ℝ, c • f x, from _root_.congr_fu
 rat.dense_embedding_coe_real.dense.equalizer
   (hf.comp $ continuous_id.smul continuous_const)
   (continuous_id.smul continuous_const)
-  (funext $ λ r, f.map_rat_cast_smul ℝ ℝ r x)
+  (funext $ λ r, map_rat_cast_smul f ℝ ℝ r x)
 
 /-- Reinterpret a continuous additive homomorphism between two real vector spaces
 as a continuous real-linear map. -/
