:: 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-2021 Association of Mizar Users

definition

let G be finite Group;

func Ordset G -> Subset of NAT equals :: GROUP_18:def 1
{ (ord a) where a is Element of G : verum } ;

coherence
{ (ord a) where a is Element of G : verum } is Subset of NAT

proof end;

end;

:: deftheorem defines Ordset GROUP_18:def 1 :
for G being finite Group holds Ordset G = { (ord a) where a is Element of G : verum } ;

registration

let G be finite Group;

cluster Ordset G -> non empty finite ;

coherence
( Ordset G is finite & not Ordset G is empty )

proof end;

end;

theorem LM202: :: GROUP_18:1

for G being finite Group ex g being Element of G st ord g = upper_bound (Ordset G)

proof end;

theorem GROUP630: :: GROUP_18:2

for G being strict Group
for N being strict normal Subgroup of G st G is commutative holds
G ./. N is commutative

proof end;

theorem GRCY26: :: GROUP_18:3

for G being finite Group
for a, b being Element of G holds
( b in gr {a} iff ex p being Element of NAT st b = a |^ p )

proof end;

theorem GRCY28: :: GROUP_18:4

for G being finite Group
for a being Element of G
for n, p, s being Element of NAT st card (gr {a}) = n & n = p * s holds
ord (a |^ p) = s

proof end;

theorem GRCY212: :: GROUP_18:5

for k being Element of NAT
for G being finite Group
for a being Element of G holds
( gr {a} = gr {(a |^ k)} iff k gcd (ord a) = 1 )

proof end;

theorem GRCY212A: :: GROUP_18:6

for k being Element of NAT
for G being finite Group
for a being Element of G st k gcd (ord a) = 1 holds
ord a = ord (a |^ k)

proof end;

theorem GRCY211: :: GROUP_18:7

for k being Element of NAT
for G being finite Group
for a being Element of G holds ord a divides k * (ord (a |^ k))

proof end;

theorem GRCY212: :: GROUP_18:8

for G being Group
for a, b being Element of G st b in gr {a} holds
gr {b} is strict Subgroup of gr {a}

proof end;

definition

let G be strict commutative Group;
let x be Element of Subgroups G;

func modetrans x -> strict normal Subgroup of G equals :: GROUP_18:def 2
x;

correctness
coherence
x is strict normal Subgroup of G;

proof end;

end;

:: deftheorem defines modetrans GROUP_18:def 2 :
for G being strict commutative Group
for x being Element of Subgroups G holds modetrans x = x;

theorem GROUP252INV: :: GROUP_18:9

for G, H being Group
for K being Subgroup of H
for f being Homomorphism of G,H ex J being strict Subgroup of G st the carrier of J = f " the carrier of K

proof end;

theorem GRCY112: :: GROUP_18:10

for p being Nat
for G being finite Group
for x, d being Element of G st ord d = p & p is prime & x in gr {d} & not x = 1_ G holds
gr {x} = gr {d}

proof end;

theorem LM204D: :: GROUP_18:11

for G being Group
for H, K being 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

proof end;

theorem LM204L: :: GROUP_18:12

for G, F being finite commutative Group
for a being Element of G
for f being Homomorphism of G,F holds the carrier of (gr {(f . a)}) = f .: the carrier of (gr {a})

proof end;

theorem LM204E: :: GROUP_18:13

for G, F being finite commutative Group
for a being Element of G
for f being Homomorphism of G,F holds ord (f . a) <= ord a

proof end;

theorem LM204F: :: GROUP_18:14

for G, F being finite commutative Group
for a being Element of G
for f being Homomorphism of G,F st f is one-to-one holds
ord (f . a) = ord a

proof end;

theorem LM204G: :: GROUP_18:15

for G, F being Group
for H being Subgroup of G
for f being Homomorphism of G,F holds f | the carrier of H is Homomorphism of H,F

proof end;

theorem LM204H: :: GROUP_18:16

