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
[Merged by Bors] - feat: if a Lie algebra has non-degenerate Killing form then its Cartan subalgebras are Abelian #8430
Conversation
The real problem here is that the definition of `DirectSum.IsInternal.collectedBasis` commits definitional abuse by using `DFinsupp.mapRange.linearEquiv` on terms which are of type `DirectSum` rather than `DFinsupp`. One way to avoid this would be to duplicate the API for `DFinsupp.mapRange` in terms of `DirectSum` and use this in `collectedBasis`.
…rMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal'`
…n subalgebras are Abelian Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.
This PR/issue depends on: |
Can this proof be improved?
@@ -453,6 +453,13 @@ theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} ( | |||
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩ | |||
#align direct_sum.is_internal_submodule_iff_is_compl DirectSum.isInternal_submodule_iff_isCompl | |||
|
|||
-- Controversial lemma (EricW not a fan). Let's use to get sorry-free and then reconsider |
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.
This lemma was excised from a previous PR #8369
@eric-wieser raised some good points about how we should prove this lemma here
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.
Now that this PR compiles, what is the status here?
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 have removed this code comment in the commit 4f9a599
I believe Eric's position was that it might be worth proving this lemma without using DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top
so that we would be able to apply it to additive monoids. I feel this is a large detour considering we have no application in mind and this is only a two-line proof. However I recognise his position is reasonable.
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.
Ok, then I'm going to merge. We can refactor later if needed.
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.
There's one open conversation. The rest LGTM.
@@ -453,6 +453,13 @@ theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} ( | |||
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩ | |||
#align direct_sum.is_internal_submodule_iff_is_compl DirectSum.isInternal_submodule_iff_isCompl | |||
|
|||
-- Controversial lemma (EricW not a fan). Let's use to get sorry-free and then reconsider |
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.
Now that this PR compiles, what is the status here?
This should be (and now is) raised on GitHub instead of in a code comment
Thanks 🎉 bors merge |
…n subalgebras are Abelian (#8430) Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.
Pull request successfully merged into master. Build succeeded: |
…n subalgebras are Abelian (#8430) Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.
…n subalgebras are Abelian (#8430) Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.
…n subalgebras are Abelian (#8430) Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.
Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.