matrices = linear maps

Stream: Is there code for X?

[Kevin Buzzard]

If V and W are k-vector spaces with bases indexed by I and J, and if W is finite-dimensional then (unless I've made a mistake!) there's a linear equiv between V →ₗ[k] W and matrices with rows indexed by J and colums indexed by I. I couldn't find this in mathlib! mathlib's linear_map.to_matrix (to my surprise) has what seems to me to be a superfluous hypothesis that V is also finite-dimensional. Am I not looking in the right place? Discovered when preparing teaching material.

import linear_algebra.matrix.to_lin

variables (k V W I J : Type) [field k] [add_comm_group V] [add_comm_group W] [module k V]
  [module k W] (B : basis I k V) (C : basis J k W) [fintype J]

noncomputable example : (V →ₗ[k] W) ≃ₗ[k] matrix J I k :=
{ to_fun := λ φ j i, C.coord j (φ (B i)),
  map_add' := sorry,
  map_smul' := sorry,
  inv_fun := λ M, B.constr k $ λ i, (basis.equiv_fun C).symm (λ j, M j i),
  left_inv := sorry,
  right_inv := sorry }

[Eric Wieser]

docs#linear_map.to_matrix'?

[Eric Wieser]

I don't see the hypothesis you're claiming exists in docs#linear_map.to_matrix

[Jireh Loreaux]

Eric, both n and m are fintypes

[Eric Wieser]

Ah, I missed that Kevin's example has only J as a fintype

[Eric Wieser]

I think the answer is "matrix used to only be defined on fintype indices" (@Eric Rodriguez since relaxed it to only need that for multiplication)

[Eric Wieser]

And we didn't ever finish cleaning that up

[Kevin Buzzard]

Got it. I've since proved left_inv and right_inv so am more confident in my assertion :-)

[Eric Wieser]

I would guess you can just edit the version in mathlib and remove the fintype, and do this recursively on the things it complains about

[Kevin Buzzard]

I tried that but unfortunately it didn't converge

[Eric Wieser]

Do you have a branch I can look at?

[Kevin Buzzard]

At some point you have to start changing I -> V to finsupp I V

[Eric Wieser]

Even for linear_map.to_matrix?

[Kevin Buzzard]

By which I mean "almost immediately"

[Eric Wieser]

It sounds like you removed both fintype assumptions but should have kept one like you did in your example?

[Jireh Loreaux]

Right, in general it's going to be (V →ₗ[k] W) ≃ₗ[k] I → (J →₀ k), right?

[Kevin Buzzard]

I'm on mobile so all I see is weird rectangles but counting the rectangles I'm going to say "yes"

[Kevin Buzzard]

Yes that's the result one should have without any fintype hypotheses and then if J is finite it's matrices

[Kevin Buzzard]

Eric the issue is that the argument in mathlib goes via functions which need to be changed to finsupps when you start dropping finiteness hypothesis

[Jireh Loreaux]

But that's only a problem for that declaration? After you finish that declaration it shouldn't be a problem anymore (except for the unused variables linter)

[Eric Wieser]

Kevin, is your version equal to the one in mathlib, or does it include a transpose?

[Jireh Loreaux]

They are the same