[Merged by Bors] - feat(data/matrix/rank): rank of Aᵀ ⬝ A and Aᴴ ⬝ A
#18818
Conversation
eric-wieser
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
|
That's a strange proof. If you're working over a field, why not first do Gaussian reduction to reduce to a diagonal-like matrix, and then argue by hand in this case? |
|
I agree that this proof is a bit strange. However, I think we probably still want a proof of So do you agree it's just the proof of |
|
Yes, we definitely want A better proof and statement for |
eric-wieser
changed the title
Aᵀ ⬝ A and Aᴴ ⬝ A
Done. I haven't attempted to expand the TODO comments yet, but there should at least be one in each place now. |
| variables [fintype m] [field R] [partial_order R] [star_ordered_ring R] | ||
|
|
||
| lemma ker_mul_vec_lin_conj_transpose_mul_self (A : matrix m n R) : | ||
| linear_map.ker (Aᴴ ⬝ A).mul_vec_lin = linear_map.ker (mul_vec_lin A):= |
There was a problem hiding this comment.
Not directly related to this PR, but I find that mul_vec_lin instead of to_lin is really obscure here. To avoid the decidable equality issue, I'd rename the current to_lin as equiv_lin and use to_lin for, well, turning a matrix into a linear map (i.e., the current mul_vec_lin)...
There was a problem hiding this comment.
If we want to do that it should be ASAP, as the file defining to_lin is almost ready to port.
The header comment is already full of refactor ideas corresponding to non-commutative rings, suggesting that we maybe have picked the wrong operator for to_lin...
There was a problem hiding this comment.
I think it's better to keep this for after the port, no need to delay things unnecessarily.
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
| /-! ### Lemmas about transpose and conjugate transpose | ||
|
|
||
| This section contains lemmas about the rank of `matrix.transpose` and `matrix.conj_transpose`. | ||
|
|
||
| Unfortunately the proofs are essentially duplicated between the two; `ℚ` is a linearly-ordered ring | ||
| but can't be a star-ordered ring, while `ℂ` is star-ordered (with `open_locale complex_order`) but | ||
| not linearly ordered. For now we don't prove the transpose case for `ℂ`. | ||
|
|
||
| TODO: the lemmas `matrix.rank_transpose` and `matrix.rank_conj_transpose` current follow a short | ||
| proof that is a simple consequence of `matrix.rank_transpose_mul_self` and | ||
| `matrix.rank_conj_transpose_mul_self`. This proof pulls in unecessary assumptions on `R`, and should | ||
| be replaced with a proof that uses Gaussian reduction or argues via linear combinations. | ||
| -/ |
There was a problem hiding this comment.
@sgouezel: I expanded this TODO comment. Happy with me merging?
|
I'll assume the TODO comment is fine. bors merge |
github-actions
bot
added
the
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Aᵀ ⬝ A and Aᴴ ⬝ AAᵀ ⬝ A and Aᴴ ⬝ A
Since these results imply it trivially, this also includes lemmas about the rank of
AᵀandAᴴ.However, these lemmas are not stated very generally, and are surely true in wider cases than the ones proven here.