Bilinear form on `finsupp`

Stream: Is there code for X?

[Heather Macbeth]

I'd like to know that A : (α × α) → R induces a bilinear form on α →₀ R, where the operation is to take two elements p q : α →₀ R, and sum A (i, j) * p i * q j for all i : α. This doesn't seem to exist.

In fact I also can't seem to find the simpler fact that A : α → R induces an element of the dual of α →₀ R, where the operation is to take an element p : α →₀ R, and sum A i * p i for all i : α. This I might well have missed, since there are small amounts of finsupp material scattered across many files in the linear algebra library.

This came up while trying to extract some of the work in #6427 as general-purpose lemmas, cc @Thomas Browning.

[Heather Macbeth]

Here's messy code for the second one, as an illustration:

import linear_algebra.finsupp

variables {R : Type*} [comm_ring R]

noncomputable example {α : Type*} (A : α → R) : (α →₀ R) →ₗ[R] R :=
{ to_fun := λ p, p.sum (λ i x, A i * x),
  map_add' := begin
    intros p q,
    let g : α → R →+ R := λ i, (A i • (linear_map.id : R →ₗ[R] R)).to_add_monoid_hom,
    exact finsupp.sum_add_index' g
  end,
  map_smul' := begin
    intros c p,
    let g : α → R → R := λ i x, A i * x,
    have : ∀ i, g i 0 = 0 := by simp [g],
    convert finsupp.sum_smul_index this,
    change _ * _ = _,
    rw finsupp.mul_sum,
    congr,
    ext i x,
    simp [g, mul_comm, mul_assoc],
  end }

[Eric Wieser]

The first one is almost docs#matrix.to_bilin

[Heather Macbeth]

Yes, it would be nice if a lot of the matrix code worked for finsupp on an arbitrary type rather than just on a fintype!

[Kevin Buzzard]

This would be the theory of finite rank endomorphisms of a module. I've used these in a paper. They even have characteristic polynomials -- det(1-XL) makes sense if L is a finite rank linear map -- you restrict to any finite dimensional subspace containing the image and the resulting poly is independent of the choice

[Heather Macbeth]

#6606