feat(algebra/big_operators): add lemmas about sum and pi.single (#…

…6390)

src/algebra/big_operators/basic.lean

@@ -525,6 +525,16 @@ lemma prod_ite_index (p : Prop) [decidable p] (s t : finset α) (f : α → β)
   (∏ x in if p then s else t, f x) = if p then ∏ x in s, f x else ∏ x in t, f x :=
 apply_ite (λ s, ∏ x in s, f x) _ _ _
 
+@[simp] lemma sum_pi_single' {ι M : Type*} [decidable_eq ι] [add_comm_monoid M]
+  (i : ι) (x : M) (s : finset ι) :
+  ∑ j in s, pi.single i x j = if i ∈ s then x else 0 :=
+sum_dite_eq' _ _ _
+
+@[simp] lemma sum_pi_single {ι : Type*} {M : ι → Type*}
+  [decidable_eq ι] [Π i, add_comm_monoid (M i)] (i : ι) (f : Π i, M i) (s : finset ι) :
+  ∑ j in s, pi.single j (f j) i = if i ∈ s then f i else 0 :=
+sum_dite_eq _ _ _
+
 /--
   Reorder a product.
 

src/algebra/big_operators/pi.lean

@@ -53,23 +53,15 @@ variables [Π i, add_comm_monoid (Z i)]
 -- As we only defined `single` into `add_monoid`, we only prove the `finset.sum` version here.
 lemma finset.univ_sum_single [fintype I] (f : Π i, Z i) :
   ∑ i, pi.single i (f i) = f :=
-begin
-  ext a,
-  rw [finset.sum_apply, finset.sum_eq_single a],
-  { simp, },
-  { intros b _ h, simp [h.symm], },
-  { intro h, exfalso, simpa using h, },
-end
+by { ext a, simp }
 
 lemma add_monoid_hom.functions_ext [fintype I] (G : Type*)
   [add_comm_monoid G] (g h : (Π i, Z i) →+ G)
   (w : ∀ (i : I) (x : Z i), g (pi.single i x) = h (pi.single i x)) : g = h :=
 begin
   ext k,
-  rw [←finset.univ_sum_single k, add_monoid_hom.map_sum, add_monoid_hom.map_sum],
-  apply finset.sum_congr rfl,
-  intros,
-  apply w,
+  rw [← finset.univ_sum_single k, g.map_sum, h.map_sum],
+  simp only [w]
 end
 
 /-- This is used as the ext lemma instead of `add_monoid_hom.functions_ext` for reasons explained in
@@ -89,8 +81,7 @@ open pi
 variables {I : Type*} [decidable_eq I] {f : I → Type*}
 variables [Π i, semiring (f i)]
 
-@[ext]
-lemma ring_hom.functions_ext [fintype I] (G : Type*) [semiring G] (g h : (Π i, f i) →+* G)
+@[ext] lemma ring_hom.functions_ext [fintype I] (G : Type*) [semiring G] (g h : (Π i, f i) →+* G)
   (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
 ring_hom.coe_add_monoid_hom_injective $
  add_monoid_hom.functions_ext G (g : (Π i, f i) →+ G) h w

src/algebra/module/linear_map.lean

@@ -194,6 +194,10 @@ theorem to_add_monoid_hom_injective :
 /-- If two `R`-linear maps from `R` are equal on `1`, then they are equal. -/
 @[ext] theorem ext_ring {f g : R →ₗ[R] M} (h : f 1 = g 1) : f = g :=
 ext $ λ x, by rw [← mul_one x, ← smul_eq_mul, f.map_smul, g.map_smul, h]
+
+theorem ext_ring_iff {f g : R →ₗ[R] M} : f = g ↔ f 1 = g 1 :=
+⟨λ h, h ▸ rfl, ext_ring⟩
+
 end
 
 section

src/algebra/module/pi.lean

@@ -88,7 +88,7 @@ instance distrib_mul_action' {g : I → Type*} {m : Π i, monoid (f i)} {n : Π
 { smul_add := by { intros, ext x, apply smul_add },
   smul_zero := by { intros, ext x, apply smul_zero } }
 
-lemma single_smul {α} {m : monoid α} {n : Π i, add_monoid $ f i}
+lemma single_smul {α} [monoid α] [Π i, add_monoid $ f i]
   [Π i, distrib_mul_action α $ f i] [decidable_eq I] (i : I) (r : α) (x : f i) :
   single i (r • x) = r • single i x :=
 begin
@@ -97,7 +97,7 @@ begin
   exact smul_zero _,
 end
 
-lemma single_smul' {g : I → Type*} {m : Π i, monoid_with_zero (f i)} {n : Π i, add_monoid (g i)}
+lemma single_smul' {g : I → Type*} [Π i, monoid_with_zero (f i)] [Π i, add_monoid (g i)]
   [Π i, distrib_mul_action (f i) (g i)] [decidable_eq I] (i : I) (r : f i) (x : g i) :
   single i (r • x) = single i r • single i x :=
 begin

src/linear_algebra/pi.lean

@@ -95,12 +95,7 @@ def lsum (S) [add_comm_monoid M] [semimodule R M] [fintype ι] [decidable_eq ι]
   inv_fun := λ f i, f.comp (single i),
   map_add' := λ f g, by simp only [pi.add_apply, add_comp, finset.sum_add_distrib],
   map_smul' := λ c f, by simp only [pi.smul_apply, smul_comp, finset.smul_sum],
-  left_inv := λ f,
-    begin
-      ext i x,
-      suffices : ∑ j, pi.single i (f i x) j = f i x, by simpa [apply_single],
-      exact (finset.sum_dite_eq' _ _ _).trans (if_pos $ finset.mem_univ i)
-    end,
+  left_inv := λ f, by { ext i x, simp [apply_single] },
   right_inv := λ f,
     begin
       ext,

src/topology/algebra/module.lean

@@ -641,7 +641,10 @@ it produces a continuous linear function into a family of topological modules. -
 def pi (f : Πi, M →L[R] φ i) : M →L[R] (Πi, φ i) :=
 ⟨linear_map.pi (λ i, f i), continuous_pi (λ i, (f i).continuous)⟩
 
-@[simp] lemma coe_pi (f : Π i, M →L[R] φ i) : ⇑(pi f) = λ c i, f i c := rfl
+@[simp] lemma coe_pi' (f : Π i, M →L[R] φ i) : ⇑(pi f) = λ c i, f i c := rfl
+@[simp] lemma coe_pi (f : Π i, M →L[R] φ i) :
+  (pi f : M →ₗ[R] Π i, φ i) = linear_map.pi (λ i, f i) :=
+rfl
 
 lemma pi_apply (f : Πi, M →L[R] φ i) (c : M) (i : ι) :
   pi f c i = f i c := rfl