Finsupp.linearCombination backwards

Stream: Is there code for X?

[Peter Nelson]

docs#Finsupp.linearCombination has the following type signature:

def Finsupp.linearCombination {α M : Type*} (R : Type*) [Semiring R] [AddCommMonoid M]
 [Module R M] (v : α → M) :
(α →₀ R) →ₗ[R] M

Is there an easy way to talk about the natural linear map with the order of arguments reversed? Something like the following:

def Finsupp.linearCombinationReverse {α M : Type*} (R : Type*) [Semiring R] [AddCommMonoid M]
 [Module R M] (v : α →₀ R) :
(α → M) →ₗ[R] M

[Kevin Buzzard]

The easiest way to get this would be to make the term of type (α → M) →ₗ[R] (α →₀ R) →ₗ[R] M and then use API which already exists with names like flip or swap.

[Kevin Buzzard]

...and when I started trying to do this I ran into the fact that R wasn't commutative so perhaps that approach is off the table (assuming you care about the non-commutative case)

[Junyan Xu]

I think you're looking for Finsupp.llift. The SMulCommClass accommodates the non-commutative case (where the map isn't R-linear but you can still take e.g. S=Nat). LinearMap.flip also works under a SMulCommClass assumption.

[Kevin Buzzard]

So you don't need CommSemiring R for that but you do need [SMulCommClass R R M] which is basically the same thing? ("R acts on M via a commutative quotient")

[Junyan Xu]

I edited the post; I think in the noncommutative case you simply don't have a linear (α → M) → M but it's still an additive map which you can get by setting S=Nat.

[Kevin Buzzard]

aah so Peter is trolling us!

import Mathlib

noncomputable
def Finsupp.linearCombinationReverse {α M : Type*} (R : Type*) [Semiring R] [AddCommMonoid M]
    [Module R M] (v : α →₀ R) : (α → M) →ₗ[R] M where
  toFun φ := Finsupp.linearCombination R φ v
  map_add' φ ψ := sorry
  map_smul' r φ := by
    simp
    induction v using Finsupp.induction_linear with
    | h0 => simp
    | hadd => sorry
    | hsingle a s =>
        simp
        -- ⊢ s • r • φ a = r • s • φ a
        sorry

[Peter Nelson]

Sorry! I hadn't given thought to commutativity at all - I just copy-pasted the type signature from docs.

[Eric Wieser]

Kevin Buzzard said:

So you don't need CommSemiring R for that but you do need [SMulCommClass R R M] which is basically the same thing? ("R acts on M via a commutative quotient")

But you can pick S = MulOpposite R

[Kevin Buzzard]

The reason I stopped was that I was waiting for Peter to clarify if they were only interested in the commutative case

[Antoine Chambert-Loir]

I wonder whether the stuff we have for weighted degrees of polynomials isn't related to you question.

[Antoine Chambert-Loir]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finsupp/Weight.html#Finsupp.weight

[Antoine Chambert-Loir]

Is there a way to refactor docs#Finsupp.linearCombination to a general bilinear map that would get both cases at once? (Unclear)