refactor(*): rename semimodule to module, delete typeclasses `mod…

…ule` and `vector_space` (#7322)

Splitting typeclasses between `semimodule`, `module` and `vector_space` was causing many (small) issues, so why don't we just get rid of this duplication?

This PR contains the following changes:
 * delete the old `module` and `vector_space` synonyms for `semimodule`
 * find and replace all instances of `semimodule` and `vector_space` to `module`
 * (thereby renaming the previous `semimodule` typeclass to `module`)
 * rename `vector_space.dim` to `module.rank` (in preparation for generalizing this definition to all modules)
 * delete a couple `module` instances that have now become redundant

This find-and-replace has been done extremely naïvely, but it seems there were almost no name clashes and no "clbuttic mistakes". I have gone through the full set of changes, finding nothing weird, and I'm fixing any build issues as they come up (I expect less than 10 declarations will cause conflicts).

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring

A good example of a workaround required by the `module` abbreviation is the [`triv_sq_zero_ext.module` instance](https://github.com/leanprover-community/mathlib/blob/3b8cfdc905c663f3d99acac325c7dff1a0ce744c/src/algebra/triv_sq_zero_ext.lean#L164).



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

archive/sensitivity.lean

@@ -164,7 +164,7 @@ by { induction n ; { dunfold V, resetI, apply_instance } }
 instance : add_comm_group (V n) :=
 by { induction n ; { dunfold V, resetI, apply_instance } }
 
-instance : vector_space ℝ (V n) :=
+instance : module ℝ (V n) :=
 by { induction n ; { dunfold V, resetI, apply_instance } }
 end V
 
@@ -225,19 +225,19 @@ def dual_pair_e_ε (n : ℕ) : dual_pair (@e n) (@ε n) :=
   total := @epsilon_total _ }
 
 /-! We will now derive the dimension of `V`, first as a cardinal in `dim_V` and,
-since this cardinal is finite, as a natural number in `findim_V` -/
+since this cardinal is finite, as a natural number in `finrank_V` -/
 
-lemma dim_V : vector_space.dim ℝ (V n) = 2^n :=
-have vector_space.dim ℝ (V n) = (2^n : ℕ),
+lemma dim_V : module.rank ℝ (V n) = 2^n :=
+have module.rank ℝ (V n) = (2^n : ℕ),
   by { rw [dim_eq_card_basis (dual_pair_e_ε _).is_basis, Q.card]; apply_instance },
 by assumption_mod_cast
 
 instance : finite_dimensional ℝ (V n) :=
 finite_dimensional.of_fintype_basis (dual_pair_e_ε _).is_basis
 
-lemma findim_V : findim ℝ (V n) = 2^n :=
+lemma finrank_V : finrank ℝ (V n) = 2^n :=
 have _ := @dim_V n,
-by rw ←findim_eq_dim at this; assumption_mod_cast
+by rw ←finrank_eq_dim at this; assumption_mod_cast
 
 /-! ### The linear map -/
 
@@ -333,9 +333,9 @@ In this section, in order to enforce that `n` is positive, we write it as
 `m + 1` for some natural number `m`. -/
 
 /-! `dim X` will denote the dimension of a subspace `X` as a cardinal. -/
-notation `dim` X:70 := vector_space.dim ℝ ↥X
+notation `dim` X:70 := module.rank ℝ ↥X
 /-! `fdim X` will denote the (finite) dimension of a subspace `X` as a natural number. -/
-notation `fdim` := findim ℝ
+notation `fdim` := finrank ℝ
 
 /-! `Span S` will denote the ℝ-subspace spanned by `S`. -/
 notation `Span` := submodule.span ℝ
@@ -373,8 +373,8 @@ begin
     rw set.range_restrict at hdW,
     convert hdW,
     rw [cardinal.mk_image_eq (dual_pair_e_ε _).is_basis.injective, cardinal.fintype_card] },
-  rw ← findim_eq_dim ℝ at ⊢ dim_le dim_add dimW,
-  rw [← findim_eq_dim ℝ, ← findim_eq_dim ℝ] at dim_add,
+  rw ← finrank_eq_dim ℝ at ⊢ dim_le dim_add dimW,
+  rw [← finrank_eq_dim ℝ, ← finrank_eq_dim ℝ] at dim_add,
   norm_cast at ⊢ dim_le dim_add dimW,
   rw pow_succ' at dim_le,
   rw set.to_finset_card at hH,

docs/overview.yaml

