Zulip Chat Archive

Stream: Is there code for X?

Topic: Bilinear form on `finsupp`


view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip Eric Wieser (Mar 07 2021 at 17:49):

The first one is almost docs#matrix.to_bilin

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Mar 09 2021 at 18:25):

#6606


Last updated: May 07 2021 at 21:10 UTC