Wprowadzone zostały: homomorfizmy i izomorfizmy grup, grupa ilorazowa.
Udowodnione zostały także, tak zwane, twierdzenia o izomorfizmach za [1].
Bibliografia:
[1] M. I. Kargapołow, J. I. Mierzlakow: "Podstawy teorii grup", PWN 1989.
Identyfikator Mizar Mathematical Library: GROUP_6.
Artykuł napisany razem z Wojciechem Trybulcem.
Abstrakt w wersji PDF: tutaj.
Uniwersytet Warszawski, 1991.
Pliki:
:: Homomorphisms and Isomorphisms of Groups. Quotient Group
:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991 Association of Mizar Users
environ
vocabularies FUNCT_1, REALSET1, GROUP_2, GROUP_3, RLSUB_1, INT_1, BOOLE,
RELAT_1, GROUP_1, RCOMP_1, SUBSET_1, GROUP_4, GROUP_5, VECTSP_1,
NATTRA_1, FINSET_1, CARD_1, BINOP_1, QC_LANG1, ABSVALUE, WELLORD1,
LATTICES, GROUP_6, FUNCOP_1, COHSP_1, NAT_1, ENDALG;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, NUMBERS, XXREAL_0,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0,
CARD_1, FINSET_1, BINOP_1, REALSET2, INT_1, RLVECT_1, GROUP_1, GROUP_2,
GROUP_3, NAT_1, NAT_D, GROUP_4, GROUP_5, INT_2;
constructors RELAT_2, PARTFUN1, DOMAIN_1, BINOP_1, FUNCOP_1, FINSUB_1,
XXREAL_0, NAT_1, INT_2, REALSET2, GROUP_4, GROUP_5, NAT_D;
registrations FINSET_1, GROUP_1, GROUP_2, GROUP_3, STRUCT_0, RELSET_1, INT_1,
FUNCT_2, PARTFUN1, XBOOLE_0;
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 onetoone 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";
canceled;
theorem :: GROUP_6:6
a * A * A = a * A & a * (A * A) = a * A &
A * A * a = A * a & A * (A * a) = A *a;
theorem :: GROUP_6:7
for G being Group, A1 being Subset of G holds
A1 = {[.a,b.] where a is Element of G,
b is Element of G : not contradiction}
implies G` = gr A1;
theorem :: GROUP_6:8
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:9
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 HGrStr of M is Subgroup of B;
func (B,M)`*` > strict normal Subgroup of B equals
:: GROUP_6:def 1
the HGrStr of M;
end;
theorem :: GROUP_6:10
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 1sorted;
redefine attr G is trivial means
:: GROUP_6:def 2
ex x st the carrier of G = {x};
end;
registration
cluster trivial Group;
end;
theorem :: GROUP_6:11
(1).G is trivial;
theorem :: GROUP_6:12
G is trivial iff ord G = 1 & G is finite;
theorem :: GROUP_6:13
for G being strict Group holds
G is trivial implies (1).G = G;
definition let G,N;
func Cosets N > set equals
:: GROUP_6:def 3
Left_Cosets N;
end;
registration let G,N;
cluster Cosets N > non empty;
end;
canceled;
theorem :: GROUP_6:15
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:16
for N being normal Subgroup of G holds
a * N in Cosets N & N * a in Cosets N;
theorem :: GROUP_6:17
for N being normal Subgroup of G holds
x in Cosets N implies x is Subset of G;
theorem :: GROUP_6:18
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 4
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 > HGrStr equals
:: GROUP_6:def 5
HGrStr (# Cosets N, CosOp N #);
end;
registration let G; let N be normal Subgroup of G;
cluster G./.N > strict non empty;
end;
canceled 3;
theorem :: GROUP_6:22
for N being normal Subgroup of G holds
the carrier of G./.N = Cosets N;
theorem :: GROUP_6:23
for N being normal Subgroup of G holds
the mult 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 6
S;
end;
theorem :: GROUP_6:24
for N being normal Subgroup of G, T1,T2 being Element of G./.N
holds @T1 * @T2 = T1 * T2;
theorem :: GROUP_6:25
@(T1 * T2) = @T1 * @T2;
registration let G; let N be normal Subgroup of G;
cluster G./.N > associative Grouplike;
end;
theorem :: GROUP_6:26
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:27
N * a is Element of G./.N &
a * N is Element of G./.N &
carr N is Element of G./.N;
theorem :: GROUP_6:28
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:29
for N being normal Subgroup of G holds
1_(G./.N) = carr N;
theorem :: GROUP_6:30
for N being normal Subgroup of G, S being Element of G./.N
st S = a * N holds S" = a" * N;
canceled;
theorem :: GROUP_6:32
for N being normal Subgroup of G holds
Ord(G./.N) = Index N;
theorem :: GROUP_6:33
for N being normal Subgroup of G holds
Left_Cosets N is finite implies ord(G./.N) = index N;
theorem :: GROUP_6:34
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:35
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:36
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 HGrStr; let f be Function of G, H;
attr f is multiplicative means
:: GROUP_6:def 7
for a, b being Element of G holds f.(a * b) = f.a * f.b;
end;
registration let G, H;
cluster multiplicative 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 g1 for Homomorphism of H,G;
reserve h1 for Homomorphism of H,I;
canceled 3;
theorem :: GROUP_6:40
g.(1_G) = 1_H;
registration let G,H;
cluster > unitypreserving Homomorphism of G,H;
end;
theorem :: GROUP_6:41
g.(a") = (g.a)";
theorem :: GROUP_6:42
g.(a ^ b) = (g.a) ^ (g.b);
theorem :: GROUP_6:43
g. [.a,b.] = [.g.a,g.b.];
theorem :: GROUP_6:44
g. [.a1,a2,a3.] = [.g.a1,g.a2,g.a3.];
theorem :: GROUP_6:45
g.(a ^ n) = (g.a) ^ n;
theorem :: GROUP_6:46
g.(a ^ i) = (g.a) ^ i;
theorem :: GROUP_6:47
id the carrier of G is Homomorphism of G,G;
theorem :: GROUP_6:48
h1 * h is Homomorphism of G,I;
definition let G,H,I,h,h1;
redefine func h1 * h > Homomorphism of G,I;
end;
definition let G,H;
func 1:(G,H) > Homomorphism of G,H means
:: GROUP_6:def 8
for a holds it.a = 1_H;
end;
theorem :: GROUP_6:49
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 > Homomorphism of G,G./.N means
:: GROUP_6:def 9
for a holds it.a = a * N;
end;
definition let G,H,g;
func Ker g > strict Subgroup of G means
:: GROUP_6:def 10
the carrier of it = {a : g.a = 1_H};
end;
registration let G,H,g;
cluster Ker g > normal;
end;
theorem :: GROUP_6:50
a in Ker h iff h.a = 1_H;
theorem :: GROUP_6:51
for G,H being strict Group holds
Ker 1:(G,H) = G;
theorem :: GROUP_6:52
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 11
the carrier of it = g .: (the carrier of G);
end;
theorem :: GROUP_6:53
rng g = the carrier of Image g;
theorem :: GROUP_6:54
x in Image g iff ex a st x = g.a;
theorem :: GROUP_6:55
Image g = gr rng g;
theorem :: GROUP_6:56
Image 1:(G,H) = (1).H;
theorem :: GROUP_6:57
for N being normal Subgroup of G holds
Image nat_hom N = G./.N;
theorem :: GROUP_6:58
h is Homomorphism of G,Image h;
theorem :: GROUP_6:59
G is finite implies Image g is finite;
theorem :: GROUP_6:60
G is commutative Group implies Image g is commutative;
theorem :: GROUP_6:61
Ord Image g <=` Ord G;
theorem :: GROUP_6:62
G is finite implies ord Image g <= ord G;
definition let G,H,h;
attr h is being_monomorphism means
:: GROUP_6:def 12
h is onetoone;
attr h is being_epimorphism means
:: GROUP_6:def 13
rng h = the carrier of H;
end;
notation let G,H,h;
synonym h is_monomorphism for h is being_monomorphism;
synonym h is_epimorphism for h is being_epimorphism;
end;
theorem :: GROUP_6:63
h is_monomorphism & c in Image h implies h.(h".c) = c;
theorem :: GROUP_6:64
h is_monomorphism implies h".(h.a) = a;
theorem :: GROUP_6:65
h is_monomorphism implies h" is Homomorphism of Image h,G;
theorem :: GROUP_6:66
h is_monomorphism iff Ker h = (1).G;
theorem :: GROUP_6:67
for H being strict Group, h being Homomorphism of G,H holds
h is_epimorphism iff Image h = H;
theorem :: GROUP_6:68
for H being strict Group, h being Homomorphism of G,H st
h is_epimorphism holds
for c being Element of H ex a st h.a = c;
theorem :: GROUP_6:69
for N being normal Subgroup of G holds
nat_hom N is_epimorphism;
definition let G,H,h;
attr h is being_isomorphism means
:: GROUP_6:def 14
h is_epimorphism & h is_monomorphism;
end;
notation let G,H,h;
synonym h is_isomorphism for h is being_isomorphism;
end;
theorem :: GROUP_6:70
h is_isomorphism iff rng h = the carrier of H & h is onetoone;
theorem :: GROUP_6:71
h is_isomorphism implies dom h = the carrier of G &
rng h = the carrier of H;
theorem :: GROUP_6:72
for H being strict Group, h being Homomorphism of G,H st
h is_isomorphism holds h" is Homomorphism of H,G;
theorem :: GROUP_6:73
h is_isomorphism & g1 = h" implies g1 is_isomorphism;
theorem :: GROUP_6:74
h is_isomorphism & h1 is_isomorphism implies h1 * h is_isomorphism;
theorem :: GROUP_6:75
for G being Group holds
nat_hom (1).G is_isomorphism;
definition let G,H;
pred G,H are_isomorphic means
:: GROUP_6:def 15
ex h st h is_isomorphism;
reflexivity;
end;
canceled;
theorem :: GROUP_6:77
for G,H being strict Group holds
G,H are_isomorphic implies H,G are_isomorphic;
definition let G,H be strict Group;
redefine pred G,H are_isomorphic;
symmetry;
end;
theorem :: GROUP_6:78
G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic;
theorem :: GROUP_6:79
h is_monomorphism implies G,Image h are_isomorphic;
theorem :: GROUP_6:80
for G,H being strict Group holds
G is trivial & H is trivial implies G,H are_isomorphic;
theorem :: GROUP_6:81
(1).G,(1).H are_isomorphic;
theorem :: GROUP_6:82
for G being strict Group holds
G,G./.(1).G are_isomorphic;
theorem :: GROUP_6:83
for G being Group holds
G./.(Omega).G is trivial;
theorem :: GROUP_6:84
for G,H being strict Group holds
G,H are_isomorphic implies Ord G = Ord H;
theorem :: GROUP_6:85
G,H are_isomorphic & G is finite implies H is finite;
theorem :: GROUP_6:86
for G,H being strict Group holds
G,H are_isomorphic & G is finite implies ord G = ord H;
theorem :: GROUP_6:87
for G,H being strict Group holds
G,H are_isomorphic & G is trivial implies H is trivial;
canceled;
theorem :: GROUP_6:89
for H being strict Group st
G,H are_isomorphic & G is commutative Group holds H is commutative Group;
theorem :: GROUP_6:90
G./.Ker g, Image g are_isomorphic;
theorem :: GROUP_6:91
ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism &
g = h * nat_hom Ker g;
theorem :: GROUP_6:92
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;
theorem :: GROUP_6:93
for N being strict normal Subgroup of G holds
(B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic;
Góra
:: Homomorphisms and Isomorphisms of Groups. Quotient Group
:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991 Association of Mizar Users
environ
vocabularies FUNCT_1, REALSET1, GROUP_2, GROUP_3, RLSUB_1, INT_1, BOOLE,
RELAT_1, GROUP_1, RCOMP_1, SUBSET_1, GROUP_4, GROUP_5, VECTSP_1,
NATTRA_1, FINSET_1, CARD_1, BINOP_1, QC_LANG1, ABSVALUE, WELLORD1,
LATTICES, GROUP_6, FUNCOP_1, COHSP_1, NAT_1, ENDALG;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, NUMBERS, XXREAL_0,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0,
CARD_1, FINSET_1, BINOP_1, REALSET2, INT_1, RLVECT_1, GROUP_1, GROUP_2,
GROUP_3, NAT_1, NAT_D, GROUP_4, GROUP_5, INT_2;
constructors RELAT_2, PARTFUN1, DOMAIN_1, BINOP_1, FUNCOP_1, FINSUB_1,
XXREAL_0, NAT_1, INT_2, REALSET2, GROUP_4, GROUP_5, NAT_D;
registrations FINSET_1, GROUP_1, GROUP_2, GROUP_3, STRUCT_0, RELSET_1, INT_1,
FUNCT_2, PARTFUN1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions XBOOLE_0, FUNCT_1, GROUP_1, GROUP_2, TARSKI, BINOP_1, REALSET1,
SUBSET_1, GROUP_4;
theorems BINOP_1, CARD_1, CARD_2, FINSET_1, FUNCT_1, FUNCT_2, GROUP_1,
GROUP_2, GROUP_3, GROUP_4, GROUP_5, TARSKI, ZFMISC_1, RLVECT_1, REALSET2,
RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1;
schemes BINOP_1, FUNCT_1, FUNCT_2, DOMAIN_1, NAT_1;
begin
theorem Th1:
for A,B being non empty set, f being Function of A,B holds
f is onetoone iff
for a,b being Element of A st f.a = f.b holds a = b
proof
let A,B be non empty set;
let f be Function of A,B;
thus f is onetoone implies
for a,b being Element of A st f.a = f.b holds a = b by FUNCT_2:25;
assume for a,b being Element of A st f.a = f.b holds a = b;
then for a,b being set st a in A & b in A & f.a = f.b holds a = b;
hence thesis by FUNCT_2:25;
end;
definition let G be Group, A be Subgroup of G;
redefine mode Subgroup of A > Subgroup of G;
coherence by GROUP_2:65;
end;
registration let G be Group;
cluster (1).G > normal;
coherence by GROUP_3:137;
cluster (Omega).G > normal;
coherence by GROUP_3:137;
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 Th2:
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
proof let X be Subgroup of A, x be Element of A;
assume A1: x = a;
set I = X qua Subgroup of G;
thus x * X c= a * I
proof let y;
assume y in x * X;
then consider g being Element of A such that
A2: y = x * g & g in X by GROUP_2:125;
reconsider h = g as Element of G by GROUP_2:51;
a * h = x * g by A1,GROUP_2:52;
hence thesis by A2,GROUP_2:125;
end;
thus a * I c= x * X
proof let y;
assume y in a * I;
then consider b such that A3: y = a * b & b in X by GROUP_2:125;
reconsider c = b as Element of X by A3,RLVECT_1:def 1;
reconsider c as Element of A by GROUP_2:51;
a * b = x * c by A1,GROUP_2:52;
hence thesis by A3,GROUP_2:125;
end;
thus X * x c= I * a
proof let y;
assume y in X * x;
then consider g being Element of A such that
A4: y = g * x & g in X by GROUP_2:126;
reconsider h = g as Element of G by GROUP_2:51;
h * a = g * x by A1,GROUP_2:52;
hence thesis by A4,GROUP_2:126;
end;
thus I * a c= X * x
proof let y;
assume y in I * a;
then consider b such that A5: y = b * a & b in X by GROUP_2:126;
reconsider c = b as Element of X by A5,RLVECT_1:def 1;
reconsider c as Element of A by GROUP_2:51;
b * a = c * x by A1,GROUP_2:52;
hence thesis by A5,GROUP_2:126;
end;
end;
theorem
for X,Y being Subgroup of A holds
(X qua Subgroup of G) /\ (Y qua Subgroup of G) = X /\ Y
proof let X,Y be Subgroup of A;
A1: the carrier of X /\ Y = (carr X) /\ (carr Y) &
the carrier of (X qua Subgroup of G) /\ (Y qua Subgroup of G) =
(carr (X qua Subgroup of G)) /\ (carr (Y qua Subgroup of G)) &
carr X = the carrier of X & the carrier of Y = carr Y &
carr (X qua Subgroup of G) = the carrier of X &
the carrier of Y = carr (Y qua Subgroup of G) by GROUP_2:def 10;
reconsider Z = X /\ Y as Subgroup of G by GROUP_2:65;
(X qua Subgroup of G) /\ (Y qua Subgroup of G) = Z by A1,GROUP_2:97;
hence thesis;
end;
theorem Th4:
a * b * a" = b ^ a" & a * (b * a") = b ^ a"
proof
thus a * b * a" = a"" * b * a" by GROUP_1:19
.= b ^ a" by GROUP_3:def 2;
hence thesis by GROUP_1:def 4;
end;
canceled;
theorem Th6:
a * A * A = a * A & a * (A * A) = a * A &
A * A * a = A * a & A * (A * a) = A *a
proof
thus a * A * A = a * (A * A) by GROUP_4:60
.= a * A by GROUP_2:91;
hence a * (A * A) = a * A by GROUP_4:60;
thus A * A * a = A * a by GROUP_2:91;
hence thesis by GROUP_4:61;
end;
theorem Th7:
for G being Group, A1 being Subset of G holds
A1 = {[.a,b.] where a is Element of G,
b is Element of G : not contradiction}
implies G` = gr A1
proof let G be Group, A1 be Subset of G;
assume A1: A1 =
{[.a,b.] where a is Element of G,
b is Element of G : not contradiction};
A1 = commutators G
proof
thus A1 c= commutators G
proof let x;
assume x in A1;
then ex a,b being Element of G st x = [.a,b.] by A1;
hence thesis by GROUP_5:65;
end;
let x;
assume x in commutators G;
then ex a,b being Element of G st x = [.a,b.] by GROUP_5:65;
hence thesis by A1;
end;
hence thesis by GROUP_5:82;
end;
theorem Th8:
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
proof let G be strict Group, B be strict Subgroup of G;
thus G` is Subgroup of B implies
for a,b being Element of G holds [.a,b.] in B
proof assume A1: G` is Subgroup of B;
let a,b be Element of G;
[.a,b.] in G` by GROUP_5:84;
hence thesis by A1,GROUP_2:49;
end;
assume A2: for a,b being Element of G holds [.a,b.] in B;
defpred P[set,set] means not contradiction;
deffunc F(Element of G,Element of G) = [.$1,$2.];
reconsider X =
{F(a,b) where a is Element of G, b is Element of G : P[a,b]}
as Subset of G from DOMAIN_1:sch 9;
X c= the carrier of B
proof let x;
assume x in X;
then ex a,b being Element of G st x = [.a,b.];
then x in B by A2;
hence thesis by RLVECT_1:def 1;
end;
then gr X is Subgroup of B by GROUP_4:def 5;
hence thesis by Th7;
end;
theorem Th9:
for N being normal Subgroup of G holds
N is Subgroup of B implies N is normal Subgroup of B
proof let N be normal Subgroup of G;
assume N is Subgroup of B;
then reconsider N' = N as Subgroup of B;
now let n be Element of B;
thus n * N' c= N' * n
proof let x;
assume x in n * N';
then consider a being Element of B such that
A1: x = n * a and A2: a in N' by GROUP_2:125;
reconsider a' = a, n' = n as Element of G
by GROUP_2:51;
x = n' * a' by A1,GROUP_2:52;
then x in n' * N & n' * N c= N * n' by A2,GROUP_2:125,GROUP_3:141;
then consider a1 such that A3: x = a1 * n' and A4: a1 in N
by GROUP_2:126;
a1 in N' by A4;
then a1 in B by GROUP_2:49;
then reconsider a1' = a1 as Element of B by RLVECT_1:def 1;
x = a1' * n by A3,GROUP_2:52;
hence thesis by A4,GROUP_2:126;
end;
end;
hence thesis by GROUP_3:141;
end;
definition let G,B; let M be normal Subgroup of G;
assume A1: the HGrStr of M is Subgroup of B;
func (B,M)`*` > strict normal Subgroup of B equals
:Def1: the HGrStr of M;
coherence
proof
reconsider x = the HGrStr of M as Subgroup of G by A1;
now let a;
thus a * x = a * M
.= M * a by GROUP_3:140
.= x * a;
end;
then x is normal Subgroup of G by GROUP_3:140;
hence thesis by A1,Th9;
end;
correctness;
end;
theorem Th10:
B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B
proof
thus
B /\ N is normal Subgroup of B
proof reconsider A = B /\ N as Subgroup of B by GROUP_2:106;
now let b be Element of B;
thus b * A c= A * b
proof let x;
assume x in b * A;
then consider a being Element of B such that
A1: x = b * a and
A2: a in A by GROUP_2:125;
A3: a in N by A2,GROUP_2:99;
reconsider a' = a, b' = b as Element of G by GROUP_2:51;
x = b' * a' by A1,GROUP_2:52;
then x in b' * N & b' * N c= N * b' by A3,GROUP_2:125,GROUP_3:141;
then consider b1 such that A4: x = b1 * b' and A5: b1 in N
by GROUP_2:126;
reconsider x' = x as Element of B by A1;
reconsider x'' = x as Element of G by A4;
b1 = x'' * b'" & b'" = b" by A4,GROUP_1:22,GROUP_2:57;
then A6:b1 = x' * b" by GROUP_2:52;
then A7: b1 in B by RLVECT_1:def 1;
reconsider b1' = b1 as Element of B by A6;
b1' * b = x & b1' in A by A4,A5,A7,GROUP_2:52,99;
hence thesis by GROUP_2:126;
end;
end;
hence thesis by GROUP_3:141;
end;
hence thesis;
end;
definition let G,B; let N be normal Subgroup of G;
redefine func B /\ N > strict normal Subgroup of B;
coherence by Th10;
end;
definition let G; let N be normal Subgroup of G; let B;
redefine func N /\ B > strict normal Subgroup of B;
coherence by Th10;
end;
definition let G be non empty 1sorted;
redefine attr G is trivial means :Def2:
ex x st the carrier of G = {x};
compatibility
proof
hereby assume A1: G is trivial;
consider y being Element of G;
for x holds x in the carrier of G iff x = y by A1,REALSET2:def 7;
then the carrier of G = {y} by TARSKI:def 1;
hence ex x st the carrier of G = {x};
end;
given x such that
A2: the carrier of G = {x};
now let a,b be Element of G;
thus a = x by A2,TARSKI:def 1 .= b by A2,TARSKI:def 1;
end;
hence thesis by REALSET2:def 7;
end;
end;
registration
cluster trivial Group;
existence
proof consider G;
take (1).G;
the carrier of (1).G = {1_G} by GROUP_2:def 7;
hence thesis by Def2;
end;
end;
theorem Th11:
(1).G is trivial
proof
the carrier of (1).G = {1_G} by GROUP_2:def 7;
hence thesis by Def2;
end;
theorem Th12:
G is trivial iff ord G = 1 & G is finite
proof
thus G is trivial implies ord G = 1 & G is finite
proof
given x such that A1: the carrier of G = {x};
G is finite by A1,GROUP_1:def 14;
then ex B being finite set st B = the carrier of G & ord G = card B
by GROUP_1:def 15;
hence thesis by A1,CARD_1:79,GROUP_1:def 14;
end;
assume
A2: ord G = 1 & G is finite;
then consider c being finite set such that
A3: c = the carrier of G & ord G = card c by GROUP_1:def 15;
thus ex x st the carrier of G = {x} by A2,A3,CARD_2:60;
end;
theorem Th13:
for G being strict Group holds
G is trivial implies (1).G = G
proof let G be strict Group;
assume G is trivial;
then A1: ord G = 1 & G is finite by Th12;
then ord G = ord (1).G by GROUP_2:81;
hence G = (1).G by A1,GROUP_2:85;
end;
definition let G,N;
func Cosets N > set equals
Left_Cosets N;
coherence;
end;
registration let G,N;
cluster Cosets N > non empty;
coherence by GROUP_2:165;
end;
Lm1:
for N being normal Subgroup of G holds
Cosets N = Left_Cosets N & Cosets N = Right_Cosets N by GROUP_3:150;
canceled;
theorem Th15:
for N being normal Subgroup of G holds
x in Cosets N implies ex a st x = a * N & x = N * a
proof let N be normal Subgroup of G;
assume x in Cosets N;
then x in Left_Cosets N;
then consider a such that A1: x = a * N by GROUP_2:def 15;
x = N * a by A1,GROUP_3:140;
hence thesis by A1;
end;
theorem Th16:
for N being normal Subgroup of G holds
a * N in Cosets N & N * a in Cosets N
proof let N be normal Subgroup of G;
A1: a * N in Left_Cosets N by GROUP_2:def 15;
N * a in Right_Cosets N by GROUP_2:def 16;
hence thesis by A1,Lm1;
end;
theorem Th17:
for N being normal Subgroup of G holds
x in Cosets N implies x is Subset of G;
theorem Th18:
for N being normal Subgroup of G holds
A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N
proof let N be normal Subgroup of G;
assume A1: A1 in Cosets N & A2 in Cosets N;
then consider a such that A2: A1 = a * N & A1 = N * a by Th15;
consider b such that A3: A2 = b * N & A2 = N * b by A1,Th15;
A1 * A2 = a * (N * (b * N)) by A2,A3,GROUP_3:11
.= a * (b * N * N) by A3,GROUP_3:15
.= a * (b * (N * N)) by GROUP_4:60
.= a * (b * N) by GROUP_2:91
.= a * b * N by GROUP_2:127;
then A1 * A2 in Left_Cosets N by GROUP_2:def 15;
hence thesis;
end;
definition let G; let N be normal Subgroup of G;
func CosOp N > BinOp of Cosets N means
:Def4: for W1,W2 being Element of Cosets N
for A1,A2 st W1 = A1 & W2 = A2 holds it.(W1,W2) = A1 * A2;
existence
proof
defpred P[Element of Cosets N,Element of Cosets N,set] means
for A1,A2 st $1 = A1 & $2 = A2 holds $3 = A1 * A2;
A1: for W1,W2 being Element of Cosets N
ex V being Element of Cosets N st P[W1,W2,V]
proof let W1,W2 be Element of Cosets N;
reconsider A1 = W1, A2 = W2 as Subset of G by Th17;
reconsider C = A1 * A2 as Element of Cosets N by Th18;
take C;
thus thesis;
end;
thus ex B being BinOp of Cosets N st
for W1,W2 being Element of Cosets N holds
P[W1,W2,B.(W1,W2)] from BINOP_1:sch 3(A1);
end;
uniqueness
proof let o1,o2 be BinOp of Cosets N;
assume A2: for W1,W2 being Element of Cosets N
for A1,A2 st W1 = A1 & W2 = A2 holds o1.(W1,W2) = A1 * A2;
assume A3: for W1,W2 being Element of Cosets N
for A1,A2 st W1 = A1 & W2 = A2 holds o2.(W1,W2) = A1 * A2;
now let x,y be set;
assume A4: x in Cosets N & y in Cosets N;
then reconsider W = x, V = y as Element of Cosets N;
reconsider A1 = x, A2 = y as Subset of G by A4;
o1.(W,V) = A1 * A2 & o2.(W,V) = A1 * A2 by A2,A3;
then o1.(x,y) = o2.(x,y) & o1. [x,y] = o1.(x,y) & o2. [x,y] = o2.(x,y);
hence o1.(x,y) = o2.(x,y);
end;
hence thesis by BINOP_1:1;
end;
end;
definition let G; let N be normal Subgroup of G;
func G./.N > HGrStr equals
HGrStr (# Cosets N, CosOp N #);
correctness;
end;
registration let G; let N be normal Subgroup of G;
cluster G./.N > strict non empty;
coherence;
end;
canceled 3;
theorem
for N being normal Subgroup of G holds
the carrier of G./.N = Cosets N;
theorem
for N being normal Subgroup of G holds
the mult 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 S;
coherence by Th17;
end;
theorem Th24:
for N being normal Subgroup of G, T1,T2 being Element of G./.N
holds @T1 * @T2 = T1 * T2 by Def4;
theorem Th25:
@(T1 * T2) = @T1 * @T2 by Th24;
registration let G; let N be normal Subgroup of G;
cluster G./.N > associative Grouplike;
coherence
proof
G./.N is associative Grouplike
proof
thus for f,g,h being Element of G./.N
holds f * (g * h) = f * g * h
proof let f,g,h be Element of G./.N;
consider a such that A1: f = a * N & f = N * a by Th15;
consider c being Element of G such that
A2: h = c * N & h = N * c by Th15;
thus f * (g * h) = @f * @(g * h) by Th24
.= (a * N) * (@g * @h) by A1,Th25
.= @f * @g * (c * N) by A1,A2,GROUP_2:14
.= @(f * g) * @h by A2,Th25
.= f * g * h by Th24;
end;
carr N in Left_Cosets N & Cosets N = Left_Cosets N
by GROUP_2:165;
then reconsider e = carr N as Element of G./.N;
take e;
let h be Element of G./.N;
consider a such that A3: h = a * N & h = N * a by Th15;
A4: @h = h & @e = e;
thus h * e = @h * @e by Th24
.= (a * N) * N by A3
.= a * (N * N) by GROUP_4:60
.= h by GROUP_2:91,A3;
thus e * h = @e * @h by Th24
.= N * (N * a) by A3
.= N * N * a by GROUP_4:61
.= h by GROUP_2:91,A3;
reconsider g = a" * N as Element of G./.N by GROUP_2:def 15;
A5: @g = g;
take g;
thus h * g = N * a * (a" * N) by A3,A4,A5,Th24
.= N * a * a" * N by GROUP_3:10
.= N * (a * a") * N by GROUP_2:129
.= N * 1_G * N by GROUP_1:def 6
.= carr N * carr N by GROUP_2:132
.= e by GROUP_2:91;
thus g * h = @g * @h by Th24
.= a" * N * a * N by A3,GROUP_3:10
.= a" * (N * a) * N by GROUP_2:128
.= a" * (a * N) * N by GROUP_3:140
.= a" * a * N * N by GROUP_2:127
.= 1_G * N * N by GROUP_1:def 6
.= 1_G * (N * N) by GROUP_4:60
.= 1_G * carr N by GROUP_2:91
.= e by GROUP_2:43;
end;
hence thesis;
end;
end;
theorem Th26:
for N being normal Subgroup of G, S being Element of G./.N
ex a st S = a * N & S = N * a by Th15;
theorem Th27:
N * a is Element of G./.N &
a * N is Element of G./.N &
carr N is Element of G./.N by Th16,GROUP_2:165;
theorem Th28:
for N being normal Subgroup of G holds
x in G./.N iff ex a st x = a * N & x = N * a
proof let N be normal Subgroup of G;
thus x in G./.N implies ex a st x = a * N & x = N * a
proof assume x in G./.N;
then x is Element of G./.N by RLVECT_1:def 1;
hence thesis by Th26;
end;
given a such that A1: x = a * N & x = N * a;
x is Element of G./.N by A1,Th27;
hence thesis by RLVECT_1:def 1;
end;
theorem Th29:
for N being normal Subgroup of G holds
1_(G./.N) = carr N
proof let N be normal Subgroup of G;
reconsider e = carr N as Element of G./.N by Th27;
now let h be Element of G./.N;
consider a such that A1: h = a * N & h = N * a by Th15;
thus h * e = @h * @e by Th24
.= (a * N) * N by A1
.= a * (N * N) by GROUP_4:60
.= h by GROUP_2:91,A1;
thus e * h = @e * @h by Th24
.= N * (N * a) by A1
.= N * N * a by GROUP_4:61
.= h by GROUP_2:91,A1;
end;
hence thesis by GROUP_1:10;
end;
theorem Th30:
for N being normal Subgroup of G, S being Element of G./.N
st S = a * N holds S" = a" * N
proof let N be normal Subgroup of G, S be Element of G./.N;
assume A1: S = a * N;
reconsider g = a" * N as Element of G./.N by Th27;
A2: S * g = @S * @g by Th24
.= N * a * (a" * N) by A1,GROUP_3:140
.= N * a * a" * N by GROUP_3:10
.= N * (a * a") * N by GROUP_2:129
.= N * 1_G * N by GROUP_1:def 6
.= carr N * carr N by GROUP_2:132
.= carr N by GROUP_2:91;
A3: g * S = @g * @S by Th24
.= a" * N * a * N by A1,GROUP_3:10
.= a" * (N * a) * N by GROUP_2:128
.= a" * (a * N) * N by GROUP_3:140
.= a" * a * N * N by GROUP_2:127
.= 1_G * N * N by GROUP_1:def 6
.= 1_G * (N * N) by GROUP_4:60
.= 1_G * carr N by GROUP_2:91
.= carr N by GROUP_2:43;
1_(G./.N) = carr N by Th29;
hence thesis by A2,A3,GROUP_1:def 6;
end;
Lm2:
for N being normal Subgroup of G holds
Left_Cosets N is finite implies G./.N is finite by GROUP_1:def 14;
canceled;
theorem
for N being normal Subgroup of G holds
Ord(G./.N) = Index N;
theorem
for N being normal Subgroup of G holds
Left_Cosets N is finite implies ord(G./.N) = index N
proof let N be normal Subgroup of G;
assume A1: Left_Cosets N is finite;
then reconsider LC = Left_Cosets N as finite set;
A2: G./.N is finite by A1,Lm2;
then reconsider GN = the carrier of G./.N as finite set by GROUP_1:def 14;
thus ord(G./.N) = card LC by A2,GROUP_1:def 15
.= index N by GROUP_2:def 18;
end;
theorem Th34:
for M being strict normal Subgroup of G holds
M is Subgroup of B implies B./.(B,M)`*` is Subgroup of G./.M
proof let M be strict normal Subgroup of G;
assume A1: M is Subgroup of B;
set I = B./.(B,M)`*`; set J = (B,M)`*`;
A2: the carrier of I c= the carrier of G./.M
proof let x;
assume A3: x in the carrier of I;
consider a being Element of B such that
A4: x = a * J & x = J * a by A3,Th15;
reconsider b = a as Element of G by GROUP_2:51;
J = M by A1,Def1;
then a * J = b * M & J * a = M * b by Th2;
then x in Cosets M & the carrier of G./.M = Cosets M by A4,Th16;
hence thesis;
end;
set g = the mult of I;
set f = the mult of G./.M;
set X = [: the carrier of I,the carrier of I :];
dom g = X & dom f = [: the carrier of G./.M,the carrier of G./.M :] &
X c= [: the carrier of G./.M,the carrier of G./.M :]
by A2,FUNCT_2:def 1,ZFMISC_1:119;
then A5: dom g = dom f /\ X by XBOOLE_1:28;
now let x;
assume A6: x in dom g;
then consider y,z such that A7: [y,z] = x by ZFMISC_1:102;
A8: y in the carrier of I & z in
the carrier of I by A6,A7,ZFMISC_1:106;
consider a being Element of B such that
A9: y = a * J & y = J * a by A8,Th15;
consider b being Element of B such that
A10: z = b * J & z = J * b by A8,Th15;
reconsider W1 = y, W2 = z as Element of Cosets J by A9,A10,Th16;
A11: g.x = g.(W1,W2) by A7
.= (a * J) * (J * b) by A9,A10,Def4
.= a * J * J * b by GROUP_3:12
.= a * (J * J) * b by GROUP_4:60
.= a * J * b by GROUP_2:91
.= a * (J * b) by GROUP_2:128
.= a * (b * J) by GROUP_3:140
.= a * b * J by GROUP_2:127;
reconsider a' = a, b' = b as Element of G
by GROUP_2:51;
A12: J = M by A1,Def1;
then A13: y = a' * M & y = M * a' & z = b' * M & z = M * b' by A9
,A10,Th2;
then reconsider V1 = y, V2 = z as Element of Cosets M by Th16;
A14: f.x = f.(V1,V2) by A7
.= (a' * M) * (M * b') by A13,Def4
.= a' * M * M * b' by GROUP_3:12
.= a' * (M * M) * b' by GROUP_4:60
.= a' * M * b' by GROUP_2:91
.= a' * (M * b') by GROUP_2:128
.= a' * (b' * M) by GROUP_3:140
.= a' * b' * M by GROUP_2:127;
a' * b' = a * b by GROUP_2:52;
hence g.x = f.x by A11,A12,A14,Th2;
end;
then g = fthe carrier of I by A5,FUNCT_1:68;
hence B./.(B,M)`*` is Subgroup of G./.M by A2,GROUP_2:def 5;
end;
theorem
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
proof let N,M be strict normal Subgroup of G;
assume A1: M is Subgroup of N;
then A2: (N,M)`*` = M by Def1;
reconsider J = N./.(N,M)`*` as Subgroup of G./.M by A1,Th34;
reconsider I = M as normal Subgroup of N by A2;
now let S be Element of G./.M;
thus S * J c= J * S
proof let x;
assume x in S * J;
then consider T being Element of G./.M such that
A3: x = S * T and A4: T in J by GROUP_2:125;
consider a such that A5: S = a * M & S = M * a by Th26;
consider c being Element of N such that
A6: T = c * I & T = I * c by A2,A4,Th28;
reconsider d = c as Element of G by GROUP_2:51;
set e = a * (d * a");
A7: c in N by RLVECT_1:def 1;
e = d ^ a" by Th4;
then e in N by A7,GROUP_5:3;
then reconsider f = e as Element of N
by RLVECT_1:def 1;
reconsider V = I * f as Element of J by A2,Th27;
A8: V in J by RLVECT_1:def 1;
reconsider V as Element of G./.M by GROUP_2:51;
A9: @S = S & @T = T & c * I = d * M & M * d = I * c & M * e = I * f &
@V = V by Th2;
then x = M * a * (M * d) by A3,A5,A6,Th24
.= M * a * (M * d * 1_G) by GROUP_2:43
.= M * a * (M * d * (a" * a)) by GROUP_1:def 6
.= M * a * (M * (d * (a" * a))) by GROUP_2:129
.= M * a * M * (d * (a" * a)) by GROUP_3:12
.= M * (a * M) * (d * (a" * a)) by GROUP_3:15
.= M * (M * a) * (d * (a" * a)) by GROUP_3:140
.= M * ((M * a) * (d * (a" * a))) by GROUP_2:118
.= M * (M * (a * (d * (a" * a)))) by GROUP_2:129
.= M * (M * (a * (d * a" * a))) by GROUP_1:def 4
.= M * (M * (a * (d * a") * a)) by GROUP_1:def 4
.= M * (M * e * a) by GROUP_2:129
.= M * (e * M * a) by GROUP_3:140
.= M * (e * (M * a)) by GROUP_2:128
.= M * e * (M * a) by GROUP_3:13
.= V * S by A5,A9,Th24;
hence x in J * S by A8,GROUP_2:126;
end;
end;
hence thesis by GROUP_3:141;
end;
theorem
for G being strict Group, N be strict normal Subgroup of G holds
G./.N is commutative Group iff G` is Subgroup of N
proof let G be strict Group, N be strict normal Subgroup of G;
thus G./.N is commutative Group implies G` is Subgroup of N
proof assume A1: G./.N is commutative Group;
now let a,b be Element of G;
reconsider S = a * N,T = b * N as Element of G./.N
by Th27;
S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by Th30;
then A2: S" * T" = (a" * N) * (b" * N) by Th24;
S = @S & T = @T;
then A3: S * T = (a * N) * (b * N) by Th24;
A4: @(S" * T") = (S" * T") & @(S * T) = (S * T);
[.S,T.] = (S" * T") * (S * T) by GROUP_5:19;
then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) &
[.S,T.] = 1_(G./.N) & 1_(G./.N) = carr N by A1,A2,A3,A4,Th24,Th29
,GROUP_5:40;
then carr N = (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:11
.= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:15
.= (a" * N) * (b" * N) * (a * (b * N * N)) by GROUP_3:140
.= (a" * N) * (b" * N) * (a * (b * N)) by Th6
.= (a" * N) * (b" * N) * (a * b * N) by GROUP_2:127
.= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:11
.= a" * (N * b" * N) * (a * b * N) by GROUP_3:15
.= a" * (b" * N * N) * (a * b * N) by GROUP_3:140
.= a" * (b" * N) * (a * b * N) by Th6
.= (a" * b" * N) * (a * b * N) by GROUP_2:127
.= (a" * b") * (N * (a * b * N)) by GROUP_3:11
.= (a" * b") * (N * (a * b) * N) by GROUP_3:15
.= (a" * b") * ((a * b) * N * N) by GROUP_3:140
.= (a" * b") * ((a * b) * N) by Th6
.= (a" * b") * (a * b) * N by GROUP_2:127
.= [.a,b.] * N by GROUP_5:19;
hence [.a,b.] in N by GROUP_2:136;
end;
hence thesis by Th8;
end;
assume A5: G` is Subgroup of N;
now let S,T be Element of G./.N;
consider a being Element of G such that
A6: S = a * N & S = N * a by Th26;
consider b being Element of G such that
A7: T = b * N & T = N * b by Th26;
[.a,b.] in N by A5,Th8;
then A8: carr N = [.a,b.] * N by GROUP_2:136
.= (a" * b") * (a * b) * N by GROUP_5:19
.= (a" * b") * ((a * b) * N) by GROUP_2:127
.= (a" * b") * ((a * b) * N * N) by Th6
.= (a" * b") * (N * (a * b) * N) by GROUP_3:140
.= (a" * b") * (N * (a * b * N)) by GROUP_3:15
.= (a" * b" * N) * (a * b * N) by GROUP_3:11
.= a" * (b" * N) * (a * b * N) by GROUP_2:127
.= a" * (b" * N * N) * (a * b * N) by Th6
.= a" * (N * b" * N) * (a * b * N) by GROUP_3:140
.= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:15
.= (a" * N) * (b" * N) * (a * b * N) by GROUP_3:11
.= (a" * N) * (b" * N) * (a * (b * N)) by GROUP_2:127
.= (a" * N) * (b" * N) * (a * (b * N * N)) by Th6
.= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:140
.= (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:15
.= (a" * N) * (b" * N) * (a * N * (b * N)) by GROUP_3:11;
S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by A6,A7,
Th30;
then A9: S" * T" = (a" * N) * (b" * N) by Th24;
S = @S & T = @T;
then A10: S * T = (a * N) * (b * N) by A6,A7,Th24;
A11: @(S" * T") = (S" * T") & @(S * T) = (S * T);
[.S,T.] = (S" * T") * (S * T) by GROUP_5:19;
then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) &
1_(G./.N) = carr N by A9,A10,A11,Th24,Th29;
hence [.S,T.] = 1_(G./.N) by A8;
end;
hence thesis by GROUP_5:40;
end;
Lm3: (for a holds f.a = 1_H) implies f.(a * b) = f.a * f.b
proof
assume A1: for a holds f.a = 1_H;
hence f.(a * b) = 1_H
.= 1_H * 1_H by GROUP_1:def 5
.= f.a * 1_H by A1
.= f.a * f.b by A1;
end;
definition let G, H be non empty HGrStr; let f be Function of G, H;
attr f is multiplicative means :Def7:
for a, b being Element of G holds f.(a * b) = f.a * f.b;
end;
registration let G, H;
cluster multiplicative Function of G, H;
existence
proof
reconsider f = (the carrier of G) > 1_H as Function of G, H
by FUNCOP_1:57;
A1:for a holds f.a = 1_H by FUNCOP_1:13;
take f;
for a, b holds f.(a * b) = f.a * f.b by A1,Lm3;
hence thesis by Def7;
end;
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 g1 for Homomorphism of H,G;
reserve h1 for Homomorphism of H,I;
canceled 3;
theorem Th40:
g.(1_G) = 1_H
proof g.(1_G) = g.(1_G * 1_G) by GROUP_1:def 5
.= g.(1_G) * g.(1_G) by Def7;
hence thesis by GROUP_1:15;
end;
registration let G,H;
cluster > unitypreserving Homomorphism of G,H;
coherence
proof
let g be Homomorphism of G,H;
thus g.1_G = 1_H by Th40;
end;
end;
theorem Th41:
g.(a") = (g.a)"
proof g.(a") * g.a = g.(a" * a) by Def7
.= g.(1_G) by GROUP_1:def 6
.= 1_H by Th40;
hence thesis by GROUP_1:20;
end;
theorem Th42:
g.(a ^ b) = (g.a) ^ (g.b)
proof
thus g.(a ^ b) = g.(b" * a * b) by GROUP_3:def 2
.= g.(b" * a) * g.b by Def7
.= g.(b") * g.a * g.b by Def7
.= (g.b)" * g.a * g.b by Th41
.= (g.a) ^ (g.b) by GROUP_3:def 2;
end;
theorem Th43:
g. [.a,b.] = [.g.a,g.b.]
proof
thus g. [.a,b.] = g.(a" * b" * a * b) by GROUP_5:19
.= g.(a" * b" * a) * g.b by Def7
.= g.(a" * b") * g.a * g.b by Def7
.= g.(a") * g.(b") * g.a * g.b by Def7
.= (g.a)" * g.(b") * g.a * g.b by Th41
.= (g.a)" * (g.b)" * g.a * g.b by Th41
.= [.g.a,g.b.] by GROUP_5:19;
end;
theorem
g. [.a1,a2,a3.] = [.g.a1,g.a2,g.a3.]
proof
thus g. [.a1,a2,a3.] = g. [.[.a1,a2.],a3.] by GROUP_5:def 3
.= [.g. [.a1,a2.],g.a3.] by Th43
.= [.[.g.a1,g.a2.],g.a3.] by Th43
.= [.g.a1,g.a2,g.a3.] by GROUP_5:def 3;
end;
theorem Th45:
g.(a ^ n) = (g.a) ^ n
proof
defpred Q[Element of NAT] means g.(a ^ $1) = (g.a) ^ $1;
A1: Q[0]
proof
thus g.(a ^ 0) = g.(1_G) by GROUP_1:43
.= 1_H by Th40
.= (g.a) ^ 0 by GROUP_1:43;
end;
A2: for n st Q[n] holds Q[n + 1]
proof
let n;
assume A3: Q[n];
thus g.(a ^ (n + 1)) = g.(a ^ n * a) by GROUP_1:49
.= (g.a) ^ n * g.a by A3,Def7
.= (g.a) ^ (n + 1) by GROUP_1:49;
end;
for n holds Q[n] from NAT_1:sch 1(A1,A2);
hence thesis;
end;
theorem
g.(a ^ i) = (g.a) ^ i
proof
per cases;
suppose A1: i >= 0;
hence g.(a ^ i) = g.(a ^ abs( i )) by GROUP_1:55
.= (g.a) ^ abs( i ) by Th45
.= (g.a) ^ i by A1,GROUP_1:55;
end;
suppose A2: i < 0;
hence g.(a ^ i) = g.(a ^ abs( i ))" by GROUP_1:56
.= (g.(a ^ abs( i )))" by Th41
.= ((g.a) ^ abs( i ))" by Th45
.= (g.a) ^ i by A2,GROUP_1:56;
end;
end;
theorem Th47:
id the carrier of G is Homomorphism of G,G
proof
reconsider f = id the carrier of G as Function of G, G;
now let a,b;
thus f.(a * b) = a * b by FUNCT_1:35
.= f.a * b by FUNCT_1:35
.= f.a * f.b by FUNCT_1:35;
end;
hence thesis by Def7;
end;
theorem Th48:
h1 * h is Homomorphism of G,I
proof
reconsider f = h1 * h as Function of G, I;
now
let a,b;
thus f.(a * b) = h1.(h.(a * b)) by FUNCT_2:21
.= h1.(h.a * h.b) by Def7
.= (h1.(h.a)) * (h1.(h.b)) by Def7
.= f.a * (h1.(h.b)) by FUNCT_2:21
.= f.a * f.b by FUNCT_2:21;
end;
hence thesis by Def7;
end;
definition let G,H,I,h,h1;
redefine func h1 * h > Homomorphism of G,I;
coherence by Th48;
end;
definition let G,H;
func 1:(G,H) > Homomorphism of G,H means
:Def8: for a holds it.a = 1_H;
existence
proof
reconsider f = (the carrier of G) > 1_H as Function of G, H
by FUNCOP_1:57;
A1: for a holds f.a = 1_H by FUNCOP_1:13;
f.(a * b) = f.a * f.b by A1,Lm3;
then reconsider g = f as Homomorphism of G,H by Def7;
take g;
thus thesis by A1;
end;
uniqueness
proof
let g,h be Homomorphism of G,H such that
A2: for a holds g.a = 1_H and
A3: for a holds h.a = 1_H;
for a holds g.a = h.a
proof
let a;
g.a = 1_H & h.a = 1_H by A2,A3;
hence thesis;
end;
hence thesis by FUNCT_2:113;
end;
end;
theorem
h1 * 1:(G,H) = 1:(G,I) & 1:(H,I) * h = 1:(G,I)
proof
A1: now let a;
thus (h1 * 1:(G,H)).a = h1.(1:(G,H).a) by FUNCT_2:21
.= h1.(1_H) by Def8
.= 1_I by Th40;
end;
now let a;
thus (1:(H,I) * h).a = 1:(H,I).(h.a) by FUNCT_2:21
.= 1_I by Def8;
end;
hence thesis by A1,Def8;
end;
definition let G; let N be normal Subgroup of G;
func nat_hom N > Homomorphism of G,G./.N means
:Def9: for a holds it.a = a * N;
existence
proof
defpred P[set,set] means ex a st $1 = a & $2 = a * N;
A1: for x,y1,y2 st x in the carrier of G & P[x,y1] & P[x,y2] holds
y1 = y2;
A2: for x st x in the carrier of G ex y st P[x,y]
proof let x;
assume x in the carrier of G;
then reconsider a = x as Element of G;
reconsider y = a * N as set;
take y;
take a;
thus thesis;
end;
consider f being Function such that A3: dom f = the carrier of G and
A4: for x st x in the carrier of G holds P[x,f.x] from FUNCT_1:sch 2
(A1,A2);
rng f c= the carrier of G./.N
proof let x;
assume x in rng f;
then consider y such that A5: y in dom f and
A6: f.y = x by FUNCT_1:def 5;
consider a such that A7: y = a & f.y = a * N by A3,A4,A5;
a * N = N * a by GROUP_3:140;
then x in G./.N by A6,A7,Th28;
hence thesis by RLVECT_1:def 1;
end;
then reconsider f as Function of G, G./.N
by A3,FUNCT_2:def 1,RELSET_1:11;
now let a,b;
consider a1 such that A8: a = a1 & f.a = a1 * N by A4;
consider b1 such that A9: b = b1 & f.b = b1 * N by A4;
A10: ex c being Element of G
st c = a * b & f.(a * b) = c * N by A4;
thus f.a * f.b = @(f.a) * @(f.b) by Th24
.= (a1 * N) * b1 * N by A8,A9,GROUP_3:10
.= a1 * (N * b1) * N by GROUP_2:128
.= a1 * (b1 * N) * N by GROUP_3:140
.= a1 * ((b1 * N) * N) by GROUP_2:116
.= a1 * (b1 * N) by Th6
.= f.(a * b) by A8,A9,A10,GROUP_2:127;
end;
then reconsider f as Homomorphism of G,G./.N by Def7;
take f;
let a;
ex b st a = b & f.a = b * N by A4;
hence thesis;
end;
uniqueness
proof let n1,n2 be Homomorphism of G,G./.N such that
A11: for a holds n1.a = a * N and
A12: for a holds n2.a = a * N;
now let a;
n1.a = a * N & n2.a = a * N by A11,A12;
hence n1.a = n2.a;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let G,H,g;
func Ker g > strict Subgroup of G means
:Def10: the carrier of it = {a : g.a = 1_H};
existence
proof
defpred P[set] means g.$1 = 1_H;
reconsider A = {a : P[a]} as Subset of G from DOMAIN_1:sch 7;
g.(1_G) = 1_H by Th40;
then A1: 1_G in A;
A2: now let a,b;
assume that A3: a in A and A4: b in A;
A5: ex a1 st a1 = a & g.a1 = 1_H by A3;
A6: ex b1 st b1 = b & g.b1 = 1_H by A4;
g.(a * b) = g.a * g.b by Def7
.= 1_H by A5,A6,GROUP_1:def 5;
hence a * b in A;
end;
now let a;
assume a in A;
then ex a1 st a1 = a & g.a1 = 1_H;
then g.(a") = (1_H)" by Th41
.= 1_H by GROUP_1:16;
hence a" in A;
end;
then consider B being strict Subgroup of G such that
A7: the carrier of B = A by A1,A2,GROUP_2:61;
reconsider B as strict Subgroup of G;
take B;
thus thesis by A7;
end;
uniqueness by GROUP_2:68;
end;
registration let G,H,g;
cluster Ker g > normal;
coherence
proof
defpred P[set] means g.$1 = 1_H;
reconsider A = {a : P[a]} as Subset of G from DOMAIN_1:sch 7;
g.(1_G) = 1_H by Th40;
then A1: 1_G in A;
A2: now let a,b;
assume that A3: a in A and A4: b in A;
A5: ex a1 st a1 = a & g.a1 = 1_H by A3;
A6: ex b1 st b1 = b & g.b1 = 1_H by A4;
g.(a * b) = g.a * g.b by Def7
.= 1_H by A5,A6,GROUP_1:def 5;
hence a * b in A;
end;
now let a;
assume a in A;
then ex a1 st a1 = a & g.a1 = 1_H;
then g.(a") = (1_H)" by Th41
.= 1_H by GROUP_1:16;
hence a" in A;
end;
then consider B being strict Subgroup of G such that
A7: the carrier of B = A by A1,A2,GROUP_2:61;
now let a;
now let b;
assume b in B ^ a;
then consider c being Element of G such that
A8: b = c ^ a and A9: c in B by GROUP_3:70;
c in A by A7,A9,RLVECT_1:def 1;
then ex a1 st c = a1 & g.a1 = 1_H;
then g.b = (1_H) ^ (g.a) by A8,Th42
.= 1_H by GROUP_3:22;
then b in A;
hence b in B by A7,RLVECT_1:def 1;
end;
hence B ^ a is Subgroup of B by GROUP_2:67;
end;
then B is normal Subgroup of G by GROUP_3:145;
hence thesis by A7,Def10;
end;
end;
theorem Th50:
a in Ker h iff h.a = 1_H
proof
thus a in Ker h implies h.a = 1_H
proof
assume a in Ker h;
then a in the carrier of Ker h by RLVECT_1:def 1;
then a in {b : h.b = 1_H} by Def10;
then ex b st a = b & h.b = 1_H;
hence thesis;
end;
assume h.a = 1_H;
then a in {b : h.b = 1_H};
then a in the carrier of Ker h by Def10;
hence thesis by RLVECT_1:def 1;
end;
theorem
for G,H being strict Group holds
Ker 1:(G,H) = G
proof let G,H be strict Group;
now let a be Element of G;
1:(G,H).a = 1_H by Def8;
hence a in Ker 1:(G,H) by Th50;
end;
hence thesis by GROUP_2:71;
end;
theorem Th52:
for N being strict normal Subgroup of G holds
Ker nat_hom N = N
proof let N be strict normal Subgroup of G;
let a;
thus a in Ker nat_hom N implies a in N
proof assume a in Ker nat_hom N;
then (nat_hom N).a = 1_(G./.N) & (nat_hom N).a = a * N &
1_(G./.N) = carr N by Def9,Th29,Th50;
hence a in N by GROUP_2:136;
end;
assume a in N;
then a * N = carr N & (nat_hom N).a = a * N &
1_(G./.N) = carr N by Def9,Th29,GROUP_2:136;
hence thesis by Th50;
end;
definition let G,H,g;
func Image g > strict Subgroup of H means
:Def11: the carrier of it = g .: (the carrier of G);
existence
proof
the carrier of G c= the carrier of G;
then reconsider X = the carrier of G as Subset of G;
set S = g .: X;
A1: dom g = the carrier of G & X /\ X = X & X <> {} by FUNCT_2:def 1;
then X meets X by XBOOLE_0:def 7;
then A2: S <> {} by A1,RELAT_1:151;
A3: now let c,d;
assume that A4: c in S and A5: d in S;
consider a such that a in X and A6: c = g.a by A4,FUNCT_2:116;
consider b such that b in X and A7: d = g.b by A5,FUNCT_2:116;
c * d = g.(a * b) & a * b in the carrier of G by A6,A7,Def7;
hence c * d in S by FUNCT_2:43;
end;
now let c;
assume c in S;
then consider a such that a in X and A8: c = g.a by FUNCT_2:116;
a" in the carrier of G & g.(a") = c" by A8,Th41;
hence c" in S by FUNCT_2:43;
end;
then consider D being strict Subgroup of H such that
A9: the carrier of D = S by A2,A3,GROUP_2:61;
take D;
thus thesis by A9;
end;
uniqueness by GROUP_2:68;
end;
theorem Th53:
rng g = the carrier of Image g
proof
the carrier of Image g = g .: (the carrier of G) by Def11
.= g .: (dom g) by FUNCT_2:def 1
.= rng g by RELAT_1:146;
hence thesis;
end;
theorem Th54:
x in Image g iff ex a st x = g.a
proof
thus x in Image g implies ex a st x = g.a
proof assume x in Image g;
then x in the carrier of Image g by RLVECT_1:def 1;
then x in g .: (the carrier of G) by Def11;
then consider y such that y in dom g and A1: y in the carrier of G and
A2: g.y = x by FUNCT_1:def 12;
reconsider y as Element of G by A1;
take y;
thus thesis by A2;
end;
given a such that A3: x = g.a;
a in the carrier of G & the carrier of G = dom g by FUNCT_2:def 1;
then x in g .: (the carrier of G) by A3,FUNCT_1:def 12;
then x in the carrier of Image g by Def11;
hence thesis by RLVECT_1:def 1;
end;
theorem
Image g = gr rng g
proof
rng g = the carrier of Image g & the carrier of Image g = carr Image g
by Th53;
hence thesis by GROUP_4:40;
end;
theorem
Image 1:(G,H) = (1).H
proof set g = 1:(G,H);
1_H in Image g by GROUP_2:55;
then 1_H in the carrier of Image g by RLVECT_1:def 1;
then A1: {1_H} c= the carrier of Image g by ZFMISC_1:37;
the carrier of Image g c= {1_H}
proof let x;
assume x in the carrier of Image g;
then x in g .: (the carrier of G) by Def11;
then consider y such that y in dom g and A2: y in the carrier of G and
A3: g.y = x by FUNCT_1:def 12;
reconsider y as Element of G by A2;
g.y = 1_H by Def8;
hence thesis by A3,TARSKI:def 1;
end;
then the carrier of Image g = {1_H} by A1,XBOOLE_0:def 10;
hence thesis by GROUP_2:def 7;
end;
theorem Th57:
for N being normal Subgroup of G holds
Image nat_hom N = G./.N
proof let N be normal Subgroup of G;
now let S be Element of G./.N;
consider a such that A1: S = a * N & S = N * a by Th26;
(nat_hom N).a = a * N by Def9;
hence S in Image nat_hom N by A1,Th54;
end;
hence thesis by GROUP_2:71;
end;
theorem Th58:
h is Homomorphism of G,Image h
proof
h is Function of G, Image h
proof
A1: rng h = the carrier of Image h by Th53;
dom h = the carrier of G by FUNCT_2:def 1;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider f' = h as Function of G, Image h;
now
let a,b;
thus f'.a * f'.b = h.a * h.b by GROUP_2:52
.= f'.(a * b) by Def7;
end;
hence thesis by Def7;
end;
theorem Th59:
G is finite implies Image g is finite
proof
assume G is finite;
then the carrier of G is finite by GROUP_1:def 14;
then g .: (the carrier of G) is finite by FINSET_1:17;
then the carrier of Image g is finite by Def11;
hence thesis by GROUP_1:def 14;
end;
Lm4: for A be commutative Group, a, b be Element of A holds a * b = b * a;
theorem
G is commutative Group implies Image g is commutative
proof assume A1: G is commutative Group;
let h1,h2 be Element of Image g;
reconsider c = h1, d = h2 as Element of H by GROUP_2:51;
h1 in Image g by RLVECT_1:def 1;
then consider a such that A2: h1 = g.a by Th54;
h2 in Image g by RLVECT_1:def 1;
then consider b such that A3: h2 = g.b by Th54;
thus h1 * h2 = c * d by GROUP_2:52
.= g.(a * b) by A2,A3,Def7
.= g.(b * a) by A1,Lm4
.= d * c by A2,A3,Def7
.= h2 * h1 by GROUP_2:52;
end;
theorem Th61:
Ord Image g <=` Ord G
proof
A1:Card (g .: (the carrier of G)) <=` Card (the carrier of G) by CARD_2:3;
Ord Image g = Card (g .: (the carrier of G)) by Def11;
hence thesis by A1;
end;
theorem
G is finite implies ord Image g <= ord G
proof
assume A1: G is finite;
then A2: Image g is finite by Th59;
consider c being finite set such that
A3: c = the carrier of G & ord G = card c by A1,GROUP_1:def 15;
consider ci being finite set such that
A4: ci = the carrier of Image g & ord Image g = card ci by A2,GROUP_1:def 15;
Ord Image g <=` Ord G by Th61;
then Card (the carrier of Image g) <=` Ord G;
then Card (the carrier of Image g) <=`
Card (the carrier of G);
hence thesis by A3,A4,CARD_2:57;
end;
definition let G,H,h;
attr h is being_monomorphism means :Def12:
h is onetoone;
attr h is being_epimorphism means :Def13:
rng h = the carrier of H;
end;
notation let G,H,h;
synonym h is_monomorphism for h is being_monomorphism;
synonym h is_epimorphism for h is being_epimorphism;
end;
theorem
h is_monomorphism & c in Image h implies h.(h".c) = c
proof
assume that A1: h is_monomorphism and
A2:c in Image h;
reconsider h' = h as Function of G,Image h by Th58;
A3: h' is onetoone by A1,Def12;
h'.(h'".c) = c
proof
A4: rng h' = the carrier of Image h by Th53;
c in the carrier of Image h by A2,RLVECT_1:def 1;
hence thesis by A3,A4,FUNCT_1:57;
end;
hence thesis;
end;
theorem Th64:
h is_monomorphism implies h".(h.a) = a
proof
assume h is onetoone;
hence thesis by FUNCT_2:32;
end;
theorem Th65:
h is_monomorphism implies h" is Homomorphism of Image h,G
proof
assume A1: h is onetoone;
then A2: h is_monomorphism by Def12;
reconsider Imh = Image h as Group;
h" is Function of Imh,G
proof
A3: h is Function of G,Imh by Th58;
rng h = the carrier of Imh by Th53;
hence thesis by A1,A3,FUNCT_2:31;
end;
then reconsider h' = h" as Function of Imh, G;
now
let a,b be Element of Imh;
reconsider a' = a, b' = b as Element of H by GROUP_2:51;
A4: a' in Imh & b' in Imh by RLVECT_1:def 1;
then consider a1 being Element of G such that
A5: h.a1 = a' by Th54;
consider b1 being Element of G such that
A6: h.b1 = b' by A4,Th54;
thus h'.(a * b) = h'.(h.a1 * h.b1) by A5,A6,GROUP_2:52
.= h'.(h.(a1 * b1)) by Def7
.= a1 * b1 by A2,Th64
.= h'.a * b1 by A2,A5,Th64
.= h'.a * h'.b by A2,A6,Th64;
end;
hence thesis by Def7;
end;
theorem Th66:
h is_monomorphism iff Ker h = (1).G
proof
thus h is_monomorphism implies Ker h = (1).G
proof
assume A1: h is onetoone;
now
let x;
thus x in the carrier of Ker h iff x = 1_G
proof
thus x in the carrier of Ker h implies x = 1_G
proof
assume A2: x in the carrier of Ker h;
then x in Ker h by RLVECT_1:def 1;
then x in G by GROUP_2:49;
then reconsider a = x as Element of G by RLVECT_1:def 1;
a in Ker h by A2,RLVECT_1:def 1;
then h.a = 1_H by Th50
.= h.(1_G) by Th40;
hence thesis by A1,Th1;
end;
assume A3: x = 1_G;
then reconsider a = x as Element of G;
h.a = 1_H by A3,Th40;
then a in Ker h by Th50;
hence thesis by RLVECT_1:def 1;
end;
end;
then the carrier of Ker h = {1_G} by TARSKI:def 1;
hence thesis by GROUP_2:def 7;
end;
assume Ker h = (1).G;
then A4: the carrier of Ker h = {1_G} by GROUP_2:def 7;
now
let a,b;
assume that
A5: a <> b and
A6: h.a = h.b;
h.a * h.(a") = h.(a * a") by Def7
.= h.(1_G) by GROUP_1:def 6
.= 1_H by Th40;
then 1_H = h.(b * a") by A6,Def7;
then b * a" in Ker h by Th50;
then A7: b * a" in the carrier of Ker h by RLVECT_1:def 1;
a = 1_G * a by GROUP_1:def 5
.= b * a" * a by A4,A7,TARSKI:def 1
.= b * (a" * a) by GROUP_1:def 4
.= b * 1_G by GROUP_1:def 6
.= b by GROUP_1:def 5;
hence contradiction by A5;
end;
then for a,b st h.a = h.b holds a = b;
then h is onetoone by Th1;
hence thesis by Def12;
end;
theorem Th67:
for H being strict Group, h being Homomorphism of G,H holds
h is_epimorphism iff Image h = H
proof let H be strict Group, h be Homomorphism of G,H;
thus h is_epimorphism implies Image h = H
proof assume rng h = the carrier of H;
then the carrier of Image h = the carrier of H by Th53;
hence thesis by GROUP_2:70;
end;
assume A1: Image h = H;
the carrier of H c= rng h
proof let x;
assume x in the carrier of H;
then x in h .: (the carrier of G) by A1,Def11;
then ex y st y in dom h & y in the carrier of G &
h.y = x by FUNCT_1:def 12;
hence thesis by FUNCT_1:def 5;
end;
then rng h = the carrier of H by XBOOLE_0:def 10;
hence thesis by Def13;
end;
theorem Th68:
for H being strict Group, h being Homomorphism of G,H st
h is_epimorphism holds
for c being Element of H ex a st h.a = c
proof let H be strict Group, h be Homomorphism of G,H;
assume h is_epimorphism;
then A1: Image h = H by Th67;
now
let c be Element of H;
c in Image h by A1,RLVECT_1:def 1;
hence ex a st h.a = c by Th54;
end;
hence thesis;
end;
theorem Th69:
for N being normal Subgroup of G holds
nat_hom N is_epimorphism
proof let N be normal Subgroup of G;
Image nat_hom N = G./.N by Th57;
hence thesis by Th67;
end;
definition let G,H,h;
attr h is being_isomorphism means :Def14:
h is_epimorphism & h is_monomorphism;
end;
notation let G,H,h;
synonym h is_isomorphism for h is being_isomorphism;
end;
theorem Th70:
h is_isomorphism iff rng h = the carrier of H & h is onetoone
proof
thus h is_isomorphism implies
rng h = the carrier of H & h is onetoone
proof
assume h is_epimorphism & h is_monomorphism;
hence thesis by Def12,Def13;
end;
assume rng h = the carrier of H & h is onetoone;
hence h is_epimorphism & h is_monomorphism by Def12,Def13;
end;
theorem
h is_isomorphism implies dom h = the carrier of G &
rng h = the carrier of H
proof
assume h is_isomorphism;
then h is_epimorphism by Def14;
hence thesis by Def13,FUNCT_2:def 1;
end;
theorem Th72:
for H being strict Group, h being Homomorphism of G,H st
h is_isomorphism holds h" is Homomorphism of H,G
proof let H be strict Group, h be Homomorphism of G,H;
assume A1: h is_epimorphism & h is_monomorphism;
then H = Image h by Th67;
hence thesis by A1,Th65;
end;
theorem Th73:
h is_isomorphism & g1 = h" implies g1 is_isomorphism
proof
assume that A1: h is_isomorphism and
A2: g1 = h";
A3: h is onetoone by A1,Th70;
then A4: g1 is onetoone by A2,FUNCT_1:62;
A5: dom h = the carrier of G by FUNCT_2:def 1;
rng g1 = dom h by A2,A3,FUNCT_1:55;
hence thesis by A4,A5,Th70;
end;
theorem Th74:
h is_isomorphism & h1 is_isomorphism implies h1 * h is_isomorphism
proof
assume A1: h is_isomorphism & h1 is_isomorphism;
then A2: h is onetoone & h1 is onetoone by Th70;
A3: rng(h1 * h) = the carrier of I
proof
A4: dom h1 = the carrier of H by FUNCT_2:def 1;
rng h = the carrier of H by A1,Th70;
hence rng(h1 * h) = rng h1 by A4,RELAT_1:47
.= the carrier of I by A1,Th70;
end;
h1 * h is onetoone by A2,FUNCT_1:46;
hence thesis by A3,Th70;
end;
theorem Th75:
for G being Group holds
nat_hom (1).G is_isomorphism
proof let G be Group;
set g = nat_hom (1).G;
Ker g = (1).G by Th52;
then g is_monomorphism & g is_epimorphism by Th66,Th69;
hence nat_hom (1).G is_isomorphism by Def14;
end;
definition let G,H;
pred G,H are_isomorphic means :Def15:
ex h st h is_isomorphism;
reflexivity
proof let G;
reconsider i = id the carrier of G as Homomorphism of G,G by Th47;
i is onetoone & rng i = the carrier of G by FUNCT_2:def 3;
then i is_isomorphism by Th70;
hence thesis;
end;
end;
canceled;
theorem Th77:
for G,H being strict Group holds
G,H are_isomorphic implies H,G are_isomorphic
proof let G,H be strict Group;
assume G,H are_isomorphic;
then consider h being Homomorphism of G,H such that
A1: h is_isomorphism by Def15;
reconsider g = h" as Homomorphism of H,G by A1,Th72;
take g;
thus thesis by A1,Th73;
end;
definition let G,H be strict Group;
redefine pred G,H are_isomorphic;
symmetry by Th77;
end;
theorem
G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic
proof
assume that
A1: G,H are_isomorphic and
A2: H,I are_isomorphic;
consider g such that A3: g is_isomorphism by A1,Def15;
consider h1 such that A4: h1 is_isomorphism by A2,Def15;
(h1 * g) is_isomorphism by A3,A4,Th74;
hence thesis by Def15;
end;
theorem
h is_monomorphism implies G,Image h are_isomorphic
proof
assume A1: h is onetoone;
reconsider ih = h as Homomorphism of G,Image h by Th58;
take ih;
A2: ih is_monomorphism by A1,Def12;
now
the carrier of Image h = rng ih by Th53;
hence ih is_epimorphism by Def13;
end;
hence thesis by A2,Def14;
end;
theorem Th80:
for G,H being strict Group holds
G is trivial & H is trivial implies G,H are_isomorphic
proof let G,H be strict Group;
assume G is trivial & H is trivial;
then A1: G = (1).G & H = (1).H by Th13;
take 1:(G,H);
set h = 1:(G,H);
A2: h is_epimorphism
proof
the carrier of (1).G = {1_G} by GROUP_2:def 7;
then rng h = {h.(1_G)} by A1,FUNCT_2:62
.= {1_H} by Def8
.= the carrier of (1).H by GROUP_2:def 7;
hence thesis by A1,Def13;
end;
h is_monomorphism
proof
now
let a,b be Element of G;
assume h.a = h.b;
a in the carrier of (1).G & b in the carrier of (1).G by A1;
then a in {1_G} & b in {1_G} by GROUP_2:def 7;
then a = 1_G & b = 1_G by TARSKI:def 1;
hence a = b;
end;
then h is onetoone by Th1;
hence thesis by Def12;
end;
hence thesis by A2,Def14;
end;
theorem
(1).G,(1).H are_isomorphic
proof
(1).G is trivial & (1).H is trivial by Th11;
hence thesis by Th80;
end;
theorem
for G being strict Group holds
G,G./.(1).G are_isomorphic
proof let G be strict Group;
nat_hom (1).G is_isomorphism by Th75;
hence G,G./.(1).G are_isomorphic by Def15;
end;
theorem
for G being Group holds
G./.(Omega).G is trivial
proof let G be Group;
the carrier of G./.(Omega).G = {the carrier of G} by GROUP_2:172;
hence thesis by Def2;
end;
theorem Th84:
for G,H being strict Group holds
G,H are_isomorphic implies Ord G = Ord H
proof let G,H be strict Group;
assume A1: G,H are_isomorphic;
then consider h being Homomorphism of G,H such that
A2: h is_isomorphism by Def15;
H,G are_isomorphic by A1;
then consider g1 being Homomorphism of H,G such that
A3: g1 is_isomorphism by Def15;
h is_epimorphism by A2,Def14;
then Image h = H by Th67;
then A4: Ord H <=` Ord G by Th61;
g1 is_epimorphism by A3,Def14;
then Image g1 = G by Th67;
then Ord G <=` Ord H by Th61;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem Th85:
G,H are_isomorphic & G is finite implies H is finite
proof
assume that A1: G,H are_isomorphic and
A2: G is finite;
consider h such that A3: h is_isomorphism by A1,Def15;
h is_epimorphism by A3,Def14;
then A4: rng h = the carrier of H by Def13;
the carrier of G is finite by A2,GROUP_1:def 14;
then dom h is finite by FUNCT_2:def 1;
then the carrier of H is finite by A4,FINSET_1:26;
hence thesis by GROUP_1:def 14;
end;
theorem Th86:
for G,H being strict Group holds
G,H are_isomorphic & G is finite implies ord G = ord H
proof let G,H be strict Group;
assume that A1: G,H are_isomorphic and
A2: G is finite;
Ord G = Ord H by A1,Th84;
then A3: Card (the carrier of G) = Card (the carrier of H);
A4: H is finite & G is finite by A1,A2,Th85;
then consider cH being finite set such that
A5: cH = the carrier of H & ord H = card cH by GROUP_1:def 15;
consider cG being finite set such that
A6: cG = the carrier of G & ord G = card cG by A4,GROUP_1:def 15;
thus thesis by A3,A5,A6;
end;
theorem
for G,H being strict Group holds
G,H are_isomorphic & G is trivial implies H is trivial
proof let G,H be strict Group;
assume that A1: G,H are_isomorphic and
A2: G is trivial;
A3: ord G = 1 & G is finite by A2,Th12;
then A4: ord H = 1 by A1,Th86;
H is finite by A1,A3,Th85;
hence thesis by A4,Th12;
end;
canceled;
theorem
for H being strict Group st
G,H are_isomorphic & G is commutative Group holds H is commutative Group
proof let H be strict Group;
assume that A1: G,H are_isomorphic and
A2:G is commutative Group;
consider h being Homomorphism of G,H such that
A3: h is_isomorphism by A1,Def15;
A4: h is_epimorphism by A3,Def14;
now
let c,d be Element of H;
consider a such that A5: h.a = c by A4,Th68;
consider b such that A6: h.b = d by A4,Th68;
thus c * d = h.(a * b) by A5,A6,Def7
.= h.(b * a) by A2,Lm4
.= d * c by A5,A6,Def7;
end;
hence thesis by GROUP_1:def 16;
end;
Lm5:
G./.Ker g,Image g are_isomorphic &
ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism &
g = h * nat_hom Ker g
proof set I = G./.Ker g; set J = Image g;
defpred P[set,set] means for a st $1 = a * Ker g holds $2 = g.a;
A1: for S being Element of I
ex T being Element of J st P[S,T]
proof let S be Element of I;
consider a such that A2: S = a * Ker g & S = Ker g * a by Th26;
g.a in J by Th54;
then reconsider T = g.a as Element of J by RLVECT_1:def 1;
take T;
let b;
assume S = b * Ker g;
then a" * b in Ker g by A2,GROUP_2:137;
then 1_H = g.(a" * b) by Th50
.= g.(a") * g.b by Def7
.= (g.a)" * g.b by Th41;
then g.b = (g.a)"" by GROUP_1:20;
hence thesis by GROUP_1:19;
end;
consider f being Function of I,J such that
A3: for S being Element of I holds P[S,f.S] from FUNCT_2:sch 3(A1);
now let S,T be Element of G./.Ker g;
consider a such that A4: S = a * Ker g and S = Ker g * a by Th26;
consider b such that A5: T = b * Ker g and A6: T = Ker g * b by Th26;
f.S = g.a & f.T = g.b by A3,A4,A5;
then A7: f.S * f.T = g.a * g.b by GROUP_2:52
.= g.(a * b) by Def7;
@S = S & @T = T;
then S * T = (a * Ker g) * (Ker g * b) by A4,A6,Th24
.= (a * Ker g) * Ker g * b by GROUP_3:12
.= a * Ker g * b by Th6
.= a * (Ker g * b) by GROUP_2:128
.= a * (b * Ker g) by GROUP_3:140
.= a * b * Ker g by GROUP_2:127;
hence f.(S * T) = f.S * f.T by A3,A7;
end;
then reconsider f as Homomorphism of G./.Ker g,J by Def7;
the carrier of J c= rng f
proof let x;
assume x in the carrier of J;
then x in Image g by RLVECT_1:def 1;
then consider a such that A8: x = g.a by Th54;
reconsider S = a * Ker g as Element of I by Th27;
f.S = g.a & S in the carrier of I & the carrier of I = dom f
by A3,FUNCT_2:def 1;
hence thesis by A8,FUNCT_1:def 5;
end;
then A9: rng f = the carrier of J by XBOOLE_0:def 10;
A10: f is onetoone
proof let y1,y2;
assume y1 in dom f & y2 in dom f;
then reconsider S = y1, T = y2 as Element of I;
consider a such that A11: S = a * Ker g and S = Ker g * a by Th26;
consider b such that A12: T = b * Ker g and T = Ker g * b by Th26;
assume A13: f.y1 = f.y2;
f.S = g.a & f.T = g.b by A3,A11,A12;
then (g.b)" * g.a = 1_H by A13,GROUP_1:def 6;
then 1_H = g.(b") * g.a by Th41
.= g.(b" * a) by Def7;
then b" * a in Ker g by Th50;
hence thesis by A11,A12,GROUP_2:137;
end;
then f is_isomorphism by A9,Th70;
hence G./.Ker g,Image g are_isomorphic by Def15;
take f;
A14: dom nat_hom Ker g = the carrier of G & dom g = the carrier of G
by FUNCT_2:def 1;
thus f is_isomorphism by A9,A10,Th70;
A15: now let x;
thus x in dom g implies x in dom nat_hom Ker g & (nat_hom Ker g).x in
dom f
proof assume A16: x in dom g;
hence x in dom nat_hom Ker g by A14;
(nat_hom Ker g).x in rng nat_hom Ker g &
rng nat_hom Ker g c= the carrier of I &
dom f = the carrier of I by A14,A16,FUNCT_1:def 5,FUNCT_2:def 1;
hence (nat_hom Ker g).x in dom f;
end;
assume x in dom nat_hom Ker g & (nat_hom Ker g).x in dom f;
hence x in dom g by A14;
end;
now let x;
assume x in dom g;
then reconsider a = x as Element of G;
(nat_hom Ker g).a = a * Ker g by Def9;
hence g.x = f.((nat_hom Ker g).x) by A3;
end;
hence thesis by A15,FUNCT_1:20;
end;
theorem
G./.Ker g, Image g are_isomorphic by Lm5;
theorem
ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism &
g = h * nat_hom Ker g by Lm5;
theorem
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
proof let M be strict normal Subgroup of G;
let J be strict normal Subgroup of G./.M;
assume that A1: J = N./.(N,M)`*` and A2: M is Subgroup of N;
defpred P[set,set] means for a st $1 = a * M holds $2 = a * N;
A3: for x being Element of G./.M
ex y being Element of G./.N st P[x,y]
proof let x be Element of G./.M;
consider a such that A4: x = a * M and x = M * a by Th26;
reconsider y = a * N as Element of G./.N by Th27;
take y;
let b;
assume x = b * M;
then a" * b in M by A4,GROUP_2:137;
then a" * b in N by A2,GROUP_2:49;
hence thesis by GROUP_2:137;
end;
consider f being Function of G./.M, G./.N
such that A5: for x being Element of G./.M holds P[x,f.x]
from FUNCT_2:sch 3(A3);
now let x,y be Element of G./.M;
consider a such that A6: x = a * M and x = M * a by Th26;
consider b such that A7: y = b * M and y = M * b by Th26;
A8: f.x = a * N & f.y = b * N by A5,A6,A7;
A9: f.x * f.y = @(f.x) * @(f.y) by Th24
.= a * N * b * N by A8,GROUP_3:10
.= a * (N * b) * N by GROUP_2:128
.= a * (b * N) * N by GROUP_3:140
.= a * ((b * N) * N) by GROUP_2:116
.= a * (b * N) by Th6
.= a * b * N by GROUP_2:127;
x * y = @x * @y by Th24
.= a * M * b * M by A6,A7,GROUP_3:10
.= a * (M * b) * M by GROUP_2:128
.= a * (b * M) * M by GROUP_3:140
.= a * ((b * M) * M) by GROUP_2:116
.= a * (b * M) by Th6
.= a * b * M by GROUP_2:127;
hence f.(x * y) = f.x * f.y by A5,A9;
end;
then reconsider f as Homomorphism of G./.M,G./.N by Def7;
A10: Ker f = J
proof let S be Element of G./.M;
thus S in Ker f implies S in J
proof assume S in Ker f;
then A11: f.S = 1_(G./.N) by Th50
.= carr N by Th29;
consider a such that A12: S = a * M & S = M * a by Th26;
f.S = a * N by A5,A12;
then a in N by A11,GROUP_2:136;
then reconsider q = a as Element of N by RLVECT_1:def 1;
(N,M)`*` = M by A2,Def1;
then S = q * (N,M)`*` & S = (N,M)`*` * q by A12,Th2;
hence thesis by A1,Th28;
end;
assume S in J;
then consider a being Element of N such that
A13: S = a * (N,M)`*` & S = (N,M)`*` * a by A1,Th28;
reconsider a' = a as Element of G by GROUP_2:51;
(N,M)`*` = M by A2,Def1;
then S = a' * M by A13,Th2;
then f.S = a' * N & a in N by A5,RLVECT_1:def 1;
then f.S = carr N by GROUP_2:136
.= 1_(G./.N) by Th29;
hence thesis by Th50;
end;
the carrier of G./.N c= rng f
proof let x;
assume x in the carrier of G./.N;
then x in G./.N by RLVECT_1:def 1;
then consider a such that A14: x = a * N & x = N * a by Th28;
reconsider S = a * M as Element of G./.M by Th27;
f.S = a * N & S in
the carrier of G./.M & dom f = the carrier of G./.M by A5,FUNCT_2:def 1;
hence thesis by A14,FUNCT_1:def 5;
end;
then rng f = the carrier of G./.N by XBOOLE_0:def 10;
then f is_epimorphism by Def13;
then Image f = G./.N by Th67;
hence thesis by A10,Lm5;
end;
theorem
for N being strict normal Subgroup of G holds
(B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic
proof let N be strict normal Subgroup of G;
set f = nat_hom N; set g = f  (the carrier of B);
set I = (B "\/" N)./.(B "\/" N,N)`*`; set J = (B "\/" N,N)`*`;
A1: B is Subgroup of B "\/" N by GROUP_4:78;
A2: dom g = dom f /\ (the carrier of B) & dom f = the carrier of G &
the carrier of B c= the carrier of G by FUNCT_2:def 1,GROUP_2:def 5
,RELAT_1:90;
then A3: dom g = the carrier of B by XBOOLE_1:28;
A4: N is Subgroup of B "\/" N by GROUP_4:78;
then A5: N = (B "\/" N,N)`*` by Def1;
A6: I is Subgroup of G./.N by A4,Th34;
rng g c= the carrier of I
proof let y;
assume y in rng g;
then consider x such that A7: x in dom g and
A8: g.x = y by FUNCT_1:def 5;
reconsider x as Element of B by A2,A7,XBOOLE_1:28;
reconsider x'' = x as Element of B "\/" N by A1,GROUP_2:51;
reconsider x' = x as Element of G by GROUP_2:51;
A9: g.x = f.x' by A7,FUNCT_1:70
.= x' * N by Def9;
then A10: g.x = N * x' by GROUP_3:140;
x'' * (B "\/" N,N)`*` = x' * N & N * x' = (B "\/" N,N)`*`
* x'' by A5,Th2;
then y in I by A8,A9,A10,Th28;
hence thesis by RLVECT_1:def 1;
end;
then reconsider g as Function of B,
(B "\/" N)./.(B "\/" N,N)`*` by A3,FUNCT_2:def 1,RELSET_1:11;
now let a,b be Element of B;
reconsider a' = a, b' = b as Element of G by GROUP_2:51;
A11: f.a' = g.a & f.b' = g.b by FUNCT_1:72;
a * b in the carrier of B & a * b = a' * b' &
a' * b' in the carrier of G by GROUP_2:52;
hence g.(a * b) = f.(a' * b') by FUNCT_1:72
.= f.a' * f.b' by Def7
.= g.a * g.b by A6,A11,GROUP_2:52;
end;
then reconsider g as Homomorphism of B,(B "\/" N)./.(B "\/" N,N)`*`
by Def7;
A12: Ker g = B /\ N
proof let b be Element of B;
reconsider c = b as Element of G by GROUP_2:51;
A13: g.b = f.c by FUNCT_1:72
.= c * N by Def9;
thus b in Ker g implies b in B /\ N
proof assume b in Ker g;
then g.b = 1_I by Th50
.= carr J by Th29
.= carr N by A5;
then b in B & b in N by A13,GROUP_2:136,RLVECT_1:def 1;
hence thesis by GROUP_2:99;
end;
assume b in B /\ N;
then b in N by GROUP_2:99;
then c * N = carr J by A5,GROUP_2:136
.= 1_I by Th29;
hence thesis by A13,Th50;
end;
the carrier of I c= rng g
proof let x;
assume x in the carrier of I;
then x in I by RLVECT_1:def 1;
then consider b being Element of B "\/" N such that
A14: x = b * J & x = J * b by Th28;
B * N = N * B & b in B "\/" N by GROUP_5:8,RLVECT_1:def 1;
then consider a1,a2 such that A15: b = a1 * a2 and
A16: a1 in B & a2 in N by GROUP_5:5;
A17: a1 in the carrier of B & a1 in the carrier of G by A16,RLVECT_1:def 1;
x = a1 * a2 * N by A5,A14,A15,Th2
.= a1 * (a2 * N) by GROUP_2:127
.= a1 * N by A16,GROUP_2:136
.= f.a1 by Def9
.= g.a1 by A17,FUNCT_1:72;
hence thesis by A3,A17,FUNCT_1:def 5;
end;
then the carrier of I = rng g by XBOOLE_0:def 10;
then g is_epimorphism by Def13;
then Image g = (B "\/" N)./.(B "\/" N,N)`*` by Th67;
hence thesis by A12,Lm5;
end;
Góra
