Finite-dimensional vector spaces

[kbuzzard]

A proposal was that we use the resource "linear algebra done right". An example of a goal would be to define the determinant of a matrix and to prove det(AB)=det(A)det(B). Another example would be to prove the Jordan Canonical Form theorem -- this is the last theorem of M2PM2. But of course there are plenty of easier theorems -- Lean might even not have the rank-nullity theorem!

[kbuzzard]

@mn492 has thought about det(AB)=det(A)det(B) but this is hard. We have a proposed definition of signature of a permutation -- count number of (i,j) with i<j and sigma(i)>sigma(j). A lot of basic infrastructure needs doing.

@Blair-Shi has a lot of lemmas to prove -- she formalised the definition of a f.d.v.s but still a lot of infrastructure needs doing. @dorhinj maybe you will need this at some point if you're doing number fields?

[kbuzzard]

OK so over lunch today I thought a bit about finite dimensional vector spaces and their link to matrices. Here are some theorems which shouldn't be too hard to prove.

Let R be an arbitrary ring (not necessarily commutative). There is a general theory of modules over a ring. One can define R^n for n : nat as being the set of maps from (fin n) to R. This should be given the structure of an abelian group (pointwise addition on R -- don't ever use any structure on fin n other than the fact that it has n elements) and then R-module.

Next prove that if M is an a x b matrix with coefficients in R then it induces a map f(M) : R^b -> R^a. Construct this as a definition -- a function from a x b matrices to R-linear maps R^b -> R^b. Conversely define a map which takes an R-linear map f R^b -> R^a and produces an a x b matrix M(f) [pretend R is a field; the general case is the same, I don't think you use commutativity or anything]. fin n is decidable so there should be no problem defining maps like "1 if i.val = m and 0 otherwise".

Now prove that this gives an equiv between a x b matrices and R-linear maps R^b -> R^a by proving that the composite in both directions is the identity. M o f = id and f o M = id

Now prove that both functions are abelian group homomorphisms.

Now prove that the functions preserve product, i.e. prove that if f : R^b -> R^a and g : R^c -> R^b then the composite f o g : R^c -> R^a has matrix M(f o g) equal to the product of the corresponding matrices M(f) * M(g). You also need the statement the other way -- f(M * N) = f(M) o f(N). This might be slightly trickier to prove -- can you deduce it from the previous statement and the fact that you have an equiv?

Now assume that R is commutative. Define an R-module structure on Hom(R^b,R^a) and prove that it matches with the R-module structure on the set of a x b matrices.

---

Now when we have finite-dimensional vector spaces over a field k, to link them to matrices all one has to do is to prove that a basis v1,v2,...,vn of a fdvs V/k is just an isomorphism k^n -> V. Then one can port the link between k^n and matrices to a general link between linear maps and matrices easily.

[kbuzzard]

So @mn492 proved the equiv! Nice work Keji! There was the added twist that to make it work in the non-commutative case he had to use row vectors and make the matrices act on the right. So there's an added extra job for this list -- defining the usual left action of matrices on vectors -- which one can do easily with a transpose trick. I guess one also has to prove that M(Nv)=(MN)v but this could be done easily if one identifies vectors with n x 1 matrices...