@@ -134,7 +134,7 @@ Linear algebra:
     module: 'module'
     linear map: 'linear_map'
     the category of modules over a ring: 'Module'
-    vector space: 'vector_space'
+    vector space: 'module'
     quotient space: 'submodule.quotient'
     tensor product: 'tensor_product'
     noetherian module: 'is_noetherian'
@@ -148,7 +148,7 @@ Linear algebra:
   Finite-dimensional vector spaces:
     finite-dimensionality : 'finite_dimensional'
     isomorphism with $K^n$: 'module_equiv_finsupp'
-    isomorphism with bidual: 'vector_space.eval_equiv'
+    isomorphism with bidual: 'module.eval_equiv'
   Matrices:
     ring-valued matrix: 'matrix'
     matrix representation of a linear map: 'linear_map.to_matrix'

docs/undergrad.yaml

@@ -4,8 +4,8 @@
 # 1.
 Linear algebra:
   Fundamentals:
-    vector space: 'vector_space'
-    product of vector spaces: 'prod.semimodule'
+    vector space: 'module'
+    product of vector spaces: 'prod.module'
     vector subspace: 'subspace'
     quotient space: 'submodule.quotient'
     sum of subspaces: 'submodule.complete_lattice'
@@ -31,7 +31,7 @@ Linear algebra:
     rank of a linear map: 'rank'
     rank of a set of vectors: ''
     rank of a system of linear equations: ''
-    isomorphism with bidual: 'vector_space.eval_equiv'
+    isomorphism with bidual: 'module.eval_equiv'
   Multilinearity:
     multilinear map: 'multilinear_map'
     determinant of vectors: 'is_basis.det'

src/algebra/algebra/basic.lean

@@ -86,10 +86,10 @@ namespace algebra
 
 variables {R : Type u} {S : Type v} {A : Type w} {B : Type*}
 
-/-- Let `R` be a commutative semiring, let `A` be a semiring with a `semimodule R` structure.
+/-- Let `R` be a commutative semiring, let `A` be a semiring with a `module R` structure.
 If `(r • 1) * x = x * (r • 1) = r • x` for all `r : R` and `x : A`, then `A` is an `algebra`
 over `R`. -/
