notation for finite free modules

Stream: maths

[Kevin Buzzard]

Some students here have developed the basic theory of free modules of finite rank over a ring (which later becomes a commutative ring and then a field). One issue I have with their work is that they are still using some placeholder notation for the fundamental construction of $R^n$, the free rank $n$ module over the ring $R$. What should the function which takes a ring R and a natural n and returns the R-module R^n be called? Any suggestions?

[Reid Barton]

I guess there are two questions: name, and notation

[Reid Barton]

For notation, assuming we can't use R^n, how about R^⊕n?

[Johan Commelin]

Why can't we use R^n? As for the name, how about finite_free_module R n?

[Reid Barton]

Maybe we can use R^n, but in that case I assumed there was no choice to be made :)