extending a finitely support function over a sigma?

Stream: Is there code for X?

[Kim Morrison]

Do we already have

import Mathlib

def Finsupp.embSigma {k : κ} (f : ι k →₀ R) : (Σ k, ι k) →₀ R :=
  Finsupp.embDomain (Function.Embedding.sigmaMk k) f

somewhere, and hopefully its basic API?

[Eric Wieser]

I'd probably claim we don't need it, since the spelling is already pretty short:

import Mathlib

-- your example isn't a mwe without these
variable {κ} {ι : κ → Type*} [Zero R]

noncomputable def Finsupp.embSigma {k : κ} (f : ι k →₀ R) : (Σ k, ι k) →₀ R :=
  f.embDomain <| .sigmaMk k

[Eric Wieser]

The argument that it's not needed is even more compelling if it's argued that your function should be called embDomainSigmaMk for clarity

[Aaron Liu]

Why do we need this? Does this combination come up a lot?

[Kim Morrison]

I'm using this in a proposed formalisation of abstract convex spaces, where it seems to work nicely.

[Kim Morrison]

I've made #31923 in the meantime.

[Kim Morrison]

I can try inlining the definition again there and see if it adds any pain.