[Merged by Bors] - refactor: change the definition of 1 : Submodule R A to the range of (· • 1)

[alreadydone]

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.

---

[github-actions]

PR summary 550d222677

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ toSpanSingleton_eq_algebra_linearMap

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.

[eric-wieser]

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.

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 commutes' field from Algebra is a fair bit of work.
@Vierkantor tried to do things in this direction before, and so did I. My motivation was to try and merge algebraMap wth Matrix.scalar, but it would also give us the canonical map between the groups of units in a tower of algebras etc.

It's perhaps too much work to allow it to hold up this PR, but I do think we should do it eventually.

[alreadydone]

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.

I think r • 1 isn't much complex than algebraMap R A 1 and they are easily connected by Algebra.algebraMap_eq_smul_one (which isn't a simp lemma).

@Vierkantor tried to do things in this direction before, and so did I. My motivation was to try and merge algebraMap wth Matrix.scalar, but it would also give us the canonical map between the groups of units in a tower of algebras etc.

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 fun r : R ↦ r • (1 : A) is a RingHom. So even when we do introduce Algebra without commutes', I don't think we should revert this PR.

[Vierkantor]

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 R. And getting that more generic inclusion to work right seems to be quite hard, so I don't think either we can try to do it in a simple way here and then fix it up later.

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 (· • 1) definition, if we leave a TODO note and an issue about changing this when we figure out how.

[Vierkantor]

LGTM, thanks!

@eric-wieser, could you do the final review please?

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style