:: Semidirect Products of Groups
:: by Alexander M. Nelson
::
:: Received May 27, 2025
:: Copyright (c) 2025 Association of Mizar Users

theorem Th121: :: GROUP_24:1

for a, b being Nat st a < b & b <> 0 holds
(2 * a) div b < 2

proof end;

LmAssoc: for G being Group
for g1, g2, g3, g4, g5 being Element of G holds (g1 * ((g2 * g3) * g4)) * g5 = (((g1 * g2) * g3) * g4) * g5

proof end;

theorem thUnitalMagmaIsGroupCond: :: GROUP_24:2

for M being non empty unital multMagma st ( for h being Element of M ex g being Element of M st
( h * g = 1_ M & g * h = 1_ M ) ) holds
M is Group-like

proof end;

theorem Th1: :: GROUP_24:3

for G being Group
for H being Subgroup of G holds multMagma(# the carrier of H, the multF of H #) is strict Subgroup of G

proof end;

theorem Th2: :: GROUP_24:4

for G being Group
for N being normal Subgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

proof end;

theorem :: GROUP_24:5

for G being Group
for H being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of H holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of ((H,N) `*`), the multF of ((H,N) `*`) #)

proof end;

theorem ThCapLemma: :: GROUP_24:6

for G being Group
for H1, H2, K being Subgroup of G
for K1, K2 being Subgroup of K st multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) & multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) holds
H1 /\ H2 = K1 /\ K2

proof end;

theorem ThProdLemma: :: GROUP_24:7

for G being Group
for H1, H2, K being Subgroup of G
for K1, K2 being Subgroup of K st multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of K1, the multF of K1 #) & multMagma(# the carrier of H2, the multF of H2 #) = multMagma(# the carrier of K2, the multF of K2 #) holds
H1 * H2 = K1 * K2

proof end;

theorem Th48: :: GROUP_24:8

for G being Group
for A being Subset of G st A = the carrier of G holds
gr A = multMagma(# the carrier of G, the multF of G #)

proof end;

theorem :: GROUP_24:9

for A being Group holds A, multMagma(# the carrier of A, the multF of A #) are_isomorphic

proof end;

theorem Th52: :: GROUP_24:10

for G being Group
for N being normal Subgroup of G
for g1, g2 being Element of G st g1 * N = g2 * N holds
ex n being Element of G st
( n in N & g1 = g2 * n )

proof end;

Th61: for G being Group
for H1, H2 being Subgroup of G holds H1 * H2 c= the carrier of (H1 "\/" H2)

proof end;

theorem Th62: :: GROUP_24:11

for G being Group
for H1, H2 being Subgroup of G holds
( H1 * H2 c= the carrier of (H1 "\/" H2) & H2 * H1 c= the carrier of (H1 "\/" H2) )

proof end;

theorem Th63: :: GROUP_24:12

for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = the carrier of (H1 "\/" H2) holds
H1 * H2 = H2 * H1

proof end;

theorem :: GROUP_24:13

for G being Group
for H, K being Subgroup of G
for HK being Subgroup of K st multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of HK, the multF of HK #) holds
carr H = carr HK ;

theorem Th40: :: GROUP_24:14

for G being Group
for H, K being Subgroup of G st H is Subgroup of K holds
for N being Subgroup of G st N is normal Subgroup of K holds
N * H = H * N

proof end;

theorem Th41: :: GROUP_24:15

for G being Group
for H being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of H holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of ((H,N) `*`), the multF of ((H,N) `*`) #)

proof end;

theorem Th42: :: GROUP_24:16

for G being Group
for H1, N1, H2, N2 being Subgroup of G st multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) & multMagma(# the carrier of N1, the multF of N1 #) = multMagma(# the carrier of N2, the multF of N2 #) holds
( H1 * N1 = H2 * N2 & H1 /\ N1 = H2 /\ N2 )

proof end;

theorem Th8: :: GROUP_24:17

for G being Group
for H, K being strict Subgroup of G st H <> K & K is Subgroup of H holds
ex g being Element of G st
( g in H & not g in K )

proof end;

registration

let G, A be Group;

cluster product (Carrier <*A,G*>) -> non empty ;

coherence
not product (Carrier <*A,G*>) is empty ;

end;

theorem Th6: :: GROUP_24:18

for G1, G2 being Group
for x being Element of (product <*G1,G2*>) holds
( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} )

proof end;

Lm1: for G1, G2 being Group
for x being Element of product (Carrier <*G1,G2*>) holds
( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} )

