chore({data,linear_algebra}/dfinsupp): Move linear_algebra stuff to i…

…ts own file (#4873)

This makes the layout of files about `dfinsupp` resemble those of `finsupp` a little better.

This also:
* Renames type arguments to match the names of those in finsupp
* Adjusts argument explicitness to match those in finsupp
* Adds `dfinsupp.lapply` to match `finsupp.lapply`

src/data/dfinsupp.lean

@@ -7,7 +7,6 @@ import algebra.module.linear_map
 import algebra.module.pi
 import algebra.big_operators.basic
 import data.set.finite
-import linear_algebra.basic
 
 /-!
 # Dependent functions with finite support
@@ -504,35 +503,6 @@ ext $ λ i, by simp only [smul_apply, mk_apply]; split_ifs; [refl, rw smul_zero]
   single i (c • x) = c • single i x :=
 ext $ λ i, by simp only [smul_apply, single_apply]; split_ifs; [cases h, rw smul_zero]; refl
 
-variable β
-/-- `dfinsupp.mk` as a `linear_map`. -/
-def lmk (s : finset ι) : (Π i : (↑s : set ι), β i.1) →ₗ[γ] Π₀ i, β i :=
-⟨mk s, λ _ _, mk_add, λ c x, by rw [mk_smul γ x]⟩
-
-/-- `dfinsupp.single` as a `linear_map` -/
-def lsingle (i) : β i →ₗ[γ] Π₀ i, β i :=
-⟨single i, λ _ _, single_add, λ _ _, single_smul _⟩
-variable {β}
-
-/-- Two `R`-linear maps from `Π₀ i, β i` which agree on each `single i x` agree everywhere. -/
-lemma lhom_ext {δ : Type*} [add_comm_monoid δ] [semimodule γ δ] ⦃φ ψ : (Π₀ i, β i) →ₗ[γ] δ⦄
-  (h : ∀ i x, φ (single i x) = ψ (single i x)) :
-  φ = ψ :=
-linear_map.to_add_monoid_hom_injective $ add_hom_ext h
-
-/-- Two `R`-linear maps from `Π₀ i, β i` which agree on each `single i x` agree everywhere.
-
-We formulate this fact using equality of linear maps `φ.comp (lsingle a)` and `ψ.comp (lsingle a)`
-so that the `ext` tactic can apply a type-specific extensionality lemma to prove equality of these
-maps. E.g., if `M = R`, then it suffices to verify `φ (single a 1) = ψ (single a 1)`. -/
-@[ext] lemma lhom_ext' {δ : Type*} [add_comm_monoid δ] [semimodule γ δ] ⦃φ ψ : (Π₀ i, β i) →ₗ[γ] δ⦄
-  (h : ∀ i, φ.comp (lsingle β γ i) = ψ.comp (lsingle β γ i)) :
-  φ = ψ :=
-lhom_ext γ $ λ i, linear_map.congr_fun (h i)
-
-@[simp] lemma lmk_apply {s : finset ι} {x} : lmk β γ s x = mk s x := rfl
-
-@[simp] lemma lsingle_apply {i : ι} {x : β i} : lsingle β γ i x = single i x := rfl
 end
 
 section support_basic
@@ -952,26 +922,6 @@ begin
   exact this,
 end
 
-/-- The `dfinsupp` version of `finsupp.lsum`,-/
-@[simps apply symm_apply]
-def lsum {R : Type*} [semiring R] [Π i, add_comm_monoid (β i)] [Π i, semimodule R (β i)]
-  [add_comm_monoid γ] [semimodule R γ] :
-    (Π i, β i →ₗ[R] γ) ≃+ ((Π₀ i, β i) →ₗ[R] γ) :=
-{ to_fun := λ F, {
-    to_fun := sum_add_hom (λ i, (F i).to_add_monoid_hom),
-    map_add' := (lift_add_hom (λ i, (F i).to_add_monoid_hom)).map_add,
-    map_smul' := λ c f, by {
-      apply dfinsupp.induction f,
-      { rw [smul_zero, add_monoid_hom.map_zero, smul_zero] },
-      { intros a b f ha hb hf,
-        rw [smul_add, add_monoid_hom.map_add, add_monoid_hom.map_add, smul_add, hf, ←single_smul,
-          sum_add_hom_single, sum_add_hom_single, linear_map.to_add_monoid_hom_coe,
-          linear_map.map_smul], } } },
-  inv_fun := λ F i, F.comp (lsingle β R i),
-  left_inv := λ F, by { ext x y, simp },
-  right_inv := λ F, by { ext x y, simp },
-  map_add' := λ F G, by { ext x y, simp } }
-
 @[to_additive]
 lemma prod_subtype_domain_index [Π i, has_zero (β i)] [Π i (x : β i), decidable (x ≠ 0)]
   [comm_monoid γ] {v : Π₀ i, β i} {p : ι → Prop} [decidable_pred p]

src/linear_algebra/dfinsupp.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Johannes Hölzl, Kenny Lau
+-/
+import data.dfinsupp
+import linear_algebra.basic
+
+/-!
+# Properties of the semimodule `Π₀ i, M i`
+
+Given an indexed collection of `R`-semimodules `M i`, the `R`-semimodule structure on `Π₀ i, M i`
+is defined in `data.dfinsupp`.
+
+In this file we define `linear_map` versions of various maps:
+
+* `dfinsupp.lsingle a : M →ₗ[R] Π₀ i, M i`: `dfinsupp.single a` as a linear map;
+
+* `dfinsupp.lmk s : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i`: `dfinsupp.single a` as a linear map;
+
+* `dfinsupp.lapply i : (Π₀ i, M i) →ₗ[R] M`: the map `λ f, f i` as a linear map;
+
+* `dfinsupp.lsum`: `dfinsupp.sum` or `dfinsupp.lift_add_hom` as a `linear_map`;
+
+## Implementation notes
+
+This file should try to mirror `linear_algebra.finsupp` where possible. The API of `finsupp` is
+much more developed, but many lemmas in that file should be eligible to copy over.
+
+## Tags
+
+function with finite support, semimodule, linear algebra
+-/
+
+variables {ι : Type*} {R : Type*} {M : ι → Type*} {N : Type*}
+
+variables [dec_ι : decidable_eq ι]
+variables [semiring R] [Π i, add_comm_monoid (M i)] [Π i, semimodule R (M i)]
+variables [add_comm_monoid N] [semimodule R N]
+
+namespace dfinsupp
+
+include dec_ι
+
+/-- `dfinsupp.mk` as a `linear_map`. -/
+def lmk (s : finset ι) : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i :=
+⟨mk s, λ _ _, mk_add, λ c x, by rw [mk_smul R x]⟩
+
+/-- `dfinsupp.single` as a `linear_map` -/
+def lsingle (i) : M i →ₗ[R] Π₀ i, M i :=
+⟨single i, λ _ _, single_add, λ _ _, single_smul _⟩
+
+/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere. -/
+lemma lhom_ext ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄
+  (h : ∀ i x, φ (single i x) = ψ (single i x)) :
+  φ = ψ :=
+linear_map.to_add_monoid_hom_injective $ add_hom_ext h
+
+/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere.
+
+We formulate this fact using equality of linear maps `φ.comp (lsingle a)` and `ψ.comp (lsingle a)`
+so that the `ext` tactic can apply a type-specific extensionality lemma to prove equality of these
+maps. E.g., if `M = R`, then it suffices to verify `φ (single a 1) = ψ (single a 1)`. -/
+@[ext] lemma lhom_ext' ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄
+  (h : ∀ i, φ.comp (lsingle i) = ψ.comp (lsingle i)) :
+  φ = ψ :=
+lhom_ext $ λ i, linear_map.congr_fun (h i)
+
+omit dec_ι
+
+/-- Interpret `λ (f : Π₀ i, M i), f i` as a linear map. -/
+def lapply (i : ι) : (Π₀ i, M i) →ₗ[R] M i :=
+{ to_fun := λ f, f i,
+  map_add' := λ f g, add_apply f g i,
+  map_smul' := λ c f, smul_apply c f i}
+
+include dec_ι
+
+@[simp] lemma lmk_apply (s : finset ι) (x) : (lmk s : _ →ₗ[R] Π₀ i, M i) x = mk s x := rfl
+
+@[simp] lemma lsingle_apply (i : ι) (x : M i) : (lsingle i : _ →ₗ[R] _) x = single i x := rfl
+
+omit dec_ι
+
+@[simp] lemma lapply_apply (i : ι) (f : Π₀ i, M i) : (lapply i : _ →ₗ[R] _) f = f i := rfl
+
+include dec_ι
+
+/-- The `dfinsupp` version of `finsupp.lsum`. -/
+@[simps apply symm_apply]
+def lsum : (Π i, M i →ₗ[R] N) ≃+ ((Π₀ i, M i) →ₗ[R] N) :=
+{ to_fun := λ F, {
+    to_fun := sum_add_hom (λ i, (F i).to_add_monoid_hom),
+    map_add' := (lift_add_hom (λ i, (F i).to_add_monoid_hom)).map_add,
+    map_smul' := λ c f, by {
+      apply dfinsupp.induction f,
+      { rw [smul_zero, add_monoid_hom.map_zero, smul_zero] },
+      { intros a b f ha hb hf,
+        rw [smul_add, add_monoid_hom.map_add, add_monoid_hom.map_add, smul_add, hf, ←single_smul,
+          sum_add_hom_single, sum_add_hom_single, linear_map.to_add_monoid_hom_coe,
+          linear_map.map_smul], } } },
+  inv_fun := λ F i, F.comp (lsingle i),
+  left_inv := λ F, by { ext x y, simp },
+  right_inv := λ F, by { ext x y, simp },
+  map_add' := λ F G, by { ext x y, simp } }
+
+end dfinsupp

src/linear_algebra/direct_sum_module.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau
 Direct sum of modules over commutative rings, indexed by a discrete type.
 -/
 import algebra.direct_sum
-import linear_algebra.basic
+import linear_algebra.dfinsupp
 
 /-!
 # Direct sum of modules over commutative rings, indexed by a discrete type.
@@ -46,11 +46,11 @@ include dec_ι
 variables R ι M
 /-- Create the direct sum given a family `M` of `R` semimodules indexed over `ι`. -/
 def lmk : Π s : finset ι, (Π i : (↑s : set ι), M i.val) →ₗ[R] (⨁ i, M i) :=
-dfinsupp.lmk M R
+dfinsupp.lmk
 
 /-- Inclusion of each component into the direct sum. -/
 def lof : Π i : ι, M i →ₗ[R] (⨁ i, M i) :=
-dfinsupp.lsingle M R
+dfinsupp.lsingle
 variables {ι M}
 
 lemma single_eq_lof (i : ι) (b : M i) :
@@ -94,7 +94,7 @@ variables {ψ} {ψ' : (⨁ i, M i) →ₗ[R] N}
 
 theorem to_module.ext (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) (f : ⨁ i, M i) :
   ψ f = ψ' f :=
-by rw dfinsupp.lhom_ext' R H
+by rw dfinsupp.lhom_ext' H
 
 /--
 The inclusion of a subset of the direct summands
@@ -107,7 +107,6 @@ to_module R _ _ $ λ i, lof R T (λ (i : subtype T), M i) ⟨i, H i.prop⟩
 omit dec_ι
 
 /-- The natural linear equivalence between `⨁ _ : ι, M` and `M` when `unique ι`. -/
--- TODO: generalize this to arbitrary index type `ι` with `unique ι`
 protected def lid (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [semimodule R M]
   [unique ι] :
   (⨁ (_ : ι), M) ≃ₗ M :=
@@ -117,9 +116,7 @@ protected def lid (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [semimo
 variables (ι M)
 /-- The projection map onto one component, as a linear map. -/
 def component (i : ι) : (⨁ i, M i) →ₗ[R] M i :=
-{ to_fun := λ f, f i,
-  map_add' := λ f g, dfinsupp.add_apply f g i,
-  map_smul' := λ c f, dfinsupp.smul_apply c f i}
+dfinsupp.lapply i
 
 variables {ι M}
 
@@ -137,7 +134,7 @@ lemma ext_iff {f g : ⨁ i, M i} : f = g ↔
 include dec_ι
 
 @[simp] lemma lof_apply (i : ι) (b : M i) : ((lof R ι M i) b) i = b :=
-by rw [lof, dfinsupp.lsingle_apply, dfinsupp.single_apply, dif_pos rfl]
+dfinsupp.single_eq_same
 
 @[simp] lemma component.lof_self (i : ι) (b : M i) :
   component R ι M i ((lof R ι M i) b) = b :=

src/linear_algebra/finsupp.lean

@@ -40,7 +40,7 @@ interpreted as a submodule of `α →₀ M`. We also define `linear_map` version
 * `finsupp.dom_lcongr`: a `linear_equiv` version of `finsupp.dom_congr`;
 
 * `finsupp.congr`: if the sets `s` and `t` are equivalent, then `supported M R s` is equivalent to
-  `supported M R t`; 
+  `supported M R t`;
 
 * `finsupp.lcongr`: a `linear_equiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃
   β` and `e' : M ≃ₗ[R] N`.