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(category_theory/preadditive): Schur's lemma #7366

Closed
wants to merge 39 commits into from
Closed

[Merged by Bors] - feat(category_theory/preadditive): Schur's lemma #7366

wants to merge 39 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Apr 26, 2021 •
edited

We prove Schur's lemma for π•œ-linear categories with finite dimensional hom spaces,
over an algebraically closed field π•œ:
the hom space X ⟢ Y between simple objects X and Y is at most one dimensional,
and is 1-dimensional iff X and Y are isomorphic.

Open in Gitpod

@semorrison
feat(category_theory): definition of R-linear category
44bf1a6
@semorrison
Module R is R linear when R is commutative
625cbe7
@semorrison
refactor(linear_algebra/eigenspace): cleanup proof
84efc74
@semorrison
lint
9709d72
@semorrison
refactor(linear_algebra/eigenspace): refactor exists_eigenvalue
fe85e21
@semorrison
move slightly
508d60a
@semorrison
Merge branch 'cleanup_exists_eigenvalue' into exists_spectrum
a7e847a
@semorrison
Merge remote-tracking branch 'origin/master' into exists_spectrum
aa4072e
@semorrison
rename
f5098a3
@semorrison
lint
f455f23
@semorrison
Merge remote-tracking branch 'origin/master' into cleanup_exists_eige…
4186bca 
…nvalue
@semorrison
merge
099a137
@semorrison
Merge branch 'linear_category' into schur2
84a9a1b
@semorrison
.
65916b3
@semorrison
uhoh, we're going to need replace_algebra_def
9df9fb1
@semorrison
.
8484078
@semorrison
???
261314d
@semorrison
yay, hopefully downhill from here
5393777
@semorrison
feat(linear_algebra/finite_dimensional): characterizations of findim …
dc1a830 
…= 1 and ≀ 1
@semorrison
Merge branch 'findim_le_one' into schur2
157614e
@semorrison
merge
8d16b1c
@semorrison
.
b0f8249
@semorrison
Merge branch 'findim_le_one' into schur2
0cfb772
@semorrison
more on finrank
7636691
@semorrison
docstrings
0abe864
@semorrison
docstrings
720481c
@semorrison
refactor, iff
e53d6d2
@semorrison
no more sorries
827abd5
@semorrison
doc-strings
7280db1
@semorrison
Merge remote-tracking branch 'origin/master' into schur2
a372aa2
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Apr 28, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels May 1, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 2, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels May 2, 2021
@github-actions
Copy link

github-actions bot commented May 2, 2021

πŸŽ‰ Great news! Looks like all the dependencies have been resolved:

πŸ’‘ To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 2, 2021
@semorrison semorrison added the awaiting-review The author would like community review of the PR label May 2, 2021
Vierkantor
Vierkantor approved these changes May 3, 2021
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.

LGTM, although I don't know much about the category theory library so I'll ask a second reviewer.

@Vierkantor Vierkantor requested a review from jcommelin May 3, 2021 08:38
jcommelin
jcommelin approved these changes May 3, 2021
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks πŸŽ‰

bors merge

bors bot pushed a commit that referenced this pull request May 3, 2021
@semorrison
feat(category_theory/preadditive): Schur's lemma (#7366)
7da8303 
We prove Schur's lemma for `π•œ`-linear categories with finite dimensional hom spaces,
over an algebraically closed field `π•œ`:
the hom space `X ⟢ Y` between simple objects `X` and `Y` is at most one dimensional,
and is 1-dimensional iff `X` and `Y` are isomorphic.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@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 May 3, 2021
@bors
Copy link

bors bot commented May 3, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/preadditive): Schur's lemma [Merged by Bors] - feat(category_theory/preadditive): Schur's lemma May 3, 2021
@bors bors bot closed this May 3, 2021
@bors bors bot deleted the schur2 branch May 3, 2021 17:06
@semorrison semorrison mentioned this pull request Apr 29, 2022
Closed
2 tasks
bors bot pushed a commit that referenced this pull request Nov 3, 2022
@semorrison
feat(representation_theory/fdRep): Schur's lemma (#13794)
b943047 
In fact, we've had Schur's lemma in mathlib for over a year, since #7366, but this was stated very abstractly: for any linear category over an algebraically closed field with finite dimensional hom spaces, and kernels.

Finally, `fdRep k G` satisfies all those hypotheses, so we can use Schur's lemma!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

@jcommelin jcommelin jcommelin approved these changes

@winston-h-zhang winston-h-zhang Awaiting requested review from winston-h-zhang

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
3 participants
@semorrison @Vierkantor @jcommelin