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.

Also:

• Change the definition of 1 : Submodule R A from the range of algebraMap R A to the R-span of {1}, which requires fixing many downstream files, but this is the only reasonable definition in the noncommutative setting.

• Generalize some lemmas and SMul to AddSubmonoids

• Redefine (Sub)module.annihilator to work in the noncommutative setting using RingHom.ker; move it from Ideal/Operations to Ideal/Maps (which only imports Ideal/Operations) because RingHom.ker is defined there.

---

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: #18092
• [x] depends on: #18094
• [x] depends on: #18096

[github-actions[bot]]

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.

[jcommelin]

Thanks for this PR. I think it is doing good things. But it is also doing a lot. Could you please split the following parts off, into preparatory PRs?

* Change the definition of `1 : Submodule R A` from the range of `algebraMap R A` to the R-span of {1}, which requires fixing many downstream files, but this is the only reasonable definition in the noncommutative setting.

* Generalize some lemmas and SMul to AddSubmonoids

* Redefine `(Sub)module.annihilator` to work in the noncommutative setting using `RingHom.ker`; move it from Ideal/Operations to Ideal/Maps (which only imports Ideal/Operations) because `RingHom.ker` is defined there.

[alreadydone]

Thanks for this PR. I think it is doing good things. But it is also doing a lot. Could you please split the following parts off, into preparatory PRs?

Good idea; #18092, #18094 and #18096 are now created.

[alreadydone]

I did further refactoring and opened dependency PR #18278 (generalize AddSubmonoid Mul lemmas to SMul). The benefit is that the AddSubmonoid SMul lemmas can be applied to both Submodule Mul and Ideal-Submodule SMul. However, 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. If @eric-wieser and @jcommelin think this is the correct thing to do, I'd oblige.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#18092~~
• ~~leanprover-community/mathlib4#18094~~
• ~~leanprover-community/mathlib4#18096~~
• ~~leanprover-community/mathlib4#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 https://github.com/leanprover-community/mathlib4/commit/e5fd5d60e8c01b2ca87642525c65ab7a1c3e004f (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.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style