Let $X \neq \emptyset$ be an arbitrary set. Let $$ d : X \times X \to \mathbb{R} $$ be a real-valued function with the following properties:
- (1) $\forall x, \in X: d(x,x) = 0,$
- (2) $\forall x,y \in X: d(x,y) = -d(y,x),$
- (3) $\forall x,y,z \in X: d(x,y) + d(y,z) = d(x,z).$
It seems the function $d$ is a type of abstraction of the subtraction operator (i.e. the minus symbol).
Note that property (3) implies properties (2) and (1). Similarly, property (2) implies property (1). In this sense, properties (1), (2), (3) are ascending in strength.
Question: Is there a formal name for this type of function? Has this type of function been researched?
Generally, let $X$ be a set and $G$ be a group. Then (I am making this term up) let's say that a $G$-division function on $X$ is a function $d : X \times X \to G$ satisfying the following axioms:
I don't know if there's a common name in use for a set $X$ equipped with a $G$-division function, so I am again going to make one up; let's call such a thing a $G$-divided set.
Intuitively speaking a $G$-divided set is like a metric space but where distances are antisymmetric rather than symmetric and measured via elements of the group $G$. A motivating example to keep in mind occurs when $X$ is the set of angles; then we can take $d$ to be the function valued in $S^1$ which measures the clockwise angular difference between two angles. Note that $X$ itself can be identified with $S^1$ but not canonically; doing so requires a choice of angle to fix as the "base angle." This is an important general feature and we'll come back to this. This means we could also justify calling $d$ a $G$-metric and calling $X$ a $G$-metric space.
So, thinking in these terms, the first observation we can make is that these axioms imply that the relation $d(x, y) = e$ is an equivalence relation; these are the elements that are "distance zero" apart in the "metric" $d$. $d$ does not distinguish between such elements, so we might as well work with the quotient $X/\sim$ by this equivalence relation. Equivalently, we could add another axiom saying that this equivalence relation is trivial:
This is the analogue in our setting of the positivity axiom for a metric space, and we could call it nondegeneracy. The second observation we can make is that the axioms imply that the image of $d$ in $G$ is closed under multiplication and inverses, so it's a subgroup $H$. From here we might as well replace $G$ by $H$, or equivalently we could add another axiom:
This axiom, together with nondegeneracy, will turn out to imply that $X$ is a structure called a $G$-torsor. This is because these axioms imply that $d$ can be used to produce a right action of $G$ on $X$, as follows: given $g \in G$ we'll define $xg = y$ iff $d(x, y) = g$. Given $x$, such a $y$ exists by axiom 5, and it's unique by axiom 4, because if $d(x, y) = d(x, y') = g$ then
$$d(y, y') = d(y, x) d(x, y') = g^{-1} g = e$$
and axiom 4 then gives $y = y'$. You can check that axioms 1, 2, and 3 imply that this really does define a right action of $G$, and moreover it's an action which is free and transitive, also known as simply transitive or regular. In this situation $X$ is also known as a $G$-torsor. Conversely, given such an action, for any $x, y \in X$ there's a unique $g \in G$ such that $xg = y$, and defining $d(x, y) = g$ produces a $G$-division function satisfying axioms 1 through 5. In conclusion:
So the study of division functions reduces immediately to the study of torsors.
This is a nice exercise which I'll leave to you. The conclusion is that a $G$-torsor is like "a copy of $G$ that has forgotten where its identity is." The example of angles that we used above is a torsor over $S^1$. Here are some other motivating examples:
Despite being in some sense trivial to classify, torsors nonetheless show up all over mathematics in a few different forms so they're important to understand (mostly because it's important to understand that a $G$-torsor cannot be canonically identified with $G$). A general way they occur is that if $x, y$ are objects in any category then the set $\text{Iso}(x, y)$ of isomorphisms between them is canonically a torsor over either $\text{Aut}(x)$ or $\text{Aut}(y)$ (our last two examples occur in this way). Also, one can consider torsors "internal to" other categories, where the classification can become interesting; this occurs in algebraic geometry and topology.
In a categorical setting the analogy between divided sets and metric spaces can be made precise using the notion of an enriched category; on the one hand metric spaces are Lawvere metric spaces which are enriched categories over the monoidal poset $[0, \infty)$ equipped with $+$ and $\le$, and on the other hand $G$-divided sets are enriched categories over $G$ regarded as a discrete monoidal category. (This doesn't impose axiom 2 directly, but as you say it follows from axiom 3.)
I happen to really like these sorts of analogies; sadly this whole discussion shows that this concept is unnecessary since we can talk about everything in the familiar language of group actions. Personally, though, I think talking about division functions / $G$-metrics has a unique flavor that suggests a different enough perspective to be worth keeping in mind. For example, we can use the enriched category language to talk about a very abstract generalization of the procedure that produces a metric space from a normed vector space by taking the norm of the difference $d(v, w) = \| v - w \|$; this corresponds exactly to first passing to a divided set given by $d(v, w) = v - w$, then applying the norm. This discussion also suggests generally that it could be fruitful to consider generalizations of metrics where distances aren't required to be symmetric; these are called quasimetrics (and Lawvere metrics are even more general).