What is a basis in a semivector space? Let $S$ be a semifield, that is an algebraic structure satisfiying all field axioms except (perhaps) the existence of additive inverses. A semivector space is a semimodule (a module without additive inverses) over a semifield. Let $V$ be a semivector space over $S.$
I would like to understand what the definition of a basis of $V$  should be. I have found very little material about semivector spaces. All I have found is some papers by Indian author W. B. Vasantha Kandasamy. She defines a basis of $V$ by copying the definition of a basis of a vector space -- a tuple of vectors $v_1,...,v_n$ that generate the whole and are linearly independent, where "linearly independent" means
$$\left(\forall a_1,...,a_n\in S\right) \;\;\left(\sum_{i=1}^{n}a_iv_i = 0 \Longrightarrow \left(\forall i\in\{1,...,n\}\right)\;\;a_i=0\right).$$
I believe this is a very unnatural definition. I think that linear independence should be always understood as "freeness" of the spanned space. I know next to nothing about category theory but I understand a free space is one "with no non-trivial relations in it". The above condition doesn't assure that there are no non-trivial relations because we cannot use subtraction to move one side of a possible non-trivial relation to the other side.
I have two questions. 


*

*Do you think I'm correct and Kandasamy's definition doesn't make much sense?

*If so, could you please help me build a correct definition of linear independence for semivector spaces? I think it's a very good exercise for me to improve my understanding of free objects. I've been trying to find a "relational" definition and then prove that it's equivalent to this defintion. But I'm not doing very well. Should I define "non-trivial relation" to be a formula of the form


$$\sum_{i=1}^{m}a_ix_i=\sum_{j=1}^{n}b_iy_i$$
for $a_i,b_j\in S,$ such that there exist $x_1,...,x_m,y_1,...,y_m$ such that the formula is not satisfied?
EDIT I have asked a follow-up question here.
 A: Fix a semifield $\mathbb{F}$. Let $B = \{ b_i \;|\; i \in I \}$ be some set. 
Let $F(B) = \{ (c_i)_{i \in I} \;|\; c_i \in \mathbb{F} \mathrm{\;and\;only\;finitely\;many\;} c_i \not=0 \}$. Define $\iota:B \to F(B)$ by $\iota(b_i)=(c_j)_{j\in I}$ where $c_j = \left\{ \begin{array}{cc} 1 & j=i \\ 0 & j \not= i \end{array} \right\}$
In particular, if $B=\{b_1,b_2,b_3\}$ then $F(B) = \mathbb{F}^3$ and $\iota(b_1)=(1,0,0)$, $\iota(b_2)=(0,1,0)$, and $\iota(b_3)=(0,0,1)$, 
Let $f:B \to W$ be a (set) map into a semivector space $W$. Then define $\bar{f}:F(B)\to W$ by $\bar{f}\left((c_i)_{i\in I}\right)=\sum\limits_{i\in I} c_if(b_i)$. Note: The sum is finite since only finitely many $c_i$ are non-zero.
Again, in particular, if $B=\{b_1,b_2,b_3\}$ and $f(b_j)=w_j$, then $f(c_1,c_2,c_3)=c_1w_1+c_2w_2+c_3w_3$ for all $c_1,c_2,c_3 \in \mathbb{F}$.
One can check that $\bar{f}$ is the unique linear map such that $\bar{f} \circ \iota = f$. 
Therefore, $F(B)$ is "the" free semivector space over $B$ [so I guess there are free objects in this category]. Remark: the same old argument that any two free objects over the generating set are isomorphic should apply here, so if $F_1$ and $F_2$ are free over $B$. Then $F_1 \cong F_2$.
Next, let's repair the definition of "basis". How about instead we say, "$B$ is a basis for $V$ if every element of $V$ can be written as a finite linear combination of elements of $B$ in a unique way." Over a field this is equivalent to the spanning+linear independence definition. But in the semifield case it avoids the unpleasantries you've brought up.
Suppose $B = \{ b_i \;|\; i \in I\}$ is a basis (in this new sense) for $V$. Define $i:B \to V$ by $i(b)=b$. Let's show $V \cong F(B)$. We can do this a couple of ways:


*

*Define the map $f:V \to F(B)$ by $f(v) = \left(c_i\right)_{i \in I}$ where $v=\sum\limits_{i \in I} c_ib_i$. Note: We know a unique collection of $c_i\in\mathbb{F}$ exist because $B$ is a basis for $V$. Also, since $v$ is a finite linear combination, only finitely many are non-zero so $\left(c_i\right)_{i \in I} \in F(B)$.
Now go through the routine check that $f$ is an isomorphism.

*Alternatively, we could show $V$ satisfies the universal property and thus is free (generated by $B$). Hence $V \cong F(B)$.
I haven't checked all of the details carefully, but I think this is what you're looking for. You are right about having to change the linear independence part of the definition of basis for a semivector space. The notion of linear independence is primarily there to guarantee that we have unique representations as linear combinations (spanning saying we have a representation).
