Commutant Problems in Loop Theory

August 2014

This page provides Web support for work in progress. For now, it's simply a log of results without much comment.

Gagola Problem (ADAM 2014)

Conjecture: Commutants in Moufang loops are normal.

See J.D.'s ADAM 2013 presentation.

Assuming an element C in the commutant,

   C * x = x * C.

we are working with 4 characterizations of normality:

condition mentioned in J.D.'s ADAM 2013 presentation

   (((C * x) * y) * (y' * x')) * z = z * (((C * x) * y) * (y' * x')) # label("Normal 1").

condition proposed by J.D. in his original input file for this problem

   % define D; A and B are arbitrary constants
   R(C,A,B) = D.

   D * x = x * D # label("Normal 2").

condition used by MK

   % define commutator (K)
   x * y = (y * x) * K(x,y) # label("commutator").

   K(R(C,x,y),z) = 1 # label("Normal 3").

Drapal Condition

   % define associator (a)
   (x * y) * z = (x * (y * z)) * a(x,y,z) # label("associator").

   % define commutator (K)
   x * y = (y * x) * K(x,y) # label("commutator").

   a(x,C,K(y,z)) = 1 # label("Drapal Condition").

Lemmas

Here are lists of candidate lemmas, some already proved, some conjectured but not proved yet.

Results

Normal 1 => {Normal 2, Normal 3, Drapal} (2014-aug-13)
Proof. (in, out, pf, xml)
Normal 3 => {Normal 1, Normal 2, Drapal} (2014-aug-13)
Proof. (in, out, pf, xml)
Drapal => {Normal 1, Normal 2, Normal 3} (2014-aug-14)
Proof. (in, out, pf, xml)
Lemma List 1 (2014-aug-19)
Proof. (in, out, pf, xml)
Normal 2 => Lemma List 2 (2014-aug-21)
Proof. (in, out, pf, xml)
Lemma List 4 (2014-aug-23)
Note: Lemmas 4-3 and 4-4 are not included.
Proof. (in, out, pf, xml)
D * (D * D) = C * (C * C) (2014-oct-01)
Note: It follows that if x^3 is injective, then D = C.
Proof. (in, out, pf, xml)
Lemma 2-13 => all of Lemma List 2 (2014-oct-01)
Note: Lemmas 2-28 and 2-36 are identical.
Proof. (in, out, pf, xml)
D * (x * (x * x)) = (x * (x * x)) * D (2014-Oct-07)
Proof. (in, out, pf, xml)
- Alternate version using defined function cb(x) = x * (x * x).
  
  Proof. (in, out, pf, xml)
- Alternate version in terms of R(C,x,y) instead of defined D.
```
   R(C,x,y) * (z * (z * z)) = (z * (z * z)) * R(C,x,y).
```
  Proof. (in, out, pf, xml)
Lemma List 0 (2015-jan-20)
Proof. (in, out, pf, xml)
Lemmas 5-1 through 5-8 (2015-jan-20)
Proof. (in, out, pf, xml)