Zulip Chat Archive

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

Johan Commelin (Sep 29 2020 at 15:19):

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: Dec 20 2023 at 11:08 UTC