:: Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups
:: by Dariusz Surowik
::
:: Received June 5, 1992
:: Copyright (c) 1992-2026 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 NUMBERS, GROUP_1, GROUP_2, GRAPH_1, GROUP_6, SUBSET_1, INT_1,
GR_CY_1, XXREAL_0, NEWTON, CARD_1, GROUP_4, STRUCT_0, FINSET_1, RELAT_1,
ARYTM_3, NAT_1, INT_2, ALGSTR_0, ARYTM_1, FINSEQ_1, FUNCT_1, TARSKI,
WELLORD1, FUNCT_2, GROUP_5, PRE_TOPC, XCMPLX_0, ORDINAL1;
notations TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, RELAT_1, FUNCT_1, FUNCT_2,
NUMBERS, INT_1, INT_2, CARD_1, NAT_D, GROUP_2, DOMAIN_1, STRUCT_0,
ALGSTR_0, GROUP_1, GROUP_3, GROUP_4, GROUP_5, GROUP_6, GR_CY_1, FINSEQ_1,
XXREAL_0;
constructors BINOP_1, DOMAIN_1, REAL_1, NAT_D, BINOP_2, GROUP_4, GROUP_5,
GROUP_6, GR_CY_1, RELSET_1;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1,
STRUCT_0, GROUP_1, GROUP_2, GR_CY_1, ORDINAL1, FINSET_1, MEMBERED,
CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCT_1, TARSKI;
equalities ALGSTR_0, GR_CY_1;
expansions GR_CY_1;
theorems FUNCT_2, GROUP_1, GROUP_2, GROUP_4, GROUP_5, FUNCT_1, GROUP_6,
GR_CY_1, NAT_1, INT_1, INT_2, FINSEQ_1, XBOOLE_0, XCMPLX_1, NEWTON,
XREAL_1, ORDINAL1, NAT_D, STRUCT_0, XXREAL_0, RELAT_1;
schemes FUNCT_2, FINSEQ_1;
begin
reserve F,G for Group;
reserve G1 for Subgroup of G;
reserve Gc for cyclic Group;
reserve H for Subgroup of Gc;
reserve f for Homomorphism of G,Gc;
reserve a,b for Element of G;
reserve g for Element of Gc;
reserve a1 for Element of G1;
reserve k,m,n,p,s for Element of NAT;
reserve i0,i,i1,i2 for Integer;
reserve j,j1 for Element of INT.Group;
reserve x,y,t for set;
theorem
ord a>1 & a=b|^k implies k<>0
proof
assume that
A1: ord a>1 and
A2: a=b|^k & k=0;
a=1_G by A2,GROUP_1:25;
hence contradiction by A1,GROUP_1:42;
end;
:: Some properties of Cyclic Groups
theorem Th2:
a in gr {a}
proof
ex i st a=a|^i
proof
reconsider i=1 as Integer;
take i;
thus thesis by GROUP_1:26;
end;
hence thesis by GR_CY_1:5;
end;
theorem Th3:
a=a1 implies gr {a} = gr {a1}
proof
reconsider Gr = gr {a1} as Subgroup of G by GROUP_2:56;
assume
A1: a= a1;
A2: for b holds b in Gr implies b in gr {a}
proof
let b;
assume
A3: b in Gr;
then b in G1 by GROUP_2:40;
then reconsider b1=b as Element of G1 by STRUCT_0:def 5;
consider i such that
A4: b1= a1|^i by A3,GR_CY_1:5;
b=a|^i by A1,A4,GROUP_4:2;
hence thesis by GR_CY_1:5;
end;
for b holds b in gr {a} implies b in Gr
proof
let b;
assume b in gr {a};
then consider i such that
A5: b= a|^i by GR_CY_1:5;
b=a1|^i by A1,A5,GROUP_4:2;
hence thesis by GR_CY_1:5;
end;
hence thesis by A2,GROUP_2:60;
end;
theorem Th4:
gr {a} is cyclic Group
proof
ex a1 being Element of gr {a} st gr {a}=gr {a1}
proof
a in gr {a} by Th2;
then reconsider a1=a as Element of gr {a} by STRUCT_0:def 5;
take a1;
thus thesis by Th3;
end;
hence thesis by GR_CY_1:def 7;
end;
theorem Th5:
for G being strict Group,b being Element of G holds ( for a
being Element of G holds ex i st a=b|^i ) iff G = gr {b}
proof
let G be strict Group;
let b be Element of G;
thus ( for a being Element of G holds ex i st a=b|^i ) implies G = gr {b}
proof
assume
A1: for a being Element of G holds ex i st a=b|^i;
for a being Element of G holds a in gr {b}
proof
let a be Element of G;
ex i st a=b|^i by A1;
hence thesis by GR_CY_1:5;
end;
hence thesis by GROUP_2:62;
end;
assume
A2: G= gr {b};
let a be Element of G;
a in gr {b} by A2,STRUCT_0:def 5;
hence thesis by GR_CY_1:5;
end;
theorem Th6:
for G being strict finite Group,b being Element of G holds (for
a being Element of G holds ex p st a=b|^p) iff G = gr {b}
proof
let G be strict finite Group,b be Element of G;
reconsider n1=card G as Integer;
thus (for a being Element of G holds ex p st a=b|^p) implies G = gr {b}
proof
assume
A1: for a being Element of G holds ex p st a=b|^p;
for a being Element of G holds ex i st a=b|^i
proof
let a be Element of G;
consider p such that
A2: a=b|^p by A1;
reconsider p1=p as Integer;
take p1;
thus thesis by A2;
end;
hence thesis by Th5;
end;
assume
A3: G= gr {b};
let a be Element of G;
consider i such that
A4: a= b|^i by A3,Th5;
reconsider p=i mod n1 as Element of NAT by INT_1:3;
take p;
a = b|^((i div n1) * n1 + (i mod n1)) by A4,NEWTON:66
.= b|^((i div n1)*n1) *(b|^(i mod n1)) by GROUP_1:33
.= b|^(i div n1)|^card G *(b|^(i mod n1)) by GROUP_1:35
.= (1_G) *(b|^(i mod n1)) by GR_CY_1:9
.= b|^(i mod n1) by GROUP_1:def 4;
hence thesis;
end;
theorem Th7:
for G being strict Group,a being Element of G holds G is finite
& G = gr {a} implies for G1 being strict Subgroup of G holds ex p st G1 = gr {a
|^p}
proof
let G be strict Group,a be Element of G;
assume that
A1: G is finite and
A2: G = gr {a};
let G1 be strict Subgroup of G;
G is cyclic Group by A2,GR_CY_1:def 7;
then G1 is cyclic Group by A1,GR_CY_1:20;
then consider b being Element of G1 such that
A3: G1 = gr {b} by GR_CY_1:def 7;
reconsider b1 = b as Element of G by GROUP_2:42;
consider p such that
A4: b1 = a|^p by A1,A2,Th6;
take p;
thus thesis by A3,A4,Th3;
end;
theorem Th8:
for G being finite Group, a being Element of G holds G=gr {a} &
card G = n & n = p * s implies ord (a|^p) = s
proof
let G be finite Group, a be Element of G;
assume that
A1: G=gr {a} and
A2: card G = n and
A3: n = p * s;
A4: a|^p is not being_of_order_0 & s <> 0 by A2,A3,GR_CY_1:6;
A5: p <> 0 by A2,A3;
A6: for k being Nat st a|^p|^ k = 1_G & k <> 0 holds s <= k
proof
let k be Nat;
assume that
A7: a|^p|^k=1_G and
A8: k <> 0 & s > k;
A9: a|^(p*k) = 1_G by A7,GROUP_1:35;
A10: ord a = n & a is not being_of_order_0 by A1,A2,GR_CY_1:6,7;
p*s > p*k & p*k <> 0 by A5,A8,XCMPLX_1:6,XREAL_1:68;
hence contradiction by A3,A10,A9,GROUP_1:def 11;
end;
a|^p|^s = a|^n by A3,GROUP_1:35
.=1_G by A2,GR_CY_1:9;
hence thesis by A4,A6,GROUP_1:def 11;
end;
theorem Th9:
s divides k implies a|^k in gr {a|^s}
proof
assume s divides k;
then consider p be Nat such that
A1: k=s*p by NAT_D:def 3;
ex i st a|^k=a|^s|^i
proof
reconsider p9=p as Integer;
take p9;
thus thesis by A1,GROUP_1:35;
end;
hence thesis by GR_CY_1:5;
end;
theorem Th10:
for G being finite Group, a being Element of G holds card gr {a
|^s} = card gr {a|^k} & a|^k in gr {a|^s} implies gr {a|^s} = gr {a|^k}
proof
let G be finite Group, a be Element of G;
assume
A1: card gr {a|^s} = card gr {a|^k};
assume a|^k in gr {a|^s};
then reconsider h=a|^k as Element of gr {a|^s} by STRUCT_0:def 5;
card gr {h} = card gr {a|^s} by A1,Th3;
hence gr {a|^s} = gr {h} by GROUP_2:73
.= gr {a|^k} by Th3;
end;
theorem Th11:
for G being finite Group, G1 being Subgroup of G, a being
Element of G holds card G = n & G=gr {a} & card G1 = p & G1= gr{a|^k} implies n
divides k*p
proof
let G be finite Group, G1 be Subgroup of G, a be Element of G;
assume that
A1: card G = n and
A2: G=gr {a} and
A3: card G1 = p and
A4: G1= gr{a|^k};
set z=k*p;
consider m,l being Nat such that
A5: z=(n*m)+l and
A6: l < n by A1,NAT_1:17;
l=0
proof
a|^k in gr {a|^k} by Th2;
then reconsider h=a|^k as Element of G1 by A4,STRUCT_0:def 5;
assume
A7: l<>0;
a|^z = a|^k|^p by GROUP_1:35
.= h|^p by GROUP_4:1
.= 1_G1 by A3,GR_CY_1:9
.= 1_G by GROUP_2:44;
then
A8: 1_G = (a|^(n*m))*(a|^l) by A5,GROUP_1:33
.= (a|^n|^m)*(a|^l) by GROUP_1:35
.= ((1_G)|^m)*(a|^l) by A1,GR_CY_1:9
.= (1_G)*(a|^l) by GROUP_1:31
.= a|^l by GROUP_1:def 4;
a is not being_of_order_0 & ord a = n by A1,A2,GR_CY_1:6,7;
hence contradiction by A6,A7,A8,GROUP_1:def 11;
end;
hence thesis by A5,NAT_D:def 3;
end;
theorem
for G being strict finite Group, a be Element of G holds G = gr {a} &
card G = n implies ( G = gr {a|^k} iff k gcd n = 1 )
proof
let G be strict finite Group, a be Element of G;
assume that
A1: G = gr {a} and
A2: card G = n;
A3: G=gr {a|^k} implies k gcd n = 1
proof
set d=k gcd n;
assume that
A4: G = gr {a|^k} and
A5: k gcd n <> 1;
d divides n by NAT_D:def 5;
then consider p be Nat such that
A6: n=d*p by NAT_D:def 3;
A7: p <> 0 by A2,A6;
A8: p <> n
proof
assume p=n;
then d*p = p*1 by A6;
hence contradiction by A5,A2,A6,XCMPLX_1:5;
end;
d divides k by NAT_D:def 5;
then consider l be Nat such that
A9: k=d*l by NAT_D:def 3;
A10: a|^k is not being_of_order_0 by GR_CY_1:6;
(a|^k)|^p = a|^((l*d)*p) by A9,GROUP_1:35
.=a|^(n*l) by A6
.=a|^n|^l by GROUP_1:35
.=(1_G)|^l by A2,GR_CY_1:9
.= 1_G by GROUP_1:31;
then
A11: ord (a|^k) <= p by A7,A10,GROUP_1:def 11;
p divides n by A6,NAT_D:def 3;
then p <= n by A2,NAT_D:7;
then p<n by A8,XXREAL_0:1;
hence contradiction by A2,A4,A11,GR_CY_1:7;
end;
k gcd n = 1 implies G=gr {a|^k}
proof
assume k gcd n = 1;
then consider i,i1 such that
A12: i*k+ i1*n=1 by NEWTON:67;
for b be Element of G holds b in gr {a|^k}
proof
let b be Element of G;
b in G by STRUCT_0:def 5;
then consider i0 such that
A13: b=a|^i0 by A1,GR_CY_1:5;
A14: i0=(k*i+n*i1)*i0 by A12
.= k*i*i0+n*i1*i0;
ex i2 st b=(a|^k)|^i2
proof
take i*i0;
b= (a|^(k*i*i0)) *a|^(n*(i1*i0)) by A13,A14,GROUP_1:33
.= (a|^(k*i*i0))*a|^n|^(i1*i0) by GROUP_1:35
.= (a|^(k*i*i0))*(1_G)|^(i1*i0) by A2,GR_CY_1:9
.= (a|^(k*i*i0))*1_G by GROUP_1:31
.= a|^(k*(i*i0)) by GROUP_1:def 4
.= a|^k|^(i*i0) by GROUP_1:35;
hence thesis;
end;
hence thesis by GR_CY_1:5;
end;
hence thesis by GROUP_2:62;
end;
hence thesis by A3;
end;
theorem Th13:
Gc = gr {g} & g in H implies the multMagma of Gc = the multMagma of H
proof
assume that
A1: Gc=gr{g} and
A2: g in H;
reconsider g9=g as Element of H by A2,STRUCT_0:def 5;
gr {g9} is Subgroup of H;
then gr {g} is Subgroup of H by Th3;
hence thesis by A1,GROUP_2:55;
end;
theorem Th14:
Gc = gr {g} implies ( Gc is finite iff ex i,i1 st i<>i1 & g|^i = g|^i1 )
proof
assume
A1: Gc = gr {g};
A2: ( ex i,i1 st i<>i1 & g|^i = g|^i1) implies Gc is finite
proof
given i,i1 such that
A3: i<>i1 and
A4: g|^i = g|^i1;
now
per cases by A3,XXREAL_0:1;
suppose
A5: i < i1;
set r = i1-i;
i1 > i+0 by A5;
then
A6: i1-i > 0 by XREAL_1:20;
then reconsider m=r as Element of NAT by INT_1:3;
(g|^i1)*g|^(-i) = (g|^i) *(g|^(i))" by A4,GROUP_1:36;
then (g|^i1)*g|^(-i) = 1_Gc by GROUP_1:def 5;
then
A7: g|^(i1+-i) = 1_Gc by GROUP_1:33;
A8: for i2 ex n st g|^i2=g|^n & n >= 0 & n < i1-i
proof
let i2;
reconsider m=i2 mod r as Element of NAT by A6,INT_1:3;
take m;
g|^i2 = g|^( (i2 div r) * r + (i2 mod r) ) by A6,NEWTON:66
.=g|^(r* (i2 div r) ) *(g|^ (i2 mod r)) by GROUP_1:33
.=(1_Gc)|^(i2 div r) *(g|^ (i2 mod r)) by A7,GROUP_1:35
.=(1_Gc) *(g|^ (i2 mod r)) by GROUP_1:31
.=g|^ (i2 mod r) by GROUP_1:def 4;
hence thesis by A6,NEWTON:65;
end;
ex F being FinSequence st rng F= the carrier of Gc
proof
deffunc F(Nat) = g|^$1;
consider F being FinSequence such that
A9: len F = m and
A10: for p be Nat holds p in dom F implies F.p = F(p) from
FINSEQ_1:sch 2;
A11: dom F = Seg m by A9,FINSEQ_1:def 3;
A12: the carrier of Gc c= rng F
proof
let y be object;
assume y in the carrier of Gc;
then reconsider a=y as Element of Gc;
a in Gc by STRUCT_0:def 5;
then
A13: ex i2 st a=g|^i2 by A1,GR_CY_1:5;
ex n st n in dom F & F.n=a
proof
consider n such that
A14: a=g|^n and
n >= 0 and
A15: n < i1-i by A8,A13;
per cases;
suppose
A16: n=0;
A17: m >= 0 +1 by A6,NAT_1:13;
then
A18: m in Seg m by FINSEQ_1:1;
A19: m in dom F by A11,A17,FINSEQ_1:1;
a = g|^m by A7,A14,A16,GROUP_1:25;
then F.m = a by A10,A11,A18;
hence thesis by A19;
end;
suppose
n >0;
then
A20: n >= 0 +1 by NAT_1:13;
then n in Seg m by A15,FINSEQ_1:1;
then
A21: F.n = a by A10,A11,A14;
n in dom F by A11,A15,A20,FINSEQ_1:1;
hence thesis by A21;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
take F;
A22: for y st y in rng F holds ex n st y=g|^n
proof
let y;
assume y in rng F;
then consider x being object such that
A23: x in dom F and
A24: F.x=y by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A23;
take n;
thus thesis by A10,A23,A24;
end;
rng F c= the carrier of Gc
proof
let y be object;
assume y in rng F;
then ex n st y= g|^n by A22;
hence thesis;
end;
hence thesis by A12,XBOOLE_0:def 10;
end;
hence thesis;
end;
suppose
A25: i1 < i;
set r = i-i1;
i > i1+0 by A25;
then
A26: i-i1 > 0 by XREAL_1:20;
then reconsider m=r as Element of NAT by INT_1:3;
(g|^i)*g|^(-i1) = (g|^i1) *(g|^(i1))" by A4,GROUP_1:36;
then (g|^i)*g|^(-i1) = 1_Gc by GROUP_1:def 5;
then
A27: g|^(i+-i1) = 1_Gc by GROUP_1:33;
A28: for i2 ex n st g|^i2=g|^n & n >= 0 & n < i-i1
proof
let i2;
reconsider m=i2 mod r as Element of NAT by A26,INT_1:3;
take m;
g|^i2 = g|^( (i2 div r) * r + (i2 mod r) ) by A26,NEWTON:66
.=g|^(r* (i2 div r) ) *(g|^ (i2 mod r)) by GROUP_1:33
.=(1_Gc)|^(i2 div r) *(g|^ (i2 mod r)) by A27,GROUP_1:35
.=(1_Gc) *(g|^ (i2 mod r)) by GROUP_1:31
.=g|^ (i2 mod r) by GROUP_1:def 4;
hence thesis by A26,NEWTON:65;
end;
ex F being FinSequence st rng F= the carrier of Gc
proof
deffunc F(Nat) = g|^$1;
consider F being FinSequence such that
A29: len F = m and
A30: for p be Nat holds p in dom F implies F.p=F(p) from
FINSEQ_1:sch 2;
A31: dom F = Seg m by A29,FINSEQ_1:def 3;
A32: the carrier of Gc c= rng F
proof
let y be object;
assume y in the carrier of Gc;
then reconsider a=y as Element of Gc;
a in Gc by STRUCT_0:def 5;
then
A33: ex i2 st a=g|^i2 by A1,GR_CY_1:5;
ex n st n in dom F & F.n=a
proof
consider n such that
A34: a=g|^n and
n >= 0 and
A35: n < i-i1 by A28,A33;
per cases;
suppose
A36: n=0;
A37: m >= 0 +1 by A26,NAT_1:13;
then
A38: m in Seg m by FINSEQ_1:1;
A39: m in dom F by A31,A37,FINSEQ_1:1;
a = g|^m by A27,A34,A36,GROUP_1:25;
then F.m = a by A30,A31,A38;
hence thesis by A39;
end;
suppose
n >0;
then
A40: n >= 0 +1 by NAT_1:13;
then n in Seg m by A35,FINSEQ_1:1;
then
A41: F.n = a by A30,A31,A34;
n in dom F by A31,A35,A40,FINSEQ_1:1;
hence thesis by A41;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
take F;
A42: for y st y in rng F holds ex n st y=g|^n
proof
let y;
assume y in rng F;
then consider x being object such that
A43: x in dom F and
A44: F.x=y by FUNCT_1:def 3;
reconsider n=x as Element of NAT by A43;
take n;
thus thesis by A30,A43,A44;
end;
rng F c= the carrier of Gc
proof
let y be object;
assume y in rng F;
then ex n st y= g|^n by A42;
hence thesis;
end;
hence thesis by A32,XBOOLE_0:def 10;
end;
hence thesis;
end;
end;
hence thesis;
end;
Gc is finite implies ex i,i1 st i<>i1 & g|^i = g|^i1
proof
assume Gc is finite;
then reconsider Gc as finite cyclic Group;
reconsider z=0,i0=card Gc as Integer;
A45: g|^z = 1_Gc by GROUP_1:25
.= g|^i0 by GR_CY_1:9;
thus thesis by A45;
end;
hence thesis by A2;
end;
registration
let n be non zero Nat;
cluster -> natural for Element of INT.Group(n);
coherence;
end;
:: Isomorphisms of Cyclic Groups.
theorem Th15:
for Gc being strict finite cyclic Group
holds INT.Group(card Gc),Gc are_isomorphic
proof
let Gc be strict finite cyclic Group;
set n = card Gc;
consider g being Element of Gc such that
A1: for h be Element of Gc ex p being Nat st h=g|^p by GR_CY_1:18;
for h be Element of Gc holds ex i st h=g|^i
proof
let h be Element of Gc;
consider p being Nat such that
A2: h=g|^p by A1;
reconsider p1=p as Integer;
take p1;
thus thesis by A2;
end;
then
A3: Gc = gr {g} by Th5;
ex h being Homomorphism of INT.Group(n),Gc st h is bijective
proof
deffunc F(Element of INT.Group(n)) = g|^$1;
consider h being Function of the carrier of INT.Group(n),the carrier of Gc
such that
A4: for p be Element of INT.Group(n) holds h.p=F(p) from FUNCT_2:sch 4;
A5: for j,j1 being Element of INT.Group(n) holds h.(j*j1)=h.(j)*h.(j1)
proof
let j,j1 be Element of INT.Group(n);
reconsider j9=j,j19=j1 as Element of Segm(n);
j*j1 = (j+j1) mod n by GR_CY_1:def 4
.=(j+j1)- n*((j+j1) div n) by NEWTON:63;
then h.(j*j1) = g|^((j+j1) +-n *((j+j1) div n)) by A4
.= g|^(j+j1) *g|^(-n *((j+j1) div n)) by GROUP_1:33
.= g|^(j+j1)*(g|^(n *((j+j1) div n)))" by GROUP_1:36
.= g|^(j+j1)*(g|^n|^((j+j1) div n))" by GROUP_1:35
.= g|^(j+j1)*((1_Gc)|^((j+j1) div n))" by GR_CY_1:9
.= g|^(j+j1)*(1_Gc)" by GROUP_1:31
.= g|^(j+j1)*(1_Gc) by GROUP_1:8
.= g|^(j+j1) by GROUP_1:def 4
.= (g|^j)*(g|^j1) by GROUP_1:33
.= h.(j)*(g|^j1) by A4
.= h.(j)*h.(j1) by A4;
hence thesis;
end;
A6: h is one-to-one
proof
let x,y be object;
assume that
A7: x in dom h and
A8: y in dom h and
A9: h.x=h.y and
A10: x<>y;
reconsider m=y as Element of INT.Group(n) by A8,FUNCT_2:def 1;
reconsider p=x as Element of INT.Group(n) by A7,FUNCT_2:def 1;
A11: g|^p=h.m by A4,A9
.= g|^m by A4;
reconsider p,m as Element of NAT by ORDINAL1:def 12;
A12: p < n by NAT_1:44;
A13: m < n by NAT_1:44;
A14: ex k st k<>0 & k < n & g|^k=1_Gc
proof
per cases by A10,XXREAL_0:1;
suppose
A15: p < m;
reconsider m1=m,p1=p as Integer;
reconsider r1 = (m1-p1) as Element of NAT by A15,INT_1:5;
per cases;
suppose
A16: r1 >0;
set z=0;
A17: r1 < n
proof
reconsider n1=n as Integer;
m1+-p1 < n1+0 by A13,XREAL_1:8;
hence thesis;
end;
g|^m1*(g|^(-p1)) = g|^(p1+-p1) by A11,GROUP_1:33;
then g|^(m1+-p1) = g|^z by GROUP_1:33;
hence thesis by A16,A17,GROUP_1:25;
end;
suppose
r1 = 0;
hence thesis by A10;
end;
end;
suppose
A18: m < p;
reconsider m1=m,p1=p as Integer;
reconsider r1 = (p1-m1) as Element of NAT by A18,INT_1:5;
per cases;
suppose
A19: r1 >0;
set z=0;
A20: r1 < n
proof
reconsider n1=n as Integer;
p1+-m1 < n1+0 by A12,XREAL_1:8;
hence thesis;
end;
g|^p1*(g|^(-m1)) = g|^(m1+-m1) by A11,GROUP_1:33;
then g|^(p1+-m1) = g|^z by GROUP_1:33;
hence thesis by A19,A20,GROUP_1:25;
end;
suppose
r1 = 0;
hence thesis by A10;
end;
end;
end;
g is not being_of_order_0 & ord g = n by A3,GR_CY_1:6,7;
hence contradiction by A14,GROUP_1:def 11;
end;
A21: dom h = the carrier of INT.Group(n) by FUNCT_2:def 1;
A22: the carrier of Gc c= rng h
proof
let x be object;
assume x in the carrier of Gc;
then reconsider z=x as Element of Gc;
consider p being Nat such that
A23: z=g|^p by A1;
set t=p mod n;
t < n by NAT_D:1;
then reconsider t9=t as Element of INT.Group(n) by NAT_1:44;
z=g|^(n * (p div n) + (p mod n)) by A23,NAT_D:2
.=g|^(n * (p div n))*(g|^(p mod n)) by GROUP_1:33
.=g |^ n |^ (p div n)*(g |^ (p mod n)) by GROUP_1:35
.=(1_Gc) |^ (p div n)*(g |^ (p mod n)) by GR_CY_1:9
.=(1_Gc)*(g |^ (p mod n)) by GROUP_1:31
.=(g |^ (p mod n)) by GROUP_1:def 4;
then t9 in dom h & x=h.(t9) by A4,A21;
hence thesis by FUNCT_1:def 3;
end;
rng h c= the carrier of Gc by RELAT_1:def 19;
then
A24: rng h = the carrier of Gc by A22,XBOOLE_0:def 10;
reconsider h as Homomorphism of INT.Group(n),Gc by A5,GROUP_6:def 6;
take h;
h is onto by A24,FUNCT_2:def 3;
hence thesis by A6,FUNCT_2:def 4;
end;
hence thesis by GROUP_6:def 11;
end;
theorem
for Gc being strict cyclic Group st Gc is infinite holds INT.Group,Gc
are_isomorphic
proof
let Gc be strict cyclic Group;
consider g being Element of Gc such that
A1: for h be Element of Gc holds ex i st h=g|^i by GR_CY_1:17;
assume
A2: Gc is infinite;
ex h being Homomorphism of INT.Group,Gc st h is bijective
proof
deffunc F(Element of INT.Group) = g|^@'$1;
consider h being Function of the carrier of INT.Group,the carrier of Gc
such that
A3: for j1 be Element of INT.Group holds h.j1=F(j1) from FUNCT_2:sch 4;
A4: Gc=gr {g} by A1,Th5;
A5: h is one-to-one
proof
let x,y be object;
assume that
A6: x in dom h and
A7: y in dom h and
A8: h.x=h.y and
A9: x<>y;
reconsider y9=y as Element of INT.Group by A7,FUNCT_2:def 1;
reconsider x9=x as Element of INT.Group by A6,FUNCT_2:def 1;
g|^@'x9=h.y9 by A3,A8
.= g|^@'y9 by A3;
hence contradiction by A2,A4,A9,Th14;
end;
A10: dom h = the carrier of INT.Group by FUNCT_2:def 1;
A11: the carrier of Gc c= rng h
proof
let x be object;
assume x in the carrier of Gc;
then reconsider z=x as Element of Gc;
consider i such that
A12: z=g|^i by A1;
reconsider i9=i as Element of INT.Group by INT_1:def 2;
i=@'i9;
then x = h.(i9) by A3,A12;
hence thesis by A10,FUNCT_1:def 3;
end;
rng h c= the carrier of Gc by RELAT_1:def 19;
then
A13: rng h = the carrier of Gc by A11,XBOOLE_0:def 10;
for j,j1 holds h.(j*j1)=h.(j)*h.(j1)
proof
let j,j1;
@'(j*j1)= @'j+@'j1;
then h.(j*j1) = g|^(@'j+@'j1) by A3
.= (g|^@'j)*(g|^@'j1) by GROUP_1:33
.= h.(j)*(g|^@'j1) by A3
.= h.(j)*h.(j1) by A3;
hence thesis;
end;
then reconsider h as Homomorphism of INT.Group,Gc by GROUP_6:def 6;
take h;
h is onto by A13,FUNCT_2:def 3;
hence thesis by A5,FUNCT_2:def 4;
end;
hence thesis by GROUP_6:def 11;
end;
theorem Th17:
for Gc, Hc being strict finite cyclic Group st card Hc = card Gc
holds Hc,Gc are_isomorphic
proof
let Gc, Hc be strict finite cyclic Group;
set p = card Hc;
assume card Hc = card Gc;
then
A1: INT.Group(p),Gc are_isomorphic by Th15;
INT.Group(p),Hc are_isomorphic by Th15;
hence thesis by A1,GROUP_6:67;
end;
theorem Th18:
for F,G being strict finite Group st card F = p & card G = p & p
is prime holds F,G are_isomorphic
proof
let F,G be strict finite Group;
assume that
A1: card F = p & card G = p and
A2: p is prime;
F is cyclic Group & G is cyclic Group by A1,A2,GR_CY_1:21;
hence thesis by A1,Th17;
end;
theorem
for F,G being strict finite Group st card F = 2 & card G = 2 holds F,G
are_isomorphic by Th18,INT_2:28;
theorem
for G being strict finite Group holds card G = 2 implies for H being
strict Subgroup of G holds H = (1).G or H = G by GR_CY_1:12,INT_2:28;
theorem
for G being strict finite Group st card G = 2 holds G is cyclic Group
by GR_CY_1:21,INT_2:28;
theorem
for G being strict finite Group st G is cyclic & card G = n holds for
p st p divides n holds ex G1 being strict Subgroup of G st card G1 = p & for G2
being strict Subgroup of G st card G2 = p holds G2=G1
proof
let G be strict finite Group;
assume that
A1: G is cyclic and
A2: card G = n;
let p such that
A3: p divides n;
ex G1 being strict Subgroup of G st card G1 = p & for G2 being strict
Subgroup of G st card G2=p holds G2=G1
proof
consider s be Nat such that
A4: n=p*s by A3,NAT_D:def 3;
consider a being Element of G such that
A5: G= gr {a} by A1;
take gr {a|^s};
A6: s in NAT by ORDINAL1:def 12;
then
A7: ord (a|^s) = p by A2,A5,A4,Th8;
then
A8: card gr {a|^s} = p by GR_CY_1:7;
for G2 being strict Subgroup of G st card G2 = p holds G2=gr {a|^s}
proof
let G2 be strict Subgroup of G such that
A9: card G2 = p;
consider k such that
A10: G2 = gr {a|^k} by A5,Th7;
n divides k*p by A2,A5,A9,A10,Th11;
then consider m be Nat such that
A11: k*p=n*m by NAT_D:def 3;
ex l be Nat st k=s*l
proof
take m;
reconsider p1=p as Integer;
A12: p<>0 by A2,A4;
(1/p1)*p1 *k = (1/p1)*(p1*s*m) by A4,A11,XCMPLX_1:4;
then 1*k = p1*(1/p1)*s*m by A12,XCMPLX_1:106;
then k = 1*s*m by A12,XCMPLX_1:106;
hence thesis;
end;
then s divides k by NAT_D:def 3;
hence thesis by A6,A8,A9,A10,Th9,Th10;
end;
hence thesis by A7,GR_CY_1:7;
end;
hence thesis;
end;
theorem
Gc=gr{g} implies for G,f holds g in Image f implies f is onto
proof
assume
A1: Gc=gr {g};
let G,f;
assume g in Image f;
then Image f = Gc by A1,Th13;
hence thesis by GROUP_6:57;
end;
theorem Th24:
for Gc being strict finite cyclic Group st (ex k st card Gc = 2*
k) holds ex g1 being Element of Gc st ord g1 = 2 & for g2 being Element of Gc
st ord g2 = 2 holds g1=g2
proof
let Gc be strict finite cyclic Group;
set n = card Gc;
given k such that
A1: n=2*k;
consider g being Element of Gc such that
A2: Gc=gr{g} by GR_CY_1:def 7;
A3: ord g = n by A2,GR_CY_1:7;
take g|^k;
A4: g|^k|^2=g|^card Gc by A1,GROUP_1:35
.= 1_Gc by GR_CY_1:9;
A5: k<>0 by A1;
A6: for p being Nat st g|^k|^ p = 1_Gc & p <> 0 holds 2 <= p
proof
let p be Nat;
assume that
A7: g|^k|^p=1_Gc and
A8: p<>0 & 2>p;
A9: g is not being_of_order_0 & 1_Gc = g|^(k*p) by A7,GROUP_1:35,GR_CY_1:6;
n>k*p & k*p<>0 by A1,A5,A8,XCMPLX_1:6,XREAL_1:68;
hence contradiction by A3,A9,GROUP_1:def 11;
end;
g|^k is not being_of_order_0 by GR_CY_1:6;
hence ord(g|^k) = 2 by A4,A6,GROUP_1:def 11;
let g2 be Element of Gc;
consider k1 being Element of NAT such that
A10: g2=g|^k1 by A2,Th6;
assume that
A11: ord g2=2 and
A12: g|^k<>g2;
now
A13: g is not being_of_order_0 by GR_CY_1:6;
consider t,t1 being Nat such that
A14: k1=(k*t)+t1 and
A15: t1<k by A5,NAT_1:17;
A16: 2*t1<n by A1,A15,XREAL_1:68;
t1<>0
proof
assume t1=0;
then
A17: g|^k1=g|^(k*( 2*(t div 2)+(t mod 2) )) by A14,NAT_D:2
.=g|^( k* 2*(t div 2)+ k*(t mod 2) )
.=g|^( k* 2*(t div 2) )*(g|^( k*(t mod 2))) by GROUP_1:33
.=g|^( k* 2)|^(t div 2) *(g|^ (k*(t mod 2))) by GROUP_1:35
.=(1_Gc)|^(t div 2) *(g|^ (k*(t mod 2))) by A4,GROUP_1:35
.=(1_Gc) *(g|^ (k*(t mod 2))) by GROUP_1:31
.=(g|^(k*(t mod 2))) by GROUP_1:def 4;
per cases by NAT_D:12;
suppose
t mod 2 = 0;
then g|^k1 = 1_Gc by A17,GROUP_1:25;
hence contradiction by A11,A10,GROUP_1:42;
end;
suppose
t mod 2 = 1;
hence contradiction by A12,A10,A17;
end;
end;
then
A18: 2*t1<>0;
1_Gc=g|^k1|^2 by A11,A10,GROUP_1:41
.=g|^(((k*t)+t1)*2) by A14,GROUP_1:35
.=g|^(n*t+t1*2) by A1
.=g|^(n*t)*(g|^(t1*2)) by GROUP_1:33
.=g|^(ord g)|^t*(g|^(t1*2)) by A3,GROUP_1:35
.=(1_Gc)|^t*(g|^(t1*2)) by GROUP_1:41
.=1_Gc*(g|^(t1*2)) by GROUP_1:31
.=g|^(2*t1) by GROUP_1:def 4;
hence contradiction by A3,A18,A16,A13,GROUP_1:def 11;
end;
hence thesis;
end;
registration
let G;
cluster center G -> normal;
coherence by GROUP_5:78;
end;
theorem
for Gc being strict finite cyclic Group st ex k st card Gc = 2*k holds
ex H being Subgroup of Gc st card H = 2 & H is cyclic Group
proof
let Gc be strict finite cyclic Group;
set n = card Gc;
assume ex k st n=2*k;
then consider g1 being Element of Gc such that
A1: ord g1 = 2 and
for g2 being Element of Gc st ord g2=2 holds g1=g2 by Th24;
take gr {g1};
thus thesis by A1,Th4,GR_CY_1:7;
end;
theorem Th26:
for G being strict Group holds for g being Homomorphism of G,F
st G is cyclic holds Image g is cyclic
proof
let G be strict Group;
let g be Homomorphism of G,F;
assume G is cyclic;
then consider a being Element of G such that
A1: G=gr{a};
ex f1 being Element of Image g st Image g=gr{f1}
proof
g.a in Image g by GROUP_6:45;
then reconsider f=g.a as Element of Image g by STRUCT_0:def 5;
take f;
for d being Element of Image g holds ex i st d=f|^i
proof
let d be Element of Image g;
d in Image g by STRUCT_0:def 5;
then consider b being Element of G such that
A2: d=g.(b) by GROUP_6:45;
b in gr{a} by A1,STRUCT_0:def 5;
then consider i such that
A3: b=a|^i by GR_CY_1:5;
take i;
d=(g.a)|^i by A2,A3,GROUP_6:37
.=f|^i by GROUP_4:2;
hence thesis;
end;
hence thesis by Th5;
end;
hence thesis;
end;
theorem
for G,F being strict Group st G,F are_isomorphic & G is cyclic holds F
is cyclic
proof
let G,F be strict Group;
assume that
A1: G,F are_isomorphic and
A2: G is cyclic;
consider h being Homomorphism of G,F such that
A3: h is bijective by A1,GROUP_6:def 11;
h is onto by A3,FUNCT_2:def 4;
then Image h = F by GROUP_6:57;
hence thesis by A2,Th26;
end;