[darcs-devel] Right and left inverses

[Jules Colding]

On 28/03/2008, at 15.16, David Roundy wrote:
> 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...

Thank you for the warning ;-)

Appendix A seemed to me the best place to start if I wanted to  
understand the theory behind darcs, which I do. Any update/rewrite  
planned?


>> 	"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.


OK, in other words:

riA rrA = I, I is the identity change

A riA = I
=> A riA rrA = rrA
=> A I = rrA
=> A = rrA

now substituting into riA rrA = I we get:

riA A = I
=> riA = liA


The only assumption I can see that is made underway is that:

IA = AI = A, where I is the identity change.

which seems logically valid although I'm not sure a mathematician  
would agree without a rigorous proof.


> 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.

Yes.


> 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.

In  other words:

A o  --> a
=> A riA o --> o
=> A riA rrA o = A o --> a

substituting (A riA = I) now gives:

rrA o --> a
=> rrA = A

The same can be done for llA. I'm sorry if my notation isn't correct,  
but the meaning should be clear.

Thank you for explaining this to me :-)

Best regards,
   jules