feat(ring_theory/matrix): category of free modules; scalar matrices

[jcommelin]

Do we want to define the identity matrix in terms of scalar?

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

[johoelzl]

These are finitely generated free modules, aren't they?
Another option would be to use finsupp, and index by arbitrary types.
scalar is quiet unrelated to the category itself.

[jcommelin]

Yes, these are indeed finitely generated free modules. For arbitrary types we wouldn't have matrices as morphisms. (At least currently, matrices are only indexed by fintypes.)
I agree that scalar is unrelated. I do think it is useful. I was just trying to get stuff from kbb into mathlib. If thought these were too trivial to split.

[johoelzl]

So should it be called different?

[jcommelin]

Well, it is in the matrix namespace, so in that case I think it is fine. But we could call it finite_free_module or something like that...

[semorrison]

`fg_free_module`?

…

On Tue, Oct 2, 2018 at 10:18 PM Johan Commelin ***@***.***> wrote: Well, it is in the matrix namespace, so in that case I think it is fine. But we could call it finite_free_module or something like that... — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#375 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBL8WJe1do-pNr9DvrEtMd8rKlByPks5ug1mXgaJpZM4W8PJB> .

[jcommelin]

Sure, it's your code anyway (-; Feel free to reclaim it and push to the matrix branch on the community fork.

[digama0]

Superceded by #406 and #404. Try again later for the free_module stuff when we have a clearer idea of what to do with it.