# Formal specification of vector space.

The declaration of a field as a triplet $(\mathbb{K},\oplus,\odot)$ is canonical and in every book I've read, the definition of field is written using it. I can use this notation to describe any field in a strict and technical way. For example, this is how I can describe the finite field $\Bbb{Z}_2$:

$(\Bbb{Z}_2:=\{0,1\},\\\ \oplus:\Bbb{Z}_2^2\to\Bbb{Z}_2:=(x+y)\mod2,\\\ \odot:\Bbb{Z}_2^2\to\Bbb{Z}_2:=(x\cdot y)\mod2)$

I'm looking for a likewise technically strict way to describe a vector space over a field, since I've only found verbose specifications in common language (e.g., "a vector space $\mathbb{V}$ with operations $\oplus$ and $\odot$ over a field $\mathbb{k}$ with operations $+$ and $\cdot$").

There is any formal notation in which I can specify a vector space in few words (actually, in no words at all) as I do with fields?

• It's not clear to me what you're missing: if a vector space $V$ (over some specified field) has addition $\oplus$ and scalar multiplication $\odot$, then you can write it as a triple $(V,\oplus,\odot)$. What more do you want? – Eric Wofsey May 21 '17 at 0:51
• @Masacroso if you understand the issue, could you clarify? What exactly is "formal" about the field definition which is missing from the usual specifications of a vector space? – Omnomnomnom May 21 '17 at 0:57
• Can you say what the purpose of having such a "formal specification" is? You seem to have some misunderstandings about how this notation is used (for instance, the notation you used to write the field $\mathbb{Z}_2$ is not standard), so it is difficult to tell what you really want. – Eric Wofsey May 21 '17 at 1:03
• @Masacroso I don't know which textbooks you've read. However, most textbooks that define a vector space define it as a set with operations $\oplus, \odot$ (or $+,\cdot$, whatever the notation happens to be) which satisfy the 8 axioms of a vector space. That seems like a pretty formal definition to me. – Omnomnomnom May 21 '17 at 1:04
• @Seninha If you are interested in formal notations and formal specifications, why not look at actual machine-checked formal specification languages such as Coq, Agda, Z, MetaMath, Isabelle/HOL, etc.? – Derek Elkins May 21 '17 at 6:35

I think one thing you're missing is that the term "vector space" doesn't really have a definition. What has a definition is the term "vector space over $(K,+,\cdot)$", where $(K,+,\cdot)$ is some field. So, if $(K,+,\cdot)$ is a field, then a vector space over $(K,+,\cdot)$ is defined as a triple $(V,\oplus,\odot)$ where $V$ is a set, $\oplus:V\times V\to V$, $\odot:K\times V\to V$, and a certain long list of axioms are satified. This is really a separate definition for every single field $(K,+,\cdot)$.

If you really want to have a definition of "vector space" without specifying the field beforehand (and this is not how people normally talk about vector spaces), you could define it as a tuple $(V,\oplus,\odot,K,+,\cdot)$ where $V$ and $K$ are sets, $\oplus:V\times V\to V$, $\odot:K\times V\to V$, $+:K\times K\to K$, $\cdot:K\times K\to K$, and an even longer list of axioms are satisfied.

Formally, I don't see any additional challenge (of course, it gets more verbose, because you have more things to ask).

Given a field $(\Bbb F,\oplus,\odot)$ a triple $(V,+,\cdot)$ is a $(\Bbb F,\oplus,\odot)$-vector space if and only if:

1. $(V,+)$ is an abelian group (= verbose subdefinition)
2. $\cdot:\Bbb F\times V\to V$ and $+:V\times V\to V$ satisfy:
• $\forall \alpha,\beta\in\Bbb K,\forall x\in V,\ (a\odot b)\cdot v=a\cdot(b\cdot v)$ or, if you want to be more formal, $\cdot(\odot(a,b),x)=\cdot(a,\cdot(b,x))$
• $\forall \alpha,\beta\in\Bbb K,\forall x\in V,\ (a\oplus b)\cdot x=(a\cdot x)+(b\cdot x)$ or, if you want to be more formal, $\cdot(\oplus(a,b),x)=+(\cdot(a,x),\cdot(b,x))$
• $\forall x\in V,\ 1_{\Bbb F}\cdot x=x$
• $\forall \alpha\in\Bbb K,\forall x,y\in V,\ \alpha\cdot(x+y)=(\alpha\cdot x)+(\beta\cdot y)$ or, if you want to be more formal, $\cdot(\alpha,+(x,y))=+(\cdot(\alpha,x),\cdot(\alpha,y))$

Typically, mathematicians (and anyone who has clear in mind what is what) swiftly adopt the big boys' notation $+:=\oplus$, $\text{nothing}:=\cdot:=\odot$, $0:=0_V$ and $0:= 0_{\Bbb F}$. This, basically because the aforementioned formal properties have the consequence of making such identifications harmless, as long as you have a way to distinguish vectors from scalars. This is acheived by noticing that, as long as multiplication by scalar acts on the left and you don't introduce a "dot product of two vectors", the only way to make sense of a "monomial" such as $abcd\in V$ is by assuming $a,b,c\in \Bbb F$ and $d\in V$, thus reading it $(a\odot b\odot c)\cdot d$. Similarly for $x(a+b)(c+d)=(x\odot(a\oplus b))\cdot (c+d)$