-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(linear_algebra/matrix): define the trace of a square matrix #1883
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
)
I am not sure we need to have both
|
Sure, but |
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). |
Given that it looks like we're not going to have linearity over
I have just added this commit which opts for the latter, as requested by @sgouezel Note that I have thus omitted simp lemmas for 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 |
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 |
I have just pushed a commit to show how things look if we want to have I think this is as far as I can take this without someone making a call on what looks best. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this looks good for now. We can generalise to semirings later.
Co-Authored-By: Johan Commelin <johan@commelin.net>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
I would prefer to make matrices classical. They are not a remotely efficient implementation anyway. I think that's a matter for another PR |
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. |
…matrices. (#1913) * feat(linear_algebra/matrix): trace AB = trace BA * Remove now-redundant matrix.smul_sum In a striking coincidence, #1910 was merged almost immediately before #1883 thus rendering matrix.smul_sum redundant. * Make arguments explicit for matrix.trace, matrix.diag * Tidy up whitespace * Remove now-redundant type ascriptions * Update src/linear_algebra/matrix.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Feedback from code review * Generalize diag_transpose, trace_transpose. With apologies to the CI for triggering another build :-/ * Explicit arguments trace, diag defs but not lemmas Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…nprover-community#1883) * feat(linear_algebra/matrix): define the trace of a square matrix * Move ring carrier to correct universe * Add lemma trace_one, and define diag as linear map * Define diag and trace solely as linear functions * Diag and trace for module-valued matrices * Fix cyclic import * Rename matrix.mul_sum' --> matrix.smul_sum Co-Authored-By: Johan Commelin <johan@commelin.net> * Trigger CI Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…matrices. (leanprover-community#1913) * feat(linear_algebra/matrix): trace AB = trace BA * Remove now-redundant matrix.smul_sum In a striking coincidence, leanprover-community#1910 was merged almost immediately before leanprover-community#1883 thus rendering matrix.smul_sum redundant. * Make arguments explicit for matrix.trace, matrix.diag * Tidy up whitespace * Remove now-redundant type ascriptions * Update src/linear_algebra/matrix.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Feedback from code review * Generalize diag_transpose, trace_transpose. With apologies to the CI for triggering another build :-/ * Explicit arguments trace, diag defs but not lemmas Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…nprover-community#1883) * feat(linear_algebra/matrix): define the trace of a square matrix * Move ring carrier to correct universe * Add lemma trace_one, and define diag as linear map * Define diag and trace solely as linear functions * Diag and trace for module-valued matrices * Fix cyclic import * Rename matrix.mul_sum' --> matrix.smul_sum Co-Authored-By: Johan Commelin <johan@commelin.net> * Trigger CI Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…matrices. (leanprover-community#1913) * feat(linear_algebra/matrix): trace AB = trace BA * Remove now-redundant matrix.smul_sum In a striking coincidence, leanprover-community#1910 was merged almost immediately before leanprover-community#1883 thus rendering matrix.smul_sum redundant. * Make arguments explicit for matrix.trace, matrix.diag * Tidy up whitespace * Remove now-redundant type ascriptions * Update src/linear_algebra/matrix.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Feedback from code review * Generalize diag_transpose, trace_transpose. With apologies to the CI for triggering another build :-/ * Explicit arguments trace, diag defs but not lemmas Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Note I ended up reverting this decision (#13687, #13712), it turned out to just be annoying to specify which ring we were talking about |
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list