Generalize Algebra to keep inclusion map without `commutes`

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 #18092.)

Start with the Algebra R A typeclass, algebraMap, and the definitions cited in #18092. Investigate the proposed non-commutative algebra abstraction and its generalization to canonical inclusions of groups and related structures. Done means the inclusion is carried by the generalized typeclasses and the Submodule definition can be reverted to use LinearMap.range (Algebra.linearMap R A).