## Stream: general

### Topic: Refactoring linear_map <-> matrix

#### Anne Baanen (Sep 29 2020 at 11:15):

Here's a refactor I would like to propose, to standardise and simplify going from matrices to linear maps and vice versa.

• linear_map.to_matrix will be the main definition, an equivalence between M₁ →ₗ[R] M₂ and matrix m n R, given bases for M₁ and M₂.
• matrix.to_lin is linear_map.to_matrix.symm
• linear_map.to_matrix' and matrix.to_lin' are the equivalences between ((n → R) →ₗ[R] (m → R)) and matrix m n R in the respective directions
• we keep matrix.mul_vec because its definition comes before linear_map
• other auxiliary definitions (e.g. the current linear_map.to_matrixₗ) will be simped to the above.

(The current situation is that we have matrix.mul_vec, matrix.eval, matrix.to_lin, linear_map.to_matrixₗ, linear_map.to_matrix, linear_equiv_matrix' and linear_equiv_matrix, each with various choices among →, →ₗ and ≃ₗ for the arrows. The most powerful, linear_equiv_matrix, is also the most inconvenient to type.)

#### Patrick Massot (Sep 29 2020 at 11:52):

I don't know what is the solution, but I very much agree that what we currently have is a mess that is very hard to navigate.

#### Anne Baanen (Sep 29 2020 at 15:18):

linear_algebra/matrix.lean compiles again: https://github.com/leanprover-community/mathlib/commit/b0375d38069d44dae15e78589bc0ab97137b6437

Cool!

#### Anne Baanen (Oct 05 2020 at 14:20):

Two more refactorings I would like to propose now #4345 is merged:

• split linear_algebra/basic.lean and linear_algebra/basis.lean into more manageably sized files
• rename module_equiv_finsupp to is_basis.repr (replacing the previous is_basis.repr) and figure out what to do with is_basis.equiv_fun

#### Patrick Massot (Oct 05 2020 at 14:27):

I don't understand the second point. We still need a version that applies in infinite dimensions, right?

#### Patrick Massot (Oct 05 2020 at 14:27):

And of course I agree with the first point and I'm very grateful for your cleaning efforts.

#### Anne Baanen (Oct 05 2020 at 14:28):

Sorry, that should be module_equiv_finsupp instead of is_basis.equiv_fun.

#### Patrick Massot (Oct 05 2020 at 14:31):

Ok. It would be nice to figure out how to make that parallel track thing (finsupp vs function) less painful.

Last updated: May 13 2021 at 18:26 UTC