## Stream: Is there code for X?

### Topic: Bilinear form on finsupp

#### Heather Macbeth (Mar 07 2021 at 17:38):

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 (Mar 07 2021 at 17:44):

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 (Mar 07 2021 at 17:49):

The first one is almost docs#matrix.to_bilin

#### Heather Macbeth (Mar 07 2021 at 17:50):

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 (Mar 07 2021 at 18:04):

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 (Mar 09 2021 at 18:25):

#6606

Last updated: May 07 2021 at 21:10 UTC