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.]



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.