refactor(*): make vector_space an abbreviation for module (#1793)

* refactor(*): make vector_space an abbreviation for module

* Remove superfluous instances

* Fix build

* Add Note[vector space definition]

* Update src/algebra/module.lean

* Fix build (hopefully)

* Update src/measure_theory/bochner_integration.lean

Author: jcommelin

src/algebra/module.lean

@@ -358,12 +358,27 @@ end ideal
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
+
+/- Note[vector space definition]:
+Vector spaces are defined as an `abbreviation` for modules,
+if the base ring is a field.
+(A previous definition made `vector_space` a structure
+defined to be `module`.)
+This has as advantage that vector spaces are completely transparant
+for type class inference, which means that all instances for modules
+are immediately picked up for vector spaces as well.
+A cosmetic disadvantage is that one can not extend vector spaces an sich,
+in definitions such as `normed_space`.
+The solution is to extend `module` instead.
+-/
+
 /-- A vector space is the same as a module, except the scalar ring is actually
   a field. (This adds commutativity of the multiplication and existence of inverses.)
   This is the traditional generalization of spaces like `ℝ^n`, which have a natural
   addition operation and a way to multiply them by real numbers, but no multiplication
   operation between vectors. -/
-class vector_space (α : Type u) (β : Type v) [discrete_field α] [add_comm_group β] extends module α β
+abbreviation vector_space (α : Type u) (β : Type v) [discrete_field α] [add_comm_group β] :=
+module α β
 end prio
 
 instance discrete_field.to_vector_space {α : Type*} [discrete_field α] : vector_space α α :=

src/algebra/pi_instances.lean

@@ -83,8 +83,6 @@ variables {I f}
 
 instance module         (α) {r : ring α}           [∀ i, add_comm_group $ f i]  [∀ i, module α $ f i]         : module α (Π i : I, f i)       := {..pi.semimodule I f α}
 
-instance vector_space   (α) {r : discrete_field α} [∀ i, add_comm_group $ f i]  [∀ i, vector_space α $ f i]   : vector_space α (Π i : I, f i) := {..pi.module α}
-
 instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] : left_cancel_semigroup (Π i : I, f i) :=
 by pi_instance
 
@@ -354,9 +352,6 @@ instance {r : semiring α} [add_comm_monoid β] [add_comm_monoid γ]
 instance {r : ring α} [add_comm_group β] [add_comm_group γ]
   [module α β] [module α γ] : module α (β × γ) := {}
 
-instance {r : discrete_field α} [add_comm_group β] [add_comm_group γ]
-  [vector_space α β] [vector_space α γ] : vector_space α (β × γ) := {}
-
 section substructures
 variables (s : set α) (t : set β)
 

src/analysis/normed_space/basic.lean

@@ -555,10 +555,11 @@ section normed_space
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
+-- see Note[vector space definition] for why we extend `module`.
 /-- A normed space over a normed field is a vector space endowed with a norm which satisfies the
 equality `∥c • x∥ = ∥c∥ ∥x∥`. -/
 class normed_space (α : Type*) (β : Type*) [normed_field α] [normed_group β]
-  extends vector_space α β :=
+  extends module α β :=
 (norm_smul : ∀ (a:α) (b:β), norm (a • b) = has_norm.norm a * norm b)
 end prio
 
@@ -661,7 +662,7 @@ instance : normed_space α (E × F) :=
   add_smul := λ r x y, prod.ext (add_smul _ _ _) (add_smul _ _ _),
   smul_add := λ r x y, prod.ext (smul_add _ _ _) (smul_add _ _ _),
   ..prod.normed_group,
-  ..prod.vector_space }
+  ..prod.module }
 
 /-- The product of finitely many normed spaces is a normed space, with the sup norm. -/
 instance pi.normed_space {E : ι → Type*} [fintype ι] [∀i, normed_group (E i)]

src/analysis/normed_space/finite_dimension.lean

@@ -43,8 +43,8 @@ open_locale classical
 
 -- To get a reasonable compile time for `continuous_equiv_fun_basis`, typeclass inference needs
 -- to be guided.
-local attribute [instance, priority 10000] pi.module normed_space.to_vector_space
-  vector_space.to_module submodule.add_comm_group submodule.module
+local attribute [instance, priority 10000] pi.module normed_space.to_module
+  submodule.add_comm_group submodule.module
   linear_map.finite_dimensional_range Pi.complete nondiscrete_normed_field.to_normed_field
 
 set_option class.instance_max_depth 100

src/analysis/normed_space/real_inner_product.lean

@@ -58,11 +58,12 @@ export has_inner (inner)
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
+-- see Note[vector space definition] for why we extend `module`.
 /--
 An inner product space is a real vector space with an additional operation called inner product.
 Inner product spaces over complex vector space will be defined in another file.
 -/
-class inner_product_space (α : Type*) extends add_comm_group α, vector_space ℝ α, has_inner α :=
+class inner_product_space (α : Type*) extends add_comm_group α, module ℝ α, has_inner α :=
 (comm      : ∀ x y, inner x y = inner y x)
 (nonneg    : ∀ x, 0 ≤ inner x x)
 (definite  : ∀ x, inner x x = 0 → x = 0)

src/linear_algebra/basic.lean

@@ -834,9 +834,6 @@ module.of_core $ by refine {smul := (•), ..};
   repeat {rintro ⟨⟩ <|> intro}; simp [smul_add, add_smul, smul_smul,
     -mk_add, (mk_add p).symm, -mk_smul, (mk_smul p).symm]
 
-instance {K M} {R:discrete_field K} [add_comm_group M] [vector_space K M]
-  (p : submodule K M) : vector_space K (quotient p) := {}
-
 end quotient
 
 end submodule

src/measure_theory/bochner_integration.lean

@@ -122,7 +122,7 @@ set_option class.instance_max_depth 100
 -- Typeclass inference has difficulty finding `has_scalar ℝ β` where `β` is a `normed_space` on `ℝ`
 local attribute [instance, priority 10000]
   mul_action.to_has_scalar distrib_mul_action.to_mul_action add_comm_group.to_add_comm_monoid
-  normed_group.to_add_comm_group normed_space.to_vector_space vector_space.to_module
+  normed_group.to_add_comm_group normed_space.to_module
   module.to_semimodule
 
 namespace measure_theory

src/ring_theory/algebra.lean

@@ -103,11 +103,6 @@ by rw [smul_def, smul_def, left_comm]
   (r • x) * y = r • (x * y) :=
 by rw [smul_def, smul_def, mul_assoc]
 
-@[priority 100] -- see Note [lower instance priority]
-instance {F : Type u} {K : Type v} [discrete_field F] [ring K] [algebra F K] :
-  vector_space F K :=
-@vector_space.mk F _ _ _ algebra.to_module
-
 /-- R[X] is the generator of the category R-Alg. -/
 instance polynomial (R : Type u) [comm_ring R] : algebra R (polynomial R) :=
 { to_fun := polynomial.C,