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(representation_theory): fdRep k G is k-linear with finite dimensional hom spaces #13789

Closed
wants to merge 91 commits into from
Closed

[Merged by Bors] - feat(representation_theory): fdRep k G is k-linear with finite dimensional hom spaces #13789

wants to merge 91 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Apr 29, 2022 •
edited by github-actions bot
Loading

@semorrison
feat(representation_theory): the category of group actions in a category
e3b13b1
@semorrison
fixes
04c528a
@semorrison
add Rep too
3ffd99e
@semorrison
limits and monoidal structure
1a1a839
@semorrison
line length
00c4e8b
@semorrison
solve timeouts
f516837
@semorrison
feat(category_theory/abelian): if D is abelian so is C ⥤ D
5045a1a
@semorrison
Merge branch 'semorrison/abelian_functor_category' into semorrison/Ac…
2b1bb22 
…tion-abelian
@semorrison
universe issues
af7d901
@semorrison
feat(representation_theory/Rep): Rep k G is abelian
c9a5ffd
@semorrison
merge
2186978
@semorrison
.
a3bf8b7
@semorrison
.
2074e89
@semorrison
lint
f54787a
@semorrison
lint
1d6ca12
@semorrison
refactor, add note explaining what's going on
66579dd
@semorrison
feat(category_theory/monoidal): transport rigid structure over an equ…
b65763b 
…ivalence
@semorrison
merge
7c342a5
@semorrison
Merge branch 'semorrison/Action' into semorrison/Rep-rigid
4c5d13c
@semorrison
move
e9f9e7a
@semorrison
Merge branch 'semorrison/transport-rigid' into semorrison/Rep-rigid
69e4356
@semorrison
oops
fdcc4b6
@semorrison
Merge branch 'semorrison/transport-rigid' into semorrison/Rep-rigid
8445e23
@semorrison
mostly there
eebd5f2
@semorrison
do it properly, and then finish dualising
c808422
@semorrison
instance names
d5b7094
@semorrison
merge
38c97b5
@semorrison
.
8172cfa
@semorrison
.
095f72a
@semorrison
oops, forgot the main file
969981a
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 13, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@antoinelab01
Copy link
Collaborator

antoinelab01 commented Aug 7, 2022 •
edited
Loading

This requires some changes to fit the subcategory refactor from #14767.

@antoinelab01 antoinelab01 mentioned this pull request Aug 13, 2022
Closed
2 tasks
@alexjbest alexjbest requested a review from a team as a code owner November 2, 2022 17:25
jcommelin
jcommelin approved these changes Nov 2, 2022
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 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

bors d=alexjbest

@bors
Copy link

bors bot commented Nov 2, 2022

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@bors
Copy link

bors bot commented Nov 2, 2022

✌️ alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Nov 2, 2022
@alexjbest
Copy link
Member

bors r+

bors bot pushed a commit that referenced this pull request Nov 3, 2022
@semorrison
feat(representation_theory): fdRep k G is k-linear with finite dimens…
ee89acd 
…ional hom spaces (#13789)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Nov 3, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(representation_theory): fdRep k G is k-linear with finite dimensional hom spaces [Merged by Bors] - feat(representation_theory): fdRep k G is k-linear with finite dimensional hom spaces Nov 3, 2022
@bors bors bot closed this Nov 3, 2022
@bors bors bot deleted the semorrison/fdRep-linear branch November 3, 2022 03:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dupuisf dupuisf dupuisf left review comments

@antoinelab01 antoinelab01 antoinelab01 left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@semorrison @mathlib-dependent-issues-bot @antoinelab01 @alexjbest @jcommelin @dupuisf @leanprover-community-bot-assistant