more theory about matrix traces #1979
Conversation
Signed-off-by: Ali Caglayan <[email protected]> <!-- ps-id: 58406d6d-8e5c-4897-91e9-52f1efd79b83 -->
Signed-off-by: Ali Caglayan <[email protected]>
| (** The trace of a matrix multiplication is the same as the trace of the reverse multiplication. *) | ||
| (** The trace of a matrix preserves addition. *) | ||
| Definition matrix_trace_plus {R : Ring} {n} (M N : Matrix R n n) | ||
| : matrix_trace (matrix_plus M N) = (matrix_trace M) + (matrix_trace N). |
There was a problem hiding this comment.
Why doesn't M + N work on the LHS? We should figure that out and use + here and in other places too.
There was a problem hiding this comment.
I didn't make those an instance, so unless they are x : abgroup_matrix they won't be interpreted that way. I can do a cleanup of that in another PR, it should be possible to make it work.
| unfold matrix_trace. | ||
| lhs nrapply path_ab_sum. | ||
| { intros i Hi. | ||
| by rewrite entry_Build_Matrix. } |
There was a problem hiding this comment.
It's too bad that none of our operations on vectors and matrices compute, requiring us to use things like entry_Build_Matrix. This is because we represent them with lists but work with them using functions on a prefix of nat. Would it work to define them to be functions on a prefix of nat? (Or should we use functions on Fin n?)
(This shouldn't block this PR, but is something to think about for the future.)
There was a problem hiding this comment.
I think we should be able to define a matrix as a finite map. IIRC it is possible to prove funext for functions from a finite domain so we could define matrices directly as functions. This would also generalise nicely to functions with finite support allowing us to write down examples of "infinite matrices" which provide nice counter examples in ring theory.
This will of course have to come later as I have to think about it some more.
There was a problem hiding this comment.
I actually experimented with this idea previously, but working with Fin was a bit more awkward and working directly with {k : nat & k < n} seemed much better. This is essentially what our matrix entry functions are mapping from.
Signed-off-by: Ali Caglayan <[email protected]>
We prove that: