chore(linear_algebra/finsupp): make lsum a linear_equiv (#6183)

src/group_theory/group_action/defs.lean

@@ -55,6 +55,24 @@ class smul_comm_class (M N α : Type*) [has_scalar M α] [has_scalar N α] : Pro
 
 export mul_action (mul_smul) smul_comm_class (smul_comm)
 
+/--
+Frequently, we find ourselves wanting to express a bilinear map `M →ₗ[R] N →ₗ[R] P` or an
+equivalence between maps `(M →ₗ[R] N) ≃ₗ[R] (M' →ₗ[R] N')` where the maps have an associated ring
+`R`. Unfortunately, using definitions like these requires that `R` satisfy `comm_semiring R`, and
+not just `semiring R`. Using `M →ₗ[R] N →+ P` and `(M →ₗ[R] N) ≃+ (M' →ₗ[R] N')` avoids this
+problem, but throws away structure that is useful for when we _do_ have a commutative (semi)ring.
+
+To avoid making this compromise, we instead state these definitions as `M →ₗ[R] N →ₗ[S] P` or
+`(M →ₗ[R] N) ≃ₗ[S] (M' →ₗ[R] N')` and require `smul_comm_class S R` on the appropriate modules. When
+the caller has `comm_semiring R`, they can set `S = R` and `smul_comm_class_self` will populate the
+instance. If the caller only has `semiring R` they can still set either `R = ℕ` or `S = ℕ`, and
+`add_comm_monoid.nat_smul_comm_class` or `add_comm_monoid.nat_smul_comm_class'` will populate
+the typeclass, which is still sufficient to recover a `≃+` or `→+` structure.
+
+An example of where this is used is `linear_map.prod_equiv`.
+-/
+library_note "bundled maps over different rings"
+
 /-- Commutativity of actions is a symmetric relation. This lemma can't be an instance because this
 would cause a loop in the instance search graph. -/
 lemma smul_comm_class.symm (M N α : Type*) [has_scalar M α] [has_scalar N α]

src/linear_algebra/direct_sum/finsupp.lean

@@ -31,7 +31,7 @@ variables (R M) (ι : Type*) [decidable_eq ι]
 copies of M indexed by ι. -/
 def finsupp_lequiv_direct_sum : (ι →₀ M) ≃ₗ[R] ⨁ i : ι, M :=
 linear_equiv.of_linear
-  (finsupp.lsum (show ι → (M →ₗ[R] ⨁ i, M), from direct_sum.lof R ι _))
+  (finsupp.lsum ℕ (show ι → (M →ₗ[R] ⨁ i, M), from direct_sum.lof R ι _))
   (direct_sum.to_module _ _ _ finsupp.lsingle)
   (linear_map.ext $ direct_sum.to_module.ext _ $ λ i,
     linear_map.ext $ λ x, by simp [finsupp.sum_single_index])

src/linear_algebra/finsupp.lean

@@ -58,8 +58,9 @@ open_locale classical big_operators
 
 namespace finsupp
 
-variables {α : Type*} {M : Type*} {N : Type*} {R : Type*}
-variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
+variables {α : Type*} {M : Type*} {N : Type*} {R : Type*} {S : Type*}
+variables [semiring R] [semiring S] [add_comm_monoid M] [semimodule R M]
+variables [add_comm_monoid N] [semimodule R N]
 
 /-- Interpret `finsupp.single a` as a linear map. -/
 def lsingle (a : α) : M →ₗ[R] (α →₀ M) :=
@@ -288,30 +289,40 @@ begin
   exact linear_map.is_linear _
 end
 
+section lsum
+
+variables (S) [semimodule S N] [smul_comm_class R S N]
+
 /-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to
 `N` using `finsupp.sum`. This is an upgraded version of `finsupp.lift_add_hom`.
-We define this as an additive equivalence. For a commutative `R`, this equivalence can be
-upgraded further to a linear equivalence. -/
-def lsum : (α → M →ₗ[R] N) ≃+ ((α →₀ M) →ₗ[R] N) :=
+
+See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
+-/
+def lsum : (α → M →ₗ[R] N) ≃ₗ[S] ((α →₀ M) →ₗ[R] N) :=
 { to_fun := λ F, {
     to_fun := λ d, d.sum (λ i, F i),
     map_add' := (lift_add_hom (λ x, (F x).to_add_monoid_hom)).map_add,
     map_smul' := λ c f, by simp [sum_smul_index', smul_sum] },
   inv_fun := λ F x, F.comp (lsingle x),
   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 } }
