:: Isomorphisms of Direct Products of Cyclic Groups of Prime-power Order
:: by Hiroshi Yamazaki , Hiroyuki Okazaki , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received October 7, 2013
:: Copyright (c) 2013-2016 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 GROUP_18, FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI,
BINOP_1, GROUP_1, XXREAL_0, GROUP_2, GROUP_3, LOPBAN_1, CARD_1, NUMBERS,
FUNCT_4, GROUP_6, GROUP_7, POWER, FUNCOP_1, ALGSTR_0, PARTFUN1, FUNCT_2,
SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1,
ARYTM_3, FINSET_1, INT_2, PBOOLE, NEWTON, INT_1, GROUP_4, CQC_SIM1,
REAL_1, XCMPLX_0, SEQ_4;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE,
CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, INT_2,
FINSEQ_1, SEQ_4, POWER, NEWTON, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2,
GROUP_3, GROUP_4, GROUP_5, GROUP_6, PRALG_1, GROUP_7, GROUP_17;
constructors REALSET1, FUNCT_4, GROUP_6, MONOID_0, PRALG_1, GROUP_4, GROUP_5,
GROUP_7, RELSET_1, WELLORD2, NAT_D, NAT_3, SEQ_4, GROUP_17, POWER;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
FUNCT_2, FUNCOP_1, GROUP_7, GROUP_3, XXREAL_0, RELSET_1, FINSEQ_1, INT_1,
GR_CY_1, FINSET_1, NAT_3, FUNCT_1, XCMPLX_0, MEMBERED, NEWTON, VALUED_0,
XXREAL_2, FINSEQ_2, PBOOLE, GROUP_6, POWER;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Basic Properties of Cyclic Groups of prime-power order
definition let G be finite Group;
func Ordset G -> Subset of NAT equals
:: GROUP_18:def 1
the set of all ord a where a is Element of G;
end;
registration let G be finite Group;
cluster Ordset G -> finite non empty;
end;
theorem :: GROUP_18:1
for G be finite Group holds
ex g be Element of G st ord g = upper_bound Ordset G;
theorem :: GROUP_18:2
for G being strict Group, N be strict normal Subgroup of G
st G is commutative
holds G./.N is commutative;
theorem :: GROUP_18:3 ::: improve GR_CY_2:6
for G being finite Group, a, b be Element of G
holds b in gr {a} iff ex p be Element of NAT st b = a |^p;
theorem :: GROUP_18:4
for G being finite Group, a be Element of G,
n, p, s being Element of NAT
st card gr{a} = n & n = p * s
holds ord(a |^ p) = s;
theorem :: GROUP_18:5
for k being Element of NAT, G being finite Group, a being Element of G
holds gr{a} = gr{(a |^ k)} iff k gcd (ord a) = 1;
theorem :: GROUP_18:6
for k being Element of NAT, G being finite Group,
a being Element of G st k gcd (ord a) = 1
holds ord a = ord(a |^ k);
theorem :: GROUP_18:7
for k being Element of NAT, G being finite Group, a being Element of G
holds (ord a) divides k * ord(a |^ k);
theorem :: GROUP_18:8
for G being Group, a, b being Element of G st b in gr{a}
holds gr{b} is strict Subgroup of gr{a};
definition
let G be strict commutative Group, x be Element of Subgroups G;
func modetrans(x) -> normal strict Subgroup of G equals
:: GROUP_18:def 2
x;
end;
theorem :: GROUP_18:9
for G, H be Group, K be Subgroup of H, f be Homomorphism of G, H holds
ex J be strict Subgroup of G
st the carrier of J = f"(the carrier of K);
theorem :: GROUP_18:10
for p being Nat, G being finite Group, x, d be Element of G
st ord d = p & p is prime & x in gr{d}
holds x = 1_G or gr{x} = gr{d};
theorem :: GROUP_18:11
for G being Group, H, K be normal Subgroup of G
st (the carrier of H) /\ (the carrier of K) = {1_G}
holds (nat_hom H) | (the carrier of K) is one-to-one;
theorem :: GROUP_18:12
for G, F being finite commutative Group, a be Element of G,
f be Homomorphism of G, F
holds the carrier of gr{f.a} = f.: (the carrier of gr{a});
theorem :: GROUP_18:13
for G, F being finite commutative Group, a be Element of G,
f be Homomorphism of G, F
holds ord(f.a) <= ord a;
theorem :: GROUP_18:14
for G, F being finite commutative Group, a be Element of G,
f be Homomorphism of G, F st f is one-to-one
holds ord(f.a) = ord a;
theorem :: GROUP_18:15
for G, F being Group, H be Subgroup of G, f be Homomorphism of G, F
holds f| (the carrier of H) is Homomorphism of H, F;
theorem :: GROUP_18:16
for G, F being finite commutative Group, a be Element of G,
f be Homomorphism of G, F
st f| (the carrier of gr{a}) is one-to-one
holds ord(f.a) = ord a;
theorem :: GROUP_18:17
for G being finite commutative Group, p being Prime, m be Nat,
a be Element of G st card(G) = p|^m & a <> 1_G
holds ex n be Nat st ord a = p|^(n+1);
theorem :: GROUP_18:18
for p being Prime, j, m, k be Nat st m = p|^k & not p divides j
holds j gcd m = 1;
begin :: Isomorphism of cyclic groups of prime-power order
theorem :: GROUP_18:19
for G being strict finite commutative Group, p being Prime, m be Nat
st card(G) = p|^m
ex K be normal strict Subgroup of G, n, k be Nat, g be Element of G st
ord g = upper_bound Ordset G & K is finite commutative
& (the carrier of K) /\ (the carrier of gr{g}) = {1_G}
& (for x be Element of G
holds ex b1, a1 be Element of G st b1 in K & a1 in gr{g} & x = b1*a1)
& ord g = p|^n
& k = m - n & n <= m
& card K = p|^k
& ex F being Homomorphism of product <*K,gr{g}*>, G st F is bijective
& for a,b be Element of G st a in K & b in gr{g}
holds F.(<*a,b*>) = a*b;
theorem :: GROUP_18:20
for G being strict finite commutative Group, p being Prime, m be Nat
st card(G) = p|^m holds
ex k be non zero Nat, a be k-element FinSequence of G,
Inda be k-element FinSequence of NAT,
F be associative Group-like commutative multMagma-Family of Seg k,
HFG be Homomorphism of product F, G
st (for i be Nat st i in Seg k
holds ex ai be Element of G
st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i))
& (for i be Nat st 1 <= i & i <= k -1 holds Inda.i <= Inda.(i+1))
& (for p,q be Element of Seg k st p <> q
holds (the carrier of (F.p)) /\ (the carrier of (F.q)) ={1_G})
& HFG is bijective
& for x be (the carrier of G)-valued total (Seg k)-defined Function
st for p be Element of Seg k holds x.p in F.p
holds x in product F & HFG.x = Product x;
theorem :: GROUP_18:21
for G being strict finite commutative Group, p being Prime, m be Nat
st card(G) = p|^m holds
ex k be non zero Nat, a be k-element FinSequence of G,
Inda be k-element FinSequence of NAT,
F be associative Group-like commutative multMagma-Family of Seg k
st (for i be Nat st i in Seg k holds ex ai be Element of G
st ai = a.i & F.i = gr{ai} & ord(ai) = p|^(Inda.i))
& (for i be Nat st 1 <= i & i <= k -1 holds Inda.i <= Inda.(i+1))
& (for p,q be Element of Seg k st p <> q
holds (the carrier of (F.p)) /\ (the carrier of (F.q)) ={1_G})
& (for y be Element of G holds
ex x be (the carrier of G)-valued total (Seg k) -defined Function
st (for p be Element of Seg k holds x.p in F.p) & y = Product x)
& for x1, x2 be (the carrier of G)-valued total (Seg k) -defined Function
st (for p be Element of Seg k holds x1.p in F.p)
& (for p be Element of Seg k holds x2.p in F.p)
& Product x1 = Product x2 holds x1 = x2;