feat(linear_algebra/matrix): define the trace of a square matrix

[ocfnash]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[jcommelin]

What you've written so far looks great to me. You could however add more simp lemmas for special cases: trace_zero, trace_one, trace_scalar etc... (edit: trace_neg)

[sgouezel]

I am not sure we need to have both trace and trace_hom: I would just go for the linear map version, and call it trace. Then all the simp lemmas trace_zero, trace_neg and so on become unnecessary, as they are already there, available for all linear functions.

diag should probably also be registered only as a linear map, by the way.

[jcommelin]

Sure, but trace_one and trace_scalar won't be automatic.

[ocfnash]

I am not sure we need to have both trace and trace_hom: I would just go for the linear map version, and call it trace. Then all the simp lemmas trace_zero, trace_neg and so on become unnecessary, as they are already there, available for all linear functions.

diag should probably also be registered only as a linear map, by the way.

I will happily reorganise you see fit but I was attempting to cater for matrices whose entries do not necessarily belong to a ring, (e.g., I would like this to work for a matrix of natural numbers).

[kbuzzard]

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear.20maps.20over.20semimodule

[ocfnash]

Given that it looks like we're not going to have linearity over semirings all that soon, I guess we have to choose between either:

• Having general trace, trace_hom as I proposed in my first commit, or
• Dropping support for matrices with entries of type add_comm_monoid

I have just added this commit which opts for the latter, as requested by @sgouezel

Note that I have thus omitted simp lemmas for trace_zero, trace_scalar, trace_neg since they all follow from the linearity and the included simp lemma trace_one. I.e., the following all compile:

lemma trace_zero [decidable_eq n] [ring R] :
  (trace : (matrix n n R) →ₗ[R] R) 0 = 0 := by simp

lemma trace_scalar [decidable_eq n] [ring R] (c : R) :
  (trace : (matrix n n R) →ₗ[R] R) (c • 1) = c * (fintype.card n) := by simp

lemma trace_neg [decidable_eq n] [ring R] (M : matrix n n R) :
  (trace : (matrix n n R) →ₗ[R] R) (-M) = -(trace : (matrix n n R) →ₗ[R] R) M := by simp

[ocfnash]

Hmm, I guess I've jumped over the half-way house of a matrix of elements of a module but I now note that the following instance does not exist:

instance matrix.module {R : Type v} {M : Type w} [ring R] [add_comm_group M] [module R M] :
  module R (matrix n n M) := infer_instance -- fails

I think I should add this instance (and likewise for semimodules) so this is still WIP I guess.

[ocfnash]

I have just pushed a commit to show how things look if we want to have diag and trace defined for module-valued matrices (rather than just ring-valued).

I think this is as far as I can take this without someone making a call on what looks best.

[jcommelin]

I think this looks good for now. We can generalise to semirings later.

[jcommelin]

I'm fine with this as it is.

My only remaining question is: do we want to have decidable_eq n or should we go classical?
@rwbarton @ChrisHughes24 @digama0

[ChrisHughes24]

I would prefer to make matrices classical. They are not a remotely efficient implementation anyway. I think that's a matter for another PR

[ChrisHughes24]

This is ready to merge, but it's not up to date and I can't update the branch because it's protected. @ocfnash could you update the branch or change some protection settings?

[ocfnash]

This is ready to merge, but it's not up to date and I can't update the branch because it's protected. @ocfnash could you update the branch or change some protection settings?

Thanks @ChrisHughes24 I have not intentionally enabled any protection settings, and GH claims to me that indeed I have none enabled, and yet I saw that GH was refusing to allow the merge. 🤷‍♂ In any case, I have merged latest master into this branch manually so hopefully that will unblock things.

[ocfnash]

Argh, still no success merging. On further inspection I have discovered (and ticked) the "Allow edits from maintainers" box:

So hopefully things should work now.

[eric-wieser]

I am not sure we need to have both trace and trace_hom: I would just go for the linear map version, and call it trace. Then all the simp lemmas trace_zero, trace_neg and so on become unnecessary, as they are already there, available for all linear functions.

diag should probably also be registered only as a linear map, by the way.

Note I ended up reverting this decision (#13687, #13712), it turned out to just be annoying to specify which ring we were talking about trace and diag being linear over, and wasn't consistent with other unbundled linear operations in the rest of the matrix api (diagonal, transpose, etc).