rfc(*): proposed refactor of (semi)module and linear_map

src/algebra/module.lean

@@ -109,13 +109,13 @@ instance ring.to_module [r : ring α] : module α α :=
 { ..semiring.to_semimodule }
 
 class is_linear_map (α : Type u) {β : Type v} {γ : Type w}
-  [ring α] [add_comm_group β] [add_comm_group γ] [module α β] [module α γ]
+  [semiring α] [add_comm_monoid β] [add_comm_monoid γ] [semimodule α β] [semimodule α γ]
   (f : β → γ) : Prop :=
 (add  : ∀x y, f (x + y) = f x + f y)
 (smul : ∀(c : α) x, f (c • x) = c • f x)
 
 structure linear_map (α : Type u) (β : Type v) (γ : Type w)
-  [ring α] [add_comm_group β] [add_comm_group γ] [module α β] [module α γ] :=
+  [semiring α] [add_comm_monoid β] [add_comm_monoid γ] [semimodule α β] [semimodule α γ] :=
 (to_fun : β → γ)
 (add  : ∀x y, to_fun (x + y) = to_fun x + to_fun y)
 (smul : ∀(c : α) x, to_fun (c • x) = c • to_fun x)
@@ -125,8 +125,10 @@ notation β ` →ₗ[`:25 α `] ` γ := linear_map α β γ
 
 namespace linear_map
 
