refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654)

These were named inconsistently, and lots of proof was duplicated.

The name changes are largely making the API for `nsmul` consistent with the one for `gsmul`:
* For `ℕ`:
  * Replaces `nat.smul_def : n • x = n •ℕ x` with `nsmul_def : n •ℕ x = n • x`
  * Renames `semimodule.nsmul_eq_smul : n •ℕ b = (n : R) • b` to `nsmul_eq_smul_cast`
  * Removes `semimodule.smul_eq_smul : n • b = (n : R) • b`
  * Adds `nsmul_eq_smul : n •ℕ b = n • b` (this is different from `nsmul_def` as described in the docstring)
  * Renames the instances to be named more consistently and all live under `add_comm_monoid.nat_*`
* For `ℤ`:
  * Renames `gsmul_eq_smul : n •ℤ x = n • x` to `gsmul_def`
  * Renames `module.gsmul_eq_smul : n •ℤ x = n • x` to `gsmul_eq_smul`
  * Renames `module.gsmul_eq_smul_cast` to `gsmul_eq_smul_cast`
  * Renames the instances to be named more consistently and all live under `add_comm_group.int_*`

Author: eric-wieser

src/algebra/module/basic.lean

@@ -263,15 +263,14 @@ library_note "vector space definition"
 abbreviation vector_space (R : Type u) (M : Type v) [field R] [add_comm_group M] :=
 semimodule R M
 
-namespace add_comm_monoid
-open add_monoid
+section add_comm_monoid
 
-variables [add_comm_monoid M]
+variables [semiring R] [add_comm_monoid M] [semimodule R M]
 
 /-- The natural ℕ-semimodule structure on any `add_comm_monoid`. -/
 -- We don't make this a global instance, as it results in too many instances,
 -- and confusing ambiguity in the notation `n • x` when `n : ℕ`.
-def nat_semimodule : semimodule ℕ M :=
+def add_comm_monoid.nat_semimodule : semimodule ℕ M :=
 { smul := nsmul,
   smul_add := λ _ _ _, nsmul_add _ _ _,
   add_smul := λ _ _ _, add_nsmul _ _ _,
@@ -280,44 +279,66 @@ def nat_semimodule : semimodule ℕ M :=
   zero_smul := zero_nsmul,
   smul_zero := nsmul_zero }
 
-instance : subsingleton (semimodule ℕ M) :=
+section
+local attribute [instance] add_comm_monoid.nat_semimodule
+/-- `nsmul` is defined as the `smul` action of `add_comm_monoid.nat_semimodule`. -/
+lemma nsmul_def (n : ℕ) (x : M) :
+  n •ℕ x = n • x :=
+rfl
+end
+
+section
+variables (R)
+/-- `nsmul` is equal to any other semimodule structure via a cast. -/
+lemma nsmul_eq_smul_cast (n : ℕ) (b : M) :
+  n •ℕ b = (n : R) • b :=
 begin
-  split,
-  intros P Q,
-  ext n,
-  -- isn't that lovely: `r • m = r • m`
-  have one_smul : by { haveI := P, exact (1 : ℕ) • m } = by { haveI := Q, exact (1 : ℕ) • m },
-    begin
-      rw [@one_smul ℕ _ _ (by { haveI := P, apply_instance, }) m],
-      rw [@one_smul ℕ _ _ (by { haveI := Q, apply_instance, }) m],
-    end,
+  rw nsmul_def,
   induction n with n ih,
-  { erw [zero_smul, zero_smul], },
-  { rw [nat.succ_eq_add_one, add_smul, add_smul],
-    erw ih,
-    rw [one_smul], }
+  { rw [nat.cast_zero, zero_smul, zero_smul] },
+  { rw [nat.succ_eq_add_one, nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul] }
 end
