Finsupp over LinearMap

Stream: Is there code for X?

[Junyan Xu]

I'm surprised nothing close to the following is in Mathlib (according to exact?/apply?):

import Mathlib

variable {R S M N ι : Type*} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N]

def LinearMap.eval (m : M) : (M →ₗ[R] N) →ₗ[S] N where
  toFun := (· m)
  map_add' := by simp
  map_smul' := by simp

/-- This is an isomorphism if ι is finite or if M is a finite R-module. -/
noncomputable def LinearMap.finsuppLinearMap : (ι →₀ M →ₗ[R] N) →ₗ[S] M →ₗ[R] ι →₀ N :=
  have := SMulCommClass.symm
  .flip
  { toFun := (Finsupp.mapRange.linearMap <| .eval ·)
    map_add' := fun _ _ ↦ by ext; simp [LinearMap.eval]
    map_smul' := fun _ _ ↦ by ext; simp [LinearMap.eval] }

Is there a more clever way to construct these?

[Eric Wieser]

I guess I'd expect that to be called LinearMap.finsupp to match LinearMap.pi

[Junyan Xu]

Oh, the first is actually .flip .id m.

[Eric Wieser]

Perhaps also docs#LinearMap.applyₗ'

[Junyan Xu]

LinearMap.applyₗ'
To make it S-linear we need to make SMulCommClass.symm a local instance.