Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space #4111

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space #4111

wants to merge 13 commits into from

Conversation

abentkamp
Copy link
Collaborator

@abentkamp abentkamp commented Sep 11, 2020 •
edited by jcommelin

@abentkamp abentkamp added the awaiting-review The author would like community review of the PR label Sep 11, 2020
@jcommelin jcommelin changed the title feature(linear_algebra/eigenspace): Add generalized eigenvectors span the entire space feature(linear_algebra/eigenspace): generalized eigenvectors span the entire space Sep 11, 2020
@jcommelin jcommelin mentioned this pull request Sep 11, 2020
Closed
abentkamp and others added 2 commits September 11, 2020 15:40
@abentkamp
axler ref
78f9b3b
@abentkamp @bryangingechen
fix citation
743bd6c 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@semorrison
Copy link
Collaborator

I wonder if we could go a bit further with consequences. e.g. for an end-user, knowing there is a direct sum decomposition into generalized eigenspaces is very helpful. I think you have the ingredients (disjointness and the supr = top statement).

(Doesn't need to happen in this PR, of course.)

@bryangingechen bryangingechen changed the title feature(linear_algebra/eigenspace): generalized eigenvectors span the entire space feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space Sep 12, 2020
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 14, 2020
@jcommelin
Copy link
Member

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234111

abentkamp and others added 2 commits September 14, 2020 11:28
@abentkamp @semorrison
Update src/linear_algebra/eigenspace.lean
b27105c 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@abentkamp @semorrison
Update src/linear_algebra/eigenspace.lean
4d1839c 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@abentkamp
Copy link
Collaborator Author

I wonder if we could go a bit further with consequences. e.g. for an end-user, knowing there is a direct sum decomposition into generalized eigenspaces is very helpful. I think you have the ingredients (disjointness and the supr = top statement).

(Doesn't need to happen in this PR, of course.)

That would be nice to have indeed! I have searched a bit just now, but could not find any lemma like "disjointness and supr = top implies direct sum decomposition". So it seems that some background library needs to be developed first to make this happen.

@abentkamp abentkamp added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 14, 2020
@abentkamp @eric-wieser
Update src/linear_algebra/eigenspace.lean
5397f9c 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Vierkantor
Vierkantor requested changes Sep 17, 2020
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good in general! Just a few nitpicks.

src/linear_algebra/basic.lean Outdated Show resolved Hide resolved
src/linear_algebra/eigenspace.lean Outdated Show resolved Hide resolved
src/linear_algebra/eigenspace.lean Outdated Show resolved Hide resolved
src/linear_algebra/eigenspace.lean Outdated Show resolved Hide resolved
src/ring_theory/algebra.lean
section ring
variables [comm_ring R] [comm_ring S] [ring A] [algebra R A]

lemma mul_sub_algebra_map_commutes (x : A) (r : R) :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is basically a case of commute.neg_right (in algebra.ring.basic).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

commute.neg_right is still pretty far away from what I actually need. What do you suggest concretely?

src/linear_algebra/eigenspace.lean Outdated Show resolved Hide resolved
src/linear_algebra/eigenspace.lean Outdated Show resolved Hide resolved
src/linear_algebra/eigenspace.lean Outdated Show resolved Hide resolved
@Vierkantor Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 17, 2020
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 19, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 19, 2020
@abentkamp abentkamp added the help-wanted The author needs attention to resolve issues label Sep 20, 2020
@abentkamp
Copy link
Collaborator Author

Does someone know what the linter is complaining about? The supposedly unused arguments definitely cannot be removed.

@bryangingechen
Copy link
Collaborator

I haven't checked in Lean, but maybe some of the new variables on line 49 are leading to duplicate instances later on?

@abentkamp
Copy link
Collaborator Author

Thanks @bryangingechen, that was the issue!

@abentkamp abentkamp removed the help-wanted The author needs attention to resolve issues label Sep 20, 2020
@abentkamp abentkamp added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 20, 2020
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 24, 2020
bors bot pushed a commit that referenced this pull request Sep 24, 2020
@abentkamp
feat(linear_algebra/eigenspace): generalized eigenvectors span the en…
e58649d 
…tire space (#4111)
@bors
Copy link

bors bot commented Sep 24, 2020

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 24, 2020
@abentkamp
feat(linear_algebra/eigenspace): generalized eigenvectors span the en…
29928ed 
…tire space (#4111)
@bors
Copy link

bors bot commented Sep 24, 2020

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 24, 2020
@abentkamp
feat(linear_algebra/eigenspace): generalized eigenvectors span the en…
ef18740 
…tire space (#4111)
@bors
Copy link

bors bot commented Sep 24, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space [Merged by Bors] - feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space Sep 24, 2020
@bors bors bot closed this Sep 24, 2020
@bors bors bot deleted the generalized-eigenspace branch September 24, 2020 05:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@semorrison semorrison semorrison left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@Vierkantor Vierkantor Vierkantor requested changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@abentkamp @semorrison @jcommelin @bryangingechen @eric-wieser @Vierkantor