:: {AIM } Loops and the {AIM } Conjecture
:: by Chad E. Brown and Karol P\kak
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1, SETFAM_1, ABIAN, KNASTER,
FUNCT_1, RELAT_1, XBOOLE_0, ALGSTR_1, ZFMISC_1, GROUP_6, GROUP_9,
MESFUNC1, VECTSP_1, TARSKI, REALSET1, COHSP_1, ARYTM_3, FUNCT_2,
PRE_TOPC, QC_LANG1, AUTGROUP, AIMLOOP, FUNCT_5, GROUP_1, FUNCOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, STRUCT_0, ALGSTR_0, ALGSTR_1,
GROUP_1, VECTSP_1, ABIAN, KNASTER, FUNCT_5;
constructors BINOP_2, ALGSTR_1, REALSET1, VECTSP_2, GR_CY_1, RELSET_1, ABIAN,
KNASTER, FUNCT_5;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, KNASTER, PARTFUN1,
FUNCT_2, REALSET1, STRUCT_0, ALGSTR_0, ALGSTR_1, VECTSP_1, RELSET_1,
FUNCOP_1;
requirements BOOLE, SUBSET;
begin :: Loops - Introduction
::We define division operations on loops,
::inner mappings T, L and R, commutators and associators
::and basic attributes of interest. We also consider
::subloops and homomorphisms. Particular subloops are
::the nucleus and center of a loop and kernels of homomorphisms.
reserve Q,Q1,Q2 for multLoop;
reserve x,y,z,w,u,v for Element of Q;
definition
let X be 1-sorted;
mode Permutation of X is Permutation of the carrier of X;
let Y be 1-sorted;
func Funcs(X,Y) -> set equals
:: AIMLOOP:def 1
Funcs(the carrier of X,the carrier of Y);
end;
registration
let X,Y be 1-sorted;
cluster Funcs(X,Y) -> functional;
end;
definition
let Q be invertible left_mult-cancelable non empty multLoopStr,
x,y be Element of Q;
func x \ y -> Element of Q means
:: AIMLOOP:def 2
x * it = y;
end;
definition
let Q be invertible right_mult-cancelable non empty multLoopStr,
x,y be Element of Q;
func x / y -> Element of Q means
:: AIMLOOP:def 3
it * y = x;
end;
registration
let Q,x,y;
reduce x \ (x * y) to y;
reduce x * (x \ y) to y;
reduce (x * y) / y to x;
reduce (x / y) * y to x;
end;
definition
let Q be invertible left_mult-cancelable non empty multLoopStr,
u,x be Element of Q;
func T_map(u,x) -> Element of Q equals
:: AIMLOOP:def 4
x \ (u * x);
end;
definition
let Q be invertible left_mult-cancelable non empty multLoopStr,
u,x,y be Element of Q;
func L_map(u,x,y) -> Element of Q equals
:: AIMLOOP:def 5
(y * x) \ (y * (x * u));
end;
definition
let Q be invertible right_mult-cancelable non empty multLoopStr,
u,x,y be Element of Q;
func R_map(u,x,y) -> Element of Q equals
:: AIMLOOP:def 6
((u * x) * y) / (x * y);
end;
definition
let Q;
attr Q is satisfying_TT means
:: AIMLOOP:def 7
for u,x,y be Element of Q holds
T_map(T_map(u,x),y) = T_map(T_map(u,y),x);
attr Q is satisfying_TL means
:: AIMLOOP:def 8
for u,x,y,z be Element of Q holds
T_map(L_map(u,x,y),z) = L_map(T_map(u,z),x,y);
attr Q is satisfying_TR means
:: AIMLOOP:def 9
for u,x,y,z be Element of Q holds
T_map(R_map(u,x,y),z) = R_map(T_map(u,z),x,y);
attr Q is satisfying_LR means
:: AIMLOOP:def 10
for u,x,y,z,w be Element of Q holds
L_map(R_map(u,x,y),z,w) = R_map(L_map(u,z,w),x,y);
attr Q is satisfying_LL means
:: AIMLOOP:def 11
for u,x,y,z,w be Element of Q holds
L_map(L_map(u,x,y),z,w) = L_map(L_map(u,z,w),x,y);
attr Q is satisfying_RR means
:: AIMLOOP:def 12
for u,x,y,z,w be Element of Q holds
R_map(R_map(u,x,y),z,w) = R_map(R_map(u,z,w),x,y);
end;
definition
let Q,x,y;
func K_op(x,y) -> Element of Q equals
:: AIMLOOP:def 13
(y * x) \ (x * y);
end;
definition
let Q,x,y,z;
func a_op(x,y,z) -> Element of Q equals
:: AIMLOOP:def 14
(x * (y * z)) \ ((x * y) * z);
end;
definition
let Q be multLoop;
attr Q is satisfying_aa1 means
:: AIMLOOP:def 15
for x,y,z,u,w be Element of Q holds a_op(a_op(x,y,z),u,w) = 1.Q;
attr Q is satisfying_aa2 means
:: AIMLOOP:def 16
for x,y,z,u,w be Element of Q holds a_op(x,a_op(y,z,u),w) = 1.Q;
attr Q is satisfying_aa3 means
:: AIMLOOP:def 17
for x,y,z,u,w be Element of Q holds a_op(x,y,a_op(z,u,w)) = 1.Q;
attr Q is satisfying_Ka means
:: AIMLOOP:def 18
for x,y,z,u be Element of Q holds K_op(a_op(x,y,z),u) = 1.Q;
attr Q is satisfying_aK1 means
:: AIMLOOP:def 19
for x,y,z,u be Element of Q holds a_op(K_op(x,y),z,u) = 1.Q;
attr Q is satisfying_aK2 means
:: AIMLOOP:def 20
for x,y,z,u be Element of Q holds a_op(x,K_op(y,z),u) = 1.Q;
attr Q is satisfying_aK3 means
:: AIMLOOP:def 21
for x,y,z,u be Element of Q holds a_op(x,y,K_op(z,u)) = 1.Q;
end;
registration
cluster strict satisfying_TT satisfying_TL satisfying_TR satisfying_LR
satisfying_LL satisfying_RR
satisfying_aa1 satisfying_aa2 satisfying_aa3
satisfying_Ka satisfying_aK1 satisfying_aK2 satisfying_aK3
for multLoop;
end;
theorem :: AIMLOOP:1
x * y = u & x * z = u implies y = z;
theorem :: AIMLOOP:2
y * x = u & z * x = u implies y = z;
theorem :: AIMLOOP:3
x * y = x * z implies y = z;
theorem :: AIMLOOP:4
y * x = z * x implies y = z;
registration
let Q,x;
reduce 1.Q \ x to x;
reduce x / 1.Q to x;
let y;
reduce y / (x \ y) to x;
reduce (y / x) \ y to x;
end;
theorem :: AIMLOOP:5
x \ x = 1.Q;
theorem :: AIMLOOP:6
x / x = 1.Q;
theorem :: AIMLOOP:7
x \ y = 1.Q implies x = y;
theorem :: AIMLOOP:8
x / y = 1.Q implies x = y;
theorem :: AIMLOOP:9
a_op(x,y,z) = 1.Q implies x*(y*z) = (x*y)*z;
theorem :: AIMLOOP:10
K_op(x,y) = 1.Q implies x*y = y*x;
theorem :: AIMLOOP:11
a_op(x,y,z) = 1.Q implies L_map(z,y,x) = z;
definition
let Q;
func Nucl_l Q -> Subset of Q means
:: AIMLOOP:def 22
x in it iff for y,z holds (x * y) * z = x * (y * z);
func Nucl_m Q -> Subset of Q means
:: AIMLOOP:def 23
y in it iff for x,z holds (x * y) * z = x * (y * z);
func Nucl_r Q -> Subset of Q means
:: AIMLOOP:def 24
z in it iff for x,y holds (x * y) * z = x * (y * z);
func Comm Q -> Subset of Q means
:: AIMLOOP:def 25
x in it iff for y holds x * y = y * x;
end;
definition
let Q;
func Nucl Q -> Subset of Q equals
:: AIMLOOP:def 26
Nucl_l Q /\ Nucl_m Q /\ Nucl_r Q;
end;
theorem :: AIMLOOP:12
x in Nucl Q iff x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q;
definition
let Q;
func Cent Q -> Subset of Q equals
:: AIMLOOP:def 27
Comm Q /\ Nucl Q;
end;
definition
let Q1,Q2 be multLoop;
let f be Function of Q1,Q2;
attr f is unity-preserving means
:: AIMLOOP:def 28
f.(1.Q1) = 1.Q2;
attr f is quasi-homomorphic means
:: AIMLOOP:def 29
for x,y being Element of Q1 holds f.(x * y) = (f.x) * (f.y);
end;
definition
let Q1,Q2 be multLoop;
let f be Function of Q1,Q2;
attr f is homomorphic means
:: AIMLOOP:def 30
f is unity-preserving quasi-homomorphic;
end;
registration
let Q1,Q2 be multLoop;
cluster unity-preserving quasi-homomorphic -> homomorphic
for Function of Q1,Q2;
cluster homomorphic -> unity-preserving quasi-homomorphic
for Function of Q1,Q2;
end;
registration
let Q1,Q2 be multLoop;
cluster [#]Q1 --> 1.Q2 -> homomorphic for Function of Q1,Q2;
end;
registration
let Q1,Q2 be multLoop;
cluster homomorphic for Function of Q1,Q2;
end;
definition
let Q,Q2;
let f be homomorphic Function of Q,Q2;
func Ker f -> Subset of Q means
:: AIMLOOP:def 31
x in it iff f.x = 1.Q2;
end;
theorem :: AIMLOOP:13
for f being homomorphic Function of Q1,Q2 holds
for x,y being Element of Q1 holds f.(x \ y) = f.x \ f.y;
theorem :: AIMLOOP:14
for f being homomorphic Function of Q1,Q2 holds
for x,y being Element of Q1 holds f.(x / y) = f.x / f.y;
theorem :: AIMLOOP:15
for f being homomorphic Function of Q1,Q2 st
(for y be Element of Q2 holds ex x being Element of Q1 st f.x = y)
&
(for x,y,z be Element of Q1 holds a_op(x,y,z) in Ker f)
holds
Q2 is associative;
theorem :: AIMLOOP:16
for Q1 being
satisfying_aa1 satisfying_aa2 satisfying_aa3
satisfying_aK1 satisfying_aK2 satisfying_aK3 multLoop
holds
for Q2 be multLoop holds
for f being homomorphic Function of Q1,Q2 st
(for y be Element of Q2 holds ex x being Element of Q1 st f.x = y)
&
Nucl Q1 c= Ker f
holds
Q2 is commutative multGroup;
theorem :: AIMLOOP:17
for Q1 being satisfying_aa1 satisfying_aa2 satisfying_aa3 satisfying_Ka
multLoop holds
for Q2 be multLoop holds
for f being homomorphic Function of Q1,Q2 st
(for y be Element of Q2 holds ex x being Element of Q1 st f.x = y)
&
Cent Q1 c= Ker f
holds
Q2 is multGroup;
:: following GROUP_2
definition
let Q be non empty multLoopStr;
mode SubLoopStr of Q -> non empty multLoopStr means
:: AIMLOOP:def 32
the carrier of it c= the carrier of Q &
the multF of it = (the multF of Q)||the carrier of it &
the OneF of it = the OneF of Q;
end;
registration
let Q be multLoop;
cluster well-unital invertible cancelable non empty strict
for SubLoopStr of Q;
end;
definition
let Q be multLoop;
mode SubLoop of Q is well-unital invertible cancelable SubLoopStr of Q;
end;
definition
let Q be non empty multLoopStr;
let H be SubLoopStr of Q;
let A be Subset of H;
func @ A -> Subset of Q equals
:: AIMLOOP:def 33
A;
end;
definition
let Q;
let H1,H2 be Subset of Q;
func loopclose1(H1,H2) -> Subset of Q means
:: AIMLOOP:def 34
x in it iff
x in H1 or x = 1.Q or
ex y,z st y in H2 & z in H2 & (x = y * z or x = y \ z or x = y / z);
end;
definition
let Q;
let H be Subset of Q;
func lp H -> strict SubLoop of Q means
:: AIMLOOP:def 35
H c= [#]it &
for H2 be SubLoop of Q st H c= [#]H2 holds [#]it c= [#]H2;
end;
theorem :: AIMLOOP:18
for H being Subset of Q st
1.Q in H & (for x,y st x in H & y in H holds x * y in H)
& (for x,y st x in H & y in H holds x \ y in H)
& (for x,y st x in H & y in H holds x / y in H)
holds
[#]lp H = H;
theorem :: AIMLOOP:19
for f being homomorphic Function of Q,Q2 holds
[#]lp (Ker f) = Ker f;
theorem :: AIMLOOP:20
1.Q in Nucl_l Q;
theorem :: AIMLOOP:21
1.Q in Nucl_m Q;
theorem :: AIMLOOP:22
1.Q in Nucl_r Q;
theorem :: AIMLOOP:23
1.Q in Nucl Q;
registration
let Q;
cluster Nucl_l Q -> non empty;
cluster Nucl_m Q -> non empty;
cluster Nucl_r Q -> non empty;
cluster Nucl Q -> non empty;
end;
theorem :: AIMLOOP:24
x in Nucl Q & y in Nucl Q implies x * y in Nucl Q;
theorem :: AIMLOOP:25
x in Nucl Q & y in Nucl Q implies x \ y in Nucl Q;
theorem :: AIMLOOP:26
x in Nucl Q & y in Nucl Q implies x / y in Nucl Q;
theorem :: AIMLOOP:27
[#]lp (Nucl Q) = Nucl Q;
theorem :: AIMLOOP:28
[#]lp (Cent Q) = Cent Q;
begin :: Multiplicative Mappings and Cosets
::We now define a set Mlt Q of multiplicative mappings of Q
::and cosets (mostly following Albert 1943 for cosets).
definition
let X be functional set;
attr X is composition-closed means
:: AIMLOOP:def 36
for f,g being Element of X st f in X & g in X holds f*g in X;
attr X is inverse-closed means
:: AIMLOOP:def 37
for f being Element of X st f in X holds f" in X;
end;
registration
let A be set;
cluster {id A} -> composition-closed inverse-closed;
end;
registration
cluster composition-closed inverse-closed non empty for functional set;
end;
registration
let Q be multLoopStr;
cluster composition-closed inverse-closed non empty for Subset of Funcs(Q,Q);
end;
definition
let Q be non empty multLoopStr;
let H be Subset of Q;
let S be Subset of Funcs(Q,Q);
pred H left-right-mult-closed S means
:: AIMLOOP:def 38
for u being Element of Q st u in H holds
(curry (the multF of Q)).u in S
&
(curry' (the multF of Q)).u in S;
end;
definition
let Q be non empty multLoopStr;
let H be Subset of Q;
let S be Subset of Funcs(Q,Q);
func MltClos1(H,S) -> Subset of Funcs(Q,Q) means
:: AIMLOOP:def 39
for f being object holds
f in it iff
(ex u be Element of Q st u in H & f = (curry' (the multF of Q)).u)
or
(ex u be Element of Q st u in H & f = (curry (the multF of Q)).u)
or
(ex g,h be Permutation of Q st g in S & h in S & f = g*h)
or
(ex g be Permutation of Q st g in S & f = g");
end;
theorem :: AIMLOOP:29
for H being Subset of Q holds
for phi being Function of bool Funcs(Q,Q),bool Funcs(Q,Q)
st
for X being Subset of Funcs(Q,Q) holds phi.X = MltClos1(H,X)
holds
phi is c=-monotone;
theorem :: AIMLOOP:30
for H being Subset of Q holds
for phi being Function of bool Funcs(Q,Q),bool Funcs(Q,Q) st
for X being Subset of Funcs(Q,Q) holds phi.X = MltClos1(H,X)
holds
for Y being Subset of Funcs(Q,Q) st phi.(Y) c= Y
holds
(for u being Element of Q st u in H holds (curry (the multF of Q)).u in Y)
&
(for u being Element of Q st u in H holds (curry' (the multF of Q)).u in Y);
theorem :: AIMLOOP:31
for H being Subset of Q holds
for phi being Function of bool Funcs(Q,Q),bool Funcs(Q,Q)
st
for X being Subset of Funcs(Q,Q) holds phi.X = MltClos1(H,X)
holds
for Y being Subset of Funcs(Q,Q)
st
for S be Subset of Funcs(Q,Q) st phi.S c= S holds Y c= S
holds
for f being Element of Funcs(Q,Q) st
f in Y holds
f is Permutation of Q;
theorem :: AIMLOOP:32
for H being Subset of Q holds
for phi being Function of bool Funcs(Q,Q),bool Funcs(Q,Q)
st
for X being Subset of Funcs(Q,Q) holds phi.X = MltClos1(H,X)
holds
for Y being Subset of Funcs(Q,Q)
st
Y is_a_fixpoint_of phi
& for S be Subset of Funcs(Q,Q) st phi.S c= S holds Y c= S
holds
Y is composition-closed
&
Y is inverse-closed;
theorem :: AIMLOOP:33
(curry (the multF of Q)).u is Permutation of Q;
theorem :: AIMLOOP:34
(curry' (the multF of Q)).u is Permutation of the carrier of Q;
definition
let Q;
let H be Subset of Q;
func Mlt H -> composition-closed inverse-closed Subset of Funcs(Q, Q) means
:: AIMLOOP:def 40
H left-right-mult-closed it
&
for X being composition-closed inverse-closed Subset of Funcs(Q,Q)
st H left-right-mult-closed X holds it c= X;
end;
theorem :: AIMLOOP:35
for H being Subset of Q holds
for u being Element of Q st u in H holds
(curry (the multF of Q)).u in Mlt H;
theorem :: AIMLOOP:36
for H being Subset of Q holds
for u being Element of Q st u in H holds
(curry' (the multF of Q)).u in Mlt H;
theorem :: AIMLOOP:37
for H being Subset of Q holds
for phi being Function of bool Funcs(Q,Q),bool Funcs(Q,Q)
st
for X being Subset of Funcs(Q,Q) holds phi.X = MltClos1(H,X)
holds
Mlt H is_a_fixpoint_of phi
&
for S be Subset of Funcs(Q,Q) st phi.S c= S holds Mlt H c= S;
theorem :: AIMLOOP:38
for H being Subset of Q holds
for f being Element of Funcs(Q,Q) st
f in Mlt H holds f is Permutation of Q;
definition
let Q;
let H be Subset of Q;
let x be Element of Q;
func x * H -> Subset of Q means
:: AIMLOOP:def 41
y in it iff ex h be Permutation of Q st h in Mlt H & y = h.x;
end;
definition
let Q;
let H be SubLoop of Q;
let x be Element of Q;
func x * H -> Subset of Q equals
:: AIMLOOP:def 42
x * (@ ([#] H));
end;
definition
let Q;
let N be SubLoop of Q;
func Cosets N -> Subset-Family of Q means
:: AIMLOOP:def 43
for H be Subset of Q holds H in it iff ex x st H = x * N;
end;
registration
let Q;
let N be SubLoop of Q;
cluster Cosets N -> non empty;
end;
begin :: Normal Subloop
::We define the notion of a normal subloop
::and construct quotients by normal subloops.
definition
let Q be multLoopStr;
let H1,H2 be Subset of Q;
func H1 * H2 -> Subset of Q means
:: AIMLOOP:def 44
for x being Element of Q holds
x in it iff
ex y,z be Element of Q st y in H1 & z in H2 & x = y * z;
func H1 \ H2 -> Subset of Q means
:: AIMLOOP:def 45
for x being Element of Q holds
x in it iff
ex y,z be Element of Q st y in H1 & z in H2 & x = y \ z;
end;
definition
let Q be multLoop;
let H be SubLoop of Q;
attr H is normal means
:: AIMLOOP:def 46
for x,y being Element of Q holds
(x * H) * (y * H) = (x * y) * H
&
for z being Element of Q holds
((x * H) * (y * H) = (x * H) * (z * H) implies (y * H) = (z * H))
&
((y * H) * (x * H) = (z * H) * (x * H) implies (y * H) = (z * H));
end;
registration
let Q;
cluster normal for SubLoop of Q;
end;
definition
let Q;
let N be normal SubLoop of Q;
func SubLoop_As_Coset N -> Element of Cosets N equals
:: AIMLOOP:def 47
1.Q * N;
end;
definition
let Q;
let N be normal SubLoop of Q;
func Coset_Loop_Op N -> BinOp of Cosets N
means
:: AIMLOOP:def 48
for H1,H2 be Element of Cosets N holds
it.(H1,H2) = H1 * H2;
end;
definition
let Q;
let N be normal SubLoop of Q;
func Q _/_ N -> strict multLoopStr equals
:: AIMLOOP:def 49
multLoopStr(#Cosets N,Coset_Loop_Op N,SubLoop_As_Coset N#);
end;
registration
let Q;
let N be normal SubLoop of Q;
cluster Q _/_ N -> non empty;
end;
registration
let Q;
let N be normal SubLoop of Q;
cluster Q _/_ N -> well-unital invertible cancelable;
end;
definition
let Q;
let N be normal SubLoop of Q;
func QuotientHom(Q,N) -> Function of Q,Q _/_ N means
:: AIMLOOP:def 50
for x holds it.x = x * N;
end;
registration
let Q;
let N be normal SubLoop of Q;
cluster QuotientHom(Q,N) -> homomorphic;
end;
theorem :: AIMLOOP:39
for H being SubLoop of Q holds
for x,y holds
for x1,y1 being Element of H st
x = x1 & y = y1
holds
x * y = x1 * y1;
theorem :: AIMLOOP:40
for H being SubLoop of Q holds
for x,y st x in the carrier of H & y in the carrier of H holds
x * y in the carrier of H;
theorem :: AIMLOOP:41
for H being SubLoop of Q holds
for x,y holds
for x1,y1 being Element of H st
x = x1 & y = y1
holds
x \ y = x1 \ y1;
theorem :: AIMLOOP:42
for H being SubLoop of Q holds
for x,y st x in the carrier of H & y in the carrier of H holds
x \ y in the carrier of H;
theorem :: AIMLOOP:43
for H being SubLoop of Q holds
for x,y holds
for x1,y1 being Element of H st
x = x1 & y = y1
holds
x / y = x1 / y1;
theorem :: AIMLOOP:44
for H being SubLoop of Q holds
for x,y st x in the carrier of H & y in the carrier of H holds
x / y in the carrier of H;
scheme :: AIMLOOP:sch 1
MltInd {Q() -> multLoop, H() -> Subset of Q(), P[Function of Q(),Q()]}:
for f being Function of Q(),Q() st f in Mlt H() holds P[f]
provided
for u being Element of Q() st u in H() holds
for f being Function of Q(),Q() st for x being Element of Q() holds
f.x = x * u holds P[f]
and
for u being Element of Q() st u in H() holds
for f being Function of Q(),Q() st for x being Element of Q() holds
f.x = u * x holds P[f]
and
for g,h being Permutation of Q() st P[g] & P[h] holds P[g*h]
and
for g being Permutation of Q() st P[g] holds P[g"];
theorem :: AIMLOOP:45
for N being SubLoop of Q holds
for f being Function of Q,Q st f in Mlt (@ ([#] N)) holds
for x holds x in (@ ([#] N)) iff f.x in (@ ([#] N));
theorem :: AIMLOOP:46
for N being normal SubLoop of Q holds
the carrier of N = 1.Q * N;
theorem :: AIMLOOP:47
for N being normal SubLoop of Q holds
Ker (QuotientHom(Q,N)) = @ ([#] N);
theorem :: AIMLOOP:48
for Q2 being multLoop holds
for f being homomorphic Function of Q,Q2 holds
for h being Function of Q,Q st h in Mlt (Ker f) holds
f*h = f;
theorem :: AIMLOOP:49
for Q2 being multLoop holds
for f being homomorphic Function of Q,Q2 holds
for x,y holds
y in x * Ker f iff f.x = f.y;
theorem :: AIMLOOP:50
for Q2 being multLoop holds
for f being homomorphic Function of Q,Q2 holds
for x,y holds
y in x * lp (Ker f) iff f.x = f.y;
theorem :: AIMLOOP:51
for Q2 being multLoop holds
for f being homomorphic Function of Q,Q2 holds
for x,y holds
x * lp (Ker f) = y * lp (Ker f) iff f.x = f.y;
theorem :: AIMLOOP:52
for Q2 being multLoop holds
for f being homomorphic Function of Q,Q2 holds
lp (Ker f) is normal;
theorem :: AIMLOOP:53
1.Q in [#] (lp (Cent Q)) & 1.Q in Cent Q;
theorem :: AIMLOOP:54
for f being Function of Q,Q st f in Mlt (Cent Q) holds
ex z st z in Cent Q & for x holds f.x = x * z;
theorem :: AIMLOOP:55
y in x * lp (Cent Q) iff ex z st z in Cent Q & y = x * z;
theorem :: AIMLOOP:56
x * lp (Cent Q) = y * lp (Cent Q) iff ex z st z in Cent Q & y = x * z;
theorem :: AIMLOOP:57
lp (Cent Q) is normal;
begin :: AIM Conjecture
::We define the set InnAut of inner mappings of Q,
::define the notion of an AIM loop and relate this to
::the conditions on T, L, and R defined by satisfies_TT, etc.
::For AIM loops we will prove the nucleus and the center are normal.
definition
let Q be multLoop;
func InnAut Q -> Subset of Funcs(Q,Q) means
:: AIMLOOP:def 51
for f being object holds
f in it iff
ex g being Function of Q,Q st
f = g & g in Mlt ([#] Q) & g.(1.Q) = 1.Q;
end;
registration
let Q be multLoop;
cluster InnAut Q -> non empty composition-closed inverse-closed;
end;
theorem :: AIMLOOP:58
for f being Function of Q,Q holds
f in InnAut Q iff f in Mlt ([#] Q) & f.(1.Q) = 1.Q;
definition
let Q be multLoop;
attr Q is AIM means
:: AIMLOOP:def 52
for f,g being Function of Q,Q st f in InnAut Q & g in InnAut Q holds
f*g = g*f;
end;
definition
let Q,x;
func T_MAP(x) -> Function of Q,Q means
:: AIMLOOP:def 53
for u holds it.u = T_map(u,x);
end;
theorem :: AIMLOOP:59
T_MAP(x) in InnAut Q;
definition
let Q,x,y;
func L_MAP(x,y) -> Function of Q,Q means
:: AIMLOOP:def 54
for u holds it.u = L_map(u,x,y);
end;
theorem :: AIMLOOP:60
L_MAP(x,y) in InnAut Q;
definition
let Q,x,y;
func R_MAP(x,y) -> Function of Q,Q means
:: AIMLOOP:def 55
for u holds it.u = R_map(u,x,y);
end;
theorem :: AIMLOOP:61
R_MAP(x,y) in InnAut Q;
registration
cluster Trivial-multLoopStr -> AIM;
end;
registration
cluster non empty strict AIM for multLoop;
end;
registration
cluster -> satisfying_TT satisfying_TL satisfying_TR satisfying_LR
satisfying_LL satisfying_RR for AIM multLoop;
end;
theorem :: AIMLOOP:62
for f being Function of Q,Q st f in Mlt (Nucl Q) holds
ex u,v st u in Nucl Q & v in Nucl Q & for x holds f.x = u * (x * v);
theorem :: AIMLOOP:63
y in x * lp (Nucl Q) iff
ex u,v st u in Nucl Q & v in Nucl Q & y = u * (x * v);
theorem :: AIMLOOP:64
x * lp (Nucl Q) = y * lp (Nucl Q) iff
ex u,v st u in Nucl Q & v in Nucl Q & y = u * (x * v);
:: Suggested result and proof by Kinyon Sep 10 2018
:: as crucial part of proving the nucleus of an AIM loop
:: is normal.
theorem :: AIMLOOP:65
for Q being AIM multLoop holds
for x,u being Element of Q holds
u in Nucl Q implies T_map(u,x) in Nucl Q;
theorem :: AIMLOOP:66
for Q being AIM multLoop holds
for x,u being Element of Q holds
u in Nucl Q implies (x * u) / x in Nucl Q;
:: This proof was difficult and required a hint from Kinyon.
:: Kinyon's hint was essentially the proof of NuclT above.
theorem :: AIMLOOP:67
Q is AIM implies lp (Nucl Q) is normal;
registration
let Q be AIM multLoop;
cluster lp (Nucl Q) -> normal;
end;
registration
let Q be multLoop;
cluster lp (Cent Q) -> normal;
end;
::$N Main Theorem The AIM Conjecture follows
::from knowing every AIM loop satisfies
::aa1, aa2, aa3, Ka, aK1, aK2 and aK3.
::This theorem justifies using first-order theorem provers
::to try to prove the AIM Conjecture.
theorem :: AIMLOOP:68
(for Q being multLoop st Q is satisfying_TT satisfying_TL satisfying_TR
satisfying_LR satisfying_LL satisfying_RR
holds Q is satisfying_aa1 satisfying_aa2 satisfying_aa3
satisfying_Ka satisfying_aK1 satisfying_aK2 satisfying_aK3)
implies
for Q being AIM multLoop holds
Q _/_ (lp (Nucl Q)) is commutative multGroup
&
Q _/_ (lp (Cent Q)) is multGroup;