proof end;

Lm2: for A, G being Group
for a being Element of A
for g being Element of G holds <*a,g*> in product (Carrier <*A,G*>)

proof end;

theorem Th7: :: GROUP_24:19

for G1, G2 being Group
for H1 being Subgroup of G1
for H2 being Subgroup of G2
for h1 being Element of G1 st h1 in H1 holds
for h2 being Element of G2 st h2 in H2 holds
<*h1,h2*> in product <*H1,H2*>

proof end;

Lm3: for G1, G2 being Group
for phi being Homomorphism of G1,G2
for a being Element of G1 holds phi . a in G2
;

theorem Th15: :: GROUP_24:20

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for g being Element of G holds (phi . (1_ A)) . g = g

proof end;

theorem Th18: :: GROUP_24:21

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a1, a2 being Element of A
for g being Element of G holds (phi . a1) . ((phi . a2) . g) = (phi . (a1 * a2)) . g

proof end;

theorem Th19: :: GROUP_24:22

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds
( (phi . (a ")) . ((phi . a) . g) = g & (phi . a) . ((phi . (a ")) . g) = g )

proof end;

definition

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

func semidirect_product (G,A,phi) -> non empty strict multMagma means :Def1: :: GROUP_24:def 1
( the carrier of it = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of it . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) );

existence
ex b₁ being non empty strict multMagma st
( the carrier of b₁ = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of b₁ . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) )

proof end;

uniqueness
for b₁, b₂ being non empty strict multMagma st the carrier of b₁ = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of b₁ . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) & the carrier of b₂ = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of b₂ . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines semidirect_product GROUP_24:def 1 :
for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for b₄ being non empty strict multMagma holds
( b₄ = semidirect_product (G,A,phi) iff ( the carrier of b₄ = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of b₄ . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) ) );

registration

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

cluster semidirect_product (G,A,phi) -> non empty strict constituted-Functions ;

coherence
semidirect_product (G,A,phi) is constituted-Functions

proof end;

end;

registration

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

cluster -> FinSequence-like for Element of the carrier of (semidirect_product (G,A,phi));

coherence
for b₁ being Element of (semidirect_product (G,A,phi)) holds b₁ is FinSequence-like

proof end;

end;

theorem Th9: :: GROUP_24:23

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds the carrier of (semidirect_product (G,A,phi)) = the carrier of (product <*G,A*>)

proof end;

theorem :: GROUP_24:24

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds <*g,a*> is Element of (semidirect_product (G,A,phi)) by Th9;

theorem Th11: :: GROUP_24:25

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) holds
( x . 1 in G & x . 2 in A & dom x = {1,2} )

proof end;

theorem Th12: :: GROUP_24:26

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) ex g being Element of G ex a being Element of A st x = <*g,a*>

proof end;

theorem Th14: :: GROUP_24:27

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x, y being Element of (semidirect_product (G,A,phi))
for a1, a2 being Element of A
for g1, g2, g3 being Element of G st x = <*g1,a1*> & y = <*g2,a2*> & g3 = (phi . a1) . g2 holds
x * y = <*(g1 * g3),(a1 * a2)*>

proof end;

theorem Th16: :: GROUP_24:28

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x, y being Element of (semidirect_product (G,A,phi))
for a being Element of A
for g being Element of G st x = <*g,(1_ A)*> & y = <*(1_ G),a*> holds
x * y = <*g,a*>

proof end;

Lm4: for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x, e being Element of (semidirect_product (G,A,phi)) st e = <*(1_ G),(1_ A)*> holds
( x * e = x & e * x = x )

proof end;

registration

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

cluster semidirect_product (G,A,phi) -> non empty strict unital ;

correctness
coherence
semidirect_product (G,A,phi) is unital ;

proof end;

end;

theorem Th17: :: GROUP_24:29

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds 1_ (semidirect_product (G,A,phi)) = <*(1_ G),(1_ A)*>

proof end;

theorem Th20: :: GROUP_24:30

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x, y being Element of (semidirect_product (G,A,phi))
for a being Element of A
for g being Element of G st x = <*g,a*> & y = <*((phi . (a ")) . (g ")),(a ")*> holds
( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) )

proof end;

registration

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

cluster semidirect_product (G,A,phi) -> non empty strict Group-like associative ;

coherence
( semidirect_product (G,A,phi) is associative & semidirect_product (G,A,phi) is Group-like )

proof end;

end;

theorem Th22: :: GROUP_24:31

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,a*> holds
x " = <*((phi . (a ")) . (g ")),(a ")*>