-variables [ring α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
-variables [module α β] [module α γ] [module α δ]
+section semimodule
+
+variables [semiring α] [add_comm_monoid β] [add_comm_monoid γ] [add_comm_monoid δ]
+variables [semimodule α β] [semimodule α γ] [semimodule α δ]
 variables (f g : β →ₗ[α] γ)
 include α
 
@@ -147,13 +149,9 @@ theorem ext_iff {f g : β →ₗ[α] γ} : f = g ↔ ∀ x, f x = g x :=
 @[simp] lemma map_zero : f 0 = 0 :=
 by rw [← zero_smul α, map_smul f 0 0, zero_smul]
 
-instance : is_add_group_hom f := ⟨map_add f⟩
-
-@[simp] lemma map_neg (x : β) : f (- x) = - f x :=
-by rw [← neg_one_smul α, map_smul, neg_one_smul]
-
-@[simp] lemma map_sub (x y : β) : f (x - y) = f x - f y :=
-by simp [map_neg, map_add]
+instance : is_add_monoid_hom f :=
+{ map_zero := by rw [← zero_smul α (0 : β), f.map_smul, zero_smul],
+  map_add := map_add f }
 
 @[simp] lemma map_sum {ι} {t : finset ι} {g : ι → β} :
   f (t.sum g) = t.sum (λi, f (g i)) :=
@@ -167,11 +165,29 @@ def id : β →ₗ[α] β := ⟨id, by simp, by simp⟩
 
 @[simp] lemma id_apply (x : β) : @id α β _ _ _ x = x := rfl
 
+end semimodule
+
+section module
+variables [ring α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
+variables [module α β] [module α γ] [module α δ]
+variables (f g : β →ₗ[α] γ)
+include α
+
+instance : is_add_group_hom f := ⟨map_add f⟩
+
+@[simp] lemma map_neg (x : β) : f (- x) = - f x :=
+by rw [← neg_one_smul α, map_smul, neg_one_smul]
+
+@[simp] lemma map_sub (x y : β) : f (x - y) = f x - f y :=
+by simp [map_neg, map_add]
+
+end module
+
 end linear_map
 
 namespace is_linear_map
-variables [ring α] [add_comm_group β] [add_comm_group γ]
-variables [module α β] [module α γ]
+variables [semiring α] [add_comm_monoid β] [add_comm_monoid γ]
+variables [semimodule α β] [semimodule α γ]
 include α
 
 def mk' (f : β → γ) (H : is_linear_map α f) : β →ₗ γ := {to_fun := f, ..H}
@@ -181,33 +197,33 @@ def mk' (f : β → γ) (H : is_linear_map α f) : β →ₗ γ := {to_fun := f,
 
 end is_linear_map
 
-/-- 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 (α : Type u) (β : Type v) [ring α]
-  [add_comm_group β] [module α β] : Type v :=
+/-- A subsmimodule of a semimodule is one which is closed under vector operations.
+  This is a sufficient condition for the subset of vectors in the subsemimodule
+  to themselves form a semimodule. -/
+structure subsemimodule (α : Type u) (β : Type v) [semiring α]
+  [add_comm_monoid β] [semimodule α β] : Type v :=
 (carrier : set β)
 (zero : (0:β) ∈ carrier)
 (add : ∀ {x y}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier)
 (smul : ∀ (c:α) {x}, x ∈ carrier → c • x ∈ carrier)
 
-namespace submodule
-variables [ring α] [add_comm_group β] [add_comm_group γ]
-variables [module α β] [module α γ]
-variables (p p' : submodule α β)
+namespace subsemimodule
+variables [semiring α] [add_comm_monoid β] [add_comm_monoid γ]
+variables [semimodule α β] [semimodule α γ]
+variables (p p' : subsemimodule α β)
 variables {r : α} {x y : β}
 
-instance : has_coe (submodule α β) (set β) := ⟨submodule.carrier⟩
-instance : has_mem β (submodule α β) := ⟨λ x p, x ∈ (p : set β)⟩
+instance : has_coe (subsemimodule α β) (set β) := ⟨subsemimodule.carrier⟩
+instance : has_mem β (subsemimodule α β) := ⟨λ x p, x ∈ (p : set β)⟩
 @[simp] theorem mem_coe : x ∈ (p : set β) ↔ x ∈ p := iff.rfl
 
-theorem ext' {s t : submodule α β} (h : (s : set β) = t) : s = t :=
+theorem ext' {s t : subsemimodule α β} (h : (s : set β) = t) : s = t :=
 by cases s; cases t; congr'
 
-protected theorem ext'_iff {s t : submodule α β}  : (s : set β) = t ↔ s = t :=
+protected theorem ext'_iff {s t : subsemimodule α β}  : (s : set β) = t ↔ s = t :=
 ⟨ext', λ h, h ▸ rfl⟩
 
-@[extensionality] theorem ext {s t : submodule α β}
+@[extensionality] theorem ext {s t : subsemimodule α β}
   (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t := ext' $ set.ext h
 
 @[simp] lemma zero_mem : (0 : β) ∈ p := p.zero
@@ -216,6 +232,59 @@ lemma add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p := p.add h₁ h₂
 
 lemma smul_mem (r : α) (h : x ∈ p) : r • x ∈ p := p.smul r h
 
+lemma sum_mem {ι : Type w} [decidable_eq ι] {t : finset ι} {f : ι → β} :
+  (∀c∈t, f c ∈ p) → t.sum f ∈ p :=
+finset.induction_on t (by simp [p.zero_mem]) (by simp [p.add_mem] {contextual := tt})
+
+instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem _ x.2 y.2⟩⟩
+instance : has_zero p := ⟨⟨0, zero_mem _⟩⟩
+instance : has_scalar α p := ⟨λ c x, ⟨c • x.1, smul_mem _ c x.2⟩⟩
+
+@[simp] lemma coe_add (x y : p) : (↑(x + y) : β) = ↑x + ↑y := rfl
+@[simp] lemma coe_zero : ((0 : p) : β) = 0 := rfl
+@[simp] lemma coe_smul (r : α) (x : p) : ((r • x : p) : β) = r • ↑x := rfl
+
+instance : add_comm_monoid p :=
+by refine {add := (+), zero := 0, ..};
+  { intros, apply set_coe.ext, simp }
+
+instance subsemimodule_is_add_submonoid : is_add_submonoid (p : set β) :=
+{ zero_mem := p.zero,
+  add_mem  := p.add }
+
+instance : semimodule α p :=
+by refine {smul := (•), ..};
+   { intros, apply set_coe.ext, simp [smul_add, add_smul, mul_smul] }
+
+protected def subtype : p →ₗ[α] β :=
+by refine {to_fun := coe, ..}; simp [coe_smul]
+
+@[simp] theorem subtype_apply (x : p) : p.subtype x = x := rfl
+
+end subsemimodule
+
+/-- 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. -/
+@[reducible] def submodule (α : Type u) (β : Type v) [ring α]
+  [add_comm_group β] [module α β] : Type v := subsemimodule α β
+
+namespace submodule
+open subsemimodule
+variables [ring α] [add_comm_group β] [add_comm_group γ]
+variables [module α β] [module α γ]
+variables (p p' : submodule α β)
+variables {r : α} {x y : β}
+
+instance : has_coe (submodule α β) (set β) := ⟨λ p, p.carrier⟩
+instance : has_mem β (submodule α β) := ⟨λ x p, x ∈ (p : set β)⟩
+@[simp] theorem mem_coe : x ∈ (p : set β) ↔ x ∈ p := iff.rfl
+
+@[extensionality] theorem ext {s t : submodule α β}
+  (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t := ext h
+
+@[simp] lemma zero_mem : (0 : β) ∈ p := p.zero
+
 lemma neg_mem (hx : x ∈ p) : -x ∈ p := by rw ← neg_one_smul α; exact p.smul_mem _ hx
 
 lemma sub_mem (hx : x ∈ p) (hy : y ∈ p) : x - y ∈ p := p.add_mem hx (p.neg_mem hy)
@@ -229,37 +298,25 @@ lemma add_mem_iff_left (h₁ : y ∈ p) : x + y ∈ p ↔ x ∈ p :=
 lemma add_mem_iff_right (h₁ : x ∈ p) : x + y ∈ p ↔ y ∈ p :=
 ⟨λ h₂, by simpa using sub_mem _ h₂ h₁, add_mem _ h₁⟩
 
-lemma sum_mem {ι : Type w} [decidable_eq ι] {t : finset ι} {f : ι → β} :
-  (∀c∈t, f c ∈ p) → t.sum f ∈ p :=
-finset.induction_on t (by simp [p.zero_mem]) (by simp [p.add_mem] {contextual := tt})
-
-instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem _ x.2 y.2⟩⟩
-instance : has_zero p := ⟨⟨0, zero_mem _⟩⟩
 instance : has_neg p := ⟨λx, ⟨-x.1, neg_mem _ x.2⟩⟩
-instance : has_scalar α p := ⟨λ c x, ⟨c • x.1, smul_mem _ c x.2⟩⟩
 
 @[simp] lemma coe_add (x y : p) : (↑(x + y) : β) = ↑x + ↑y := rfl
 @[simp] lemma coe_zero : ((0 : p) : β) = 0 := rfl
 @[simp] lemma coe_neg (x : p) : ((-x : p) : β) = -x := rfl
 @[simp] lemma coe_smul (r : α) (x : p) : ((r • x : p) : β) = r • ↑x := rfl
 
 instance : add_comm_group p :=
-by refine {add := (+), zero := 0, neg := has_neg.neg, ..};
+by refine { neg := has_neg.neg, ..subsemimodule.add_comm_monoid p, .. };
   { intros, apply set_coe.ext, simp }
 
 instance submodule_is_add_subgroup : is_add_subgroup (p : set β) :=
-{ zero_mem := p.zero,
-  add_mem  := p.add,
-  neg_mem  := λ _, p.neg_mem }
+{ neg_mem  := λ _, p.neg_mem,
+  ..subsemimodule.subsemimodule_is_add_submonoid p }
 
 lemma coe_sub (x y : p) : (↑(x - y) : β) = ↑x - ↑y := by simp
 
 instance : module α p :=
-by refine {smul := (•), ..};
-   { intros, apply set_coe.ext, simp [smul_add, add_smul, mul_smul] }
-
-protected def subtype : p →ₗ[α] β :=
-by refine {to_fun := coe, ..}; simp [coe_smul]
+{ ..subsemimodule.semimodule p }
 
 @[simp] theorem subtype_apply (x : p) : p.subtype x = x := rfl
 

src/linear_algebra/basic.lean

@@ -222,7 +222,7 @@ variables [ring α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
 variables [module α β] [module α γ] [module α δ]
 variables (p p' : submodule α β) (q q' : submodule α γ)
 variables {r : α} {x y : β}
-open set lattice
+open set lattice subsemimodule
 
 instance : partial_order (submodule α β) :=
 partial_order.lift (coe : submodule α β → set β) $ λ a b, ext'
@@ -234,11 +234,15 @@ lemma le_def' {p p' : submodule α β} : p ≤ p' ↔ ∀ x ∈ p, x ∈ p' := i
 def of_le {p p' : submodule α β} (h : p ≤ p') : p →ₗ[α] p' :=
 linear_map.cod_restrict _ p.subtype $ λ ⟨x, hx⟩, h hx
 
+set_option class.instance_max_depth 41
+
 @[simp] theorem of_le_apply {p p' : submodule α β} (h : p ≤ p')
   (x : p) : (of_le h x : β) = x := rfl
 
+set_option class.instance_max_depth 32
+
 lemma subtype_comp_of_le (p q : submodule α β) (h : p ≤ q) :
-  (submodule.subtype q).comp (of_le h) = submodule.subtype p :=
+  (subsemimodule.subtype q).comp (of_le h) = subsemimodule.subtype p :=
 by ext ⟨b, hb⟩; simp
 
 instance : has_bot (submodule α β) :=
@@ -363,7 +367,7 @@ submodule.ext $ λ a, by simp
 
 lemma map_comp (f : β →ₗ[α] γ) (g : γ →ₗ[α] δ) (p : submodule α β) :
   map (g.comp f) p = map g (map f p) :=
-submodule.ext' $ by simp [map_coe]; rw ← image_comp
+ext' $ by simp [map_coe]; rw ← image_comp
 
 lemma map_mono {f : β →ₗ[α] γ} {p p' : submodule α β} : p ≤ p' → map f p ≤ map f p' :=
 image_subset _
@@ -386,7 +390,7 @@ def comap (f : β →ₗ[α] γ) (p : submodule α γ) : submodule α β :=
   x ∈ comap f p ↔ f x ∈ p := iff.rfl
 
 lemma comap_id : comap linear_map.id p = p :=
-submodule.ext' rfl
+ext' rfl
 
 lemma comap_comp (f : β →ₗ[α] γ) (g : γ →ₗ[α] δ) (p : submodule α δ) :
   comap (g.comp f) p = comap f (comap g p) := rfl
@@ -772,7 +776,7 @@ theorem range_comp_le_range (f : β →ₗ[α] γ) (g : γ →ₗ[α] δ) : rang
 by rw range_comp; exact map_mono le_top
 
 theorem range_eq_top {f : β →ₗ[α] γ} : range f = ⊤ ↔ surjective f :=
-by rw [← submodule.ext'_iff, range_coe, top_coe, set.range_iff_surjective]
+by rw [← subsemimodule.ext'_iff, range_coe, top_coe, set.range_iff_surjective]
 
 lemma range_le_iff_comap {f : β →ₗ[α] γ} {p : submodule α γ} : range f ≤ p ↔ comap f p = ⊤ :=
 by rw [range, map_le_iff_le_comap, eq_top_iff]
@@ -1153,6 +1157,8 @@ def of_top (p : submodule α β) (h : p = ⊤) : p ≃ₗ[α] β :=
   right_inv := λ x, rfl,
   .. p.subtype }
 
+set_option class.instance_max_depth 43
+
 @[simp] theorem of_top_apply (p : submodule α β) {h} (x : p) :
   of_top p h x = x := rfl
 
@@ -1169,6 +1175,8 @@ begin
   exact congr_arg (coe : p → β) this.symm
 end
 
+set_option class.instance_max_depth 32
+
 end ring
 
 section comm_ring
@@ -1217,6 +1225,8 @@ variables [ring α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
 variables [module α β] [module α γ] [module α δ]
 variables (f : β →ₗ[α] γ)
 
+set_option class.instance_max_depth 39
+
 /-- First Isomorphism Law -/
 noncomputable def quot_ker_equiv_range : f.ker.quotient ≃ₗ[α] f.range :=
 have hr : ∀ x : f.range, ∃ y, f y = ↑x := λ x, x.2.imp $ λ _, and.right,
@@ -1239,7 +1249,7 @@ def sup_quotient_to_quotient_inf (p p' : submodule α β) :
 rw [ker_comp, of_le, comap_cod_restrict, ker_mkq, map_comap_subtype],
 exact comap_mono (inf_le_inf le_sup_left (le_refl _)) end
 
-set_option class.instance_max_depth 41
+set_option class.instance_max_depth 70
 
 /-- Second Isomorphism Law -/
 noncomputable def sup_quotient_equiv_quotient_inf (p p' : submodule α β) :