:: Solvable Groups
:: by Katarzyna Zawadzka
::
:: Received October 23, 1994
:: Copyright (c) 1994-2021 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 NUMBERS, SUBSET_1, GROUP_1, FINSEQ_1, GROUP_3, XXREAL_0, CARD_1,
FUNCT_1, RLSUB_1, GROUP_2, RELAT_1, ARYTM_3, STRUCT_0, PRE_TOPC, GROUP_6,
BINOP_1, TARSKI, XBOOLE_0, QC_LANG1, WELLORD1, NAT_1, FUNCT_2, ALGSTR_0,
GRAPH_1, GRSOLV_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
STRUCT_0, ALGSTR_0, BINOP_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
GR_CY_1, FINSEQ_1, GROUP_1, GROUP_2, GROUP_3, GROUP_6, XXREAL_0;
constructors BINOP_1, FINSUB_1, REALSET1, GROUP_6, GR_CY_1, RELSET_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0,
GROUP_2, GROUP_3, GROUP_6, GR_CY_1, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve i for Element of NAT;
definition
let IT be Group;
attr IT is solvable means
:: 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 st i in dom F & i+1 in dom F
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;
registration
cluster solvable strict for Group;
end;
theorem :: GRSOLV_1:1
for G being Group, H,F1,F2 being strict Subgroup of G st
F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H;
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;
theorem :: GRSOLV_1:3
for G being Group for H,F2 being Subgroup of G
for F1 being normal Subgroup of F2 holds
for G2 being Subgroup of G st G2 = H /\ F2
for G1 being normal Subgroup of G2 st G1 = H /\ F1
ex G3 being Subgroup of F2./.F1 st G2./.G1, G3 are_isomorphic;
theorem :: GRSOLV_1:4
for G being Group for H,F2 being Subgroup of G
for F1 being normal Subgroup of F2 holds
for G2 being Subgroup of G st G2 = F2/\H
for G1 being normal Subgroup of G2 st G1 = F1/\H
ex G3 being Subgroup of F2./.F1 st G2./.G1, G3 are_isomorphic;
theorem :: GRSOLV_1:5
for G being strict solvable Group, H being strict Subgroup of G
holds H is solvable;
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 st i in dom F & i+1 in dom F
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;
theorem :: GRSOLV_1:7
for G being strict commutative Group holds G is solvable;
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);
end;
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);
end;
theorem :: GRSOLV_1:8
for G,H being Group, g being Homomorphism of G,H
for A being Subgroup of G holds
the carrier of (g.: A) = g.:(the carrier of A);
theorem :: GRSOLV_1:9
for G,H being Group, h being Homomorphism of G,H holds
for A being strict Subgroup of G holds
Image(h|A) is strict Subgroup of Image h;
theorem :: GRSOLV_1:10
for G,H being Group, h being Homomorphism of G,H holds for A
being strict Subgroup of G holds h.:A is strict Subgroup of Image h;
theorem :: GRSOLV_1:11
for G,H being Group, h being Homomorphism of G,H holds
h.:((1).G)=(1).H & h.:((Omega).G)=(Omega).(Image h);
theorem :: GRSOLV_1:12
for G,H being Group, h being Homomorphism of G,H
for A,B being Subgroup of G holds
A is Subgroup of B implies h.:A is Subgroup of h.:B;
theorem :: GRSOLV_1:13
for G,H being strict Group, 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);
theorem :: GRSOLV_1:14
for G,H being strict Group, h being Homomorphism of G,H for A,B
being Subset of G holds h.:A* h.:B=h.:(A*B);
theorem :: GRSOLV_1:15
for G,H being strict Group, h being Homomorphism of G,H for A,B
being strict Subgroup of G holds A is strict normal Subgroup of B implies h.:A
is strict normal Subgroup of h.:B;
theorem :: GRSOLV_1:16
for G,H being strict Group, h being Homomorphism of G,H holds G is
solvable Group implies Image h is solvable;