matrices

Stream: Is there code for X?

[Alex Zhang]

Are the identity matrices and permutation matrices defined in mathlib?

[Yaël Dillies]

The identity matrix is simply 1 in the correct type. I don't know about permutation matrices.

[Johan Commelin]

perm.to_matrix would be a good definition. I don't think it exists yet.

[Anne Baanen]

At this moment you can compose docs#pequiv.to_matrix and docs#equiv.to_pequiv

[Anne Baanen]

See for example docs#matrix.det_permutation for how this is used

[Alex Zhang]

How about anything related to permutation equivalence or similarity of matrices?

[Scott Morrison]

Where is the correspondence between matrices and linear maps?

[Scott Morrison]

matrix/to_lin.lean.

[Scott Morrison]

Ugh, this is too horrible. I want to use the fact that invertible matrices over a ring with invariant basis number are square. However our definition of IBN is in terms of linear maps, not matrices. So fine, you say, let's use matrix.to_lin' and linear_map.to_matrix' to convert. However, these are set up as R-linear equivalences, and in order to have that, whoever wrote the file assumed the ring was commutative. This means that I can't cope with division rings. Now everything is fine, you can define matrix.to_lin' as an additive equivalence just fine when R is non-commutative (and it still plays well with composition/matrix multiplication). But it means that I need to rip out and rewrite linear_algebra/matrix/to_lin.lean to handle noncommutative rings... :-(

[Scott Morrison]

Oh ****, it's even worse than that. Because we've set up the scalar action of a ring on functions to that ring by left multiplication (perfectly reasonably), if we want to convert a matrix to an R-linear map we need to use matrix.vec_mul, not matrix.mul_vec. Making that change at this point is too horrible to contemplate right now.

[Scott Morrison]

I am going to go to sleep and hope that in the meantime someone says "oh, I love doing refactors like that".

[Eric Wieser]

docs#matrix.to_lin could be a made a linear map over a different ring

[Scott Morrison]

We just need to get on with the bimodule / two-sided scalar actions refactor. Given a not-necessarily-commutative ring R, R is an R-R bimodule, and functions X -> R are an R-R bimodule, and also has actions by matrices from the left and from the right. Acting by a matrix on the left gives a function X -> R to Y -> R, and this is linear with respect to the right action by R. Conversely on the other side.

[Scott Morrison]

We need to admit to these facts in linear_algebra/matrix/to_lin.lean. :-)

[Scott Morrison]

A good challenge, I think, is proving that invertible matrices over a ring with invariant basis number are square. This is absolutely maths-trivial, but unspeakable in current mathlib.

[Eric Wieser]

I think we have all the pieces you need for the bimodules spelling already

[Eric Wieser]

You can make to_lin a (n → R) →ₗ [Rᵐᵒᵖ] (n → R) today

[Eric Wieser]

Note that it's not possible to have an action of matrix m n R on n → R (at least, not a mul_action), because rectangular matrices have a type incompatible with has_mul

[Scott Morrison]

I don't mind that we can't have matrices act by a mul_action.

[Scott Morrison]

I've put up #13845, which illustrates the change I'd like: matrix.square_of_invertible to work without the commutativity assumption.

[Scott Morrison]

I don't think having to_lin' produce a (n → R) →ₗ [Rᵐᵒᵖ] (n → R) is actually that helpful. Instead I want to_lin to use vec_mul instead of mul_vec, but I have no idea how much refactoring that will take.

[Scott Morrison]

I guess there should just be two versions of to_lin', one via the right action (giving an R-linear map) and one via the left action (giving an R^mop-linear map).

[Eric Wieser]

My claim is that the one via the left action that we currently have is the map that people would expect to find, and that →ₗ [Rᵐᵒᵖ] is unhelpful only because we're missing generalizations elsewhere too

[Scott Morrison]

Okay, #13870 does the bare beginnings of this refactor, for now just giving me what I need to proceed with some representation theory, and an extensive note explaining what will need to happen later.

[James Wiles]

hey all, is there Lean code for matrices with strides and the concept of merging or mergeability?

[Eric Wieser]

Striding (at least in the numpy sense) is usually an implementation detail; but maybe this helps?

import Mathlib

def A : Matrix (Fin 2) (Fin 4) ℕ := !![1, 2, 3, 4; 5, 4, 6, 7]

-- Check what A is
#eval A

-- Take `A` in strides of 2
#eval Matrix.of fun (i : Fin 2) (j : Fin 2) => A i (j * 2)