[Merged by Bors] - chore(algebra/algebra/restrict_scalars): put a right action on restricted scalars #13996
Conversation
semorrison
added
the
awaiting-review
| instance restrict_scalars.op_module [module Sᵐᵒᵖ M] : module Rᵐᵒᵖ (restrict_scalars R S M) := | ||
| begin | ||
| letI : module Sᵐᵒᵖ (restrict_scalars R S M) := ‹module Sᵐᵒᵖ M›, | ||
| exact module.comp_hom M (algebra_map R S).op | ||
| end |
There was a problem hiding this comment.
Oh, I am surprised by this one!
If something happens to have both an S and an Smop action, why would restricting scalars for the S action also restrict the Smop action? In particular, a common application in my mind (from the theory of subfactors) is an inclusion of algebras A into B naturally giving us the A-B bimodule B. (Where we start with B as a B-B bimodule, and then restrict the left action.)
There was a problem hiding this comment.
I would have said that if you have commuting actions on the original module of any two rings, and you restrict one of them, you still have a commuting action with the other ring. (In fact, when I read the title and PR description this is what I was expecting to see.)
There was a problem hiding this comment.
The motivation for this is #10716, where I need both a left and right action in order for restrict_scalars S R A to be considered an S-algebra. This comes up immediately; restrict_scalars.lsmul : S →ₐ[R] module.End R (restrict_scalars R S M) only makes sense if (restrict_scalars R S M) is a bimodule, as otherwise module.End.algebra can't exist.
I would have said that if you have commuting actions on the original module of any two rings, and you restrict one of them, you still have a commuting action with the other ring.
Sure, but we can't even state the actions commute without first copying them across; and we can't copy across all of them, as:
- This would create diamonds if
Malready has anS-action - This would entail copying across the
R-action onMwhich you just removed.
There was a problem hiding this comment.
Discussion continued on zulip.
semorrison
added
awaiting-author
eric-wieser
added
awaiting-review
|
bors merge |
github-actions
bot
added
ready-to-merge
…cted scalars (#13996) This provides `module Rᵐᵒᵖ (restrict_scalars R S M)` in terms of a `module Sᵐᵒᵖ M` action, by sending `Rᵐᵒᵖ` to `Sᵐᵒᵖ` through `algebra_map R S`. This means that `restrict_scalars R S M` now works for right-modules and bi-modules in addition to left-modules. This will become important if we change `algebra R A` to require `A` to be an `R`-bimodule, as otherwise `restrict_scalars R S A` would no longer be an algebra. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313996.20right.20actions.20on.20restrict_scalars/near/282045994)
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This provides
module Rᵐᵒᵖ (restrict_scalars R S M)in terms of amodule Sᵐᵒᵖ Maction, by sendingRᵐᵒᵖtoSᵐᵒᵖthroughalgebra_map R S.This means that
restrict_scalars R S Mnow works for right-modules and bi-modules in addition to left-modules.This will become important if we change
algebra R Ato requireAto be anR-bimodule, as otherwiserestrict_scalars R S Awould no longer be an algebra.Zulip