chore(algebra/module/linear_map): move map_sum lemmas (#18106)

The lemmas `linear_map.map_sum` and `linear_equiv.map_sum` exist only for dot notation convenience, since `linear_map`s are of `add_monoid_hom_class` and therefore the generic lemma `map_sum` can replace them. Since these lemmas are the only reason that finsets are imported to `algebra/module/linear_map`, I propose deleting that import and moving the lemmas to `linear_algebra/basic`. This should open several files for porting.
leanprover-community · Jan 9, 2023 · 40acfb6 · 40acfb6
1 parent 247a102
commit 40acfb6
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/src/algebra/module/equiv.lean b/src/algebra/module/equiv.lean
@@ -34,7 +34,6 @@ linear equiv, linear equivalences, linear isomorphism, linear isomorphic
 -/
 
 open function
-open_locale big_operators
 
 universes u u' v w x y z
 variables {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
@@ -375,9 +374,6 @@ theorem map_smul (e : N₁ ≃ₗ[R₁] N₂) (c : R₁) (x : N₁) :
   e (c • x) = c • e x := map_smulₛₗ e c x
 omit module_N₁ module_N₂
 
-@[simp] lemma map_sum {s : finset ι} (u : ι → M) : e (∑ i in s, u i) = ∑ i in s, e (u i) :=
-e.to_linear_map.map_sum
-
 @[simp] theorem map_eq_zero_iff {x : M} : e x = 0 ↔ x = 0 :=
 e.to_add_equiv.map_eq_zero_iff
 theorem map_ne_zero_iff {x : M} : e x ≠ 0 ↔ x ≠ 0 :=

diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne Baanen,
   Frédéric Dupuis, Heather Macbeth
 -/
-import algebra.big_operators.basic
 import algebra.hom.group_action
 import algebra.module.pi
 import algebra.star.basic
@@ -53,8 +52,10 @@ To ensure that composition works smoothly for semilinear maps, we use the typecl
 linear map
 -/
 
+assert_not_exists submonoid
+assert_not_exists finset
+
 open function
-open_locale big_operators
 
 universes u u' v w x y z
 variables {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
@@ -365,10 +366,6 @@ end restrict_scalars
 
 variable {R}
 
-@[simp] lemma map_sum {ι} {t : finset ι} {g : ι → M} :
-  f (∑ i in t, g i) = (∑ i in t, f (g i)) :=
-f.to_add_monoid_hom.map_sum _ _
-
 theorem to_add_monoid_hom_injective :
   function.injective (to_add_monoid_hom : (M →ₛₗ[σ] M₃) → (M →+ M₃)) :=
 λ f g h, ext $ add_monoid_hom.congr_fun h

diff --git a/src/algebra/module/submodule/basic.lean b/src/algebra/module/submodule/basic.lean
@@ -247,7 +247,7 @@ lemma injective_subtype : injective p.subtype := subtype.coe_injective
 
 /-- Note the `add_submonoid` version of this lemma is called `add_submonoid.coe_finset_sum`. -/
 @[simp] lemma coe_sum (x : ι → p) (s : finset ι) : ↑(∑ i in s, x i) = ∑ i in s, (x i : M) :=
-p.subtype.map_sum
+map_sum p.subtype _ _
 
 section restrict_scalars
 variables (S) [semiring S] [module S M] [module R M] [has_smul S R] [is_scalar_tower S R M]

diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
@@ -146,6 +146,10 @@ variables [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_tripl
 variables (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃)
 include R R₂
 
+@[simp] lemma map_sum {ι : Type*} {t : finset ι} {g : ι → M} :
+  f (∑ i in t, g i) = (∑ i in t, f (g i)) :=
+f.to_add_monoid_hom.map_sum _ _
+
 theorem comp_assoc (h : M₃ →ₛₗ[σ₃₄] M₄) :
   ((h.comp g : M₂ →ₛₗ[σ₂₄] M₄).comp f : M →ₛₗ[σ₁₄] M₄)
   = h.comp (g.comp f : M →ₛₗ[σ₁₃] M₃) := rfl
@@ -1514,6 +1518,9 @@ variables {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
 variables {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂}
 variables (e e' : M ≃ₛₗ[σ₁₂] M₂)
 
+@[simp] lemma map_sum {s : finset ι} (u : ι → M) : e (∑ i in s, u i) = ∑ i in s, e (u i) :=
+e.to_linear_map.map_sum
+
 lemma map_eq_comap {p : submodule R M} :
   (p.map (e : M →ₛₗ[σ₁₂] M₂) : submodule R₂ M₂) = p.comap (e.symm : M₂ →ₛₗ[σ₂₁] M) :=
 set_like.coe_injective $ by simp [e.image_eq_preimage]