[Merged by Bors] - feat(linear_algebra/matrix/nonsingular_inverse): 2×2 block triangular matrices are invertible iff their diagonal is #18849
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ck matrices with an invertible corner
… matrices are invertible iff their diagonal is This follows the pattern used for `submatrix` and `diagonal` of setting up ```lean invertible (from_blocks A B 0 D) ≃ invertible A × invertible D ``` and using it to prove ```lean is_unit (from_blocks A B 0 D) ↔ is_unit A ∧ is_unit D ``` These results fall out as the special case of the general formula; though my hope is that they can also be used to prove it.
eric-wieser
added
WIP
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
github-actions
bot
removed
the
awaiting-CI
eric-wieser
added
awaiting-CI
github-actions
bot
added
the
modifies-synchronized-file
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
awaiting-CI
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
eric-wieser
removed
the
modifies-synchronized-file
2 tasks
eric-wieser
added
awaiting-review
eric-wieser
added
the
wait-requested-on
Vierkantor
reviewed
Jun 9, 2023
| def invertible_of_from_blocks_zero₁₂_invertible | ||
| (A : matrix m m α) (C : matrix n m α) (D : matrix n n α) | ||
| [invertible (from_blocks A 0 C D)] : invertible A × invertible D := | ||
| { fst := invertible_of_right_inverse _ (⅟(from_blocks A 0 C D)).to_blocks₁₁ $ begin |
There was a problem hiding this comment.
I suppose here again a symmetry argument is too much work?
There was a problem hiding this comment.
Yes; combined with the fact that this is a definition, and the version derived with a symmetry argument is probably going to end up carrying data that doesn't quite match.
Vierkantor
reviewed
Jun 9, 2023
| /-- `invertible_of_from_blocks_zero₂₁_invertible` and `from_blocks_zero₂₁_invertible` form | ||
| an equivalence. -/ | ||
| def from_blocks_zero₂₁_invertible_equiv (A : matrix m m α) (B : matrix m n α) (D : matrix n n α) : | ||
| invertible (from_blocks A B 0 D) ≃ invertible A × invertible D := |
There was a problem hiding this comment.
I suppose iff wouldn't work here because the two sides aren't Prop-valued? Showing an equiv between two subsingletons seems overly complicated...
There was a problem hiding this comment.
Yes, exactly. The iff version is spelt with is_unit, but it's easiest to derive it from this result.
Vierkantor
reviewed
Jun 9, 2023
Comment on lines
158
to
164
| /-- When lowered to a prop, `matrix.from_blocks_zero₂₁_invertible_equiv` forms an `iff`. -/ | ||
| @[simp] lemma is_unit_from_blocks_zero₂₁ {A : matrix m m α} {B : matrix m n α} {D : matrix n n α} : | ||
| is_unit (from_blocks A B 0 D) ↔ is_unit A ∧ is_unit D := | ||
| by simp only [← nonempty_invertible_iff_is_unit, ←nonempty_prod, | ||
| (from_blocks_zero₂₁_invertible_equiv _ _ _).nonempty_congr] | ||
|
|
||
| /-- When lowered to a prop, `matrix.from_blocks_zero₁₂_invertible_equiv` forms an `iff`. -/ |
There was a problem hiding this comment.
I would write the docstrings so that these are the "main theorems". At least these are the ones I'd be looking for from a mathematician's point of view, and the _equiv forms feel more like implementation details.
Vierkantor
approved these changes
Jun 9, 2023
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jun 9, 2023
… matrices are invertible iff their diagonal is (#18849)
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
It's not clear to me whether it is easier to prove these results first, then combine the results to prove the contents of #18843; or to recover the lemmas in this PR as a special case of those. Unfortunately theinvertibleAPI makes this all rather unpleasant.In #19156 I was able to prove the general results in terms of these results; I needed to add a substantial amount of
invertibleboilerplate, but I think the result is more mathematically interesting than proving the general result with a pile of algebra and deriving special cases from it. So I think this PR should go ahead, and #18843 can be abandoned in favor of #19156