# Zulip Chat Archive

## 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):

Last updated: May 07 2021 at 21:10 UTC