:: Homomorphisms and Isomorphisms of Groups. Quotient Group :: by Wojciech A. Trybulec and Micha{\l} J. Trybulec :: :: Received October 3, 1991 :: Copyright (c) 1991-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 XBOOLE_0, FUNCT_1, SUBSET_1, GROUP_1, GROUP_2, PRE_TOPC, RLSUB_1, NUMBERS, INT_1, STRUCT_0, RELAT_1, TARSKI, NEWTON, XXREAL_1, GROUP_4, GROUP_5, ALGSTR_0, NATTRA_1, ZFMISC_1, CARD_1, FINSET_1, BINOP_1, QC_LANG1, CQC_SIM1, REALSET1, MSSUBFAM, FUNCOP_1, ARYTM_3, XXREAL_0, COMPLEX1, FUNCT_2, WELLORD1, EQREL_1, GROUP_6, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, BINOP_1, INT_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, NAT_1, GROUP_4, GROUP_5, INT_2; constructors RELAT_2, PARTFUN1, BINOP_1, FUNCOP_1, FINSUB_1, XXREAL_0, NAT_1, REAL_1, INT_2, REALSET2, GROUP_4, GROUP_5, RELSET_1, BINOP_2; registrations FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, XREAL_0, INT_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, ORDINAL1, RELSET_1; requirements NUMERALS, SUBSET, BOOLE; begin theorem :: GROUP_6:1 for A,B being non empty set, f being Function of A,B holds f is one-to-one iff for a,b being Element of A st f.a = f.b holds a = b; definition let G be Group, A be Subgroup of G; redefine mode Subgroup of A -> Subgroup of G; end; registration let G be Group; cluster (1).G -> normal; cluster (Omega).G -> normal; end; reserve n for Element of NAT; reserve i for Integer; reserve G,H,I for Group; reserve A,B for Subgroup of G; reserve N for normal Subgroup of G; reserve a,a1,a2,a3,b,b1 for Element of G; reserve c,d for Element of H; reserve f for Function of the carrier of G, the carrier of H; reserve x,y,y1,y2,z for set; reserve A1,A2 for Subset of G; theorem :: GROUP_6:2 for X being Subgroup of A, x being Element of A st x = a holds x * X = a * (X qua Subgroup of G) & X * x = (X qua Subgroup of G) * a; theorem :: GROUP_6:3 for X,Y being Subgroup of A holds (X qua Subgroup of G) /\ (Y qua Subgroup of G) = X /\ Y; theorem :: GROUP_6:4 a * b * a" = b |^ a" & a * (b * a") = b |^ a"; theorem :: GROUP_6:5 a * A * A = a * A & a * (A * A) = a * A & A * A * a = A * a & A * (A * a) = A *a; theorem :: GROUP_6:6 for G being Group, A1 being Subset of G holds A1 = the set of all [.a,b.] where a is Element of G, b is Element of G implies G` = gr A1; theorem :: GROUP_6:7 for G being strict Group, B being strict Subgroup of G holds G` is Subgroup of B iff for a,b being Element of G holds [.a,b.] in B; theorem :: GROUP_6:8 for N being normal Subgroup of G holds N is Subgroup of B implies N is normal Subgroup of B; definition let G,B; let M be normal Subgroup of G; assume the multMagma of M is Subgroup of B; func (B,M)`*` -> strict normal Subgroup of B equals :: GROUP_6:def 1 the multMagma of M; end; theorem :: GROUP_6:9 B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B; definition let G,B; let N be normal Subgroup of G; redefine func B /\ N -> strict normal Subgroup of B; end; definition let G; let N be normal Subgroup of G; let B; redefine func N /\ B -> strict normal Subgroup of B; end; definition let G be non empty 1-sorted; redefine attr G is trivial means :: GROUP_6:def 2 ex x being object st the carrier of G = {x}; end; theorem :: GROUP_6:10 (1).G is trivial; registration let G; cluster (1).G -> trivial; end; registration cluster strict trivial for Group; end; theorem :: GROUP_6:11 (for G being trivial Group holds card G = 1 & G is finite) & for G being finite Group st card G = 1 holds G is trivial; theorem :: GROUP_6:12 for G being strict trivial Group holds (1).G = G; notation let G,N; synonym Cosets N for Left_Cosets N; end; registration let G,N; cluster Cosets N -> non empty; end; theorem :: GROUP_6:13 for x being object holds for N being normal Subgroup of G holds x in Cosets N implies ex a st x = a * N & x = N * a; theorem :: GROUP_6:14 for N being normal Subgroup of G holds a * N in Cosets N & N * a in Cosets N; theorem :: GROUP_6:15 for N being normal Subgroup of G holds x in Cosets N implies x is Subset of G; theorem :: GROUP_6:16 for N being normal Subgroup of G holds A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N; definition let G; let N be normal Subgroup of G; func CosOp N -> BinOp of Cosets N means :: GROUP_6:def 3 for W1,W2 being Element of Cosets N for A1,A2 st W1 = A1 & W2 = A2 holds it.(W1,W2) = A1 * A2; end; definition let G; let N be normal Subgroup of G; func G./.N -> multMagma equals :: GROUP_6:def 4 multMagma (# Cosets N, CosOp N #); end; registration let G; let N be normal Subgroup of G; cluster G./.N -> strict non empty; end; theorem :: GROUP_6:17 for N being normal Subgroup of G holds the carrier of G./.N = Cosets N; theorem :: GROUP_6:18 for N being normal Subgroup of G holds the multF of G./.N = CosOp N; reserve N for normal Subgroup of G; reserve S,T1,T2 for Element of G./.N; definition let G,N,S; func @S -> Subset of G equals :: GROUP_6:def 5 S; end; theorem :: GROUP_6:19 for N being normal Subgroup of G, T1,T2 being Element of G./.N holds @ T1 * @T2 = T1 * T2; theorem :: GROUP_6:20 @(T1 * T2) = @T1 * @T2; registration let G; let N be normal Subgroup of G; cluster G./.N -> associative Group-like; end; theorem :: GROUP_6:21 for N being normal Subgroup of G, S being Element of G./.N ex a st S = a * N & S = N * a; theorem :: GROUP_6:22 N * a is Element of G./.N & a * N is Element of G./.N & carr N is Element of G./.N; theorem :: GROUP_6:23 for x being object holds for N being normal Subgroup of G holds x in G./.N iff ex a st x = a * N & x = N * a; theorem :: GROUP_6:24 for N being normal Subgroup of G holds 1_(G./.N) = carr N; theorem :: GROUP_6:25 for N being normal Subgroup of G, S being Element of G./.N st S = a * N holds S" = a" * N; theorem :: GROUP_6:26 for N being normal Subgroup of G holds card(G./.N) = Index N; theorem :: GROUP_6:27 for N being normal Subgroup of G holds Left_Cosets N is finite implies card(G./.N) = index N; theorem :: GROUP_6:28 for M being strict normal Subgroup of G holds M is Subgroup of B implies B./.(B,M)`*` is Subgroup of G./.M; theorem :: GROUP_6:29 for N,M being strict normal Subgroup of G holds M is Subgroup of N implies N./.(N,M)`*` is normal Subgroup of G./.M; theorem :: GROUP_6:30 for G being strict Group, N be strict normal Subgroup of G holds G./.N is commutative Group iff G` is Subgroup of N; definition let G, H be non empty multMagma; let f be Function of G, H; attr f is multiplicative means :: GROUP_6:def 6 for a, b being Element of G holds f.(a * b) = f.a * f.b; end; registration let G, H be unital non empty multMagma; cluster multiplicative for Function of G, H; end; definition let G,H; mode Homomorphism of G,H is multiplicative Function of G, H; end; reserve g,h for Homomorphism of G,H; reserve h1 for Homomorphism of H,I; theorem :: GROUP_6:31 g.(1_G) = 1_H; registration let G,H; cluster -> unity-preserving for Homomorphism of G,H; end; theorem :: GROUP_6:32 g.(a") = (g.a)"; theorem :: GROUP_6:33 g.(a |^ b) = (g.a) |^ (g.b); theorem :: GROUP_6:34 g. [.a,b.] = [.g.a,g.b.]; theorem :: GROUP_6:35 g. [.a1,a2,a3.] = [.g.a1,g.a2,g.a3.]; theorem :: GROUP_6:36 g.(a |^ n) = (g.a) |^ n; theorem :: GROUP_6:37 g.(a |^ i) = (g.a) |^ i; theorem :: GROUP_6:38 for G being non empty multMagma holds id the carrier of G is multiplicative; theorem :: GROUP_6:39 for G,H,I being unital non empty multMagma, h being multiplicative Function of G,H, h1 being multiplicative Function of H,I holds h1 * h is multiplicative; registration let G,H,I be unital non empty multMagma, h be multiplicative Function of G,H, h1 be multiplicative Function of H,I; cluster h1 * h -> multiplicative for Function of G,I; end; definition let G,H be non empty multMagma; func 1:(G,H) -> Function of G,H equals :: GROUP_6:def 7 G --> 1_H; end; registration let G,H be unital non empty multMagma; cluster 1:(G,H) -> multiplicative; end; theorem :: GROUP_6:40 h1 * 1:(G,H) = 1:(G,I) & 1:(H,I) * h = 1:(G,I); definition let G; let N be normal Subgroup of G; func nat_hom N -> Function of G,G./.N means :: GROUP_6:def 8 for a holds it.a = a * N; end; registration let G; let N be normal Subgroup of G; cluster nat_hom N -> multiplicative; end; definition let G,H,g; func Ker g -> strict Subgroup of G means :: GROUP_6:def 9 the carrier of it = {a : g. a = 1_H}; end; registration let G,H,g; cluster Ker g -> normal; end; theorem :: GROUP_6:41 a in Ker h iff h.a = 1_H; theorem :: GROUP_6:42 for G,H being strict Group holds Ker 1:(G,H) = G; theorem :: GROUP_6:43 for N being strict normal Subgroup of G holds Ker nat_hom N = N; definition let G,H,g; func Image g -> strict Subgroup of H means :: GROUP_6:def 10 the carrier of it = g .: (the carrier of G); end; theorem :: GROUP_6:44 rng g = the carrier of Image g; theorem :: GROUP_6:45 for x being object holds x in Image g iff ex a st x = g.a; theorem :: GROUP_6:46 Image g = gr rng g; theorem :: GROUP_6:47 Image 1:(G,H) = (1).H; theorem :: GROUP_6:48 for N being normal Subgroup of G holds Image nat_hom N = G./.N; theorem :: GROUP_6:49 h is Homomorphism of G,Image h; theorem :: GROUP_6:50 G is finite implies Image g is finite; registration let G be finite Group; let H be Group; let g be Homomorphism of G,H; cluster Image g -> finite; end; theorem :: GROUP_6:51 G is commutative Group implies Image g is commutative; theorem :: GROUP_6:52 card Image g c= card G; theorem :: GROUP_6:53 for G being finite Group, H being Group, g being Homomorphism of G,H holds card Image g <= card G; theorem :: GROUP_6:54 h is one-to-one & c in Image h implies h.(h".c) = c; theorem :: GROUP_6:55 h is one-to-one implies h" is Homomorphism of Image h,G; theorem :: GROUP_6:56 h is one-to-one iff Ker h = (1).G; theorem :: GROUP_6:57 for H being strict Group, h being Homomorphism of G,H holds h is onto iff Image h = H; theorem :: GROUP_6:58 for G,H being non empty set, h being Function of G,H st h is onto for c being Element of H ex a being Element of G st h.a = c; theorem :: GROUP_6:59 for N being normal Subgroup of G holds nat_hom N is onto; theorem :: GROUP_6:60 for G,H being set for h being Function of G,H holds h is bijective iff rng h = H & h is one-to-one; theorem :: GROUP_6:61 for G being set, H being non empty set for h being Function of G,H holds h is bijective implies dom h = G & rng h = H; theorem :: GROUP_6:62 for H being Group, h being Homomorphism of G,H st h is bijective holds h" is Homomorphism of H,G; theorem :: GROUP_6:63 for G being set, H being non empty set for h being Function of G,H holds for g1 being Function of H,G holds h is bijective & g1 = h" implies g1 is bijective; theorem :: GROUP_6:64 for G being set, H,I being non empty set for h being Function of G,H holds for h1 being Function of H,I holds h is bijective & h1 is bijective implies h1 * h is bijective; theorem :: GROUP_6:65 for G being Group holds nat_hom (1).G is bijective; definition let G,H; pred G,H are_isomorphic means :: GROUP_6:def 11 ex h st h is bijective; reflexivity; end; theorem :: GROUP_6:66 for G,H being Group holds G,H are_isomorphic implies H,G are_isomorphic; definition let G,H be Group; redefine pred G,H are_isomorphic; symmetry; end; theorem :: GROUP_6:67 G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic; theorem :: GROUP_6:68 h is one-to-one implies G,Image h are_isomorphic; theorem :: GROUP_6:69 for G,H being strict Group holds G is trivial & H is trivial implies G,H are_isomorphic; theorem :: GROUP_6:70 (1).G,(1).H are_isomorphic; theorem :: GROUP_6:71 for G being Group holds G,G./.(1).G are_isomorphic; theorem :: GROUP_6:72 for G being Group holds G./.(Omega).G is trivial; theorem :: GROUP_6:73 for G,H being strict Group holds G,H are_isomorphic implies card G = card H; theorem :: GROUP_6:74 G,H are_isomorphic & G is finite implies H is finite; theorem :: GROUP_6:75 for G,H being strict Group holds G,H are_isomorphic implies card G = card H; theorem :: GROUP_6:76 for G being strict trivial Group, H being strict Group holds G,H are_isomorphic implies H is trivial; theorem :: GROUP_6:77 for H being Group st G,H are_isomorphic & G is commutative holds H is commutative; theorem :: GROUP_6:78 G./.Ker g, Image g are_isomorphic; ::$N First isomorphism theorem for groups theorem :: GROUP_6:79 ex h being Homomorphism of G./.Ker g,Image g st h is bijective & g = h * nat_hom Ker g; ::$N Third isomorphism theorem for groups theorem :: GROUP_6:80 for M being strict normal Subgroup of G for J being strict normal Subgroup of G./.M st J = N./.(N,M)`*` & M is Subgroup of N holds (G./.M)./.J,G ./.N are_isomorphic; ::$N Second isomorphism theorem for groups theorem :: GROUP_6:81 for N being strict normal Subgroup of G holds (B "\/" N)./.(B "\/" N,N )`*`, B./.(B /\ N) are_isomorphic;