+  map_add' := λ F G, by { ext x y, simp },
+  map_smul' := λ F G, by { ext x y, simp } }
 
-@[simp] lemma coe_lsum (f : α → M →ₗ[R] N) : (lsum f : (α →₀ M) → N) = λ d, d.sum (λ i, f i) := rfl
+@[simp] lemma coe_lsum (f : α → M →ₗ[R] N) : (lsum S f : (α →₀ M) → N) = λ d, d.sum (λ i, f i) :=
+rfl
 
 theorem lsum_apply (f : α → M →ₗ[R] N) (l : α →₀ M) :
-  finsupp.lsum f l = l.sum (λ b, f b) := rfl
+  finsupp.lsum S f l = l.sum (λ b, f b) := rfl
 
 theorem lsum_single (f : α → M →ₗ[R] N) (i : α) (m : M) :
-  finsupp.lsum f (finsupp.single i m) = f i m :=
+  finsupp.lsum S f (finsupp.single i m) = f i m :=
 finsupp.sum_single_index (f i).map_zero
 
-theorem lsum_symm_apply (f : (α →₀ M) →ₗ[R] N) (x : α) : lsum.symm f x = f.comp (lsingle x) := rfl
+theorem lsum_symm_apply (f : (α →₀ M) →ₗ[R] N) (x : α) :
+  (lsum S).symm f x = f.comp (lsingle x) := rfl
+
+end lsum
 
 section lmap_domain
 variables {α' : Type*} {α'' : Type*} (M R)
@@ -380,7 +391,7 @@ variables (α) {α' : Type*} (M) {M' : Type*} (R)
 
 /-- Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and
     evaluates this linear combination. -/
-protected def total : (α →₀ R) →ₗ[R] M := finsupp.lsum (λ i, linear_map.id.smul_right (v i))
+protected def total : (α →₀ R) →ₗ[R] M := finsupp.lsum ℕ (λ i, linear_map.id.smul_right (v i))
 
 variables {α M v}
 

src/linear_algebra/prod.lean

@@ -27,13 +27,6 @@ It contains theorems relating these to each other, as well as to `submodule.prod
   - `linear_map.prod_map`
   - `linear_equiv.prod_map`
   - `linear_equiv.skew_prod`
-
-## Implementation notes
-
-`linear_map.prod_equiv` and `linear_map.coprod_equiv` are `linear_equiv`s in `S` between
-`linear_map`s in `R`. When we have `comm_ring R`, `S = R` can be used (via `nat_smul_comm_class`).
-When we don't, these equivs can always be instantiated with `S = ℕ` (via
-`add_comm_monoid.nat_smul_comm_class`).
 -/
 
 universes u v w x y z u' v' w' y'
@@ -80,7 +73,9 @@ end
 by ext; refl
 
 /-- Taking the product of two maps with the same domain is equivalent to taking the product of
-their codomains. -/
+their codomains.
+
+See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
 @[simps] def prod_equiv
   [semimodule S M₂] [semimodule S M₃] [smul_comm_class R S M₂] [smul_comm_class R S M₃] :
   ((M →ₗ[R] M₂) × (M →ₗ[R] M₃)) ≃ₗ[S] (M →ₗ[R] M₂ × M₃) :=
@@ -143,7 +138,9 @@ theorem fst_eq_coprod : fst R M M₂ = coprod linear_map.id 0 := by ext; simp
 theorem snd_eq_coprod : snd R M M₂ = coprod 0 linear_map.id := by ext; simp
 
 /-- Taking the product of two maps with the same codomain is equivalent to taking the product of
-their domains. -/
+their domains.
+
+See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
 @[simps] def coprod_equiv [semimodule S M₃] [smul_comm_class R S M₃] :
   ((M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ≃ₗ[S] (M × M₂ →ₗ[R] M₃) :=
 { to_fun := λ f, f.1.coprod f.2,