[Merged by Bors] - refactor(algebra/algebra/basic): change submodule.restrict_scalars to use is_scalar_tower #6745
Conversation
… use is_scalar_tower
eric-wieser
force-pushed
the
eric-wieser/submodule.restrict_scalars'
branch
from
c1122fe
to
51c2e1b
Compare
eric-wieser
added
the
awaiting-review
src/algebra/algebra/basic.lean
Outdated
| @@ -1449,54 +1449,72 @@ restrict_scalars.is_scalar_tower R A V | |||
|
|
|||
| end type_synonym | |||
|
|
|||
| /-! TODO: The following lemmas no longer involve `algebra` at all, and could be moved elsewhere. -/ | |||
There was a problem hiding this comment.
I agree with the TODO: could you put them in algebra/module/submodule.lean? (It looks like there is no import needed to make the definitions work there.)
There was a problem hiding this comment.
ker and range don't exist yet in that file, as they're defined in linear_algebra/basic.
There was a problem hiding this comment.
That's annoying. I guess they can stay here, with a TODO to move them once ker and range are moved somewhere else in the hierarcjy.
src/algebra/algebra/basic.lean
Outdated
| variables (R A M N : Type*) [comm_semiring R] [semiring A] [algebra R A] | ||
| variables [add_comm_monoid M] [semimodule R M] [semimodule A M] [is_scalar_tower R A M] | ||
| variables [add_comm_monoid N] [semimodule R N] [semimodule A N] [is_scalar_tower R A N] | ||
| variables (S R M N : Type*) [semiring S] [semiring R] [has_scalar S R] |
There was a problem hiding this comment.
It is mildly irritating that there is a has_scalar S R instance here, where usually we assume has_scalar R S (or algebra R S), see e.g. monoid_algebra.lean, linear_algebra/matrix.lean, algebra/tower.lean, finsupp.smul_comm_class, ...
If we're going to move the definitions anyway, it will blow away the history anyway, so there is no need to preserve the previous variable names.
There was a problem hiding this comment.
My thinking here was to have the "main" submodule continue to be a submodule R M, rather than switching to submodule S M here.
I can use R' instead of S if that's less objectionable?
There was a problem hiding this comment.
it will blow away the history anyway
My intent in modifying these in place was to not blow away history and change type-class paths in the same PR; just in case this breaks someone and they end up having to bisect.
There was a problem hiding this comment.
My thinking here was to have the "main" submodule continue to be a
submodule R M, rather than switching tosubmodule S Mhere.
I have to admit I don't see why this is important, but has_scalar R' R is fine to me as well.
There was a problem hiding this comment.
My intent in modifying these in place was to not blow away history and change type-class paths in the same PR; just in case this breaks someone and they end up having to bisect.
When I find the PR that breaks my code in bisection, I look at the discussion on github. So as long as the change happens in multiple commits in the PR, I can figure out what happened. But I see how this can be annoying to do.
How about this: change the TODO: move this comment to something like TODO: move this to a suitable file once linear_map.keris split fromlinear_algebra/basic.lean`, so that we can tell in the future if we can do the move yet.
Vierkantor
added
awaiting-author
github-actions
bot
added
ready-to-merge
… use is_scalar_tower (#6745)
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
I'm not 100% certain that this actually weakens the requirements in a meaningful way; but it definitely allows both
RandSto be non-commutative, which previously they were not.