If $R$ is a domain, and $M$ a (left) $R$-module, what are the different notions of dimension of $M$ and their respective assets, what do they measure?
I found out that if $\dim_RM$ is the cardinal of any maximal independent subset of $M$, then it does not depend of maximal independent subset chosen if $R$ is a left-Ore domain, and the rank-nullity theorem holds for $\dim_R$. This seems very natural, and I wonder whether this is known:
Do you happen to know any reference for that?
Edit. Let me still give a proof that would fit in a second year algebra course.
Let $R$ be a left-Ore domain, that is for any no-zero $a,b\in R$, one as $Ra\cap Rb\neq(0)$. Let $M$ be a left $R$-module. Call a family $\bar v\in M^n$ dependent if there is a non-zero $\bar r\in R^n$ s.t. $r_1v_1+\dots+r_nv_n=0$, or independent otherwise. It is a basis if independent and maximal such.
Lemma (incomplete basis). Any independent family extends to a (possibly empty) basis.
If $\bar b$ is a basis of $M$, for every $v\in M\setminus\bar b$, the set $\bar b\cup\{v\}$ is dependent, so there is a non-zero $r\in R$ such that $rv\in (\bar b)$. For any $S\subset M$ and $v\in M$, say that $v$ is algebraic over $S$ if there is a nonzero $r\in R$ st $rv\in(S)$.
Lemma (transitivity of agebraicity). Let $A,B,C$ be subsets of $M$. If $A$ is algebraic over $B$ and $B$ over $C$, then $A$ is algebraic over $C$.
Key idea of the 8 lines proof. Suppose $ra=sb$ and $tb=uc$ with $r$ and $t$ nonzero. By assumption, there is a nonzero $r's=r''t\in Rs\cap Rt$, so $r'ra=r''uc$, hence $a$ is algebraic over $c$.$\square$
Theorem. All basis of $M$ have the same cardinality, written $\dim_R M$.
Proof. Standard argument using transitivity and exchange property: Treat the particular case where $M$ has a finite basis $\bar b=(b_1,\dots,b_n)$. Let $(c_1,\dots,c_m,\dots)$ be another basis of $M$. By maximality of $\bar b$, one can write $\displaystyle rc_1=\sum r_ib_i$ for some non-zero $r\in R$. As $c_1$ is free, $r_1$ say is nonzero. So $b_1$ is algebraic over $(c_1,b_2,\dots,b_n)$. As $M$ is algebraic over $\bar b$, by transitivity, $M$ is algebraic over $(c_1,b_2,\dots,b_n)$. One concludes in a similar way that $M$ is algebraic over $(c_1,c_2,b_3,\dots,b_n)$, and iterating, one can add every $c_i$. If $m>n$, we conclude that $c_{m}$ is algebraic over its predecessors, a contradiction, so $m\leqslant n$, and all basis of $M$ are finite. By symmetry, one has $n=m$.$\square$
Lemma. Let $M$ be an $R$-module.
(1) Let $N$ be an $R$-module, then $$\dim_R M\oplus N=\dim_R M+\dim_R N.$$
(2) Let $N\subset M$ be a submodule, then $$\dim_R M=\dim_R M/N+\dim_R N.$$
(3) Let $f:M\rightarrow N$ be a morphism of $R$-module, then $$\dim_R M=\dim_R\ker f+\dim_R {\rm Im} f.$$
Proof (sketch). (1) If $\bar b$ and $\bar c$ are basis of $M$ and $N$, there union is a basis of $M\oplus N$ (uses the Ore-condition again). (2) If $\bar b+N$ is a basis for $M/N$ and $\bar c$ for $N$, then $\bar b\cup \bar c$ is a basis for $M$. (3) Considering the induced bijection $M/\ker f\rightarrow {\rm Im}f$ and in view of (2), we may assume that $f$ is bijective. It is then straightforeward that $\bar b$ is independent in $M$ iff $f(\bar b)$ is independent in $N$.$\square$