proof end;

theorem Th23: :: GROUP_24:32

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for g1, g2 being Element of G
for x, y, z being Element of (semidirect_product (G,A,phi)) st x = <*g1,(1_ A)*> & y = <*g2,(1_ A)*> & z = <*(g1 * g2),(1_ A)*> holds
x * y = z

proof end;

theorem Th24: :: GROUP_24:33

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,(1_ A)*> holds
x " = <*(g "),(1_ A)*>

proof end;

theorem Th25: :: GROUP_24:34

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi))
for g being Element of G st x = <*g,(1_ A)*> holds
for i being Integer holds x |^ i = <*(g |^ i),(1_ A)*>

proof end;

theorem Th26: :: GROUP_24:35

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a1, a2 being Element of A
for x, y, z being Element of (semidirect_product (G,A,phi)) st x = <*(1_ G),a1*> & y = <*(1_ G),a2*> & z = <*(1_ G),(a1 * a2)*> holds
x * y = z

proof end;

theorem Th27: :: GROUP_24:36

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for x being Element of (semidirect_product (G,A,phi)) st x = <*(1_ G),a*> holds
x " = <*(1_ G),(a ")*>

proof end;

theorem Th28: :: GROUP_24:37

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for i being Integer
for x being Element of (semidirect_product (G,A,phi))
for a being Element of A st x = <*(1_ G),a*> holds
x |^ i = <*(1_ G),(a |^ i)*>

proof end;

definition

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

func incl1 (G,A,phi) -> Function of G,(semidirect_product (G,A,phi)) means :Def2: :: GROUP_24:def 2
for g being Element of G holds it . g = <*g,(1_ A)*>;

existence
ex b₁ being Function of G,(semidirect_product (G,A,phi)) st
for g being Element of G holds b₁ . g = <*g,(1_ A)*>

proof end;

uniqueness
for b₁, b₂ being Function of G,(semidirect_product (G,A,phi)) st ( for g being Element of G holds b₁ . g = <*g,(1_ A)*> ) & ( for g being Element of G holds b₂ . g = <*g,(1_ A)*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines incl1 GROUP_24:def 2 :
for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for b₄ being Function of G,(semidirect_product (G,A,phi)) holds
( b₄ = incl1 (G,A,phi) iff for g being Element of G holds b₄ . g = <*g,(1_ A)*> );

:: Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.2)

registration

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

cluster incl1 (G,A,phi) -> one-to-one multiplicative ;

coherence
( incl1 (G,A,phi) is multiplicative & incl1 (G,A,phi) is one-to-one )

proof end;

end;

definition

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

func incl2 (G,A,phi) -> Function of A,(semidirect_product (G,A,phi)) means :Def3: :: GROUP_24:def 3
for a being Element of A holds it . a = <*(1_ G),a*>;

existence
ex b₁ being Function of A,(semidirect_product (G,A,phi)) st
for a being Element of A holds b₁ . a = <*(1_ G),a*>

proof end;

uniqueness
for b₁, b₂ being Function of A,(semidirect_product (G,A,phi)) st ( for a being Element of A holds b₁ . a = <*(1_ G),a*> ) & ( for a being Element of A holds b₂ . a = <*(1_ G),a*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines incl2 GROUP_24:def 3 :
for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for b₄ being Function of A,(semidirect_product (G,A,phi)) holds
( b₄ = incl2 (G,A,phi) iff for a being Element of A holds b₄ . a = <*(1_ G),a*> );

:: Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.2)

registration

let G, A be Group;
let phi be Homomorphism of A,(AutGroup G);

cluster incl2 (G,A,phi) -> one-to-one multiplicative ;

coherence
( incl2 (G,A,phi) is multiplicative & incl2 (G,A,phi) is one-to-one )

proof end;

end;

:: Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.3)

theorem Th30: :: GROUP_24:38

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds Image (incl1 (G,A,phi)) is normal Subgroup of semidirect_product (G,A,phi)

proof end;

registration

let A, G be Group;
let phi be Homomorphism of A,(AutGroup G);

cluster Image (incl1 (G,A,phi)) -> normal ;

correctness
coherence
Image (incl1 (G,A,phi)) is normal ;
by Th30;

end;

theorem :: GROUP_24:39

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) = (1). (semidirect_product (G,A,phi))

proof end;

theorem Th32: :: GROUP_24:40

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) ex g being Element of G ex a being Element of A st ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x

proof end;

theorem Th33: :: GROUP_24:41

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))) = the carrier of (semidirect_product (G,A,phi))

proof end;

theorem :: GROUP_24:42

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds (Image (incl1 (G,A,phi))) "\/" (Image (incl2 (G,A,phi))) = semidirect_product (G,A,phi)

proof end;

:: Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.3)

theorem :: GROUP_24:43

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds G, Image (incl1 (G,A,phi)) are_isomorphic by GROUP_6:68;

:: Note there is a sign error in Aschbacher's book, due to different
:: notational conventions with function composition being written
:: backwards (as is the style in finite group theory).
::
:: Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.4)

theorem Th36: :: GROUP_24:44

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . a) = <*((phi . (a ")) . g),(1_ A)*>

proof end;

theorem :: GROUP_24:45

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . (a ")) = <*((phi . a) . g),(1_ A)*>

proof end;

theorem Th38: :: GROUP_24:46

for G, A being Group holds semidirect_product (G,A,(1: (A,(AutGroup G)))) = product <*G,A*>

proof end;

definition

let G, H, N be Group;

pred H,N are_complements_in G means :: GROUP_24:def 4
ex H1 being strict Subgroup of G ex N1 being strict normal Subgroup of G st
( H1 = multMagma(# the carrier of H, the multF of H #) & N1 = multMagma(# the carrier of N, the multF of N #) & H1 * N1 = the carrier of G & H1 /\ N1 = (1). G );

end;

:: deftheorem defines are_complements_in GROUP_24:def 4 :
for G, H, N being Group holds
( H,N are_complements_in G iff ex H1 being strict Subgroup of G ex N1 being strict normal Subgroup of G st
( H1 = multMagma(# the carrier of H, the multF of H #) & N1 = multMagma(# the carrier of N, the multF of N #) & H1 * N1 = the carrier of G & H1 /\ N1 = (1). G ) );

definition

let G be Group;
let H, N be Subgroup of G;

redefine pred H,N are_complements_in G means :: GROUP_24:def 5
( N is normal & H * N = the carrier of G & H /\ N = (1). G );

compatibility
( H,N are_complements_in G iff ( N is normal & H * N = the carrier of G & H /\ N = (1). G ) )

proof end;

end;

:: deftheorem defines are_complements_in GROUP_24:def 5 :
for G being Group
for H, N being Subgroup of G holds
( H,N are_complements_in G iff ( N is normal & H * N = the carrier of G & H /\ N = (1). G ) );

theorem Th43: :: GROUP_24:47

for G being Group
for H, K being Subgroup of G st H is Subgroup of K holds
for N being Subgroup of G st N is normal Subgroup of K holds
( H,N are_complements_in K iff ( N * H = the carrier of K & H /\ N = (1). K ) )

proof end;

theorem :: GROUP_24:48

for G being Group
for H, K being Subgroup of G st H is Subgroup of K holds
for N being Subgroup of G st N is normal Subgroup of K holds
( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) )

proof end;

theorem Th45: :: GROUP_24:49

for G being Group
for H, K being Subgroup of G st H is Subgroup of K holds
for N being normal Subgroup of G st N is Subgroup of K holds
( H,(K,N) `*` are_complements_in K iff ( N * H = the carrier of K & H /\ N = (1). K ) )

proof end;

theorem Th46: :: GROUP_24:50

for G being Group
for H, K being Subgroup of G st H is Subgroup of K holds
for N being normal Subgroup of G st N is Subgroup of K holds
( H,N are_complements_in K iff H,(K,N) `*` are_complements_in K )

proof end;

theorem :: GROUP_24:51

for G being Group
for K being Subgroup of G
for H being Subgroup of K
for N being normal Subgroup of G st N is Subgroup of K holds
( H,N are_complements_in K iff H,(K,N) `*` are_complements_in K ) by Th46;

theorem Th49: :: GROUP_24:52

for G being Group
for H being Subgroup of G
for N being normal Subgroup of G holds
( H,N are_complements_in G iff ( H "\/" N = multMagma(# the carrier of G, the multF of G #) & H /\ N = (1). G ) )

proof end;

:: Universal Property of Quotient Groups

theorem UniversalPropertyQuotientGroups: :: GROUP_24:53

for G1, G2 being Group
for N being normal Subgroup of G1
for f being Homomorphism of G1,G2 st N is Subgroup of Ker f holds
ex fBar being Homomorphism of (G1 ./. N),G2 st f = fBar * (nat_hom N)

proof end;

theorem :: GROUP_24:54

for G1, G2 being Group
for N1 being normal Subgroup of G1
for N2 being normal Subgroup of G2
for phi being Homomorphism of G1,G2 st phi is bijective & phi .: the carrier of N1 = the carrier of N2 holds
G1 ./. N1,G2 ./. N2 are_isomorphic

proof end;

theorem Th55: :: GROUP_24:55

for G being Group
for H being Subgroup of G
for N being normal Subgroup of G st H,N are_complements_in G holds
ex phi being Homomorphism of H,(G ./. N) st
( ( for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N ) & phi is bijective )

proof end;

theorem Th56: :: GROUP_24:56

for G being Group
for H being Subgroup of G
for N being normal Subgroup of G st H,N are_complements_in G holds
G ./. N,H are_isomorphic

proof end;

theorem :: GROUP_24:57

for G being Group
for H1, H2 being Subgroup of G
for N being normal Subgroup of G st H1,N are_complements_in G & H2,N are_complements_in G holds
H1,H2 are_isomorphic

proof end;

:: Bourbaki~\cite[I \S6.1]{BourbakiAlgI}, Corollary to Proposition 4

theorem Th58: :: GROUP_24:58

for G being Group
for H, K being Subgroup of G
for phi being Function of (product <*H,K*>),G st ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) holds
( phi is one-to-one iff H /\ K = (1). G )

proof end;

theorem Th59: :: GROUP_24:59

for G being Group
for H, K being Subgroup of G ex phi being Function of (product (Carrier <*H,K*>)),G st
( ( for h, k being Element of G st h in H & k in K holds
phi . <*h,k*> = h * k ) & ( phi is one-to-one implies H /\ K = (1). G ) & ( H /\ K = (1). G implies phi is one-to-one ) )

proof end;

theorem Th60: :: GROUP_24:60

for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G
for phi being Homomorphism of H,(AutGroup N) ex psi being Function of (semidirect_product (N,H,phi)),G st
( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) )

proof end;

theorem Th64: :: GROUP_24:61

for G being Group
for H being Subgroup of G
for N being normal Subgroup of G st H,N are_complements_in G holds
( H * N = the carrier of G & N * H = the carrier of G )

proof end;

:: Aschbacher~\cite{aschbacher2000finite}, Theorem 10.2

theorem :: GROUP_24:62

for G being Group
for N being strict normal Subgroup of G
for H being Subgroup of G st H,N are_complements_in G holds
for alpha being Homomorphism of H,(AutGroup N) st ( for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ) holds
ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective )

proof end;

:: Bourbaki, General Topology, Chapter 3, section 2, p.240, Proposition 27
:: Universal Property of Semidirect Products (Bourbaki~\cite[III \S2.10]{bourbaki2013general} Proposition 27)

theorem :: GROUP_24:63

for H, G being Group
for N being strict Group
for f being Homomorphism of N,G
for g being Homomorphism of H,G
for phi being Homomorphism of H,(AutGroup N) st ( for n being Element of N
for h being Element of H holds f . ((phi . h) . n) = ((g . h) * (f . n)) * (g . (h ")) ) holds
ex k being Homomorphism of (semidirect_product (N,H,phi)),G st
( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) )

proof end;

registration

let G be finite strict Group;
let A be finite Group;
let phi be Homomorphism of A,(AutGroup G);

cluster semidirect_product (G,A,phi) -> non empty finite strict ;

correctness
coherence
semidirect_product (G,A,phi) is finite ;

proof end;

end;

::: theorem :: TH67
::: Image (1:(G1,G2)) = (1).G2 by GROUP_6:47;

theorem Th68: :: GROUP_24:64

for G1, G2 being Group st G2 is trivial holds
for phi being Homomorphism of G1,G2 holds phi = 1: (G1,G2)

proof end;

theorem Th69: :: GROUP_24:65

for G being Group holds Aut ((1). G) = {(id ((1). G))}

proof end;

theorem Th70: :: GROUP_24:66

for G being Group st G is strict & G is trivial holds
AutGroup G is trivial

proof end;

theorem :: GROUP_24:67

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) st G is strict & G is trivial holds
phi = 1: (A,(AutGroup G))

proof end;

theorem Th72: :: GROUP_24:68

for G1, G2 being Group st G1 is trivial holds
product <*G1,G2*>,G2 are_isomorphic

proof end;

theorem Th73: :: GROUP_24:69

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) st G is strict & G is trivial holds
semidirect_product (G,A,phi),A are_isomorphic

proof end;

theorem Th74: :: GROUP_24:70

for G, A being finite Group
for phi being Homomorphism of A,(AutGroup G) holds card (semidirect_product (G,A,phi)) = (card G) * (card A)

proof end;

registration

cluster non empty infinite Group-like associative -> non trivial for multMagma ;

coherence
for b₁ being Group st b₁ is infinite holds
not b₁ is trivial ;

cluster non empty trivial Group-like associative -> finite for multMagma ;

coherence
for b₁ being Group st b₁ is trivial holds
b₁ is finite ;

end;

theorem Th75: :: GROUP_24:71

for n being non zero Nat holds the multF of (INT.Group n) = addint n

proof end;

theorem Th76: :: GROUP_24:72

for n being non zero Nat holds the carrier of (INT.Group n) = Segm n

proof end;

registration

cluster INT.Group 1 -> trivial ;

correctness
coherence
INT.Group 1 is trivial ;

proof end;

end;

registration

let n be non zero Nat;

reduce card (INT.Group n) to n;

correctness
reducibility
card (INT.Group n) = n;

proof end;

end;

Lm6: for n being non zero even Nat holds 1 in Segm n

proof end;

theorem Th77: :: GROUP_24:73

for G being Group holds
( G is trivial iff for x being Element of G holds x = 1_ G )

proof end;

theorem Th78: :: GROUP_24:74

for G being Group
for H being Subgroup of G holds
( H is trivial iff for x being Element of G holds
( x in H iff x = 1_ G ) )

proof end;

ThTrivialCriterion: for G being Group holds
( G is trivial iff card G = 1 )
by GROUP_6:11;

theorem ThTrivialCyclicGroupCriterion1: :: GROUP_24:75

for n being non zero Nat holds
( INT.Group n is trivial iff n = 1 )

proof end;

theorem ThTrivialCyclicGroupCriterion: :: GROUP_24:76

for n being non zero Nat holds
( not INT.Group n is trivial iff n > 1 ) by NAT_1:53, ThTrivialCyclicGroupCriterion1;

registration

cluster non empty non trivial infinite strict unital Group-like associative cyclic left-invertible right-invertible invertible left-cancelable right-cancelable cancelable for multMagma ;

existence
ex b₁ being Group st
( not b₁ is trivial & b₁ is cyclic & b₁ is strict & b₁ is infinite )

proof end;

cluster non empty non trivial finite strict unital Group-like associative cyclic left-invertible right-invertible invertible left-cancelable right-cancelable cancelable for multMagma ;

existence
ex b₁ being Group st
( not b₁ is trivial & b₁ is cyclic & b₁ is strict & b₁ is finite )

proof end;

end;

:: Now, the random results concerning INT.Group 2 in particular

theorem Th82: :: GROUP_24:77

for g being Element of (INT.Group 2) st g = 1 holds
g * g = 1_ (INT.Group 2)

proof end;

theorem EltsOfINTGroup2: :: GROUP_24:78

for x being object holds
( x in INT.Group 2 iff ( x = 0 or x = 1 ) )

proof end;

theorem ThMultTableINTGroup2: :: GROUP_24:79

for x, y being Element of (INT.Group 2) holds
( ( x = 0 implies x * y = y ) & ( y = 0 implies x * y = x ) & ( x = 1 & y = 1 implies x * y = 1_ (INT.Group 2) ) )

proof end;

theorem :: GROUP_24:80

for n, k being non zero Nat
for g being Element of (INT.Group n) st g = k holds
g " = (n - k) mod n

proof end;

theorem Th86: :: GROUP_24:81

for n being non zero Nat
for x being Element of (INT.Group n) holds x " = x |^ (n - 1)

proof end;

theorem :: GROUP_24:82

for G being finite Group
for x being Element of G holds
( 0 < ord x & ord x <= card G )

proof end;

theorem ThINTGroupOrd: :: GROUP_24:83

for n being non zero Nat
for g, g1 being Element of (INT.Group n) st g1 = 1 holds
ex k being Nat st
( g = g1 |^ k & g = k mod n )

proof end;

theorem :: GROUP_24:84

for n being non zero Nat
for g, g1 being Element of (INT.Group n) st g1 = 1 holds
ex k being Nat st
( k < n & g = g1 |^ k & g = k mod n )

proof end;

theorem :: GROUP_24:85

for G being Group
for g being Element of G
for i, j being Integer st g |^ i = g |^ j holds
g |^ (- i) = g |^ (- j)

proof end;

theorem LmINTGroupOrd3: :: GROUP_24:86

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for i being Nat holds g1 |^ i = i mod n

proof end;

theorem ThINTGroupOrd3: :: GROUP_24:87

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for i, j being Nat holds
( g1 |^ i = g1 |^ j iff i mod n = j mod n )

proof end;

theorem :: GROUP_24:88

for A being Group st A is commutative holds
inverse_op A is Automorphism of A ;

definition

let G be strict commutative Group;

func inversions G -> Function of (INT.Group 2),(AutGroup G) means :DefInversions: :: GROUP_24:def 6
( it . 0 = id G & it . 1 = inverse_op G );

existence
ex b₁ being Function of (INT.Group 2),(AutGroup G) st
( b₁ . 0 = id G & b₁ . 1 = inverse_op G )

proof end;

uniqueness
for b₁, b₂ being Function of (INT.Group 2),(AutGroup G) st b₁ . 0 = id G & b₁ . 1 = inverse_op G & b₂ . 0 = id G & b₂ . 1 = inverse_op G holds
b₁ = b₂

proof end;

end;

:: deftheorem DefInversions defines inversions GROUP_24:def 6 :
for G being strict commutative Group
for b₂ being Function of (INT.Group 2),(AutGroup G) holds
( b₂ = inversions G iff ( b₂ . 0 = id G & b₂ . 1 = inverse_op G ) );

theorem ThInverseOpGSquaresToIdentity: :: GROUP_24:89

for G being Group holds (inverse_op G) * (inverse_op G) = id G

proof end;

theorem ThCommutationEq: :: GROUP_24:90

for G being strict commutative Group
for a, b being Element of (INT.Group 2) st b = 0 holds
( ((inversions G) . b) * ((inversions G) . a) = (inversions G) . a & ((inversions G) . a) * ((inversions G) . b) = (inversions G) . a )

proof end;

theorem ThCommutationEq2: :: GROUP_24:91

for G being strict commutative Group
for a, b being Element of (INT.Group 2) st a = 1 & b = 1 holds
((inversions G) . b) * ((inversions G) . a) = (inversions G) . (a * b)

proof end;

registration

let G be strict commutative Group;

cluster inversions G -> multiplicative ;

coherence
inversions G is multiplicative

proof end;

end;

definition

let G be strict commutative Group;
:: original: inversions
redefine func inversions G -> Homomorphism of (INT.Group 2),(AutGroup G);
coherence
inversions G is Homomorphism of (INT.Group 2),(AutGroup G) ;

end;

definition

let n be non zero ExtNat;

func Dihedral_group n -> strict Group means :DefDihedral: :: GROUP_24:def 7
( ( n = +infty implies it = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & it = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) );

existence
ex b₁ being strict Group st
( ( n = +infty implies b₁ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₁ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict Group st ( n = +infty implies b₁ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₁ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) & ( n = +infty implies b₂ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₂ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) holds
b₁ = b₂ ;

end;

:: deftheorem DefDihedral defines Dihedral_group GROUP_24:def 7 :
for n being non zero ExtNat
for b₂ being strict Group holds
( b₂ = Dihedral_group n iff ( ( n = +infty implies b₂ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₂ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) ) );

definition

let n be non zero Nat;

redefine func Dihedral_group n equals :: GROUP_24:def 8
semidirect_product ((INT.Group n),(INT.Group 2),(inversions (INT.Group n)));

compatibility
for b₁ being strict Group holds
( b₁ = Dihedral_group n iff b₁ = semidirect_product ((INT.Group n),(INT.Group 2),(inversions (INT.Group n))) ) by DefDihedral;

end;

:: deftheorem defines Dihedral_group GROUP_24:def 8 :
for n being non zero Nat holds Dihedral_group n = semidirect_product ((INT.Group n),(INT.Group 2),(inversions (INT.Group n)));

theorem :: GROUP_24:92

for n being non zero Nat holds card (Dihedral_group n) = 2 * n

proof end;

registration

let n be non zero Nat;

cluster Dihedral_group n -> finite strict ;

coherence
Dihedral_group n is finite ;

end;

definition

let n be non natural ExtNat;

redefine func Dihedral_group n equals :: GROUP_24:def 9
semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group));

compatibility
for b₁ being strict Group holds
( b₁ = Dihedral_group n iff b₁ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) )

proof end;

end;

:: deftheorem defines Dihedral_group GROUP_24:def 9 :
for n being non natural ExtNat holds Dihedral_group n = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group));

theorem :: GROUP_24:93

for g1 being Element of INT.Group
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group +infty) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ INT.Group),a2*> holds
y * x = (x ") * y

proof end;

theorem Th99: :: GROUP_24:94

for n being non zero Nat
for g1 being Element of (INT.Group n)
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
y * x = (x ") * y

proof end;

theorem Th100: :: GROUP_24:95

for n being non zero Nat
for g1 being Element of (INT.Group n)
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
y * x = (x |^ (n - 1)) * y

proof end;

theorem Th101: :: GROUP_24:96

for n being non zero Nat
for g1 being Element of (INT.Group n)
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
x |^ n = 1_ (Dihedral_group n)

proof end;

theorem Th102: :: GROUP_24:97

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for k being Nat st k <> 0 & k < n holds
x |^ k <> 1_ (Dihedral_group n)

proof end;

theorem Th103: :: GROUP_24:98

for n being non zero Nat
for g1 being Element of (INT.Group n)
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
x " = x |^ (n - 1)

proof end;

theorem :: GROUP_24:99

for n being non zero Nat
for g1 being Element of (INT.Group n)
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for j being Nat holds (x |^ j) " = x |^ (n - j)

proof end;

theorem Th105: :: GROUP_24:100

for n being non zero Nat
for g1 being Element of (INT.Group n)
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
y * x = (x |^ (- 1)) * y

proof end;

theorem Th106: :: GROUP_24:101

for n being non zero Nat
for g1 being Element of (INT.Group n)
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for i being Nat holds y * (x |^ i) = (x |^ (n - i)) * y

proof end;

theorem Th107: :: GROUP_24:102

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for z being Element of (Dihedral_group n) ex k being Nat st
( z = (x |^ k) * y or z = x |^ k )

proof end;

theorem Th108: :: GROUP_24:103

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for z being Element of (Dihedral_group n) ex k being Nat st
( k < n & ( z = (x |^ k) * y or z = x |^ k ) )

proof end;

theorem Th109: :: GROUP_24:104

for n being non zero Nat
for g1 being Element of (INT.Group n)
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * y

proof end;

theorem :: GROUP_24:105

for n being non zero Nat
for a2 being Element of (INT.Group 2)
for y being Element of (Dihedral_group n) st y = <*(1_ (INT.Group n)),a2*> holds
y * y = 1_ (Dihedral_group n)

proof end;

theorem ThD1Commutative: :: GROUP_24:106

( Dihedral_group 1, INT.Group 2 are_isomorphic & Dihedral_group 1 is commutative )

proof end;

theorem :: GROUP_24:107

Dihedral_group 2 is commutative

proof end;

theorem :: GROUP_24:108

for n being non zero Nat st n > 2 holds
not Dihedral_group n is commutative

proof end;

theorem Th114: :: GROUP_24:109

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y, z being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
( z in center (Dihedral_group n) iff ( y * z = z * y & ( for i being Nat holds (x |^ i) * z = z * (x |^ i) ) ) )

proof end;

theorem :: GROUP_24:110

for n being non zero Nat
for z being Element of (Dihedral_group n) holds
( z in center (Dihedral_group n) iff for g1 being Element of (INT.Group n) st g1 = 1 holds
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
( y * z = z * y & ( for i being Nat holds (x |^ i) * z = z * (x |^ i) ) ) )

proof end;

theorem :: GROUP_24:111

center (Dihedral_group 1) = Dihedral_group 1 by ThD1Commutative, GROUP_5:82;

theorem Th117: :: GROUP_24:112

for n being non zero odd Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for i being Nat holds
( not i < n or i = 0 or x |^ i <> x |^ (n - i) )

proof end;

theorem :: GROUP_24:113

for n being odd Nat st n > 1 holds
center (Dihedral_group n) is trivial

proof end;

theorem :: GROUP_24:114

for n being non zero even Nat
for k being Nat st n = 2 * k holds
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
(x |^ k) |^ 2 = 1_ (Dihedral_group n)

proof end;

theorem Th120: :: GROUP_24:115

for n being non zero even Nat
for k being Nat st n = 2 * k holds
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
x |^ k in center (Dihedral_group n)

proof end;

theorem Th122: :: GROUP_24:116

for n being non zero even Nat
for k being Nat st n = 2 * k & n > 2 holds
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) )

proof end;

theorem :: GROUP_24:117

for n being non zero even Nat st n > 2 holds
INT.Group 2, center (Dihedral_group n) are_isomorphic

proof end;