+end
+
+/-- `nsmul` is equal to any `ℕ`-semimodule structure. -/
+lemma nsmul_eq_smul [semimodule ℕ M] (n : ℕ) (b : M) : n •ℕ b = n • b :=
+by rw [nsmul_eq_smul_cast ℕ, n.cast_id]
+
+/-- All `ℕ`-semimodule structures are equal. -/
+instance add_comm_monoid.nat_semimodule.subsingleton : subsingleton (semimodule ℕ M) :=
+⟨λ P Q, by {
+  ext n,
+  rw [←nsmul_eq_smul, ←nsmul_eq_smul], }⟩
 
 /-- Note this does not depend on the `nat_semimodule` definition above, to avoid issues when
 diamonds occur in finding `semimodule ℕ M` instances. -/
-instance nat_is_scalar_tower [semiring S] [semimodule S M] [semimodule ℕ S] [semimodule ℕ M] :
-  is_scalar_tower ℕ S M :=
+instance add_comm_monoid.nat_is_scalar_tower [semimodule ℕ R] [semimodule ℕ M] :
+  is_scalar_tower ℕ R M :=
 { smul_assoc := λ n x y, nat.rec_on n
     (by simp only [zero_smul])
     (λ n ih, by simp only [nat.succ_eq_add_one, add_smul, one_smul, ih]) }
 
+instance add_comm_monoid.nat_smul_comm_class [semimodule ℕ M] : smul_comm_class ℕ R M :=
+{ smul_comm := λ n r m, nat.rec_on n
+    (by simp only [zero_smul, smul_zero])
+    (λ n ih, by simp only [nat.succ_eq_add_one, add_smul, one_smul, ←ih, smul_add]) }
+
+-- `smul_comm_class.symm` is not registered as an instance, as it would cause a loop
+instance add_comm_monoid.nat_smul_comm_class' [semimodule ℕ M] : smul_comm_class R ℕ M :=
+smul_comm_class.symm _ _ _
+
 end add_comm_monoid
 
-namespace add_comm_group
+section add_comm_group
 
-variables [add_comm_group M]
+variables [semiring S] [ring R] [add_comm_group M] [semimodule S M] [semimodule R M]
 
 /-- The natural ℤ-module structure on any `add_comm_group`. -/
 -- We don't immediately make this a global instance, as it results in too many instances,
 -- and confusing ambiguity in the notation `n • x` when `n : ℤ`.
 -- We do turn it into a global instance, but only at the end of this file,
 -- and I remain dubious whether this is a good idea.
-def int_module : module ℤ M :=
+def add_comm_group.int_module : module ℤ M :=
 { smul := gsmul,
   smul_add := λ _ _ _, gsmul_add _ _ _,
   add_smul := λ _ _ _, add_gsmul _ _ _,
@@ -326,114 +347,53 @@ def int_module : module ℤ M :=
   zero_smul := zero_gsmul,
   smul_zero := gsmul_zero }
 
-instance : subsingleton (module ℤ M) :=
-begin
-  split,
-  intros P Q,
-  ext,
-  -- isn't that lovely: `r • m = r • m`
-  have one_smul : by { haveI := P, exact (1 : ℤ) • m } = by { haveI := Q, exact (1 : ℤ) • m },
-    begin
-      rw [@one_smul ℤ _ _ (by { haveI := P, apply_instance, }) m],
-      rw [@one_smul ℤ _ _ (by { haveI := Q, apply_instance, }) m],
-    end,
-  have nat_smul : ∀ n : ℕ, by { haveI := P, exact (n : ℤ) • m } = by { haveI := Q, exact (n : ℤ) • m },
-    begin
-      intro n,
-      induction n with n ih,
-      { erw [zero_smul, zero_smul], },
-      { rw [int.coe_nat_succ, add_smul, add_smul],
-        erw ih,
-        rw [one_smul], }
-    end,
-  cases r,
-  { rw [int.of_nat_eq_coe, nat_smul], },
-  { rw [int.neg_succ_of_nat_coe, neg_smul, neg_smul, nat_smul], }
-end
-
-instance int_is_scalar_tower [ring S] [module S M] [semimodule ℤ S] [semimodule ℤ M] :
-  is_scalar_tower ℤ S M :=
-{ smul_assoc := λ n x y, int.induction_on n
-    (by simp only [zero_smul])
-    (λ n ih, by simp only [one_smul, add_smul, ih])
-    (λ n ih, by simp only [one_smul, sub_smul, ih]) }
-
-end add_comm_group
-
 section
