:: The {J}ordan-H\"older Theorem
:: by Marco Riccardi
::
:: Received April 20, 2007
:: Copyright (c) 2007-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, FUNCT_1, FUNCT_2, SUBSET_1, RELAT_1, TARSKI, ZFMISC_1,
SETFAM_1, FINSEQ_1, CARD_3, CARD_1, NAT_1, ARYTM_3, XXREAL_0, XBOOLE_0,
ORDINAL4, GROUP_1, STRUCT_0, LATTICES, GROUP_6, ALGSTR_0, BINOP_1,
PARTFUN1, GROUP_2, REALSET1, RLSUB_1, PRE_TOPC, GLIB_000, MATRIX_1,
QC_LANG1, MSSUBFAM, WELLORD1, EQREL_1, ARYTM_1, NEWTON, INT_1, GROUP_4,
NATTRA_1, FINSEQ_2, ISOCAT_1, FINSEQ_3, FINSET_1, ORDINAL2, MEMBERED,
FINSEQ_5, RFINSEQ, GROUP_9, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, XREAL_0, STRUCT_0, ALGSTR_0, PARTFUN1, FINSEQ_1,
ZFMISC_1, CARD_1, XXREAL_2, FINSET_1, INT_1, NAT_1, FINSEQ_2, FINSEQ_3,
GROUP_1, GROUP_2, GROUP_3, XXREAL_0, SETFAM_1, GROUP_4, FINSEQ_5,
NUMBERS, MEMBERED, MATRIX_1, RFINSEQ, BINOP_1, REALSET1, GROUP_6, NAT_D,
RFUNCT_2;
constructors BINOP_1, REAL_1, NAT_D, RFINSEQ, BINARITH, FINSEQ_5, REALSET2,
GROUP_4, GROUP_6, MATRIX_1, XXREAL_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1,
PRE_CIRC, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, GROUP_6, MATRIX_1,
VALUED_0, XXREAL_2, CARD_1, RELSET_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Actions and Groups with Operators
:: ALG I.3.2 Definition 2
definition
let O,E be set;
let A be Action of O,E;
let IT be set;
pred IT is_stable_under_the_action_of A means
:: GROUP_9:def 1
for o being Element of
O, f being Function of E, E st o in O & f = A.o holds (f .: IT) c= IT;
end;
definition
let O,E be set;
let A be Action of O,E;
let X be Subset of E;
func the_stable_subset_generated_by(X,A) -> Subset of E means
:: GROUP_9:def 2
X c= it & it is_stable_under_the_action_of A & for Y being Subset of E st Y
is_stable_under_the_action_of A & X c= Y holds it c= Y;
end;
definition
let O,E be set;
let A be Action of O,E;
let F be FinSequence of O;
func Product(F,A) -> Function of E,E means
:: GROUP_9:def 3
it = id E if len F = 0
otherwise ex PF being FinSequence of Funcs(E,E) st it = PF.(len F) & len PF =
len F & PF.1 = A.(F.1) & for n being Nat st n<>0 & n set, multF -> BinOp of the
carrier, action -> Action of O, the carrier #);
end;
registration
let O be set;
cluster non empty for HGrWOpStr over O;
end;
definition
let O be set;
let IT be non empty HGrWOpStr over O;
attr IT is distributive means
:: GROUP_9:def 5
for G being Group, a being Action of O,
the carrier of G st a = the action of IT & the multMagma of G = the multMagma
of IT holds a is distributive;
end;
registration
let O be set;
cluster strict distributive Group-like associative for
non empty HGrWOpStr over
O;
end;
:: ALG I.4.2 Definition 2
definition
let O be set;
mode GroupWithOperators of O is distributive Group-like associative non
empty HGrWOpStr over O;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let o be Element of O;
func G^o -> Homomorphism of G, G equals
:: GROUP_9:def 6
(the action of G).o if o in O
otherwise id the carrier of G;
end;
definition
let O be set;
let G be GroupWithOperators of O;
mode StableSubgroup of G -> distributive Group-like associative non empty
HGrWOpStr over O means
:: GROUP_9:def 7
it is Subgroup of G & for o being Element of O
holds it^o = (G^o)|the carrier of it;
end;
registration
let O be set;
let G be GroupWithOperators of O;
cluster strict for StableSubgroup of G;
end;
definition
let O be set;
let G be GroupWithOperators of O;
func (1).G -> strict StableSubgroup of G means
:: GROUP_9:def 8
the carrier of it = { 1_G};
end;
definition
let O be set;
let G be GroupWithOperators of O;
func (Omega).G -> strict StableSubgroup of G equals
:: GROUP_9:def 9
the HGrWOpStr of G;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let IT be StableSubgroup of G;
attr IT is normal means
:: GROUP_9:def 10
for H being strict Subgroup of G st H = the
multMagma of IT holds H is normal;
end;
registration
let O be set;
let G be GroupWithOperators of O;
cluster strict normal for StableSubgroup of G;
end;
registration
let O be set;
let G be GroupWithOperators of O;
let H be StableSubgroup of G;
cluster normal for StableSubgroup of H;
end;
registration
let O be set;
let G be GroupWithOperators of O;
cluster (1).G -> normal;
cluster (Omega).G -> normal;
end;
definition
let O be set;
let G be GroupWithOperators of O;
func the_stable_subgroups_of G -> set means
:: GROUP_9:def 11
for x being object holds x in it iff x is strict StableSubgroup of G;
end;
registration
let O be set;
let G be GroupWithOperators of O;
cluster the_stable_subgroups_of G -> non empty;
end;
definition
let IT be Group;
attr IT is simple means
:: GROUP_9:def 12
IT is not trivial & not ex H being strict
normal Subgroup of IT st H <> (Omega).IT & H <> (1).IT;
end;
registration
cluster strict simple for Group;
end;
:: ALG I.4.4 Definition 7
definition
let O be set;
let IT be GroupWithOperators of O;
attr IT is simple means
:: GROUP_9:def 13
IT is not trivial & not ex H being strict
normal StableSubgroup of IT st H <> (Omega).IT & H <> (1).IT;
end;
registration
let O be set;
cluster strict simple for GroupWithOperators of O;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func Cosets N -> set means
:: GROUP_9:def 14
for H being strict normal Subgroup of G
st H = the multMagma of N holds it = Cosets H;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func CosOp N -> BinOp of Cosets N means
:: GROUP_9:def 15
for H being strict normal
Subgroup of G st H = the multMagma of N holds it = CosOp H;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func CosAc N -> Action of O, Cosets N means
:: GROUP_9:def 16
for o being Element of O
holds it.o = {[A,B] where A,B is Element of Cosets N: ex g,h being Element of G
st g in A & h in B & h = (G^o).g} if O is not empty otherwise it=[:{},{id
Cosets N}:];
end;
definition
let O be set;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func G./.N -> HGrWOpStr over O equals
:: GROUP_9:def 17
HGrWOpStr (# Cosets N, CosOp N, CosAc
N #);
end;
registration
let O be set;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
cluster G./.N -> non empty;
cluster G./.N -> distributive Group-like associative;
end;
:: ALG I.4.2 Definition 3
definition
let O be set;
let G,H be GroupWithOperators of O;
let f be Function of G, H;
attr f is homomorphic means
:: GROUP_9:def 18
for o being Element of O, g being
Element of G holds f.((G^o).g) = (H^o).(f.g);
end;
registration
let O be set;
let G,H be GroupWithOperators of O;
cluster multiplicative homomorphic for Function of G, H;
end;
definition
let O be set;
let G,H be GroupWithOperators of O;
mode Homomorphism of G, H is multiplicative homomorphic Function of G, H;
end;
definition
let O be set;
let G,H,I be GroupWithOperators of O;
let h be Homomorphism of G, H;
let h1 be Homomorphism of H, I;
redefine func h1 * h -> Homomorphism of G,I;
end;
definition
let O be set;
let G,H be GroupWithOperators of O;
pred G,H are_isomorphic means
:: GROUP_9:def 19
ex h being Homomorphism of G,H st h is bijective;
reflexivity;
end;
definition
let O be set, G,H be GroupWithOperators of O;
redefine pred G,H are_isomorphic;
symmetry;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func nat_hom N -> Homomorphism of G, G./.N means
:: GROUP_9:def 20
for H being strict
normal Subgroup of G st H = the multMagma of N holds it = nat_hom H;
end;
definition
let O be set;
let G,H be GroupWithOperators of O;
let g be Homomorphism of G, H;
func Ker g -> strict StableSubgroup of G means
:: GROUP_9:def 21
the carrier of it = { a where a is Element of G: g.a = 1_H};
end;
registration
let O be set;
let G,H be GroupWithOperators of O;
let g be Homomorphism of G, H;
cluster Ker g -> normal;
end;
definition
let O be set;
let G,H be GroupWithOperators of O;
let g be Homomorphism of G, H;
func Image g -> strict StableSubgroup of H means
:: GROUP_9:def 22
the carrier of it = g.:(the carrier of G);
end;
definition
let O be set;
let G be GroupWithOperators of O;
let H be StableSubgroup of G;
func carr(H) -> Subset of G equals
:: GROUP_9:def 23
the carrier of H;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let H1,H2 be StableSubgroup of G;
func H1 * H2 -> Subset of G equals
:: GROUP_9:def 24
carr H1 * carr H2;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let H1,H2 be StableSubgroup of G;
func H1 /\ H2 -> strict StableSubgroup of G means
:: GROUP_9:def 25
the carrier of it = carr(H1) /\ carr(H2);
commutativity;
end;
:: like GROUP_4:def 5
definition
let O be set;
let G be GroupWithOperators of O;
let A be Subset of G;
func the_stable_subgroup_of A -> strict StableSubgroup of G means
:: GROUP_9:def 26
A c= the carrier of it & for H being strict StableSubgroup of G st A c= the
carrier of H holds it is StableSubgroup of H;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let H1,H2 be StableSubgroup of G;
func H1 "\/" H2 -> strict StableSubgroup of G equals
:: GROUP_9:def 27
the_stable_subgroup_of
(carr H1 \/ carr H2);
end;
begin :: Some Theorems on Groups reformulated for Groups with Operators
reserve x,O for set,
o for Element of O,
G,H,I for GroupWithOperators of O,
A, B for Subset of G,
N for normal StableSubgroup of G,
H1,H2,H3 for StableSubgroup of G,
g1,g2 for Element of G,
h1,h2 for Element of H1,
h for Homomorphism of G,H;
:: GROUP_2:49
theorem :: GROUP_9:1
for x being object holds x in H1 implies x in G;
:: GROUP_2:51
theorem :: GROUP_9:2
h1 is Element of G;
:: GROUP_2:52
theorem :: GROUP_9:3
h1 = g1 & h2 = g2 implies h1 * h2 = g1 * g2;
:: GROUP_2:53
theorem :: GROUP_9:4
1_G = 1_H1;
:: GROUP_2:55
theorem :: GROUP_9:5
1_G in H1;
:: GROUP_2:57
theorem :: GROUP_9:6
h1 = g1 implies h1" = g1";
:: GROUP_2:59
theorem :: GROUP_9:7
g1 in H1 & g2 in H1 implies g1 * g2 in H1;
:: GROUP_2:60
theorem :: GROUP_9:8
g1 in H1 implies g1" in H1;
:: GROUP_2:61
theorem :: GROUP_9:9
A <> {} & (for g1,g2 st g1 in A & g2 in A holds g1 * g2 in A) & (for
g1 st g1 in A holds g1" in A) & (for o,g1 st g1 in A holds (G^o).g1 in A)
implies ex H being strict StableSubgroup of G st the carrier of H = A;
:: GROUP_2:63
theorem :: GROUP_9:10
G is StableSubgroup of G;
:: GROUP_2:65
theorem :: GROUP_9:11
for G1,G2,G3 being GroupWithOperators of O holds G1 is
StableSubgroup of G2 & G2 is StableSubgroup of G3 implies G1 is StableSubgroup
of G3;
:: GROUP_2:66
theorem :: GROUP_9:12
the carrier of H1 c= the carrier of H2 implies H1 is StableSubgroup of
H2;
:: GROUP_2:67
theorem :: GROUP_9:13
(for g being Element of G st g in H1 holds g in H2) implies H1
is StableSubgroup of H2;
:: GROUP_2:68
theorem :: GROUP_9:14
for H1,H2 being strict StableSubgroup of G st the carrier of H1 = the
carrier of H2 holds H1 = H2;
:: GROUP_2:75
theorem :: GROUP_9:15
(1).G = (1).H1;
:: GROUP_2:77
theorem :: GROUP_9:16
(1).G is StableSubgroup of H1;
:: GROUP_2:93
theorem :: GROUP_9:17
carr H1 * carr H2 = carr H2 * carr H1 implies ex H being strict
StableSubgroup of G st the carrier of H=carr H1 * carr H2;
:: GROUP_2:97
theorem :: GROUP_9:18
(for H being StableSubgroup of G st H = H1 /\ H2 holds the
carrier of H = (the carrier of H1) /\ (the carrier of H2)) & for H being strict
StableSubgroup of G holds the carrier of H = (the carrier of H1) /\ (the
carrier of H2) implies H = H1 /\ H2;
:: GROUP_2:100
theorem :: GROUP_9:19
for H being strict StableSubgroup of G holds H /\ H = H;
:: GROUP_2:102
theorem :: GROUP_9:20
H1 /\ H2 /\ H3 = H1 /\ (H2 /\ H3);
:: GROUP_2:103
theorem :: GROUP_9:21
(1).G /\ H1 = (1).G & H1 /\ (1).G = (1).G;
:: GROUP_2:167
theorem :: GROUP_9:22
union Cosets N = the carrier of G;
:: GROUP_3:149
theorem :: GROUP_9:23
for N1,N2 being strict normal StableSubgroup of G ex N being
strict normal StableSubgroup of G st the carrier of N = carr N1 * carr N2;
:: GROUP_4:37
theorem :: GROUP_9:24
g1 in the_stable_subgroup_of A iff ex F being FinSequence of the
carrier of G, I being FinSequence of INT, C being Subset of G st C =
the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c=
C & Product(F |^ I) = g1;
:: GROUP_4:40
theorem :: GROUP_9:25
for H being strict StableSubgroup of G holds
the_stable_subgroup_of carr H = H;
:: GROUP_4:41
theorem :: GROUP_9:26
A c= B implies the_stable_subgroup_of A is StableSubgroup of
the_stable_subgroup_of B;
scheme :: GROUP_9:sch 1
MeetSbgWOpEx{O() -> set, G() -> GroupWithOperators of O(), P[set]}: ex H
being strict StableSubgroup of G() st the carrier of H = meet{A where A is
Subset of G() : ex K being strict StableSubgroup of G() st A = the carrier of K
& P[K]}
provided
ex H being strict StableSubgroup of G() st P[H];
:: GROUP_4:43
theorem :: GROUP_9:27
the carrier of the_stable_subgroup_of A = meet{B where B is
Subset of G: ex H being strict StableSubgroup of G st B = the carrier of H & A
c= carr H};
:: GROUP_4:64
theorem :: GROUP_9:28
for N1,N2 being strict normal StableSubgroup of G holds N1 * N2 = N2 * N1;
:: GROUP_4:68
theorem :: GROUP_9:29
H1 "\/" H2 = the_stable_subgroup_of(H1 * H2);
:: GROUP_4:69
theorem :: GROUP_9:30
H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2;
:: GROUP_4:71
theorem :: GROUP_9:31
for N1,N2 being strict normal StableSubgroup of G holds the
carrier of N1 "\/" N2 = N1 * N2;
:: GROUP_4:72
theorem :: GROUP_9:32
for N1,N2 being strict normal StableSubgroup of G holds N1 "\/"
N2 is normal StableSubgroup of G;
:: GROUP_4:76
theorem :: GROUP_9:33
for H being strict StableSubgroup of G holds (1).G "\/" H = H &
H "\/" (1).G = H;
:: GROUP_4:77
theorem :: GROUP_9:34
(Omega).G "\/" H1 = (Omega).G & H1 "\/" (Omega).G = (Omega).G;
:: GROUP_4:78
theorem :: GROUP_9:35
H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2;
:: GROUP_4:79
theorem :: GROUP_9:36
for H2 being strict StableSubgroup of G holds H1 is
StableSubgroup of H2 iff H1 "\/" H2 = H2;
:: GROUP_4:81
theorem :: GROUP_9:37
for H3 being strict StableSubgroup of G holds H1 is
StableSubgroup of H3 & H2 is StableSubgroup of H3 implies H1 "\/" H2 is
StableSubgroup of H3;
:: GROUP_4:82
theorem :: GROUP_9:38
for H2,H3 being strict StableSubgroup of G holds H1 is
StableSubgroup of H2 implies H1 "\/" H3 is StableSubgroup of H2 "\/" H3;
:: GROUP_6:3
theorem :: GROUP_9:39
for X,Y being StableSubgroup of H1, X9,Y9 being StableSubgroup
of G st X = X9 & Y = Y9 holds X9 /\ Y9 = X /\ Y;
:: GROUP_6:9
theorem :: GROUP_9:40
N is StableSubgroup of H1 implies N is normal StableSubgroup of H1;
:: GROUP_6:10
theorem :: GROUP_9:41
H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal
StableSubgroup of H1;
:: GROUP_6:13
theorem :: GROUP_9:42
for G being strict GroupWithOperators of O holds G is trivial
implies (1).G = G;
:: GROUP_6:29
theorem :: GROUP_9:43
1_(G./.N) = carr N;
:: GROUP_6:35
theorem :: GROUP_9:44
for M,N being strict normal StableSubgroup of G, MN being normal
StableSubgroup of N st MN=M & M is StableSubgroup of N holds N./.MN is normal
StableSubgroup of G./.M;
:: GROUP_6:40
theorem :: GROUP_9:45
h.(1_G)=1_H;
:: GROUP_6:41
theorem :: GROUP_9:46
h.(g1")=(h.g1)";
:: GROUP_6:50
theorem :: GROUP_9:47
g1 in Ker h iff h.g1 = 1_H;
:: GROUP_6:52
theorem :: GROUP_9:48
for N being strict normal StableSubgroup of G holds Ker nat_hom N = N;
:: GROUP_6:53
theorem :: GROUP_9:49
rng h = the carrier of Image h;
:: GROUP_6:57
theorem :: GROUP_9:50
Image nat_hom N = G./.N;
:: GROUP_6:67
theorem :: GROUP_9:51
for H being strict GroupWithOperators of O, h being Homomorphism
of G,H holds h is onto iff Image h = H;
:: GROUP_6:68
theorem :: GROUP_9:52
for H being strict GroupWithOperators of O, h being Homomorphism
of G,H st h is onto holds for c being Element of H ex a being Element of G st h
.a = c;
:: GROUP_6:69
theorem :: GROUP_9:53
nat_hom N is onto;
:: GROUP_6:75
theorem :: GROUP_9:54
nat_hom (1).G is bijective;
:: GROUP_6:78
theorem :: GROUP_9:55
G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic;
:: GROUP_6:82
theorem :: GROUP_9:56
for G being strict GroupWithOperators of O holds G,G./.(1).G are_isomorphic;
:: GROUP_6:83
theorem :: GROUP_9:57
for G being strict GroupWithOperators of O holds G./.(Omega).G is trivial;
:: GROUP_6:87
theorem :: GROUP_9:58
for G,H being strict GroupWithOperators of O holds G,H
are_isomorphic & G is trivial implies H is trivial;
:: GROUP_6:90
theorem :: GROUP_9:59
G./.Ker h, Image h are_isomorphic;
:: GRSOLV_1:1
theorem :: GROUP_9:60
for H,F1,F2 being strict StableSubgroup of G st F1 is normal
StableSubgroup of F2 holds H /\ F1 is normal StableSubgroup of H /\ F2;
begin :: Other Theorems on Actions and Groups with Operators
reserve E for set,
A for Action of O,E,
C for Subset of G,
N1 for normal StableSubgroup of H1;
theorem :: GROUP_9:61
[#]E is_stable_under_the_action_of A;
theorem :: GROUP_9:62
[:O,{id E}:] is Action of O, E;
theorem :: GROUP_9:63
for O being non empty set, E being set, o being Element of O, A being
Action of O,E holds Product(<*o*>,A) = A.o;
theorem :: GROUP_9:64
for O being non empty set, E being set, F1,F2 being FinSequence of O,
A being Action of O,E holds Product(F1^F2,A) = Product(F1,A) * Product(F2,A);
theorem :: GROUP_9:65
for F being FinSequence of O, Y being Subset of E st Y
is_stable_under_the_action_of A holds Product(F,A) .: Y c= Y;
theorem :: GROUP_9:66
for E being non empty set, A being Action of O,E holds for X being
Subset of E, a being Element of E st X is not empty holds a in
the_stable_subset_generated_by(X,A) iff ex F being FinSequence of O, x being
Element of X st Product(F,A).x = a;
theorem :: GROUP_9:67
for G being strict Group holds ex H being strict GroupWithOperators of
O st G = the multMagma of H;
theorem :: GROUP_9:68
the multMagma of H1 is strict Subgroup of G;
theorem :: GROUP_9:69
the multMagma of N is strict normal Subgroup of G;
theorem :: GROUP_9:70
g1 in H1 implies (G^o).g1 in H1;
theorem :: GROUP_9:71
for O being set, G,H being GroupWithOperators of O, G9 being strict
StableSubgroup of G, f being Homomorphism of G,H holds ex H9 being strict
StableSubgroup of H st the carrier of H9 = f.:(the carrier of G9);
theorem :: GROUP_9:72
B is empty implies the_stable_subgroup_of B = (1).G;
theorem :: GROUP_9:73
B = the carrier of gr C implies the_stable_subgroup_of C =
the_stable_subgroup_of B;
theorem :: GROUP_9:74
for N9 being normal Subgroup of G st N9 = the multMagma of N holds G
./.N9 = the multMagma of G./.N & 1_(G./.N9) = 1_(G./.N);
theorem :: GROUP_9:75
the carrier of H1 = the carrier of H2 implies the HGrWOpStr of
H1 = the HGrWOpStr of H2;
theorem :: GROUP_9:76
H1./.N1 is trivial implies the HGrWOpStr of H1 = the HGrWOpStr of N1;
theorem :: GROUP_9:77
the carrier of H1 = the carrier of N1 implies H1./.N1 is trivial;
:: ALG I.4.6 Proposition 7(a)
theorem :: GROUP_9:78
for G,H being GroupWithOperators of O, N being StableSubgroup of
G, H9 being strict StableSubgroup of H, f being Homomorphism of G,H st N = Ker
f holds ex G9 being strict StableSubgroup of G st the carrier of G9 = f"(the
carrier of H9) & (H9 is normal implies N is normal StableSubgroup of G9 & G9 is
normal);
:: ALG I.4.6 Proposition 7(b)
theorem :: GROUP_9:79
for G,H being GroupWithOperators of O, N being StableSubgroup of
G, G9 being strict StableSubgroup of G, f being Homomorphism of G,H st N = Ker
f holds ex H9 being strict StableSubgroup of H st the carrier of H9 = f.:(the
carrier of G9) & f"(the carrier of H9) = the carrier of G9"\/"N & (f is onto &
G9 is normal implies H9 is normal);
theorem :: GROUP_9:80
for G being strict GroupWithOperators of O, N being strict
normal StableSubgroup of G, H being strict StableSubgroup of G./.N st the
carrier of G = (nat_hom N)"(the carrier of H) holds H = (Omega).(G./.N);
theorem :: GROUP_9:81
for G being strict GroupWithOperators of O, N being strict
normal StableSubgroup of G, H being strict StableSubgroup of G./.N st the
carrier of N = (nat_hom N)"(the carrier of H) holds H = (1).(G./.N);
theorem :: GROUP_9:82
for G,H being strict GroupWithOperators of O st G,H
are_isomorphic & G is simple holds H is simple;
theorem :: GROUP_9:83
for G being GroupWithOperators of O, H being StableSubgroup of G
, FG being FinSequence of the carrier of G, FH being FinSequence of the carrier
of H, I be FinSequence of INT st FG=FH & len FG = len I holds Product(FG |^ I)
= Product(FH |^ I);
theorem :: GROUP_9:84
for O,E1,E2 being set, A1 being Action of O,E1, A2 being Action
of O,E2, F being FinSequence of O st E1 c= E2 & (for o being Element of O, f1
being Function of E1,E1, f2 being Function of E2,E2 st f1=A1.o & f2=A2.o holds
f1 = f2|E1) holds Product(F,A1) = Product(F,A2)|E1;
theorem :: GROUP_9:85
for N1,N2 being strict StableSubgroup of H1, N19,N29 being
strict StableSubgroup of G st N1 = N19 & N2 = N29 holds N19 * N29 = N1 * N2;
theorem :: GROUP_9:86
for N1,N2 being strict StableSubgroup of H1, N19,N29 being
strict StableSubgroup of G st N1 = N19 & N2 = N29 holds N19 "\/" N29 = N1 "\/"
N2;
theorem :: GROUP_9:87
for N1,N2 being strict StableSubgroup of G st N1 is normal
StableSubgroup of H1 & N2 is normal StableSubgroup of H1 holds N1 "\/" N2 is
normal StableSubgroup of H1;
theorem :: GROUP_9:88
for f being Homomorphism of G,H holds for g being Homomorphism
of H,I holds the carrier of Ker(g*f) = f"(the carrier of Ker g);
theorem :: GROUP_9:89
for G9 being StableSubgroup of G, H9 being StableSubgroup of H,
f being Homomorphism of G,H st the carrier of H9 = f.:(the carrier of G9) or
the carrier of G9 = f"(the carrier of H9) holds f|(the carrier of G9) is
Homomorphism of G9,H9;
:: ALG I.4.6 Corollary 2
theorem :: GROUP_9:90
for G,H being strict GroupWithOperators of O, N,L,G9 being
strict StableSubgroup of G, f being Homomorphism of G,H st N = Ker f & L is
strict normal StableSubgroup of G9 holds L"\/"(G9/\N) is normal StableSubgroup
of G9 & L"\/"N is normal StableSubgroup of G9"\/"N & for N1 being strict normal
StableSubgroup of G9"\/"N, N2 being strict normal StableSubgroup of G9 st N1=L
"\/"N & N2=L"\/"(G9/\N) holds (G9"\/"N)./.N1, G9./.N2 are_isomorphic;
:: ALG I.4.7 Lemma 1
begin :: The Zassenhaus Butterfly Lemma
theorem :: GROUP_9:91
for H,K,H9,K9 being strict StableSubgroup of G, JH being normal
StableSubgroup of H9"\/"(H/\K), HK being normal StableSubgroup of H/\K st H9 is
normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9"\/"(H/\
K9) & HK=(H9/\K)"\/"(K9/\H) holds (H9"\/"(H/\K))./.JH, (H/\K)./.HK
are_isomorphic;
theorem :: GROUP_9:92
for H,K,H9,K9 being strict StableSubgroup of G st H9 is normal
StableSubgroup of H & K9 is normal StableSubgroup of K holds H9"\/"(H/\K9) is
normal StableSubgroup of H9"\/"(H/\K);
::$N Zassenhaus Lemma
theorem :: GROUP_9:93
for H,K,H9,K9 being strict StableSubgroup of G, JH being normal
StableSubgroup of H9"\/"(H/\K), JK being normal StableSubgroup of K9"\/"(K/\H)
st JH = H9"\/"(H/\K9) & JK= K9"\/"(K/\H9) & H9 is normal StableSubgroup of H &
K9 is normal StableSubgroup of K holds (H9"\/"(H/\K))./.JH, (K9"\/"(K/\H))./.JK
are_isomorphic;
begin :: Composition Series
:: ALG I.4.7 Definition 9
definition
let O be set;
let G be GroupWithOperators of O;
let IT be FinSequence of the_stable_subgroups_of G;
attr IT is composition_series means
:: GROUP_9:def 28
IT.1=(Omega).G & IT.(len IT)=
(1).G & for i being Nat st i in dom IT & i+1 in dom IT for H1,H2 being
StableSubgroup of G st H1=IT.i & H2=IT.(i+1) holds H2 is normal StableSubgroup
of H1;
end;
registration
let O be set;
let G be GroupWithOperators of O;
cluster composition_series for FinSequence of the_stable_subgroups_of G;
end;
definition
let O be set;
let G be GroupWithOperators of O;
mode CompositionSeries of G is composition_series FinSequence of
the_stable_subgroups_of G;
end;
:: ALG I.4.7 Definition 9
definition
let O be set;
let G be GroupWithOperators of O;
let s1,s2 be CompositionSeries of G;
pred s1 is_finer_than s2 means
:: GROUP_9:def 29
ex x being set st x c= dom s1 & s2 = s1 * Sgm x;
reflexivity;
end;
definition
let O be set;
let G be GroupWithOperators of O;
let IT be CompositionSeries of G;
attr IT is strictly_decreasing means
:: GROUP_9:def 30
for i being Nat st i in dom IT
& i+1 in dom IT for H being StableSubgroup of G, N being normal StableSubgroup
of H st H=IT.i & N=IT.(i+1) holds H./.N is not trivial;
end;
:: ALG I.4.7 Definition 10
definition
let O be set;
let G be GroupWithOperators of O;
let IT be CompositionSeries of G;
attr IT is jordan_holder means
:: GROUP_9:def 31
IT is strictly_decreasing & not ex s
being CompositionSeries of G st s<>IT & s is strictly_decreasing & s
is_finer_than IT;
end;
:: ALG I.4.7 Definition 9
definition
let O be set;
let G1,G2 be GroupWithOperators of O;
let s1 be CompositionSeries of G1;
let s2 be CompositionSeries of G2;
pred s1 is_equivalent_with s2 means
:: GROUP_9:def 32
len s1 = len s2 & for n being
Nat st n + 1 = len s1 holds ex p being Permutation of Seg n st for H1 being
StableSubgroup of G1, H2 being StableSubgroup of G2, N1 being normal
StableSubgroup of H1, N2 being normal StableSubgroup of H2, i,j being Nat st 1
<=i & i<=n & j=p.i & H1=s1.i & H2=s2.j & N1=s1.(i+1) & N2=s2.(j+1) holds H1./.
N1,H2./.N2 are_isomorphic;
end;
:: ALG I.4.7 Definition 9
definition
let O be set;
let G be GroupWithOperators of O;
let s be CompositionSeries of G;
func the_series_of_quotients_of s -> FinSequence means
:: GROUP_9:def 33
len s = len
it + 1 & for i being Nat st i in dom it for H being StableSubgroup of G, N
being normal StableSubgroup of H st H=s.i & N=s.(i+1) holds it.i = H./.N if len
s > 1 otherwise it={};
end;
definition
let O be set;
let f1,f2 be FinSequence;
let p be Permutation of dom f1;
pred f1,f2 are_equivalent_under p,O means
:: GROUP_9:def 34
len f1 = len f2 & for H1,
H2 being GroupWithOperators of O, i,j being Nat st i in dom f1 & j=p".i & H1=f1
.i & H2=f2.j holds H1,H2 are_isomorphic;
end;
reserve y for set,
H19,H29 for StableSubgroup of G,
N19 for normal StableSubgroup of H19,
s1,s19,s2,s29 for CompositionSeries of G,
fs for FinSequence of the_stable_subgroups_of G,
f1,f2 for FinSequence,
i,j,n for Nat;
theorem :: GROUP_9:94
i in dom s1 & i+1 in dom s1 & s1.i=s1.(i+1) & fs=Del(s1,i)
implies fs is composition_series;
theorem :: GROUP_9:95
s1 is_finer_than s2 implies ex n st len s1 = len s2 + n;
theorem :: GROUP_9:96
len s2 = len s1 & s2 is_finer_than s1 implies s1 = s2;
theorem :: GROUP_9:97
s1 is not empty & s2 is_finer_than s1 implies s2 is not empty;
theorem :: GROUP_9:98
s1 is_finer_than s2 & s1 is jordan_holder & s2 is jordan_holder implies s1=s2
;
theorem :: GROUP_9:99
i in dom s1 & i+1 in dom s1 & s1.i = s1.(i+1) & s19 = Del(s1,i)
& s2 is jordan_holder & s1 is_finer_than s2 implies s19 is_finer_than s2;
theorem :: GROUP_9:100
len s1 > 1 & s2<>s1 & s2 is strictly_decreasing & s2
is_finer_than s1 implies ex i,j st i in dom s1 & i in dom s2 & i+1 in dom s1 &
i+1 in dom s2 & j in dom s2 & i+1s2.(i+1) & s1.(i+1)
=s2.j;
theorem :: GROUP_9:101
i in dom s1 & j in dom s1 & i<=j & H1 = s1.i & H2 = s1.j
implies H2 is StableSubgroup of H1;
theorem :: GROUP_9:102
y in rng the_series_of_quotients_of s1 implies y is strict
GroupWithOperators of O;
theorem :: GROUP_9:103
i in dom the_series_of_quotients_of s1 & (for H st H=(
the_series_of_quotients_of s1).i holds H is trivial) implies i in dom s1 & i+1
in dom s1 & s1.i=s1.(i+1);
theorem :: GROUP_9:104
i in dom s1 & i+1 in dom s1 & s1.i=s1.(i+1) & s2=Del(s1,i)
implies the_series_of_quotients_of s2=Del(the_series_of_quotients_of s1,i);
theorem :: GROUP_9:105
f1=the_series_of_quotients_of s1 & i in dom f1 & (for H st H = f1.i
holds H is trivial) implies Del(s1,i) is CompositionSeries of G & for s2 st s2
= Del(s1,i) holds the_series_of_quotients_of s2 = Del(f1,i);
theorem :: GROUP_9:106
i in dom f1 & (ex p being Permutation of dom f1
st f1,f2 are_equivalent_under p,O & j = p".i) implies ex p9 being Permutation
of dom Del(f1,i) st Del(f1,i),Del(f2,j) are_equivalent_under p9,O;
theorem :: GROUP_9:107
for G1,G2 being GroupWithOperators of O, s1 being
CompositionSeries of G1, s2 being CompositionSeries of G2 st s1 is empty & s2
is empty holds s1 is_equivalent_with s2;
theorem :: GROUP_9:108
for G1,G2 being GroupWithOperators of O, s1 be
CompositionSeries of G1, s2 be CompositionSeries of G2 st s1 is not empty & s2
is not empty holds s1 is_equivalent_with s2 iff ex p being Permutation of dom
the_series_of_quotients_of s1 st the_series_of_quotients_of s1,
the_series_of_quotients_of s2 are_equivalent_under p,O;
theorem :: GROUP_9:109
s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2
implies ex i st i in dom the_series_of_quotients_of s1 & for H st H = (
the_series_of_quotients_of s1).i holds H is trivial;
:: ALG I.4.7 Proposition 9
theorem :: GROUP_9:110
len s1 > 1 implies (s1 is jordan_holder iff for i st i in dom
the_series_of_quotients_of s1 holds (the_series_of_quotients_of s1).i is strict
simple GroupWithOperators of O);
theorem :: GROUP_9:111
1<=i & i<=len s1-1 implies s1.i is strict StableSubgroup of G &
s1.(i+1) is strict StableSubgroup of G;
theorem :: GROUP_9:112
1<=i & i<=len s1-1 & H1=s1.i & H2=s1.(i+1) implies H2 is normal
StableSubgroup of H1;
theorem :: GROUP_9:113
s1 is_equivalent_with s1;
theorem :: GROUP_9:114
(len s1<=1 or len s2<=1) & len s1<=len s2 implies s2 is_finer_than s1;
theorem :: GROUP_9:115
s1 is_equivalent_with s2 & s1 is jordan_holder implies s2 is jordan_holder;
begin :: The Schreier Refinement Theorem
definition
let O,G,s1,s2;
assume that
len s1>1 and
len s2>1;
func the_schreier_series_of(s1,s2) -> CompositionSeries of G means
:: GROUP_9:def 35
for k,i,j being Nat, H1,H2,H3 being StableSubgroup of G holds (k=(i-1)*(len s2-
1)+j & 1<=i & i<=len s1-1 & 1<=j & j<=len s2-1 & H1=s1.(i+1) & H2=s1.i & H3=s2.
j implies it.k = H1"\/"(H2/\H3)) & (k=(len s1-1)*(len s2-1) + 1 implies it.k =
(1).G) & len it = (len s1-1)*(len s2-1) + 1;
end;
theorem :: GROUP_9:116
len s1>1 & len s2>1 implies the_schreier_series_of(s1,s2) is_finer_than s1;
theorem :: GROUP_9:117
len s1>1 & len s2>1 implies the_schreier_series_of(s1,s2)
is_equivalent_with the_schreier_series_of(s2,s1);
:: ALG I.4.7 Theorem 5
::$N Schreier Refinement Theorem
theorem :: GROUP_9:118
ex s19,s29 st s19 is_finer_than s1 & s29 is_finer_than s2 & s19
is_equivalent_with s29;
begin :: The Jordan-H\"older Theorem
:: ALG I.4.7 Theorem 6
::$N Jordan-H\"older Theorem
theorem :: GROUP_9:119
s1 is jordan_holder & s2 is jordan_holder implies s1 is_equivalent_with s2;
begin :: Appendix
theorem :: GROUP_9:120
for P,R being Relation holds P = (rng P)|`R iff P~ = (R~)|(dom (P~));
theorem :: GROUP_9:121
for X being set, P,R being Relation holds P*(R|X) = (X|`P)*R;
theorem :: GROUP_9:122
for n being Nat, X being set, f being PartFunc of REAL, REAL st X c=
Seg n & X c= dom f & f|X is increasing & f.:X c= NAT \ {0} holds Sgm(f.:X) = f
* Sgm X;
theorem :: GROUP_9:123
for y being set, i,n being Nat st y c= Seg(n+1) & i in Seg(n+1) & not
i in y holds ex x st Sgm x = Sgm(Seg(n+1)\{i})" * Sgm y & x c= Seg n;
theorem :: GROUP_9:124
for D being non empty set, f being FinSequence of D, p being Element
of D, n being Nat st n in dom f holds f = Del(Ins(f,n,p),n+1);
theorem :: GROUP_9:125
for G,H being Group, F1 being FinSequence of the carrier of G, F2
being FinSequence of the carrier of H, I being FinSequence of INT, f being
Homomorphism of G,H st (for k being Nat st k in dom F1 holds F2.k = f.(F1.k)) &
len F1 = len I & len F2 = len I holds f.(Product(F1 |^ I)) = Product(F2 |^ I)
;