# Why are modules also rings in the HOL-Algebra library?

We would like to use vectors and matrices (2x2 and 3x3) in a project, and have found the Jordan Normal Form AFP entry (Matrix.thy) which provides a concrete implementation. It relies on the HOL-Algebra implementation of modules but this theory seems really bizarre, as though it gets everything the wrong way around.

To have this question self-contained, recall that in the simplest case a module $$M$$ is typically defined over a commutative ring $$(R, +_R, \cdot_R)$$, such that $$(M, +_M)$$ is an Abelian group and there is a 'multiplicative' action $$\circ : R \times M \rightarrow M$$ which distributes over both $$+_M$$ and $$+_R$$, is associative w.r.t $$\cdot_R$$, and for which $$1_R$$ is also an identity.

This definition may be generalized to a module $$M$$ over an Abelian Group $$(G, +_G)$$ instead of a ring. In that case we still require $$(M, +_M)$$ to be an Abelian group, and there to be an action $$\circ : G \times M \rightarrow M$$ but it only needs to distribute over both additions.

Now, HOL-Algebra/Module.thy claims to define "modules over an Abelian group." There is a record of what an ('a, 'b) module is with an action smult : ['a, 'b] => 'b. This is followed by a locale module which seems alright (but clearly defines modules over a ring, not over an Abelian group). However, weirdly, the record ('a, 'b) module requires 'b, i.e. the module itself, to be a ring. In my understanding, if anything, we should require 'a to be a ring (namely $$R$$ in the definition above!). Better yet, 'b should be an Abelian group, and in order to define modules over an Abelian group as claimed, 'a should also be such.

As a consequence, for the Jordan Normal Form entry to show that for 'a :: semiring_1, the type 'a vec of vectors over 'a forms a module*, they have to specify mult = undefined, one = undefined in the definition of the record. Given HOL-Algebra as it is, this makes sense as there is no natural multiplication or multiplicative identity in the space of generic vectors.

Is there a reason for these akward definitions?

[*To be very precise, a module over a semiring is only required to be a commutative monoid not a full Abelian group.]