-local attribute [instance] add_comm_monoid.nat_semimodule
-
-lemma semimodule.smul_eq_smul (R : Type*) [semiring R]
-  {M : Type*} [add_comm_monoid M] [semimodule R M]
-  (n : ℕ) (b : M) : n • b = (n : R) • b :=
-begin
-  induction n with n ih,
-  { rw [nat.cast_zero, zero_smul, zero_smul] },
-  { change (n + 1) • b = (n + 1 : R) • b,
-    rw [add_smul, add_smul, one_smul, ih, one_smul] }
-end
-
-lemma semimodule.nsmul_eq_smul (R : Type*) [semiring R]
-  {M : Type*} [add_comm_monoid M] [semimodule R M] (n : ℕ) (b : M) :
-  n •ℕ b = (n : R) • b :=
-semimodule.smul_eq_smul R n b
-
-lemma nat.smul_def {M : Type*} [add_comm_monoid M] (n : ℕ) (x : M) :
-  n • x = n •ℕ x :=
-rfl
-
+local attribute [instance] add_comm_group.int_module
+/-- `gsmul` is defined as the `smul` action of `add_comm_group.int_module`. -/
+lemma gsmul_def (n : ℤ) (x : M) : gsmul n x = n • x := rfl
 end
 
-namespace nat
-
-variables [semiring R] [add_comm_monoid M] [semimodule R M] [semimodule ℕ M]
-
-instance smul_comm_class : smul_comm_class ℕ R M :=
-{ smul_comm := λ n r m, nat.rec_on n
-    (by simp only [zero_smul, smul_zero])
-    (λ n ih, by simp only [succ_eq_add_one, add_smul, one_smul, ←ih, smul_add]) }
-
--- `smul_comm_class.symm` is not registered as an instance, as it would cause a loop
-instance smul_comm_class' : smul_comm_class R ℕ M := smul_comm_class.symm _ _ _
-
-end nat
-
 section
-local attribute [instance] add_comm_group.int_module
-
-lemma gsmul_eq_smul {M : Type*} [add_comm_group M] (n : ℤ) (x : M) : gsmul n x = n • x := rfl
-
-lemma module.gsmul_eq_smul_cast (R : Type*) [ring R] {M : Type*} [add_comm_group M] [module R M]
-  (n : ℤ) (b : M) : gsmul n b = (n : R) • b :=
+variables (R)
+/-- `gsmul` is equal to any other module structure via a cast. -/
+lemma gsmul_eq_smul_cast (n : ℤ) (b : M) : gsmul n b = (n : R) • b :=
 begin
-  cases n,
-  { apply semimodule.nsmul_eq_smul, },
-  { dsimp,
-    rw semimodule.nsmul_eq_smul R,
-    push_cast,
-    rw neg_smul, }
+  rw gsmul_def,
+  induction n using int.induction_on with p hp n hn,
+  { rw [int.cast_zero, zero_smul, zero_smul] },
+  { rw [int.cast_add, int.cast_one, add_smul, add_smul, one_smul, one_smul, hp] },
+  { rw [int.cast_sub, int.cast_one, sub_smul, sub_smul, one_smul, one_smul, hn] },
 end
-
 end
 
