[Merged by Bors] - refactor: change the definition of 1 : Submodule R A to the range of (· • 1)#18092
[Merged by Bors] - refactor: change the definition of 1 : Submodule R A to the range of (· • 1)#18092alreadydone wants to merge 4 commits intomasterfrom
1 : Submodule R A to the range of (· • 1)#18092Conversation
PR summary 550d222677Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
1 : Submodule R A to the image of (· • 1)1 : Submodule R A to the range of (· • 1)
cc98b4e to
5c6ef2c
Compare
I don't think I agree with this outlook idealistically; the basic premise is that the "inclusion map" has the best defeq / is most simp-normal, so if it exists it's best to use it. However, I do agree that removing the It's perhaps too much work to allow it to hold up this PR, but I do think we should do it eventually. |
I think
Yeah probably we should do it eventually. @mariainesdff is visiting and when we talked she expressed the desire to have such a class in her work. I told her the ringHomEquivModuleIsScalarTower trick but I'm not sure how useful it is. I think there will be declarations that only require the SMul, which should only assume Module+IsScalarTower (like here), and declarations that only require the RingHom which should just use the RingHom (not a typeclass). For example, in Module.Finite.trans we wouldn't like to switch back to Algebra, even though the assumptions imply that |
|
I agree with Eric that this solution is definitely not ideal and we should be using a class with a usefully-defined inclusion map instead, even if perhaps it is just for the reason that this is morally supposed to be the "same", i.e. image, of On the other hand, I want that consideration to be remembered for future refactors, if we can ever make the inclusion work well. So I think it's okay to merge the PR with the |
Vierkantor
left a comment
There was a problem hiding this comment.
LGTM, thanks!
@eric-wieser, could you do the final review please?
|
Thanks 🎉 bors merge |
…f `(· • 1)` (#18092) Previously, it's defined to be the range of `algebraMap R A`. In the noncommutative setting, we want to write `1 : Ideal R` where `Ideal R := Submodule R R`, but `R` isn't an `R`-algebra if `R` is not commutative. If we were to introduce a new typeclass by removing the `commutes'` field from `Algebra`, we could keep the current definition, but I'd argue that it's still better to use SMul to define `1 : Submodule R A`, because `Submodule` only depends on the Module/SMul, not on the algebraMap/RingHom. Requires fixes in 11 other files.
|
Pull request successfully merged into master. Build succeeded: |
1 : Submodule R A to the range of (· • 1)1 : Submodule R A to the range of (· • 1)
Previously, it's defined to be the range of
algebraMap R A. In the noncommutative setting, we want to write1 : Ideal RwhereIdeal R := Submodule R R, butRisn't anR-algebra ifRis not commutative. If we were to introduce a new typeclass by removing thecommutes'field fromAlgebra, we could keep the current definition, but I'd argue that it's still better to use SMul to define1 : Submodule R A, becauseSubmoduleonly depends on the Module/SMul, not on the algebraMap/RingHom.Requires fixes in 11 other files.