Hace $ab=1$ implica $ba=1$ en un anillo?

Question

Dejemos que $R$ sea un anillo con unidad $1$ y que $a,b\in R$ no sea divisor cero s. ¿Hay algún contraejemplo para: $$ab=1\quad\Rightarrow \quad ba=1$$

Answer 1

Supongamos que $ab=1$ y $b$ no es un divisor de cero. Entonces $bab=b\cdot ab=b\cdot 1=b$ Por lo tanto $(ba-1)b=0$ , lo que implica $ba-1=0$ como $b$ no es un divisor de cero. Por lo tanto, $ba=1$ .

Answer 2

Si se elimina la condición "no hay divisores de cero", hay contraejemplos:

Hay anillos con elementos invertibles a la izquierda, pero no invertibles a la derecha. Ejemplo estándar: Consideremos un espacio vectorial $V$ con la base infinita contable $\{v_1,v_2,\ldots\}$ y que $R$ sea el anillo de endomorfismo de $V$ . Ahora el endomorfismo $b$ inducido por $v_1\mapsto v_2$ , $v_2\mapsto v_3$ , $v_3\mapsto v_4$ etc. es invertible a la izquierda, pero no a la derecha. Sin embargo, es un divisor cero a la derecha en $R$ .

(Explicación: se me escapó la condición "no hay divisores de cero" en primer lugar).

Answer 3

Sugerencia $\ $ Explotar conjugación $\rm\ \ 1\!-\!ba\, =\, b\, (1\!-\!ab)\, b^{-1}.\ $ [Multiplícalo por $\rm\:b\:$ para eliminar $\rm\:b^{-1}]$

Nota: $\ $ Para saber más sobre este tipo de anillos, busque "Dedekind finito". También puede disfrutar de esto tantalizante problema de Halmos: explicar por qué la siguiente "prueba" formal de series de potencias del hecho de que si $\rm\:(1\!-\!ab)^{-1}\:$ existe entonces $\rm\:(1\!-\!ba)^{-1}\:$ existe, y tiene el valor

$$\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}$$

Answer 4

Podemos dar una prueba automatizada de este resultado utilizando Prover9 . Introducimos los axiomas del anillo, y la suposición de $1$ y ningún divisor cero, y el objetivo $xy=1 \implies yx=1$ de la siguiente manera:

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.

Aquí está la prueba que genera:

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

Sí, no es fácil de leer para un humano, pero hay algo definitivo en tener una prueba computarizada, ya que utiliza lógica de bajo nivel (y también hay un factor "cool").