[Haskell-cafe] Is there a name for this property: x + x - x == x

[wren romano]

On Wed, Jun 4, 2014 at 10:34 AM, Omari Norman <omari at smileystation.com> wrote:
> It's not quite idempotence, because more than one function is involved.

It's a restricted version of the quasigroup law. For non-commutative
operators there are actually two laws:

    left-division:  forall a, b. exists (a\b). a*(a\b) == b
        N.B., it follows that: forall a, b. a \ (a*b) == b

    right-division: forall a, b. exists (b/a). (b/a)*a == b
        N.B., it follows that: forall a, b. (a*b) / b == a

The "division" in the name just comes from assuming (*) is a
"multiplication", as is usually assumed in group theory. We call (*) a
left- or right-quasigroup depending on which law holds, or call it a
quasigroup if both laws hold. If the quasigroup has an identity
element, then it's called a loop, and we can define left- and
right-inverse operators by (x\1) and (1/x). If we have various weak
forms of associativity then we get left Bol loops, right Bol loops,
and Moufang loops depending on what sort of weak associativity we
have. If we have full associativity then the loop is a monoid. If the
left- and right-inverses coincide, then this monoid is in fact a
group.

cf., <http://winterkoninkje.dreamwidth.org/79868.html>
also <http://en.wikipedia.org/wiki/Quasigroup>


Alternatively, if you want to view the law as being associated the
other way — i.e., (x*y)/y == x — then, as Alexander Vieth said, the
way to think about it is in terms of the endomorphism group. That is,
given any monoid (G,(*)) we can construct a monoid (Endo(G),(.)) where
forall x:G we have (_*x) : Endo(G), and where (.) is function
composition. When G happens to be a group every element has a unique
multiplicative inverse, therefore every endomorphism has a unique
compositional inverse, hence Endo(G) is a group. Thus, we'd just call
(_*x) and (_/x) inverses since they're inverse elements in Endo(G).

If you want to get fancy, whenever r . s == id we say that s is a
"section" of r, and that r is a "retraction" of s. So you could use
that terminology, though it's more general and it loses the fact that
we actually have both (_*x).(_/x) == id and also (_/x).(_*x) == id.

-- 
Live well,
~wren