[darcs-devel] Right and left inverses

[David Roundy]

On Thu, Mar 27, 2008 at 09:56:18PM +0100, Jules Colding wrote:
> I'm still reading appendix A in the darcs2 manual. Right after theorem  
> 1 it is said that:

Perhaps I should belatedly warn you that the appendix A is in need of
considerable work...

> 	"it is possible to show that the right inverse of a patch is equal to  
> its left inverse"
> 
> How?

You simply consider the inverse of the inverse.  If the inverse of the
inverse is the original patch, then the right inverse is the same as the
left inverse.

let riA = right-invert A

which means that

  A riA has same effect as the identity change

let liA = left-invert A

means that

  liA A has the same effect as the identity change

So now consider

rrA = right-invert riA

so riA rrA has the same effect as identity

Now if rrA is the same as A, we conclude that riA == liA.

So I've shown that the statement you were asking about right/left inverse
equality is the same as the statement that the right-invert (or
alternatively left-invert) is a self-inverting function.

So how do we know that inversion is self-inverting? That comes from the
effect of identity.

If we begin in state o, then applying A gives us state a.  Then applying
riA gives us the state o.  Applying rrA must give us the state a again
(since it's the right-invert of riA), and the patch that takes us from o to
a is A.
-- 
David Roundy
Department of Physics
Oregon State University