Modules in Mizar

The difficulty which first presents itself for thinking about the tensor product for two modules, well, the tensor product is an Abelian group. We need to prove \(M_{1}\otimes M_{2}\) is a module (left/right/bi, according to the situation). Then we need to register this as a fact, or redefine the tensor product (ugh).

I also would have to prove \(M_{1}\otimes(M_{2}\otimes M_{3}) = (M_{1}\otimes M_{2})\otimes M_{3}\) which then establishes \(M_{1}\otimes M_{2}\otimes M_{3}\) is unambiguous. This requires some care with the exact definition of the tensor product, because some definitions make this an isomorphism rather than an exact equality.

I think we need \(R\) to be a commutative associative ring with unit, and \(M\) to be a unitary module over \(R\). This is because \(T^{0}(M)=R\) must be an module over \(R\), which forces us to insist on \(R\) being associative.

A unitary module \(M\) over \(R\) means:

• For left $R$-modules, for all \(m\in M\) we have \(m\mapsto 1\cdot m\) be the identity automorphism of \(M\)
• For right $R$-modules, for all \(m\in M\) we have \(m\mapsto m\cdot 1\) be the identity automorphism of \(M\)
• For bimodules, both of these are the identity automorphism

This obviously requires \(R\) being a unital ring.

Why do we need \(R\) to be commutative? Well, if we consider \(m_{1}\otimes m_{2}\in M\otimes M\) and \(r,s\in R\), then:

…which will end up imposing commutativity on the ring, since we just proved \(rs(m_{1}\otimes m_{2})=sr(m_{1}\otimes m_{2})\). So it's unusual to find tensor products of modules over noncommutative rings, but we could do it; and for the tensor algebra, it's just extra baggage we have to eventually jettison.