[Merged by Bors] - feat(linear_algebra/finsupp): lemmas for finsupp_tensor_finsupp

src/linear_algebra/direct_sum/finsupp.lean

@@ -50,6 +50,7 @@ end finsupp_lequiv_direct_sum
 
 section tensor_product
 
+open tensor_product
 open_locale tensor_product
 
 /-- The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N). -/
@@ -69,6 +70,24 @@ linear_equiv.trans
   finsupp.single (i, k) (m ⊗ₜ n) :=
 by simp [finsupp_tensor_finsupp]
 
+@[simp] theorem finsupp_tensor_finsupp_apply (R M N ι κ : Sort*) [comm_ring R]
+  [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+  (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
+  finsupp_tensor_finsupp R M N ι κ (f ⊗ₜ g) (i, k) = f i ⊗ₜ g k :=
+begin
+  apply finsupp.induction_linear f,
+  { simp, },
+  { intros f₁ f₂ hf₁ hf₂, simp [add_tmul, hf₁, hf₂], },
+  { intros i' m,
+    apply finsupp.induction_linear g,
+    { simp, },
+    { intros g₁ g₂ hg₁ hg₂, simp [tmul_add, hg₁, hg₂], },
+    { intros k' n,
+      simp only [finsupp_tensor_finsupp_single],
+      simp only [finsupp.single, finsupp.coe_mk],
+      split_ifs; finish, } }
+end
+
 @[simp] theorem finsupp_tensor_finsupp_symm_single (R M N ι κ : Sort*) [comm_ring R]
   [add_comm_group M] [module R M] [add_comm_group N] [module R N]
   (i : ι × κ) (m : M) (n : N) :
@@ -77,4 +96,21 @@ by simp [finsupp_tensor_finsupp]
 prod.cases_on i $ λ i k, (linear_equiv.symm_apply_eq _).2
   (finsupp_tensor_finsupp_single _ _ _ _ _ _ _ _ _).symm
 
+variables (S : Type*) [comm_ring S] (α β : Type*)
+
+/--
+A variant of `finsupp_tensor_finsupp` where both modules are the ground ring.
+-/
+def finsupp_tensor_finsupp' : ((α →₀ S) ⊗[S] (β →₀ S)) ≃ₗ[S] (α × β →₀ S) :=
+(finsupp_tensor_finsupp S S S α β).trans (finsupp.lcongr (equiv.refl _) (tensor_product.lid S S))
+
+@[simp] lemma finsupp_tensor_finsupp'_apply_apply (f : α →₀ S) (g : β →₀ S) (a : α) (b : β) :
+  finsupp_tensor_finsupp' S α β (f ⊗ₜ[S] g) (a, b) = f a * g b :=
+by simp [finsupp_tensor_finsupp']
+
+@[simp] lemma finsupp_tensor_finsupp'_single_tmul_single (a : α) (b : β) (r₁ r₂ : S) :
+  finsupp_tensor_finsupp' S α β (finsupp.single a r₁ ⊗ₜ[S] finsupp.single b r₂) =
+    finsupp.single (a, b) (r₁ * r₂) :=
+by { ext ⟨a', b'⟩, simp [finsupp.single], split_ifs; finish }
+
 end tensor_product

src/linear_algebra/finsupp.lean

@@ -609,10 +609,43 @@ corresponding finitely supported functions. -/
 def lcongr {ι κ : Sort*} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : (ι →₀ M) ≃ₗ[R] (κ →₀ N) :=
 (finsupp.dom_lcongr e₁).trans (map_range.linear_equiv e₂)
 
-@[simp] theorem lcongr_single {ι κ : Sort*} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N)
-  (i : ι) (m : M) : lcongr e₁ e₂ (finsupp.single i m) = finsupp.single (e₁ i) (e₂ m) :=
+@[simp] theorem lcongr_single {ι κ : Sort*} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
+  lcongr e₁ e₂ (finsupp.single i m) = finsupp.single (e₁ i) (e₂ m) :=
 by simp [lcongr]
 
+@[simp] lemma lcongr_apply_apply {ι κ : Sort*} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (f : ι →₀ M) (k : κ) :
+  lcongr e₁ e₂ f k = e₂ (f (e₁.symm k)) :=
+begin
+  apply finsupp.induction_linear f,
+  { simp, },
+  { intros f g hf hg, simp [map_add, hf, hg], },
+  { intros i m,
+    simp only [finsupp.lcongr_single],
+    simp only [finsupp.single, equiv.eq_symm_apply, finsupp.coe_mk],
+    split_ifs; simp, },
+end
+
+theorem lcongr_symm_single {ι κ : Sort*} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
+  (lcongr e₁ e₂).symm (finsupp.single k n) = finsupp.single (e₁.symm k) (e₂.symm n) :=
+begin
+  apply_fun lcongr e₁ e₂ using (lcongr e₁ e₂).injective,
+  simp,
+end
+
+@[simp] lemma lcongr_symm {ι κ : Sort*} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) :
+  (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm :=
+begin
+  ext f i,
+  simp only [equiv.symm_symm, finsupp.lcongr_apply_apply],
+  apply finsupp.induction_linear f,
+  { simp, },
+  { intros f g hf hg, simp [map_add, hf, hg], },
+  { intros k m,
+    simp only [finsupp.lcongr_symm_single],
+    simp only [finsupp.single, equiv.symm_apply_eq, finsupp.coe_mk],
+    split_ifs; simp, },
+end
+
 end finsupp
 
 variables {R : Type*} {M : Type*} {N : Type*}