Generalize Algebra to keep inclusion map without commutes

[Vierkantor]

This was raised in the discussion of #18092 but has been around for a long time:

We currently have the Algebra R A typeclass for commutative algebras that carries an inclusion map algebraMap : R -> A. We can also express non-commutative algebras using a combination of other typeclasses, but then the inclusion becomes a derived definition (for example, as (· • 1)). For better defeqs, if not simply mirroring actual mathematical practice, we should instead have a typeclass for non-commutative algebras that carries the inclusion map.

And in turn we should try to generalize this to canonical inclusions of groups etc.

When this issue is resolved:, it should be possible to revert the following definitions:

• 1 : Submodule R A changes back from (· • 1) to LinearMap.range (Algebra.linearMap R A). (See [Merged by Bors] - refactor: change the definition of 1 : Submodule R A to the range of (· • 1) #18092.)