refactor(*): fix field names in linear_map and submodule (#3032)

* `linear_map` now uses `map_add'` and `map_smul`';
* `submodule` now `extends add_submonoid` and adds `smul_mem'`;
* no more `submodule.is_add_subgroup` instance;
* `open_subgroup` now uses bundled subgroups;
* `is_linear_map` is not a `class` anymore: we had a couple of
  `instances` but zero lemmas taking it as a typeclass argument;
* `subgroup.mem_coe` now takes `{g : G}` as it should, not `[g : G]`.

Author: urkud

src/algebra/category/Group/Z_Module_equivalence.lean

@@ -20,9 +20,10 @@ open category_theory.equivalence
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is full. -/
 instance : full (forget₂ (Module ℤ) AddCommGroup) :=
 { preimage := λ A B f,
+  -- TODO: why `add_monoid_hom.to_int_linear_map` doesn't work here?
   { to_fun := f,
-    add := λ x y, add_monoid_hom.map_add f x y,
-    smul := λ n x, by convert add_monoid_hom.map_int_module_smul f n x } }
+    map_add' := add_monoid_hom.map_add f,
+    map_smul' := λ n x, by convert add_monoid_hom.map_int_module_smul f n x } }
 
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
 instance : ess_surj (forget₂ (Module ℤ) AddCommGroup) :=

src/algebra/category/Module/basic.lean

@@ -81,9 +81,6 @@ variables {R} {M N U : Module R}
 @[simp] lemma coe_comp (f : M ⟶ N) (g : N ⟶ U) :
   ((f ≫ g) : M → U) = g ∘ f := rfl
 
-instance hom_is_module_hom (f : M ⟶ N) :
-  is_linear_map R (f : M → N) := linear_map.is_linear _
-
 end Module
 
 variables {R}
@@ -108,8 +105,8 @@ def to_linear_equiv {X Y : Module.{u} R} (i : X ≅ Y) : X ≃ₗ[R] Y :=
   inv_fun   := i.inv,
   left_inv  := by tidy,
   right_inv := by tidy,
-  add       := by tidy,
-  smul      := by tidy, }.
+  map_add'  := by tidy,
+  map_smul' := by tidy, }.
 
 end category_theory.iso
 

src/algebra/lie_algebra.lean

