feat(data/finsupp/to_dfinsupp): add sigma_finsupp_lequiv_dfinsupp (#7818)

Equivalences between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`.

- [x] depends on: #7819 



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: riccardobrasca

src/data/finsupp/to_dfinsupp.lean

@@ -15,12 +15,17 @@ It is in its own file since neither `finsupp` or `dfinsupp` depend on each other
 
 ## Main definitions
 
-* `finsupp.to_dfinsupp : (ι →₀ M) → (Π₀ i : ι, M)`
-* `dfinsupp.to_finsupp : (Π₀ i : ι, M) → (ι →₀ M)`
-* Bundled equiv versions of the above:
-  * `finsupp_equiv_dfinsupp : (ι →₀ M) ≃ (Π₀ i : ι, M)`
-  * `finsupp_add_equiv_dfinsupp : (ι →₀ M) ≃+ (Π₀ i : ι, M)`
-  * `finsupp_lequiv_dfinsupp R : (ι →₀ M) ≃ₗ[R] (Π₀ i : ι, M)`
+* "identity" maps between `finsupp` and `dfinsupp`:
+  * `finsupp.to_dfinsupp : (ι →₀ M) → (Π₀ i : ι, M)`
+  * `dfinsupp.to_finsupp : (Π₀ i : ι, M) → (ι →₀ M)`
+  * Bundled equiv versions of the above:
+    * `finsupp_equiv_dfinsupp : (ι →₀ M) ≃ (Π₀ i : ι, M)`
+    * `finsupp_add_equiv_dfinsupp : (ι →₀ M) ≃+ (Π₀ i : ι, M)`
+    * `finsupp_lequiv_dfinsupp R : (ι →₀ M) ≃ₗ[R] (Π₀ i : ι, M)`
+* stronger versions of `finsupp.split`:
+  * `sigma_finsupp_equiv_dfinsupp : ((Σ i, η i) →₀ N) ≃ (Π₀ i, (η i →₀ N))`
+  * `sigma_finsupp_add_equiv_dfinsupp : ((Σ i, η i) →₀ N) ≃+ (Π₀ i, (η i →₀ N))`
+  * `sigma_finsupp_lequiv_dfinsupp : ((Σ i, η i) →₀ N) ≃ₗ[R] (Π₀ i, (η i →₀ N))`
 
 ## Theorems
 
@@ -187,4 +192,87 @@ noncomputable def finsupp_lequiv_dfinsupp
   map_add' := finsupp.to_dfinsupp_add,
   .. finsupp_equiv_dfinsupp}
 
+section sigma
+/-- ### Stronger versions of `finsupp.split` -/
+
+noncomputable theory
+open_locale classical
+
+variables {η : ι → Type*} {N : Type*} [semiring R]
+
+open finsupp
+
+/-- `finsupp.split` is an equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
+def sigma_finsupp_equiv_dfinsupp [has_zero N] : ((Σ i, η i) →₀ N) ≃ (Π₀ i, (η i →₀ N)) :=
+{ to_fun := λ f, ⟦⟨split f, (split_support f : finset ι).val, λ i,
+    begin
+    rw [← finset.mem_def, mem_split_support_iff_nonzero],
+    exact (decidable.em _).symm
+    end⟩⟧,
+  inv_fun := λ f,
+  begin
+    refine on_finset (finset.sigma f.support (λ j, (f j).support)) (λ ji, f ji.1 ji.2)
+      (λ g hg, finset.mem_sigma.mpr ⟨_, mem_support_iff.mpr hg⟩),
+    simp only [ne.def, dfinsupp.mem_support_to_fun],
+    intro h,
+    rw h at hg,
+    simpa using hg
+  end,
+  left_inv := λ f, by { ext, simp [split] },
+  right_inv := λ f, by { ext, simp [split] } }
+
+@[simp]
+lemma sigma_finsupp_equiv_dfinsupp_apply [has_zero N] (f : (Σ i, η i) →₀ N) :
+  (sigma_finsupp_equiv_dfinsupp f : Π i, (η i →₀ N)) = finsupp.split f := rfl
+
+@[simp]
+lemma sigma_finsupp_equiv_dfinsupp_symm_apply [has_zero N] (f : Π₀ i, (η i →₀ N)) (s : Σ i, η i) :
+  (sigma_finsupp_equiv_dfinsupp.symm f : (Σ i, η i) →₀ N) s = f s.1 s.2 := rfl
+
+@[simp]
+lemma sigma_finsupp_equiv_dfinsupp_support [has_zero N] (f : (Σ i, η i) →₀ N) :
+  (sigma_finsupp_equiv_dfinsupp f).support = finsupp.split_support f :=
+begin
+  ext,
+  rw dfinsupp.mem_support_to_fun,
+  exact (finsupp.mem_split_support_iff_nonzero _ _).symm,
+end
+
+-- Without this Lean fails to find the `add_zero_class` instance on `Π₀ i, (η i →₀ N)`.
+local attribute [-instance] finsupp.has_zero
+
+@[simp]
+lemma sigma_finsupp_equiv_dfinsupp_add [add_zero_class N] (f g : (Σ i, η i) →₀ N) :
+  sigma_finsupp_equiv_dfinsupp (f + g) =
+  (sigma_finsupp_equiv_dfinsupp f + (sigma_finsupp_equiv_dfinsupp g) : (Π₀ (i : ι), η i →₀ N)) :=
+by {ext, refl}
+
+/-- `finsupp.split` is an additive equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
+@[simps]
+def sigma_finsupp_add_equiv_dfinsupp [add_zero_class N] : ((Σ i, η i) →₀ N) ≃+ (Π₀ i, (η i →₀ N)) :=
+{ to_fun := sigma_finsupp_equiv_dfinsupp,
+  inv_fun := sigma_finsupp_equiv_dfinsupp.symm,
+  map_add' := sigma_finsupp_equiv_dfinsupp_add,
+  .. sigma_finsupp_equiv_dfinsupp }
+
+local attribute [-instance] finsupp.add_zero_class
+
+--tofix: r • (sigma_finsupp_equiv_dfinsupp f) doesn't work.
+@[simp]
+lemma sigma_finsupp_equiv_dfinsupp_smul {R} [monoid R] [add_monoid N] [distrib_mul_action R N]
+  (r : R) (f : (Σ i, η i) →₀ N) : sigma_finsupp_equiv_dfinsupp (r • f) =
+  @has_scalar.smul R (Π₀ i, η i →₀ N) mul_action.to_has_scalar r (sigma_finsupp_equiv_dfinsupp f) :=
+by { ext, refl }
+
+local attribute [-instance] finsupp.add_monoid
+
+/-- `finsupp.split` is a linear equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
+@[simps]
+def sigma_finsupp_lequiv_dfinsupp [add_comm_monoid N] [module R N] :
+  ((Σ i, η i) →₀ N) ≃ₗ[R] (Π₀ i, (η i →₀ N)) :=
+{ map_smul' := sigma_finsupp_equiv_dfinsupp_smul,
+  .. sigma_finsupp_add_equiv_dfinsupp }
+
+end sigma
+
 end equivs