Does $ab=1$ imply $ba=1$ in a ring?

Solution 1:

Assume $ab=1$ and $b$ is not a zero-divisor. Then $bab=b\cdot ab=b\cdot 1=b$, hence $(ba-1)b=0$, which implies $ba-1=0$ as $b$ is not a divisor of zero. Thus $ba=1$.

Solution 2:

Hint $\ $ Exploit conjugation $\rm\ \ 1\!-\!ba\, =\, b\, (1\!-\!ab)\, b^{-1}.\ $ [Multiply it by $\rm\:b\:$ to eliminate $\rm\:b^{-1}]$

Remark $\ $ To learn more about such look up "Dedekind finite" rings. You might also enjoy this tantalizing Halmos problem: explain why the following formal power series "proof" of the fact that if $\rm\:(1\!-\!ab)^{-1}\:$ exists then $\rm\:(1\!-\!ba)^{-1}\:$ exists, and has the value

$$\rm\begin{eqnarray} (1\!−\!ba)^{−1} &=&\rm 1+ba+b\color{#C00}{ab}a+b\color{#0A0}{abab}a+\ \cdots \\ &=&\rm 1+b(1\!+\,\color{#C00}{ab}\ \ \,+\ \ \color{#0A0}{abab}\ \ +\ \cdots)\,a\\ &=&\rm 1+b(1\!−\!ab)^{-1} a\end{eqnarray}$$

Solution 3:

If you drop the condition "no zero-divisors", there are counterexamples:

There are rings with elements which are left-invertible, but not right-invertible. Standard example: Consider a vector space $V$ with the countable infinite basis $\{v_1,v_2,\ldots\}$ and let $R$ be the endomorphism ring of $V$. Now the endomorphism $b$ induced by $v_1\mapsto v_2$, $v_2\mapsto v_3$, $v_3\mapsto v_4$ etc. is left-invertible, but not right-invertible. However, it is a right zero divisor in $R$.

(Explanation: I missed the condition "no zero-divisors" in the first place.)

Solution 4:

We can give an automated proof of this result using Prover9. We input the ring axioms, and the assumption of $1$ and no zero divisors, and the goal $xy=1 \implies yx=1$ as follows:

formulas(assumptions).

  (x + y) + z = x + (y + z).  % + is associative
  x + y = y + x.  % + is commutative

  x + 0 = x.  % additive identity
  0 + x = x.

  x + -x = 0.  % additive inverse
  -x + x = 0.

  x * (y + z) = (x * y) + (x * z).  % distributivity
  (x + y) * z = (x * z) + (y * z).

  (x * y) * z = x * (y * z). % * is associative

  x * 1 = x.  % multiplicative identity
  1 * x = x.

  x * y = 0 -> (x = 0 | y = 0).  % no zero divisors

end_of_list.

formulas(goals).

  x * y = 1 -> y * x = 1.

end_of_list.

Here's the proof it generates:

============================== PROOF =================================

% Proof 1 at 0.03 (+ 0.01) seconds.
% Length of proof is 42.
% Level of proof is 11.
% Maximum clause weight is 17.
% Given clauses 87.

1 x * y = 0 -> x = 0 | y = 0 # label(non_clause).  [assumption].
2 x * y = 1 -> y * x = 1 # label(non_clause) # label(goal).  [goal].
3 (x + y) + z = x + (y + z).  [assumption].
4 x + y = y + x.  [assumption].
5 x + 0 = x.  [assumption].
6 0 + x = x.  [assumption].
7 x + -x = 0.  [assumption].
9 x * (y + z) = (x * y) + (x * z).  [assumption].
10 (x + y) * z = (x * z) + (y * z).  [assumption].
11 (x * y) * z = x * (y * z).  [assumption].
12 x * 1 = x.  [assumption].
13 1 * x = x.  [assumption].
14 x * y != 0 | 0 = x | 0 = y.  [clausify(1)].
15 c1 * c2 = 1.  [deny(2)].
16 1 = c1 * c2.  [copy(15),flip(a)].
17 c2 * c1 != 1.  [deny(2)].
18 c2 * c1 != c1 * c2.  [copy(17),rewrite([16(4)])].
20 c1 * (c2 * x) = x.  [back_rewrite(13),rewrite([16(1),11(4)])].
21 x * (c1 * c2) = x.  [back_rewrite(12),rewrite([16(1)])].
22 x + (y + z) = y + (x + z).  [para(4(a,1),3(a,1,1)),rewrite([3(2)])].
23 x + (-x + y) = y.  [para(7(a,1),3(a,1,1)),rewrite([6(2)]),flip(a)].
27 (x * 0) + (x * y) = x * y.  [para(6(a,1),9(a,1,2)),flip(a)].
28 (x * y) + (x * -y) = x * 0.  [para(7(a,1),9(a,1,2)),flip(a)].
29 (x * y) + (0 * y) = x * y.  [para(5(a,1),10(a,1,1)),flip(a)].
32 (x * y) + (x * z) != 0 | 0 = x | y + z = 0.  [para(9(a,1),14(a,1)),flip(c)].
40 x + (y + -x) = y.  [para(7(a,1),22(a,1,2)),rewrite([5(2)]),flip(a)].
42 --x = x.  [para(7(a,1),23(a,1,2)),rewrite([5(2)]),flip(a)].
62 -x + (y + x) = y.  [para(42(a,1),40(a,1,2,2))].
109 x * 0 = 0.  [para(27(a,1),62(a,1,2)),rewrite([4(4),7(4)]),flip(a)].
111 (x * y) + (x * -y) = 0.  [back_rewrite(28),rewrite([109(6)])].
112 x * (0 * y) = 0 * y.  [para(109(a,1),11(a,1,1)),flip(a)].
131 -(x * -y) = x * y.  [para(111(a,1),62(a,1,2)),rewrite([4(5),6(5)])].
135 x + (0 * (c2 * x)) = x.  [para(20(a,1),29(a,1,1)),rewrite([20(9)])].
139 x * -y = -(x * y).  [para(131(a,1),42(a,1,1)),flip(a)].
144 -(0 * (c2 * x)) = 0.  [para(135(a,1),23(a,1,2)),rewrite([7(2),139(5),139(6)]),flip(a)].
147 -(0 * x) = 0.  [para(112(a,1),144(a,1,1,2)),rewrite([112(4)])].
148 0 * x = 0.  [para(147(a,1),7(a,1,2)),rewrite([4(4),6(4)])].
156 (c1 * x) + y != 0 | c1 = 0 | x + (c2 * y) = 0.  [para(20(a,1),32(a,1,2)),flip(b)].
321 c1 = 0 | x + -(c2 * (c1 * x)) = 0.  [resolve(156,a,40,a),rewrite([6(9),139(8)])].
354 c1 = 0 | c2 * (c1 * x) = x.  [para(321(b,1),23(a,1,2)),rewrite([5(5),139(7),139(8),42(9)]),flip(b)].
368 c1 = 0.  [para(21(a,1),354(b,1,2)),unit_del(b,18)].
380 $F.  [back_rewrite(18),rewrite([368(2),109(3),368(2),148(4)]),xx(a)].

============================== end of proof ==========================

Yes, it's not easy for a human to read, but there's something final about having a computerised proof since it uses low-level logic (and there's also a "cool" factor).