@@ -354,14 +354,14 @@ lemma endo_algebra_bracket (M : Type v) [add_comm_group M] [module R M] (f g : m
 /--
 The adjoint action of a Lie algebra on itself.
 -/
-def Ad : L →ₗ⁅R⁆ module.End R L := {
-  to_fun  := λ x, {
-    to_fun := has_bracket.bracket x,
-    add    := by { intros, apply lie_add, },
-    smul   := by { intros, apply lie_smul, } },
-  add     := by { intros, ext, simp, },
-  smul    := by { intros, ext, simp, },
-  map_lie := by {
+def Ad : L →ₗ⁅R⁆ module.End R L :=
+{ to_fun    := λ x,
+  { to_fun    := has_bracket.bracket x,
+    map_add'  := by { intros, apply lie_add, },
+    map_smul' := by { intros, apply lie_smul, } },
+  map_add'  := by { intros, ext, simp, },
+  map_smul' := by { intros, ext, simp, },
+  map_lie   := by {
     intros x y, ext z,
     rw endo_algebra_bracket,
     suffices : ⁅⁅x, y⁆, z⁆ = ⁅x, ⁅y, z⁆⁆ + ⁅⁅x, z⁆, y⁆, by simpa [sub_eq_add_neg],

src/algebra/module.lean

@@ -223,11 +223,11 @@ def ring_hom.to_semimodule [semiring R] [semiring S] (f : R →+* S) : semimodul
 `f (x + y) = f x + f y` and `f (c • x) = c • f x`. The predicate `is_linear_map R f` asserts this
 property. A bundled version is available with `linear_map`, and should be favored over
 `is_linear_map` most of the time. -/
-class is_linear_map (R : Type u) {M : Type v} {M₂ : Type w}
+structure is_linear_map (R : Type u) {M : Type v} {M₂ : Type w}
   [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂]
   (f : M → M₂) : Prop :=
-(add [] : ∀ x y, f (x + y) = f x + f y)
-(smul [] : ∀ (c : R) x, f (c • x) = c • f x)
+(map_add : ∀ x y, f (x + y) = f x + f y)
+(map_smul : ∀ (c : R) x, f (c • x) = c • f x)
 
 /-- A map `f` between semimodules over a semiring is linear if it satisfies the two properties
 `f (x + y) = f x + f y` and `f (c • x) = c • f x`. Elements of `linear_map R M M₂` (available under
@@ -236,8 +236,8 @@ the predicate `is_linear_map`, but it should be avoided most of the time. -/
 structure linear_map (R : Type u) (M : Type v) (M₂ : Type w)
   [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] :=
 (to_fun : M → M₂)
-(add  : ∀x y, to_fun (x + y) = to_fun x + to_fun y)
-(smul : ∀(c : R) x, to_fun (c • x) = c • to_fun x)
+(map_add'  : ∀x y, to_fun (x + y) = to_fun x + to_fun y)
+(map_smul' : ∀(c : R) x, to_fun (c • x) = c • to_fun x)
 
 infixr ` →ₗ `:25 := linear_map _
 notation M ` →ₗ[`:25 R:25 `] `:0 M₂:0 := linear_map R M M₂
@@ -274,7 +274,7 @@ variables (f g : M →ₗ[R] M₂)
 
 @[simp] lemma to_fun_eq_coe : f.to_fun = ⇑f := rfl
 
-theorem is_linear : is_linear_map R f := {..f}
+theorem is_linear : is_linear_map R f := ⟨f.2, f.3⟩
 
 variables {f g}
 @[ext] theorem ext (H : ∀ x, f x = g x) : f = g :=
@@ -288,9 +288,9 @@ theorem ext_iff : f = g ↔ ∀ x, f x = g x :=
 
 variables (f g)
 
-@[simp] lemma map_add (x y : M) : f (x + y) = f x + f y := f.add x y
+@[simp] lemma map_add (x y : M) : f (x + y) = f x + f y := f.map_add' x y
 
-@[simp] lemma map_smul (c : R) (x : M) : f (c • x) = c • f x := f.smul c x
+@[simp] lemma map_smul (c : R) (x : M) : f (c • x) = c • f x := f.map_smul' c x
 
 @[simp] lemma map_zero : f 0 = 0 :=
 by rw [← zero_smul R, map_smul f 0 0, zero_smul]
@@ -356,7 +356,7 @@ variables [semimodule R M] [semimodule R M₂]
 include R
 
 /-- Convert an `is_linear_map` predicate to a `linear_map` -/
-def mk' (f : M → M₂) (H : is_linear_map R f) : M →ₗ M₂ := {to_fun := f, ..H}
+def mk' (f : M → M₂) (H : is_linear_map R f) : M →ₗ M₂ := ⟨f, H.1, H.2⟩
 
 @[simp] theorem mk'_apply {f : M → M₂} (H : is_linear_map R f) (x : M) :
   mk' f H x = f x := rfl
@@ -379,10 +379,6 @@ include M M₂ lin
 
 lemma map_zero : f (0 : M) = (0 : M₂) := (lin.mk' f).map_zero
 
-lemma map_add : ∀ x y, f (x + y) = f x + f y := lin.add
-
-lemma map_smul (c : R) (x : M) : f (c • x) = c • f x := (lin.mk' f).map_smul c x
-
 end add_comm_monoid
 
 section add_comm_group
@@ -410,35 +406,53 @@ end is_linear_map
 abbreviation module.End (R : Type u) (M : Type v)
   [semiring R] [add_comm_monoid M] [semimodule R M] := M →ₗ[R] M
 
+set_option old_structure_cmd true
+
 /-- A submodule of a module is one which is closed under vector operations.
   This is a sufficient condition for the subset of vectors in the submodule
   to themselves form a module. -/
 structure submodule (R : Type u) (M : Type v) [semiring R]
-  [add_comm_monoid M] [semimodule R M] : Type v :=
-(carrier : set M)
-(zero : (0:M) ∈ carrier)
-(add : ∀ {x y}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier)
-(smul : ∀ (c:R) {x}, x ∈ carrier → c • x ∈ carrier)
+  [add_comm_monoid M] [semimodule R M] extends add_submonoid M : Type v :=
+(smul_mem' : ∀ (c:R) {x}, x ∈ carrier → c • x ∈ carrier)
+
+/-- Reinterpret a `submodule` as an `add_submonoid`. -/
+add_decl_doc submodule.to_add_submonoid
 
 namespace submodule
 
 variables [semiring R] [add_comm_monoid M] [semimodule R M]
 
-instance : has_coe (submodule R M) (set M) := ⟨submodule.carrier⟩
+instance : has_coe_t (submodule R M) (set M) := ⟨λ s, s.carrier⟩
 instance : has_mem M (submodule R M) := ⟨λ x p, x ∈ (p : set M)⟩
 instance : has_coe_to_sort (submodule R M) := ⟨_, λ p, {x : M // x ∈ p}⟩
 
-end submodule
+variables (p q : submodule R M)
+
+@[simp, norm_cast] theorem coe_sort_coe : ↥(p : set M) = p := rfl
+
+variables {p q}
+
+protected theorem «exists» {q : p → Prop} : (∃ x, q x) ↔ (∃ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.exists
+
+protected theorem «forall» {q : p → Prop} : (∀ x, q x) ↔ (∀ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.forall
+
+theorem ext' : injective (coe : submodule R M → set M) :=
+λ p q h, by cases p; cases q; congr'
+
+@[simp, norm_cast] theorem coe_set_eq : (p : set M) = q ↔ p = q := ext'.eq_iff
+
+theorem ext'_iff : p = q ↔ (p : set M) = q := coe_set_eq.symm
 
-protected theorem submodule.exists [semiring R] [add_comm_monoid M] [semimodule R M] {p : submodule R M}
-  {q : p → Prop} :
-  (∃ x, q x) ↔ (∃ x (hx : x ∈ p), q ⟨x, hx⟩) :=
-set_coe.exists
+@[ext] theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := ext' $ set.ext h
 
-protected theorem submodule.forall [semiring R] [add_comm_monoid M] [semimodule R M] {p : submodule R M}
-  {q : p → Prop} :
-  (∀ x, q x) ↔ (∀ x (hx : x ∈ p), q ⟨x, hx⟩) :=
-set_coe.forall
+theorem to_add_submonoid_injective :
+  injective (to_add_submonoid : submodule R M → add_submonoid M) :=
+λ p q h, ext'_iff.2 $ add_submonoid.ext'_iff.1 h
+
+@[simp] theorem to_add_submonoid_eq : p.to_add_submonoid = q.to_add_submonoid ↔ p = q :=
+to_add_submonoid_injective.eq_iff
+
+end submodule
 
 namespace submodule
 
@@ -452,30 +466,17 @@ variables {semimodule_M : semimodule R M}
 variables {p q : submodule R M}
 variables {r : R} {x y : M}
 
-theorem ext' (h : (p : set M) = q) : p = q :=
-by cases p; cases q; congr'
-
-protected theorem ext'_iff : (p : set M) = q ↔ p = q :=
-⟨ext', λ h, h ▸ rfl⟩
-
-@[ext] theorem ext
-  (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := ext' $ set.ext h
-
 variables (p)
 @[simp] theorem mem_coe : x ∈ (p : set M) ↔ x ∈ p := iff.rfl
 
-@[simp] lemma zero_mem : (0 : M) ∈ p := p.zero
+@[simp] lemma zero_mem : (0 : M) ∈ p := p.zero_mem'
 
-lemma add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p := p.add h₁ h₂
+lemma add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p := p.add_mem' h₁ h₂
 
-lemma smul_mem (r : R) (h : x ∈ p) : r • x ∈ p := p.smul r h
+lemma smul_mem (r : R) (h : x ∈ p) : r • x ∈ p := p.smul_mem' r h
 
-lemma sum_mem {t : finset ι} {f : ι → M} :
-  (∀c∈t, f c ∈ p) → (∑ i in t, f i) ∈ p :=
-begin
-  classical,
-  exact finset.induction_on t (by simp [p.zero_mem]) (by simp [p.add_mem] {contextual := tt})
-end
+lemma sum_mem {t : finset ι} {f : ι → M} : (∀c∈t, f c ∈ p) → (∑ i in t, f i) ∈ p :=
+p.to_add_submonoid.sum_mem
 
 @[simp] lemma smul_mem_iff' (u : units R) : (u:R) • x ∈ p ↔ x ∈ p :=
 ⟨λ h, by simpa only [smul_smul, u.inv_mul, one_smul] using p.smul_mem ↑u⁻¹ h, p.smul_mem u⟩
@@ -501,8 +502,7 @@ variables {p}
 variables (p)
 
 instance : add_comm_monoid p :=
-by refine {add := (+), zero := 0, ..};
-  { intros, apply set_coe.ext, simp [add_comm, add_left_comm] }
+{ add := (+), zero := 0, .. p.to_add_submonoid.to_add_comm_monoid }
 
 instance : semimodule R p :=
 by refine {smul := (•), ..};
@@ -527,10 +527,15 @@ variables {r : R} {x y : M}
 
 lemma neg_mem (hx : x ∈ p) : -x ∈ p := by rw ← neg_one_smul R; exact p.smul_mem _ hx
 
+/-- Reinterpret a submodule as an additive subgroup. -/
+def to_add_subgroup : add_subgroup M :=
+{ neg_mem' := λ _, p.neg_mem , .. p.to_add_submonoid }
+
+@[simp] lemma coe_to_add_subgroup : (p.to_add_subgroup : set M) = p := rfl
+
 lemma sub_mem (hx : x ∈ p) (hy : y ∈ p) : x - y ∈ p := p.add_mem hx (p.neg_mem hy)
 
-lemma neg_mem_iff : -x ∈ p ↔ x ∈ p :=
-⟨λ h, by simpa using neg_mem p h, neg_mem p⟩
+@[simp] lemma neg_mem_iff : -x ∈ p ↔ x ∈ p := p.to_add_subgroup.neg_mem_iff
 
 lemma add_mem_iff_left (h₁ : y ∈ p) : x + y ∈ p ↔ x ∈ p :=
 ⟨λ h₂, by simpa using sub_mem _ h₂ h₁, λ h₂, add_mem _ h₂ h₁⟩
@@ -543,13 +548,7 @@ instance : has_neg p := ⟨λx, ⟨-x.1, neg_mem _ x.2⟩⟩
 @[simp, norm_cast] lemma coe_neg (x : p) : ((-x : p) : M) = -x := rfl
 
 instance : add_comm_group p :=
-by refine {add := (+), zero := 0, neg := has_neg.neg, ..};
-  { intros, apply set_coe.ext, simp [add_comm, add_left_comm] }
-
-instance submodule_is_add_subgroup : is_add_subgroup (p : set M) :=
-{ zero_mem := p.zero,
-  add_mem  := p.add,
-  neg_mem  := λ _, p.neg_mem }
+{ add := (+), zero := 0, neg := has_neg.neg, ..p.to_add_subgroup.to_add_comm_group }
 
 @[simp, norm_cast] lemma coe_sub (x y : p) : (↑(x - y) : M) = ↑x - ↑y := rfl
 

src/analysis/analytic/composition.lean

@@ -143,9 +143,11 @@ multilinear map, called `q.comp_along_composition p c` below. -/
 def comp_along_composition_multilinear {n : ℕ}
   (q : formal_multilinear_series 𝕜 F G) (p : formal_multilinear_series 𝕜 E F)
   (c : composition n) : multilinear_map 𝕜 (λ i : fin n, E) G :=
-{ to_fun := λ v, q c.length (p.apply_composition c v),
-  add    := λ v i x y, by simp only [apply_composition_update, continuous_multilinear_map.map_add],
-  smul   := λ v i c x, by simp only [apply_composition_update, continuous_multilinear_map.map_smul] }
+{ to_fun    := λ v, q c.length (p.apply_composition c v),
+  map_add'  := λ v i x y, by simp only [apply_composition_update,
+    continuous_multilinear_map.map_add],
+  map_smul' := λ v i c x, by simp only [apply_composition_update,
+    continuous_multilinear_map.map_smul] }
 
 /-- The norm of `q.comp_along_composition_multilinear p c` is controlled by the product of
 the norms of the relevant bits of `q` and `p`. -/

src/analysis/complex/basic.lean

@@ -82,8 +82,8 @@ attribute [instance, priority 900] complex.normed_space.restrict_scalars_real
 /-- Linear map version of the real part function, from `ℂ` to `ℝ`. -/
 def linear_map.re : ℂ →ₗ[ℝ] ℝ :=
 { to_fun := λx, x.re,
-  add := by simp,
-  smul := λc x, by { change ((c : ℂ) * x).re = c * x.re, simp } }
+  map_add' := by simp,
+  map_smul' := λc x, by { change ((c : ℂ) * x).re = c * x.re, simp } }
 
 @[simp] lemma linear_map.re_apply (z : ℂ) : linear_map.re z = z.re := rfl
 
@@ -112,8 +112,8 @@ end
 /-- Linear map version of the imaginary part function, from `ℂ` to `ℝ`. -/
 def linear_map.im : ℂ →ₗ[ℝ] ℝ :=
 { to_fun := λx, x.im,
-  add := by simp,
-  smul := λc x, by { change ((c : ℂ) * x).im = c * x.im, simp } }
+  map_add' := by simp,
+  map_smul' := λc x, by { change ((c : ℂ) * x).im = c * x.im, simp } }
 
 @[simp] lemma linear_map.im_apply (z : ℂ) : linear_map.im z = z.im := rfl
 
@@ -143,8 +143,8 @@ end
 /-- Linear map version of the canonical embedding of `ℝ` in `ℂ`. -/
 def linear_map.of_real : ℝ →ₗ[ℝ] ℂ :=
 { to_fun := λx, of_real x,
-  add := by simp,
-  smul := λc x, by { simp, refl } }
+  map_add' := by simp,
+  map_smul' := λc x, by { simp, refl } }
 
 @[simp] lemma linear_map.of_real_apply (x : ℝ) : linear_map.of_real x = x := rfl
 

src/analysis/convex/basic.lean

@@ -209,7 +209,7 @@ lemma convex.is_linear_image (hs : convex s) {f : E → F} (hf : is_linear_map 
   convex (f '' s) :=
 begin
   rintros _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩ a b ha hb hab,
-  exact ⟨a • x + b • y, hs hx hy ha hb hab, by simp only [hf.add,hf.smul]⟩
+  exact ⟨a • x + b • y, hs hx hy ha hb hab, by simp only [hf.map_add,hf.map_smul]⟩
 end
 
 lemma convex.linear_image (hs : convex s) (f : E →ₗ[ℝ] F) : convex (image f s) :=
@@ -220,7 +220,7 @@ lemma convex.is_linear_preimage {s : set F} (hs : convex s) {f : E → F} (hf :
 begin
   intros x y hx hy a b ha hb hab,
   convert hs hx hy ha hb hab,
-  simp only [mem_preimage, hf.add, hf.smul]
+  simp only [mem_preimage, hf.map_add, hf.map_smul]
 end
 
 lemma convex.linear_preimage {s : set F} (hs : convex s) (f : E →ₗ[ℝ] F) :

src/analysis/normed_space/bounded_linear_maps.lean

@@ -38,7 +38,7 @@ lemma is_linear_map.with_bound
 /-- A continuous linear map satisfies `is_bounded_linear_map` -/
 lemma continuous_linear_map.is_bounded_linear_map (f : E →L[𝕜] F) : is_bounded_linear_map 𝕜 f :=
 { bound := f.bound,
-  ..f.to_linear_map }
+  ..f.to_linear_map.is_linear }
 
 namespace is_bounded_linear_map
 
@@ -165,8 +165,8 @@ lemma is_bounded_linear_map_prod_multilinear
   {E : ι → Type*} [∀i, normed_group (E i)] [∀i, normed_space 𝕜 (E i)] :
   is_bounded_linear_map 𝕜
   (λ p : (continuous_multilinear_map 𝕜 E F) × (continuous_multilinear_map 𝕜 E G), p.1.prod p.2) :=
-{ add := λ p₁ p₂, by { ext1 m, refl },
-  smul := λ c p, by { ext1 m, refl },
+{ map_add := λ p₁ p₂, by { ext1 m, refl },
+  map_smul := λ c p, by { ext1 m, refl },
   bound := ⟨1, zero_lt_one, λ p, begin
     rw one_mul,
     apply continuous_multilinear_map.op_norm_le_bound _ (norm_nonneg _) (λ m, _),
@@ -244,9 +244,9 @@ calc f (x, y - z) = f (x, y + (-1 : 𝕜) • z) : by simp [sub_eq_add_neg]
 
 lemma is_bounded_bilinear_map.is_bounded_linear_map_left (h : is_bounded_bilinear_map 𝕜 f) (y : F) :
   is_bounded_linear_map 𝕜 (λ x, f (x, y)) :=
-{ add   := λ x x', h.add_left _ _ _,
-  smul  := λ c x, h.smul_left _ _ _,
-  bound := begin
+{ map_add  := λ x x', h.add_left _ _ _,
+  map_smul := λ c x, h.smul_left _ _ _,
+  bound    := begin
     rcases h.bound with ⟨C, C_pos, hC⟩,
     refine ⟨C * (∥y∥ + 1), mul_pos C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ x, _⟩,
     have : ∥y∥ ≤ ∥y∥ + 1, by simp [zero_le_one],
@@ -258,9 +258,9 @@ lemma is_bounded_bilinear_map.is_bounded_linear_map_left (h : is_bounded_bilinea
 
 lemma is_bounded_bilinear_map.is_bounded_linear_map_right (h : is_bounded_bilinear_map 𝕜 f) (x : E) :
   is_bounded_linear_map 𝕜 (λ y, f (x, y)) :=
-{ add   := λ y y', h.add_right _ _ _,
-  smul  := λ c y, h.smul_right _ _ _,
-  bound := begin
+{ map_add  := λ y y', h.add_right _ _ _,
+  map_smul := λ c y, h.smul_right _ _ _,
+  bound    := begin
     rcases h.bound with ⟨C, C_pos, hC⟩,
     refine ⟨C * (∥x∥ + 1), mul_pos C_pos (lt_of_lt_of_le (zero_lt_one) (by simp)), λ y, _⟩,
     have : ∥x∥ ≤ ∥x∥ + 1, by simp [zero_le_one],
@@ -357,12 +357,12 @@ is indeed the derivative of `f` is proved in `is_bounded_bilinear_map.has_fderiv
 def is_bounded_bilinear_map.linear_deriv (h : is_bounded_bilinear_map 𝕜 f) (p : E × F) :
   (E × F) →ₗ[𝕜] G :=
 { to_fun := λq, f (p.1, q.2) + f (q.1, p.2),
-  add := λq₁ q₂, begin
+  map_add' := λq₁ q₂, begin
     change f (p.1, q₁.2 + q₂.2) + f (q₁.1 + q₂.1, p.2) =
       f (p.1, q₁.2) + f (q₁.1, p.2) + (f (p.1, q₂.2) + f (q₂.1, p.2)),
     simp [h.add_left, h.add_right], abel
   end,
-  smul := λc q, begin
+  map_smul' := λc q, begin
     change f (p.1, c • q.2) + f (c • q.1, p.2) = c • (f (p.1, q.2) + f (q.1, p.2)),
     simp [h.smul_left, h.smul_right, smul_add]
   end }