Reflexive pair in an additive category is an internal groupoid (source code)

= Reflexive pair in an additive category is an internal groupoid

Let $f,g:A\rightrightarrows B$ be a <reflexive pair> in an <additive category> with <finite limits>, with common section $r:B\to A$. Regard $f$ as source and $g$ as target. For arrows $x,y:C\to A$ satisfying $gx=fy$, define
$$
x\circledast y=x+y-rgx.
$$
The identity at $b:C\to B$ is $rb$, and the inverse of $x$ is $rfx+rgx-x$. These operations define an <internal groupoid>. The <finite limits> hypothesis supplies the objects of composable arrows needed for the groupoid diagrams.

The source of the composite is $fx+fy-gx=fx$, and its target is $gx+gy-gx=gy$. The common-section identities prove both identity laws and both inverse laws. For a composable triple $x,y,z$, either parenthesization gives $x+y+z-rgx-rgy$, proving associativity. Bilinearity makes these formulas compatible with precomposition in $C$.

The limit hypothesis cannot simply be discarded. Take the full <subcategory> of finite-dimensional <vector spaces> whose dimensions are $3a+5b$, for nonnegative <integers> $a,b$. A projection $k^5\to k^3$ has a common section with itself, but its composable-pair <pullback in a category> in <vector spaces> has dimension $7$, which is not of the allowed form. Testing the <pullback in a category> property on $k^3$ would force that same dimension, so the smaller category has no such <pullback in a category>. The <reflexive-pair groupoid formula in a preadditive category> still makes sense on generalized arrows without asserting existence of this object.