-def of_semimodule' [comm_semiring R] [semiring A] [semimodule R A]
+def of_module' [comm_semiring R] [semiring A] [module R A]
   (h₁ : ∀ (r : R) (x : A), (r • 1) * x = r • x)
   (h₂ : ∀ (r : R) (x : A), x * (r • 1) = r • x) : algebra R A :=
 { to_fun := λ r, r • 1,
@@ -100,13 +100,13 @@ def of_semimodule' [comm_semiring R] [semiring A] [semimodule R A]
   commutes' := λ r x, by simp only [h₁, h₂],
   smul_def' := λ r x, by simp only [h₁] }
 
-/-- Let `R` be a commutative semiring, let `A` be a semiring with a `semimodule R` structure.
+/-- Let `R` be a commutative semiring, let `A` be a semiring with a `module R` structure.
 If `(r • x) * y = x * (r • y) = r • (x * y)` for all `r : R` and `x y : A`, then `A`
 is an `algebra` over `R`. -/
-def of_semimodule [comm_semiring R] [semiring A] [semimodule R A]
+def of_module [comm_semiring R] [semiring A] [module R A]
   (h₁ : ∀ (r : R) (x y : A), (r • x) * y = r • (x * y))
   (h₂ : ∀ (r : R) (x y : A), x * (r • y) = r • (x * y)) : algebra R A :=
-of_semimodule' (λ r x, by rw [h₁, one_mul]) (λ r x, by rw [h₂, mul_one])
+of_module' (λ r x, by rw [h₁, one_mul]) (λ r x, by rw [h₂, mul_one])
 
 section semiring
 
@@ -140,7 +140,7 @@ begin
 end
 
 @[priority 200] -- see Note [lower instance priority]
-instance to_semimodule : semimodule R A :=
+instance to_module : module R A :=
 { one_smul := by simp [smul_def''],
   mul_smul := by simp [smul_def'', mul_assoc],
   smul_add := by simp [smul_def'', mul_add],
@@ -228,7 +228,7 @@ variables (R A B)
 instance : algebra R (A × B) :=
 { commutes' := by { rintro r ⟨a, b⟩, dsimp, rw [commutes r a, commutes r b] },
   smul_def' := by { rintro r ⟨a, b⟩, dsimp, rw [smul_def r a, smul_def r b] },
-  .. prod.semimodule,
+  .. prod.module,
   .. ring_hom.prod (algebra_map R A) (algebra_map R B) }
 
 variables {R A B}
@@ -308,7 +308,7 @@ variables (R)
 
 /-- A `semiring` that is an `algebra` over a commutative ring carries a natural `ring` structure. -/
 def semiring_to_ring [semiring A] [algebra R A] : ring A := {
-  ..semimodule.add_comm_monoid_to_add_comm_group R,
+  ..module.add_comm_monoid_to_add_comm_group R,
   ..(infer_instance : semiring A) }
 
 variables {R}
@@ -367,7 +367,7 @@ instance : algebra R Aᵒᵖ :=
 end opposite
 
 namespace module
-variables (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [semimodule R M]
+variables (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M]
 
 instance endomorphism_algebra : algebra R (M →ₗ[R] M) :=
 { to_fun    := λ r, r • linear_map.id,
@@ -385,7 +385,7 @@ lemma algebra_map_End_eq_smul_id (a : R) :
   (algebra_map R (End R M)) a m = a • m := rfl
 
 @[simp] lemma ker_algebra_map_End (K : Type u) (V : Type v)
-  [field K] [add_comm_group V] [vector_space K V] (a : K) (ha : a ≠ 0) :
+  [field K] [add_comm_group V] [module K V] (a : K) (ha : a ≠ 0) :
   ((algebra_map K (End K V)) a).ker = ⊥ :=
 linear_map.ker_smul _ _ ha
 
@@ -1223,9 +1223,9 @@ by { ext, simp only [lmul_right_apply, linear_map.comp_apply, mul_assoc] }
 @[simp] lemma lmul'_apply {x y : A} : lmul' R (x ⊗ₜ y) = x * y :=
 by simp only [algebra.lmul', tensor_product.lift.tmul, alg_hom.to_linear_map_apply, lmul_apply]
 
-instance linear_map.semimodule' (R : Type u) [comm_semiring R]
-  (M : Type v) [add_comm_monoid M] [semimodule R M]
-  (S : Type w) [comm_semiring S] [algebra R S] : semimodule S (M →ₗ[R] S) :=
+instance linear_map.module' (R : Type u) [comm_semiring R]
+  (M : Type v) [add_comm_monoid M] [module R M]
+  (S : Type w) [comm_semiring S] [algebra R S] : module S (M →ₗ[R] S) :=
 { smul := λ s f, linear_map.llcomp _ _ _ _ (algebra.lmul R S s) f,
   one_smul := λ f, linear_map.ext $ λ x, one_mul _,
   mul_smul := λ s₁ s₂ f, linear_map.ext $ λ x, mul_assoc _ _ _,
@@ -1319,8 +1319,8 @@ section is_scalar_tower
 
 variables {R : Type*} [comm_semiring R]
 variables (A : Type*) [semiring A] [algebra R A]
-variables {M : Type*} [add_comm_monoid M] [semimodule A M] [semimodule R M] [is_scalar_tower R A M]
-variables {N : Type*} [add_comm_monoid N] [semimodule A N] [semimodule R N] [is_scalar_tower R A N]
+variables {M : Type*} [add_comm_monoid M] [module A M] [module R M] [is_scalar_tower R A M]
+variables {N : Type*} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A N]
 
 lemma algebra_compatible_smul (r : R) (m : M) : r • m = ((algebra_map R A) r) • m :=
 by rw [←(one_smul A m), ←smul_assoc, algebra.smul_def, mul_one, one_smul]
@@ -1356,9 +1356,9 @@ variables (R) {A M N}
   ((f : M →ₗ[R] N) : M → N) = f := rfl
 
 /-- `A`-linearly coerce a `R`-linear map from `M` to `A` to a function, given an algebra `A` over
-a commutative semiring `R` and `M` a semimodule over `R`. -/
+a commutative semiring `R` and `M` a module over `R`. -/
 def lto_fun (R : Type u) (M : Type v) (A : Type w)
-  [comm_semiring R] [add_comm_monoid M] [semimodule R M] [comm_ring A] [algebra R A] :
+  [comm_semiring R] [add_comm_monoid M] [module R M] [comm_ring A] [algebra R A] :
   (M →ₗ[R] A) →ₗ[A] (M → A) :=
 { to_fun := linear_map.to_fun,
   map_add' := λ f g, rfl,
@@ -1392,20 +1392,20 @@ instance [I : add_comm_monoid M] : add_comm_monoid (restrict_scalars R A M) := I
 
 instance [I : add_comm_group M] : add_comm_group (restrict_scalars R A M) := I
 
-instance restrict_scalars.module_orig [semiring A] [add_comm_monoid M] [I : semimodule A M] :
-  semimodule A (restrict_scalars R A M) := I
+instance restrict_scalars.module_orig [semiring A] [add_comm_monoid M] [I : module A M] :
+  module A (restrict_scalars R A M) := I
 
 variables [comm_semiring R] [semiring A] [algebra R A]
-variables [add_comm_monoid M] [semimodule A M]
+variables [add_comm_monoid M] [module A M]
 
 /--
 When `M` is a module over a ring `A`, and `A` is an algebra over `R`, then `M` inherits a
 module structure over `R`.
 
 The preferred way of setting this up is `[module R M] [module A M] [is_scalar_tower R A M]`.
 -/
-instance : semimodule R (restrict_scalars R A M) :=
-semimodule.comp_hom M (algebra_map R A)
+instance : module R (restrict_scalars R A M) :=
+module.comp_hom M (algebra_map R A)
 
 lemma restrict_scalars_smul_def (c : R) (x : restrict_scalars R A M) :
   c • x = ((algebra_map R A c) • x : M) := rfl
@@ -1414,8 +1414,8 @@ instance : is_scalar_tower R A (restrict_scalars R A M) :=
 ⟨λ r A M, by { rw [algebra.smul_def, mul_smul], refl }⟩
 
 instance submodule.restricted_module (V : submodule A M) :
-  semimodule R V :=
-restrict_scalars.semimodule R A V
+  module R V :=
+restrict_scalars.module R A V
 
 instance submodule.restricted_module_is_scalar_tower (V : submodule A M) :
   is_scalar_tower R A V :=
@@ -1426,12 +1426,12 @@ end type_synonym
 /-! TODO: The following lemmas no longer involve `algebra` at all, and could be moved closer
 to `algebra/module/submodule.lean`. Currently this is tricky because `ker`, `range`, `⊤`, and `⊥`
 are all defined in `linear_algebra/basic.lean`. -/
-section semimodule
-open semimodule
+section module
+open module
 
 variables (R S M N : Type*) [semiring R] [semiring S] [has_scalar R S]
-variables [add_comm_monoid M] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
-variables [add_comm_monoid N] [semimodule R N] [semimodule S N] [is_scalar_tower R S N]
+variables [add_comm_monoid M] [module R M] [module S M] [is_scalar_tower R S M]
+variables [add_comm_monoid N] [module R N] [module S N] [is_scalar_tower R S N]
 
 variables {S M N}
 
@@ -1481,15 +1481,15 @@ lemma linear_map.ker_restrict_scalars (f : M →ₗ[S] N) :
   (f.restrict_scalars R).ker = f.ker.restrict_scalars R :=
 rfl
 
-end semimodule
+end module
 
 end restrict_scalars
 
 namespace submodule
 
 variables (R A M : Type*)
 variables [comm_semiring R] [semiring A] [algebra R A] [add_comm_monoid M]
-variables [semimodule R M] [semimodule A M] [is_scalar_tower R A M]
+variables [module R M] [module A M] [is_scalar_tower R A M]
 
 /-- If `A` is an `R`-algebra such that the induced morhpsim `R →+* A` is surjective, then the
 `R`-module generated by a set `X` equals the `A`-module generated by `X`. -/

src/algebra/algebra/operations.lean

@@ -248,7 +248,7 @@ instance : comm_semiring (submodule R A) :=
 variables (R A)
 
 /-- R-submodules of the R-algebra A are a module over `set A`. -/
-instance semimodule_set : semimodule (set_semiring A) (submodule R A) :=
+instance module_set : module (set_semiring A) (submodule R A) :=
 { smul := λ s P, span R s * P,
   smul_add := λ _ _ _, mul_add _ _ _,
   add_smul := λ s t P, show span R (s ⊔ t) * P = _, by { erw [span_union, right_distrib] },

src/algebra/algebra/ordered.lean

@@ -21,7 +21,7 @@ i.e. `A ≤ B` iff `B - A = star R * R` for some `R`.
 ## Implementation
 
 Because the axioms for an ordered algebra are exactly the same as those for the underlying
-module being ordered, we don't actually introduce a new class, but just use the `ordered_semimodule`
+module being ordered, we don't actually introduce a new class, but just use the `ordered_module`
 mixin.
 
 ## Tags
@@ -33,7 +33,7 @@ section ordered_algebra
 
 variables {R A : Type*} {a b : A} {r : R}
 
-variables [ordered_comm_ring R] [ordered_ring A] [algebra R A] [ordered_semimodule R A]
+variables [ordered_comm_ring R] [ordered_ring A] [algebra R A] [ordered_module R A]
 
 lemma algebra_map_monotone : monotone (algebra_map R A) :=
 λ a b h,
@@ -50,7 +50,7 @@ section instances
 
 variables {R : Type*} [linear_ordered_comm_ring R]
 
-instance linear_ordered_comm_ring.to_ordered_semimodule : ordered_semimodule R R :=
+instance linear_ordered_comm_ring.to_ordered_module : ordered_module R R :=
 { smul_lt_smul_of_pos       := ordered_semiring.mul_lt_mul_of_pos_left,
   lt_of_smul_lt_smul_of_pos := λ a b c w₁ w₂, (mul_lt_mul_left w₂).mp w₁ }
 

src/algebra/algebra/tower.lean

@@ -26,7 +26,7 @@ variables (R : Type u) (S : Type v) (A : Type w) (B : Type u₁) (M : Type v₁)
 namespace algebra
 
 variables [comm_semiring R] [semiring A] [algebra R A]
-variables [add_comm_monoid M] [semimodule R M] [semimodule A M] [is_scalar_tower R A M]
+variables [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M]
 
 variables {A}
 
@@ -53,16 +53,16 @@ end algebra
 
 namespace is_scalar_tower
 
-section semimodule
+section module
 
 variables [comm_semiring R] [semiring A] [algebra R A]
-variables [add_comm_monoid M] [semimodule R M] [semimodule A M] [is_scalar_tower R A M]
+variables [add_comm_monoid M] [module R M] [module A M] [is_scalar_tower R A M]
 
 variables {R} (A) {M}
 theorem algebra_map_smul (r : R) (x : M) : algebra_map R A r • x = r • x :=
 by rw [algebra.algebra_map_eq_smul_one, smul_assoc, one_smul]
 
-end semimodule
+end module
 
 section semiring
 variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B]
@@ -270,7 +270,7 @@ section semiring
 
 variables {R S A}
 variables [comm_semiring R] [semiring S] [add_comm_monoid A]
-variables [algebra R S] [semimodule S A] [semimodule R A] [is_scalar_tower R S A]
+variables [algebra R S] [module S A] [module R A] [is_scalar_tower R S A]
 
 namespace submodule
 
@@ -318,7 +318,7 @@ section ring
 namespace algebra
 
 variables [comm_semiring R] [ring A] [algebra R A]
-variables [add_comm_group M] [module A M] [semimodule R M] [is_scalar_tower R A M]
+variables [add_comm_group M] [module A M] [module R M] [is_scalar_tower R A M]
 
 lemma lsmul_injective [no_zero_smul_divisors A M] {x : A} (hx : x ≠ 0) :
   function.injective (lsmul R M x) :=

src/algebra/category/Module/limits.lean

@@ -49,19 +49,19 @@ def sections_submodule (F : J ⥤ Module R) :
   ..(AddGroup.sections_add_subgroup
           (F ⋙ forget₂ (Module R) AddCommGroup.{v} ⋙ forget₂ AddCommGroup AddGroup.{v})) }
 
+-- Adding the following instance speeds up `limit_module` noticeably,
+-- by preventing a bad unfold of `limit_add_comm_group`.
+instance limit_add_comm_monoid (F : J ⥤ Module R) :
+  add_comm_monoid (types.limit_cone (F ⋙ forget (Module.{v} R))).X :=
+show add_comm_monoid (sections_submodule F), by apply_instance
+
 instance limit_add_comm_group (F : J ⥤ Module R) :
   add_comm_group (types.limit_cone (F ⋙ forget (Module.{v} R))).X :=
-begin
-  change add_comm_group (sections_submodule F),
-  apply_instance,
-end
+show add_comm_group (sections_submodule F), by apply_instance
 
 instance limit_module (F : J ⥤ Module R) :
   module R (types.limit_cone (F ⋙ forget (Module.{v} R))).X :=
-begin
-  change module R (sections_submodule F),
-  apply_instance,
-end
+show module R (sections_submodule F), by apply_instance
 
 /-- `limit.π (F ⋙ forget Ring) j` as a `ring_hom`. -/
 def limit_π_linear_map (F : J ⥤ Module R) (j) :