:: 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) ;