-lemma module.gsmul_eq_smul {M : Type*} [add_comm_group M] [module ℤ M]
-  (n : ℤ) (b : M) : gsmul n b = n • b :=
-by rw [module.gsmul_eq_smul_cast ℤ, int.cast_id]
+/-- `gsmul` is equal to any `ℤ`-module structure. -/
+lemma gsmul_eq_smul [semimodule ℤ M] (n : ℤ) (b : M) : n •ℤ b = n • b :=
+by rw [gsmul_eq_smul_cast ℤ, n.cast_id]
 
-namespace int
+/-- All `ℤ`-module structures are equal. -/
+instance add_comm_group.int_module.subsingleton : subsingleton (semimodule ℤ M) :=
+⟨λ P Q, by {
+  ext n,
+  rw [←gsmul_eq_smul, ←gsmul_eq_smul], }⟩
 
-variables [semiring R] [add_comm_group M] [semimodule R M] [semimodule ℤ M]
+instance add_comm_group.int_is_scalar_tower [semimodule ℤ R] [semimodule ℤ M] :
+  is_scalar_tower ℤ R M :=
+{ smul_assoc := λ n x y, int.induction_on n
+    (by simp only [zero_smul])
+    (λ n ih, by simp only [one_smul, add_smul, ih])
+    (λ n ih, by simp only [one_smul, sub_smul, ih]) }
 
-instance smul_comm_class : smul_comm_class ℤ R M :=
+instance add_comm_group.int_smul_comm_class [semimodule ℤ M] : smul_comm_class ℤ S M :=
 { smul_comm := λ n x y, int.induction_on n
     (by simp only [zero_smul, smul_zero])
     (λ n ih, by simp only [one_smul, add_smul, smul_add, ih])
     (λ n ih, by simp only [one_smul, sub_smul, smul_sub, ih]) }
 
 -- `smul_comm_class.symm` is not registered as an instance, as it would cause a loop
-instance smul_comm_class' : smul_comm_class R ℤ M := smul_comm_class.symm _ _ _
+instance add_comm_group.int_smul_comm_class' [semimodule ℤ M] : smul_comm_class S ℤ M :=
+smul_comm_class.symm _ _ _
 
-end int
+end add_comm_group
 
 namespace add_monoid_hom
 
@@ -442,18 +402,18 @@ namespace add_monoid_hom
 lemma map_int_module_smul
   [add_comm_group M] [add_comm_group M₂]
   [module ℤ M] [module ℤ M₂] (f : M →+ M₂) (x : ℤ) (a : M) : f (x • a) = x • f a :=
-by simp only [← module.gsmul_eq_smul, f.map_gsmul]
+by simp only [←gsmul_eq_smul, f.map_gsmul]
 
 lemma map_int_cast_smul
   [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂]
   (f : M →+ M₂) (x : ℤ) (a : M) : f ((x : R) • a) = (x : R) • f a :=
-by simp only [← module.gsmul_eq_smul_cast, f.map_gsmul]
+by simp only [←gsmul_eq_smul_cast, f.map_gsmul]
 
 lemma map_nat_cast_smul
   [semiring R] [add_comm_monoid M] [add_comm_monoid M₂]
   [semimodule R M] [semimodule R M₂] (f : M →+ M₂) (x : ℕ) (a : M) :
   f ((x : R) • a) = (x : R) • f a :=
-by simp only [← semimodule.nsmul_eq_smul, f.map_nsmul]
+by simp only [←nsmul_eq_smul_cast, f.map_nsmul]
 
 lemma map_rat_cast_smul {R : Type*} [division_ring R] [char_zero R]
   {E : Type*} [add_comm_group E] [module R E] {F : Type*} [add_comm_group F] [module R F]
@@ -500,29 +460,33 @@ end
 
 end add_monoid_hom
 
--- We finally turn on these instances globally:
-attribute [instance] add_comm_monoid.nat_semimodule add_comm_group.int_module
-
 section module_division_ring
 /-! Some tests for the vanishing of elements in modules over division rings. -/
 
 variables (R) [division_ring R] [add_comm_group M] [module R M]
 
