begin
:: deftheorem Def1 defines is_stable_under_the_action_of GROUP_9:def 1 :
Lm1:
for O, E being set
for A being Action of O,E holds [#] E is_stable_under_the_action_of A
:: deftheorem Def2 defines the_stable_subset_generated_by GROUP_9:def 2 :
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 :
Def3:
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 < len F holds
ex
f,
g being
Function of
E,
E st
(
f = PF . n &
g = A . (F . (n + 1)) &
PF . (n + 1) = f * g ) ) );
existence
( ( len F = 0 implies ex b1 being Function of E,E st b1 = id E ) & ( not len F = 0 implies ex b1 being Function of E,E ex PF being FinSequence of Funcs E,E st
( b1 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) )
uniqueness
for b1, b2 being Function of E,E holds
( ( len F = 0 & b1 = id E & b2 = id E implies b1 = b2 ) & ( not len F = 0 & ex PF being FinSequence of Funcs E,E st
( b1 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) & ex PF being FinSequence of Funcs E,E st
( b2 = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) implies b1 = b2 ) )
consistency
for b1 being Function of E,E holds verum
;
end;
:: deftheorem Def3 defines Product GROUP_9:def 3 :
:: deftheorem Def4 defines distributive GROUP_9:def 4 :
:: deftheorem Def5 defines distributive GROUP_9:def 5 :
Lm2:
for O, E being set holds [:O,{(id E)}:] is Action of O,E
Lm3:
for O being set
for G being strict Group ex H being non empty HGrWOpStr of O st
( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H,the multF of H #) )
:: deftheorem Def6 defines ^ GROUP_9:def 6 :
:: deftheorem Def7 defines StableSubgroup GROUP_9:def 7 :
Lm4:
for O being set
for G being GroupWithOperators of O holds HGrWOpStr(# the carrier of G,the multF of G,the action of G #) is StableSubgroup of G
Lm5:
for O being set
for G being GroupWithOperators of O
for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
H1 = H2
:: deftheorem Def8 defines (1). GROUP_9:def 8 :
:: deftheorem defines (Omega). GROUP_9:def 9 :
:: deftheorem Def10 defines normal GROUP_9:def 10 :
:: deftheorem Def11 defines the_stable_subgroups_of GROUP_9:def 11 :
:: deftheorem Def12 defines simple GROUP_9:def 12 :
Lm6:
Group_of_Perm 2 is simple
:: deftheorem Def13 defines simple GROUP_9:def 13 :
Lm7:
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds multMagma(# the carrier of N,the multF of N #) is strict normal Subgroup of G
Lm8:
for G1, G2 being Group
for A1 being Subset of
for A2 being Subset of
for H1 being strict Subgroup of G1
for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1,the multF of G1 #) = multMagma(# the carrier of G2,the multF of G2 #) & A1 = A2 & H1 = H2 holds
( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )
:: deftheorem Def14 defines Cosets GROUP_9:def 14 :
:: deftheorem Def15 defines CosOp GROUP_9:def 15 :
Lm9:
for G being Group
for N being normal Subgroup of G
for A being Element of Cosets N
for g being Element of holds
( g in A iff A = g * N )
Lm10:
for O being set
for o being Element of O
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of st g in H holds
(G ^ o) . g in H
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 :
Def16:
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 st
( g in A & h in B & h = (G ^ o) . g ) } if not
O is
empty otherwise it = [:{} ,{(id (Cosets N))}:];
existence
( ( not O is empty implies ex b1 being Action of O,(Cosets N) st
for o being Element of O holds b1 . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of st
( g in A & h in B & h = (G ^ o) . g ) } ) & ( O is empty implies ex b1 being Action of O,(Cosets N) st b1 = [:{} ,{(id (Cosets N))}:] ) )
uniqueness
for b1, b2 being Action of O,(Cosets N) holds
( ( not O is empty & ( for o being Element of O holds b1 . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of st
( g in A & h in B & h = (G ^ o) . g ) } ) & ( for o being Element of O holds b2 . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of st
( g in A & h in B & h = (G ^ o) . g ) } ) implies b1 = b2 ) & ( O is empty & b1 = [:{} ,{(id (Cosets N))}:] & b2 = [:{} ,{(id (Cosets N))}:] implies b1 = b2 ) )
correctness
consistency
for b1 being Action of O,(Cosets N) holds verum;
;
end;
:: deftheorem Def16 defines CosAc GROUP_9:def 16 :
:: deftheorem defines ./. GROUP_9:def 17 :
:: deftheorem Def18 defines homomorphic GROUP_9:def 18 :
Lm11:
for O being set
for G, H, I being GroupWithOperators of O
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I
:: deftheorem GROUP_9:def 19 :
canceled;
:: deftheorem GROUP_9:def 20 :
canceled;
:: deftheorem GROUP_9:def 21 :
canceled;
:: deftheorem Def22 defines are_isomorphic GROUP_9:def 22 :
Lm12:
for O being set
for G, H being GroupWithOperators of O st G,H are_isomorphic holds
H,G are_isomorphic
:: deftheorem Def23 defines nat_hom GROUP_9:def 23 :
Lm13:
for O being set
for G, H being GroupWithOperators of O
for g being Homomorphism of G,H holds g . (1_ G) = 1_ H
Lm14:
for O being set
for G, H being GroupWithOperators of O
for a being Element of
for g being Homomorphism of G,H holds g . (a " ) = (g . a) "
Lm15:
for O being set
for G being GroupWithOperators of O
for A being Subset of st A <> {} & ( for g1, g2 being Element of st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of st g in A holds
g " in A ) & ( for o being Element of O
for g being Element of st g in A holds
(G ^ o) . g in A ) holds
ex H being strict StableSubgroup of G st the carrier of H = A
:: deftheorem Def24 defines Ker GROUP_9:def 24 :
Lm16:
for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G holds multMagma(# the carrier of H,the multF of H #) is strict Subgroup of G
Lm17:
for O being set
for G, H being GroupWithOperators of O
for G' being strict StableSubgroup of G
for f being Homomorphism of G,H ex H' being strict StableSubgroup of H st the carrier of H' = f .: the carrier of G'
:: deftheorem Def25 defines Image GROUP_9:def 25 :
:: deftheorem defines carr GROUP_9:def 26 :
:: deftheorem defines * GROUP_9:def 27 :
Lm18:
for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G holds 1_ G in H
Lm19:
for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g1, g2 being Element of st g1 in H & g2 in H holds
g1 * g2 in H
Lm20:
for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of st g in H holds
g " in H
:: deftheorem Def28 defines /\ GROUP_9:def 28 :
Lm21:
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is StableSubgroup of H2
:: deftheorem Def29 defines the_stable_subgroup_of GROUP_9:def 29 :
:: deftheorem defines "\/" GROUP_9:def 30 :
begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
Lm22:
for O being set
for G being GroupWithOperators of O
for H2 being StableSubgroup of G
for H1 being strict StableSubgroup of G holds
( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )
theorem Th21:
theorem Th22:
theorem Th23:
Lm23:
for F1 being FinSequence
for y being Element of NAT st y in dom F1 holds
( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )
Lm24:
for G, H being Group
for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for 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)
theorem Th24:
Lm25:
for O being set
for G being GroupWithOperators of O
for A being Subset of st A is empty holds
the_stable_subgroup_of A = (1). G
Lm26:
for O being non empty set
for E being set
for o being Element of O
for A being Action of O,E holds Product <*o*>,A = A . o
Lm27:
for O being non empty set
for E being set
for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product (F ^ <*o*>),A = (Product F,A) * (Product <*o*>,A)
Lm28:
for O being non empty set
for E being set
for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product (<*o*> ^ F),A = (Product <*o*>,A) * (Product F,A)
Lm29:
for O being non empty set
for E being set
for F1, F2 being FinSequence of O
for A being Action of O,E holds Product (F1 ^ F2),A = (Product F1,A) * (Product F2,A)
Lm30:
for O, E being set
for F being FinSequence of O
for Y being Subset of
for A being Action of O,E st Y is_stable_under_the_action_of A holds
(Product F,A) .: Y c= Y
Lm31:
for O being set
for E being non empty set
for A being Action of O,E
for X being Subset of
for a being Element of E st not X is empty holds
( a in the_stable_subset_generated_by X,A iff ex F being FinSequence of O ex x being Element of X st (Product F,A) . x = a )
theorem Th25:
theorem Th26:
theorem Th27:
Lm32:
for O being set
for G being GroupWithOperators of O
for B, A being Subset of st B = the carrier of (gr A) holds
the_stable_subgroup_of A = the_stable_subgroup_of B
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
Lm33:
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 is StableSubgroup of H1 "\/" H2
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
Lm34:
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 /\ H2 is StableSubgroup of H1
theorem Th41:
theorem Th42:
Lm35:
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for N' being normal Subgroup of G st N' = multMagma(# the carrier of N,the multF of N #) holds
( G ./. N' = multMagma(# the carrier of (G ./. N),the multF of (G ./. N) #) & 1_ (G ./. N') = 1_ (G ./. N) )
theorem Th43:
theorem Th44:
theorem
theorem
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
begin
theorem Th91:
theorem Th92:
theorem Th93:
begin
:: deftheorem Def31 defines composition_series GROUP_9:def 31 :
:: deftheorem Def32 defines is_finer_than GROUP_9:def 32 :
:: deftheorem Def33 defines strictly_decreasing GROUP_9:def 33 :
:: deftheorem Def34 defines jordan_holder GROUP_9:def 34 :
:: deftheorem Def35 defines is_equivalent_with GROUP_9:def 35 :
:: deftheorem Def36 defines the_series_of_quotients_of GROUP_9:def 36 :
:: deftheorem Def37 defines are_equivalent_under GROUP_9:def 37 :
theorem Th94:
theorem Th95:
theorem Th96:
theorem Th97:
theorem Th98:
Lm36:
for P, R being Relation holds
( P = (rng P) | R iff P ~ = (R ~ ) | (dom (P ~ )) )
Lm37:
for X being set
for P, R being Relation holds P * (R | X) = (X | P) * R
Lm38:
for n being Nat
for X being set
for f being PartFunc of , 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)
Lm39:
for y being set
for n, i being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds
ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) " ) * (Sgm y) & x c= Seg n )
theorem Th99:
theorem Th100:
theorem Th101:
theorem Th102:
theorem Th103:
theorem Th104:
theorem
theorem Th106:
for
O being
set for
G being
GroupWithOperators of
O for
s1,
s2 being
CompositionSeries of
G for
f1,
f2 being
FinSequence for
i,
j being
Nat st
f1 = the_series_of_quotients_of s1 &
f2 = the_series_of_quotients_of s2 &
i in dom f1 & ex
p being
Permutation of
dom f1 st
(
f1,
f2 are_equivalent_under p,
O &
j = (p " ) . i ) holds
ex
p' being
Permutation of
dom (Del f1,i) st
Del f1,
i,
Del f2,
j are_equivalent_under p',
O
theorem Th107:
theorem Th108:
theorem Th109:
Lm40:
for k, m being Element of NAT holds
( k < m iff k <= m - 1 )
Lm41:
for a being Element of NAT
for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )
Lm42:
for a being Element of NAT
for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del fs,a = fs1 ^ fs2
Lm43:
for a being Element of NAT
for fs1, fs2 being FinSequence holds
( ( a <= len fs1 implies Del (fs1 ^ fs2),a = (Del fs1,a) ^ fs2 ) & ( a >= 1 implies Del (fs1 ^ fs2),((len fs1) + a) = fs1 ^ (Del fs2,a) ) )
Lm44:
for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat st n in dom f holds
f = Del (Ins f,n,p),(n + 1)
theorem Th110:
theorem Th111:
theorem Th112:
theorem Th113:
theorem Th114:
theorem Th115:
Lm45:
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for k, l being Nat st k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds
ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )
Lm46:
for O being set
for G being GroupWithOperators of O
for i1, j1, i2, j2 being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 holds
( j1 = j2 & i1 = i2 )
Lm47:
for O being set
for G being GroupWithOperators of O
for k being integer number
for i, j being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )
begin
definition
let O be
set ;
let G be
GroupWithOperators of
O;
let s1,
s2 be
CompositionSeries of
G;
assume that A1:
len s1 > 1
and A2:
len s2 > 1
;
func the_schreier_series_of s1,
s2 -> CompositionSeries of
G means :
Def38:
for
k,
i,
j being
Nat for
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 );
existence
ex b1 being CompositionSeries of G st
for k, i, j being Nat
for 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 b1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b1 . k = (1). G ) & len b1 = (((len s1) - 1) * ((len s2) - 1)) + 1 )
uniqueness
for b1, b2 being CompositionSeries of G st ( for k, i, j being Nat
for 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 b1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b1 . k = (1). G ) & len b1 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) & ( for k, i, j being Nat
for 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 b2 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b2 . k = (1). G ) & len b2 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) holds
b1 = b2
end;
:: deftheorem Def38 defines the_schreier_series_of GROUP_9:def 38 :
theorem Th116:
theorem Th117:
theorem Th118:
begin
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem