:: Solvable Groups
:: by Katarzyna Zawadzka
::
:: Received October 23, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users

definition

let IT be Group;

attr IT is solvable means :Def1: :: GRSOLV_1:def 1
ex F being FinSequence of Subgroups IT st
( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) );

end;

:: deftheorem Def1 defines solvable GRSOLV_1:def 1 :
for IT being Group holds
( IT is solvable iff ex F being FinSequence of Subgroups IT st
( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) ) ) );

registration

cluster non empty strict Group-like associative solvable for multMagma ;

existence
ex b₁ being Group st
( b₁ is solvable & b₁ is strict )

proof end;

end;

theorem Th1: :: GRSOLV_1:1

for G being Group
for H, F1, F2 being strict Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H

proof end;

theorem :: GRSOLV_1:2

for G being Group
for F2 being Subgroup of G
for F1 being normal Subgroup of F2
for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1

proof end;

theorem :: GRSOLV_1:3

for G being Group
for H, F2 being Subgroup of G
for F1 being normal Subgroup of F2
for G2 being Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic

proof end;

theorem Th4: :: GRSOLV_1:4

for G being Group
for H, F2 being Subgroup of G
for F1 being normal Subgroup of F2
for G2 being Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic

proof end;

theorem :: GRSOLV_1:5

for G being strict solvable Group
for H being strict Subgroup of G holds H is solvable

proof end;

theorem :: GRSOLV_1:6

for G being Group st ex F being FinSequence of Subgroups G st
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is cyclic Group ) ) ) ) holds
G is solvable

proof end;

theorem :: GRSOLV_1:7

for G being strict commutative Group holds G is solvable

proof end;

definition

let G, H be Group;
let g be Homomorphism of G,H;
let A be Subgroup of G;

func g | A -> Homomorphism of A,H equals :: GRSOLV_1:def 2
g | the carrier of A;

coherence
g | the carrier of A is Homomorphism of A,H

proof end;

end;

:: deftheorem defines | GRSOLV_1:def 2 :
for G, H being Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g | A = g | the carrier of A;

definition

let G, H be Group;
let g be Homomorphism of G,H;
let A be Subgroup of G;

func g .: A -> strict Subgroup of H equals :: GRSOLV_1:def 3
Image (g | A);

coherence
Image (g | A) is strict Subgroup of H ;

end;

:: deftheorem defines .: GRSOLV_1:def 3 :
for G, H being Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g .: A = Image (g | A);

theorem Th8: :: GRSOLV_1:8

for G, H being Group
for g being Homomorphism of G,H
for A being Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A

proof end;

theorem Th9: :: GRSOLV_1:9

for G, H being Group
for h being Homomorphism of G,H
for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h

proof end;

theorem :: GRSOLV_1:10

for G, H being Group
for h being Homomorphism of G,H
for A being strict Subgroup of G holds h .: A is strict Subgroup of Image h by Th9;

theorem Th11: :: GRSOLV_1:11

for G, H being Group
for h being Homomorphism of G,H holds
( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )

proof end;

theorem Th12: :: GRSOLV_1:12

for G, H being Group
for h being Homomorphism of G,H
for A, B being Subgroup of G st A is Subgroup of B holds
h .: A is Subgroup of h .: B

proof end;

theorem Th13: :: GRSOLV_1:13

for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G
for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )

proof end;

theorem Th14: :: GRSOLV_1:14

for G, H being strict Group
for h being Homomorphism of G,H
for A, B being Subset of G holds (h .: A) * (h .: B) = h .: (A * B)

proof end;

theorem Th15: :: GRSOLV_1:15

for G, H being strict Group
for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B

proof end;

theorem :: GRSOLV_1:16

for G, H being strict Group
for h being Homomorphism of G,H st G is solvable Group holds
Image h is solvable

proof end;