-lemma smul_nat_eq_zero [char_zero R] {v : M} {n : ℕ} :
+lemma smul_nat_eq_zero [semimodule ℕ M] [char_zero R] {v : M} {n : ℕ} :
   n • v = 0 ↔ n = 0 ∨ v = 0 :=
-by { rw [semimodule.smul_eq_smul R, smul_eq_zero], simp }
+by { rw [←nsmul_eq_smul, nsmul_eq_smul_cast R, smul_eq_zero], simp }
 
-lemma eq_zero_of_smul_two_eq_zero [char_zero R] {v : M} (hv : 2 • v = 0) : v = 0 :=
+lemma eq_zero_of_smul_two_eq_zero [semimodule ℕ M] [char_zero R] {v : M} (hv : 2 • v = 0) : v = 0 :=
 ((smul_nat_eq_zero R).mp hv).resolve_left (by norm_num)
 
 lemma eq_zero_of_eq_neg [char_zero R] {v : M} (hv : v = - v) : v = 0 :=
 begin
+  -- any semimodule will do
+  haveI : semimodule ℕ M := add_comm_monoid.nat_semimodule,
   refine eq_zero_of_smul_two_eq_zero R _,
+  rw ←nsmul_eq_smul,
   convert add_eq_zero_iff_eq_neg.mpr hv,
   abel
 end
 
 lemma ne_neg_of_ne_zero [char_zero R] {v : R} (hv : v ≠ 0) : v ≠ -v :=
-λ h, hv (eq_zero_of_eq_neg R h)
+λ h, have semimodule ℕ R := add_comm_monoid.nat_semimodule, by exactI hv (eq_zero_of_eq_neg R h)
 
 end module_division_ring
+
+-- We finally turn on these instances globally. By doing this here, we ensure that none of the
+-- lemmas about nat semimodules above are specific to these instances.
+attribute [instance] add_comm_monoid.nat_semimodule add_comm_group.int_module

src/linear_algebra/alternating.lean

@@ -408,7 +408,7 @@ lemma coe_alternatization [fintype ι] (a : alternating_map R M N' ι) :
   (↑a : multilinear_map R (λ ι, M) N').alternatization = nat.factorial (fintype.card ι) • a :=
 begin
   ext,
-  simp only [multilinear_map.alternatization_apply, map_perm, smul_smul, ←nat.smul_def, coe_mk,
+  simp only [multilinear_map.alternatization_apply, map_perm, smul_smul, nsmul_eq_smul, coe_mk,
     smul_apply, add_monoid_hom.coe_mk, finset.sum_const, coe_multilinear_map, one_smul,
     multilinear_map.dom_dom_congr_apply, int.units_coe_mul_self,
     finset.card_univ, fintype.card_perm],

src/number_theory/arithmetic_function.lean

@@ -833,7 +833,7 @@ begin
   apply forall_congr,
   intro a,
   apply imp_congr (iff.refl _) (eq.congr_left (sum_congr rfl (λ x hx, _))),
-  rw [← module.gsmul_eq_smul, gsmul_eq_mul],
+  rw [←gsmul_eq_smul, gsmul_eq_mul],
 end
 
 /-- Möbius inversion for functions to a `comm_group`. -/

src/representation_theory/maschke.lean

@@ -129,9 +129,7 @@ begin
     equivariant_of_linear_of_comm_apply, sum_of_conjugates],
   rw [linear_map.sum_apply],
   simp only [conjugate_i π i h],
-  rw [finset.sum_const, finset.card_univ,
-    @semimodule.nsmul_eq_smul k _
-      V _ _ (fintype.card G) v,
+  rw [finset.sum_const, finset.card_univ, nsmul_eq_smul_cast k,
     ←mul_smul, invertible.inv_of_mul_self, one_smul],
 end
 end