Are these two definitions of a semimodule basis equivalent?
This question is related to this one. This will be quite a long post. Section "Introduction" may be skipped at first. I will refer to it later but it may be easier to only skim that section first (especially given that it's common knowledge).
Preliminary definitons
A semiring is a set with two operations $+$ and $\cdot$ which satisfy all axioms of a unitary ring except the axiom demanding the existence of additive inverses.
A left semimodule over a semiring $R$ is a commutative monoid $M$ (whose operation is denoted by $+$ too) with a function $ R\times M\longrightarrow M$ satisfying all axioms of a module over a ring except the axiom demanding the existence of additive inverses. A right semimodule is defined analogously.
Introduction
There are two equivalent definitions of a basis of a left $R$-module $M$ for a nontrivial unitary ring $R$.
Definition 1. A set $X\subset M$ is a basis of $M$ when $X$ is linearly independent (that is a linear combination of elements of $X$ is zero iff its coefficients are all zero), and $X$ generates $M$.
Definition 2. A set $X\subset M$ is a basis of $M$ when for every left $R$-module $N$ and every function $f:X\longrightarrow N$ there exists a unique $R$-module homomorphism $\bar f:M\longrightarrow N$ such that $\bar f|_X=f.$
I will prove the equivalence of these definitions now so that I can show where I have problems with the analogous defintions for semimodules.
Proof. Suppose $X$ satisfies Definition 1. Let $N$ be a left $R$-module and $f:X\longrightarrow N.$ We define $\bar f:M\longrightarrow N$ by $$\bar f\left(\sum_{i=1}^nr_ix_i\right)=\sum_{i=1}^nr_if(x_i).$$
Since $X$ generates $M$, this defines $\bar f$ for every $m\in M$. We have to show that it is well defined. Suppose $$\sum_{i=1}^nr_ix_i=\sum_{i=1}^ns_ix_i.$$ Then, by the linear independence of $X$, $$r_i=s_i$$ for all $i=1,\ldots,n.$ Therefore,
$$\bar f\left(\sum_{i=1}^nr_ix_i\right)=\sum_{i=1}^nr_if(x_i)=\sum_{i=1}^ns_if(x_i)=\bar f\left(\sum_{i=1}^ns_ix_i\right).$$ We have proved the existence of $\bar f$. We need to show its uniqueness. Suppose $g:M\longrightarrow N$ is a homomorphism, and $g|_X=f$. Then
$$g\left(\sum_{i=1}^nr_ix_i\right)=\sum_{i=1}^nr_ig(x_i)=\sum_{i=1}^nr_if(x_i)=\bar f\left(\sum_{i=1}^nr_ix_i\right),$$ and since $X$ generates $M,$ this proves the uniqueness of $\bar f.$
Conversely, suppose $X$ satisfies Definition 2. We will first prove that $X$ is linearly independent. Suppose $$\sum_{i=1}^nr_ix_i=0,$$ and $r_1\neq 0$. Let $f:X\longrightarrow R$ be defined by $$f(x)=\begin{cases}1 & \text {for } x=x_1,\\0 & \text {otherwise.}\end{cases}$$
Then there exists an $R$-module homomorphism $\bar f:M\longrightarrow R$ such that $\bar f|_X=f.$ We have $$0=\bar f(0)=\bar f\left(\sum_{i=1}^nr_ix_i\right)=\sum_{i=1}^nr_if(x_i)=r_1.$$ This is a contradiction, and $X$ must be linearly independent. We need to show that $X$ generates $M$. Let $M_1\subseteq M$ be the submodule generated by $X.$ Let $\bar f:M\longrightarrow M/M_1$ be the canonical homomorphism. Clearly, for all $x\in X,$ we have $\bar f(x)=0.$ Then $\bar f$ and the zero homomorphism restricted to $X$ are equal, and must therefore be equal. Hence $M/M_1=0,$ and so $M=M_1,$ which ends the proof. $\square$
Question
As said in the question I linked to at the beginning, the definition of linear independence in semimodules requires a bit of tweaking. If I understand correctly what Bill Cook wrote in his answer and what I later read in a book on semirings, the correct definition is this:
Definition 3. For a semiring $R$ and a left $R$-semimodule $M,$ a set $X\subset M$ is linearly independent iff for any two linear combinations of elements of $X$, their equality implies the equality of their coefficients.
This gives us two possible definitions of a basis of a left $R$-semimodule $M$ over a semiring $R$ obtained by re-writing Definition 1 and Definition 2, but now considering $M$ to be a semimodule over a semiring $R$. Let's call these definitions Definition 1s and Definition 2s.
Are these definitions also equivalent? I think they should be. Definition 1s is part of the definition of a free semimodule given by J. S. Golan in Semirings and Their Applications. But a definition of a free semimodule using Definition 2s should also be possible. However, it's difficult for me to generalize the proof I gave above. Most of it generalizes easily. I will not write those parts again, now for semimodules, but it is easy to check that Definition 1s implies Definition 2s by imitating the proof above. It also allows one to prove that Definition 2s implies the linear independence of $X$. What doesn't seem to be working is the proof that Definition 2s implies that $X$ generates $M$. The problem is that quotient structures are not very nice for semimodules. When we quotient out a submodule of a module over a ring, we use subtraction implicitly -- $m, m'$ being in the same coset means that $m-m'\in M_1.$ Quotient semimodules are generally defined not by subsemimodules, but by congruences. (As it is the case for semigroups.)
I've found a definition of a quotient semimodule $M/N$ for a subsemimodule $N\subseteq M$, but I don't think it works here. It is defined by the so-called Bourne relation.
Definition 4. Let $R$ be a semiring and $M$ a left $R$-semimodule. Let $N\subseteq M$ be a subsemimodule. We define the relation $\equiv_N$ on $M$ by $$m\equiv_N m'\iff (\exists n,n'\in N)\; m+n=m'+n'.$$
This relation can be shown to be a congruence. Now we simply define $M/N$ as $M/\equiv_N.$ This is easily seen to be equivalent to the standard definition in the case of modules over a ring.
However, as far as I can see, under this definition, $M/N=0$ doesn't imply $M=N$ in the general case. And this is what we want to use...
I think we gave up on the "normal" definition of a quotient semimodule too early, and then got distracted with the Bourne relation.
We can't write $r\sim s\iff r-s\in N$ as you said, but we can write $r\sim s \iff r+N=s+N$.
This resembles the Bourne relation written above, but of course the quantifiers are different. This equality of sets allows much more flexibility, and not just the existence of two things in $N$ "lining up" $r$ and $s$.
Now if $M/N=0$ in this relation, and $M$ and $N$ contain additive identity $0$ (which I presume was intended to be kept in the definition of semimodule above) then $m\sim 0$ implies $m+N=0+N$ for all $m\in M$, and so in particular $m+0\in N$, i.e. $m\in N$. Hence, $M\subseteq N$.
So I think your original argument does work.
There is a different proof working for modules and semimodules. I show only the generating property from Definition 2.
Let $X$ satisfy Definition 2. Let $M_1$ be the subsemimodule of $M$ generated by $X$. Let $i: X \to M_1$ and $j: M_1 \to M$ be the embeddings. Use $f = i: X \to M_1$. Then there is a unique $\bar f: M \to M_1$ with $\bar fji = f$. Because of $j\bar fji = jf = ji = id_M ji$ we get $j\bar f = id_M$ by the uniqueness requirement. Hence the embedding $j$ is surjective and thus the identity.
Here is an interesting example (theorem) w.r.t. $M/N = 0$. I am using the congruence relation in Definition 4.
Thm: Let $N$ be a subsemimodule of $N_0$, the natural numbers. Then $N_0/N = 0$ iff there are $a, b$ in $N$ with $a = b+1$. (1 not necessarily in $N$.)
There are infinitely many such subsemimodules in $N_0$.