:: Solvable Groups
::
:: 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
existence
ex b1 being Group st
( b1 is solvable & b1 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). () )
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;