[Merged by Bors] - refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting

[alreadydone]

Instead of using Submodule.map₂ (which doesn't apply in the noncommutative setting), redefine the Mul and SMul to be defeq to AddSubmonoid.mul. In general, if a semiring A is a module over a semiring R such that IsScalarTower R A A is true, then the product of a Submodule R A with a Set A will be a Submodule R A, but we do not need this heterogeneous multiplication yet. We mainly intend to apply this to the case A = R.

---

Preparation for the Hopkins–Levitzki theorem #17908. E.g. this is necessary to state that the Jacobson radical of an Artinian ring is nilpotent.

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

[github-actions]

PR summary 3c5a448021

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance : NonUnitalSemiring (Submodule R A)
+ instance : Pow (Submodule R A) ℕ
+ instance : SMul (Ideal R) (Submodule R M)
+ instance [NoZeroDivisors R] : NoZeroDivisors (Ideal R)
+ instance {S A : Type*} [Semiring S] [SMul R S] [AddCommMonoid A] [Module R A] [Module S A]
+ mul_eq_map₂
+ npowRec_add
+ npowRec_succ
+ pow_eq_npowRec
+ pow_one
+ pow_succ
+ pow_zero
+ smul_eq_map₂
+ smul_toAddSubmonoid
- hasSMul'
- instance : Mul (Ideal R)
- instance {R : Type*} [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R)
- instance {R : Type*} [CommSemiring R] {S : Type*} [CommRing S] [Algebra R S]

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 script/declarations_diff.sh contains some details about this script.

[jjaassoonn]

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

[alreadydone]

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.

[mathlib4-dependent-issues-bot]

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!

[jcommelin]

[...] 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

[alreadydone]

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.

[eric-wieser]

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

[alreadydone]

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

Okay, opened #18419 for that.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style