PR summary 3c5a448021

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

I might have get the situation completely wrong.
I think now the assumption in "ideal R \bu Submodule R A" is exactly the same as "Set R \bu Submodule R A"in Submodule.pointwiseSetSMul; do we still need "ideal \bu Submodule R A" at all

I might have get the situation completely wrong. I think now the assumption in "ideal R \bu Submodule R A" is exactly the same as "Set R \bu Submodule R A"in Submodule.pointwiseSetSMul; do we still need "ideal \bu Submodule R A" at all

It's true that Ideal R \bu Submodule R A can be made a special case of Set R \bu Submodule R A under the current definition of Set R \bu Submodule R A, but I think maybe Set R \bu Submodule R A should only be defined for commutative R. Under mathematical convention, S • M consists of finite sums of products of the form s • m with s in S and m in M. When M is a R-submodule, S • M is also a R-submodule if R is commutative, but may not be in general, unless you artificially take the R-span, which is equivalent to what you do in Submodule.pointwiseSetSMul. This makes S • M (as a set) dependent on R, and deviates from mathematical convention.

My definition when specialized to the situation Ideal R \bu Ideal R is defeq to the multiplication Submodule R R * Submodule R R (also generalized to noncommutative setting in this PR). My Ideal R \bu Submodule R A factors through AddSubmonoid R \bu AddSubmonoid A and Submodule R A * Submodule R A factors through AddSubmonoid A * AddSubmonoid A, ensuring they don't rely on the R-action. This feature results in nice defeq properties (better than the original map₂ definition) and allows restrictScalars_mul etc. to be proven by rfl.

This PR/issue depends on:

• [Merged by Bors] - refactor: change the definition of 1 : Submodule R A to the range of (· • 1) #18092
• [Merged by Bors] - refactor: redefine Module.annihilator using RingHom.ker #18094
• [Merged by Bors] - feat: SMul instance for AddSubmonoid and lemmas #18096
• [Merged by Bors] - refactor: generalize AddSubmonoid Mul lemmas to SMul #18278
  By Dependent Issues (🤖). Happy coding!

[...] due to the lack of a typeclass that provides both left and right distributivity for SMul (unless you go all the way to Module), not all lemmas can be generalized. It would still be possible to unify Submodule Mul and Ideal-Submodule SMul, by generalizing to SMul (Submodule R A) (Submodule R M) assuming Module A M and IsScalarTower R A M. This will require moving the SMul to the same file as Mul and earlier than Mul.

Please record these observations/todos in the module docstring un ## Implementation notes and/or ## Todo.

Otherwise, LGTM

I've implemented SMul (Submodule R A) (Submodule R M) in e5fd5d6 (should I merge?), so there's no need of the TODO. I'll add a comment (implementation note?) in the module docstring about AddSubmonoid SMul lemmas.

I worry that creates diamonds, so would prefer that commit to be reviewed separately

I worry that creates diamonds, so would prefer that commit to be reviewed separately

Okay, opened #18419 for that.

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style