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.

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(representation_theory/basic): representation theory without scalar actions #13573

Closed
wants to merge 4 commits into from

Conversation

antoinelab01
Copy link
Collaborator

This PR rewrites the files representation_theory/basic and representation_theory/invariants so that they avoid making use of scalar actions. It also includes the new definitions and lemmas of PR #13502 written with this new approach.


Open in Gitpod

@antoinelab01 antoinelab01 added the awaiting-review The author would like community review of the PR label Apr 21, 2022
@semorrison
Copy link
Collaborator

I'm in favour!

@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 Apr 27, 2022
bors bot pushed a commit that referenced this pull request Apr 27, 2022
…ar actions (#13573)

This PR rewrites the files `representation_theory/basic` and `representation_theory/invariants` so that they avoid making use of scalar actions. It also includes the new definitions and lemmas of PR #13502 written with this new approach.



Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
@bors
Copy link

bors bot commented Apr 27, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(representation_theory/basic): representation theory without scalar actions [Merged by Bors] - feat(representation_theory/basic): representation theory without scalar actions Apr 27, 2022
@bors bors bot closed this Apr 27, 2022
@bors bors bot deleted the rep_theory_without_smul branch April 27, 2022 02:36
bors bot pushed a commit that referenced this pull request Apr 29, 2022
)

We define `Rep k G`, the category of `k`-linear representations of a monoid `G`.

Happily, by abstract nonsense we get that this has (co)limits and a monoidal structure for free.

This should play well with the new design for representations in #13573.




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
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
Development

Successfully merging this pull request may close these issues.

None yet

3 participants