for G, F being finite commutative Group
for a being Element of G
for f being Homomorphism of G,F st f | the carrier of (gr {a}) is one-to-one holds
ord (f . a) = ord a

proof end;

theorem LM204I: :: GROUP_18:17

for G being finite commutative Group
for p being Prime
for m being Nat
for a being Element of G st card G = p |^ m & a <> 1_ G holds
ex n being Nat st ord a = p |^ (n + 1)

proof end;

LM204K1: for p being Prime
for m, k being Nat st m divides p |^ k & m <> 1 holds
ex j being Nat st m = p |^ (j + 1)

proof end;

theorem LM204K: :: GROUP_18:18

for p being Prime
for j, m, k being Nat st m = p |^ k & not p divides j holds
j gcd m = 1

proof end;

LM204A: for G being finite strict commutative Group
for p being Prime
for m being Nat
for g being Element of G st card G = p |^ m & ord g = upper_bound (Ordset G) holds
ex K being strict normal Subgroup of G st
( the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being Element of G st
( b1 in K & a1 in gr {g} & x = b1 * a1 ) ) )

proof end;

theorem LM204: :: GROUP_18:19

for G being finite strict commutative Group
for p being Prime
for m being Nat st card G = p |^ m holds
ex K being strict normal Subgroup of G ex n, k being Nat ex g being Element of G st
( ord g = upper_bound (Ordset G) & K is finite & K is commutative & the carrier of K /\ the carrier of (gr {g}) = {(1_ G)} & ( for x being Element of G ex b1, a1 being 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 being Element of G st a in K & b in gr {g} holds
F . <*a,b*> = a * b ) ) )

proof end;

theorem LM205A: :: GROUP_18:20

for G being finite strict commutative Group
for p being Prime
for m being Nat st card G = p |^ m holds
ex k being non zero Nat ex a being b₄ -element FinSequence of G ex Inda being b₄ -element FinSequence of NAT ex F being Group-like associative commutative multMagma-Family of Seg k ex HFG being Homomorphism of (product F),G st
( ( for i being Nat st i in Seg k holds
ex ai being Element of G st
( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) ) & ( for i being Nat st 1 <= i & i <= k - 1 holds
Inda . i <= Inda . (i + 1) ) & ( for p, q being 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 being Seg b₄ -defined the carrier of b₁ -valued total Function st ( for p being Element of Seg k holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )

proof end;

XLM18Th401: for I being non empty finite set
for F being Group-like associative multMagma-Family of I
for x being set st x in the carrier of (product F) holds
x is b₁ -defined total Function

proof end;

XLM18Th402: for I being non empty finite set
for F being Group-like associative multMagma-Family of I
for f being Function st f in the carrier of (product F) holds
for x being set st x in I holds
ex R being non empty multMagma st
( R = F . x & f . x in the carrier of R )

proof end;

theorem :: GROUP_18:21

for G being finite strict commutative Group
for p being Prime
for m being Nat st card G = p |^ m holds
ex k being non zero Nat ex a being b₄ -element FinSequence of G ex Inda being b₄ -element FinSequence of NAT ex F being Group-like associative commutative multMagma-Family of Seg k st
( ( for i being Nat st i in Seg k holds
ex ai being Element of G st
( ai = a . i & F . i = gr {ai} & ord ai = p |^ (Inda . i) ) ) & ( for i being Nat st 1 <= i & i <= k - 1 holds
Inda . i <= Inda . (i + 1) ) & ( for p, q being Element of Seg k st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & ( for y being Element of G ex x being Seg b₄ -defined the carrier of b₁ -valued total Function st
( ( for p being Element of Seg k holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being Seg b₄ -defined the carrier of b₁ -valued total Function st ( for p being Element of Seg k holds x1 . p in F . p ) & ( for p being Element of Seg k holds x2 . p in F . p ) & Product x1 = Product x2 holds
x1 = x2 ) )

proof end;