:: Homomorphisms and Isomorphisms of Groups. Quotient Group
:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Copyright (c) 1991-2019 Association of Mizar Users

theorem Th1: :: GROUP_6:1
for A, B being non empty set
for 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 )
proof end;

definition
let G be Group;
let A be Subgroup of G;
:: original: Subgroup
redefine mode Subgroup of A -> Subgroup of G;
coherence
for b1 being Subgroup of A holds b1 is Subgroup of G
by GROUP_2:56;
end;

registration
let G be Group;
coherence
(1). G is normal
by GROUP_3:114;
coherence by GROUP_3:114;
end;

theorem Th2: :: GROUP_6:2
for G being Group
for A being Subgroup of G
for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )
proof end;

theorem :: GROUP_6:3
for G being Group
for A being Subgroup of G
for X, Y being Subgroup of A holds X /\ Y = X /\ Y
proof end;

theorem Th4: :: GROUP_6:4
for G being Group
for a, b being Element of G holds
( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") )
proof end;

theorem Th5: :: GROUP_6:5
for G being Group
for A being Subgroup of G
for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
proof end;

theorem Th6: :: GROUP_6:6
for G being Group
for A1 being Subset of G st A1 = { [.a,b.] where a, b is Element of G : verum } holds
G  = gr A1
proof end;

theorem Th7: :: GROUP_6:7
for G being strict Group
for 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 end;

theorem Th8: :: GROUP_6:8
for G being Group
for B being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B
proof end;

definition
let G be Group;
let B be Subgroup of G;
let M be normal Subgroup of G;
assume A1: multMagma(# the carrier of M, the multF of M #) is Subgroup of B ;
func (B,M) * -> strict normal Subgroup of B equals :Def1: :: GROUP_6:def 1
multMagma(# the carrier of M, the multF of M #);
coherence
multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B
proof end;
correctness
;
end;

:: deftheorem Def1 defines * GROUP_6:def 1 :
for G being Group
for B being Subgroup of G
for M being normal Subgroup of G st multMagma(# the carrier of M, the multF of M #) is Subgroup of B holds
(B,M) * = multMagma(# the carrier of M, the multF of M #);

theorem Th9: :: GROUP_6:9
for G being Group
for B being Subgroup of G
for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )
proof end;

definition
let G be Group;
let B be Subgroup of G;
let N be normal Subgroup of G;
:: original: /\
redefine func B /\ N -> strict normal Subgroup of B;
coherence
B /\ N is strict normal Subgroup of B
by Th9;
end;

definition
let G be Group;
let N be normal Subgroup of G;
let B be Subgroup of G;
:: original: /\
redefine func N /\ B -> strict normal Subgroup of B;
coherence
N /\ B is strict normal Subgroup of B
by Th9;
end;

definition
let G be non empty 1-sorted ;
redefine attr G is trivial means :Def2: :: GROUP_6:def 2
ex x being object st the carrier of G = {x};
compatibility
( G is trivial iff ex x being object st the carrier of G = {x} )
proof end;
end;

:: deftheorem Def2 defines trivial GROUP_6:def 2 :
for G being non empty 1-sorted holds
( G is trivial iff ex x being object st the carrier of G = {x} );

theorem Th10: :: GROUP_6:10
for G being Group holds (1). G is trivial
proof end;

registration
let G be Group;
coherence
(1). G is trivial
by Th10;
end;

registration
existence
ex b1 being Group st
( b1 is strict & b1 is trivial )
proof end;
end;

theorem Th11: :: 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 ) )
proof end;

theorem Th12: :: GROUP_6:12
for G being trivial strict Group holds (1). G = G
proof end;

notation
let G be Group;
let N be normal Subgroup of G;
synonym Cosets N for Left_Cosets N;
end;

registration
let G be Group;
let N be normal Subgroup of G;
cluster Cosets N -> non empty ;
coherence
not Cosets N is empty
by GROUP_2:135;
end;

theorem Th13: :: GROUP_6:13
for G being Group
for x being object
for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )
proof end;

theorem Th14: :: GROUP_6:14
for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )
proof end;

theorem Th15: :: GROUP_6:15
for G being Group
for x being set
for N being normal Subgroup of G st x in Cosets N holds
x is Subset of G ;

theorem Th16: :: GROUP_6:16
for G being Group
for A1, A2 being Subset of G
for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N
proof end;

definition
let G be Group;
let N be normal Subgroup of G;
func CosOp N -> BinOp of () means :Def3: :: GROUP_6:def 3
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
it . (W1,W2) = A1 * A2;
existence
ex b1 being BinOp of () st
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2
proof end;
uniqueness
for b1, b2 being BinOp of () st ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b2 . (W1,W2) = A1 * A2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines CosOp GROUP_6:def 3 :
for G being Group
for N being normal Subgroup of G
for b3 being BinOp of () holds
( b3 = CosOp N iff for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b3 . (W1,W2) = A1 * A2 );

definition
let G be Group;
let N be normal Subgroup of G;
func G ./. N -> multMagma equals :: GROUP_6:def 4
multMagma(# (),() #);
correctness
coherence
multMagma(# (),() #) is multMagma
;
;
end;

:: deftheorem defines ./. GROUP_6:def 4 :
for G being Group
for N being normal Subgroup of G holds G ./. N = multMagma(# (),() #);

registration
let G be Group;
let N be normal Subgroup of G;
cluster G ./. N -> non empty strict ;
coherence
( G ./. N is strict & not G ./. N is empty )
;
end;

theorem :: GROUP_6:17
for G being Group
for N being normal Subgroup of G holds the carrier of (G ./. N) = Cosets N ;

theorem :: GROUP_6:18
for G being Group
for N being normal Subgroup of G holds the multF of (G ./. N) = CosOp N ;

definition
let G be Group;
let N be normal Subgroup of G;
let S be Element of (G ./. N);
func @ S -> Subset of G equals :: GROUP_6:def 5
S;
coherence
S is Subset of G
by Th15;
end;

:: deftheorem defines @ GROUP_6:def 5 :
for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) holds @ S = S;

theorem :: GROUP_6:19
for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds (@ T1) * (@ T2) = T1 * T2 by Def3;

theorem :: GROUP_6:20
for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds @ (T1 * T2) = (@ T1) * (@ T2) by Def3;

registration
let G be Group;
let N be normal Subgroup of G;
coherence
( G ./. N is associative & G ./. N is Group-like )
proof end;
end;

theorem :: GROUP_6:21
for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) ex a being Element of G st
( S = a * N & S = N * a ) by Th13;

theorem :: GROUP_6:22
for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( N * a is Element of (G ./. N) & a * N is Element of (G ./. N) & carr N is Element of (G ./. N) ) by ;

theorem Th23: :: GROUP_6:23
for G being Group
for x being object
for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) ) by ;

theorem Th24: :: GROUP_6:24
for G being Group
for N being normal Subgroup of G holds 1_ (G ./. N) = carr N
proof end;

theorem Th25: :: GROUP_6:25
for G being Group
for a being Element of G
for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N
proof end;

theorem :: GROUP_6:26
for G being Group
for N being normal Subgroup of G holds card (G ./. N) = Index N ;

theorem :: GROUP_6:27
for G being Group
for N being normal Subgroup of G st Left_Cosets N is finite holds
card (G ./. N) = index N
proof end;

theorem Th28: :: GROUP_6:28
for G being Group
for B being Subgroup of G
for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. ((B,M) *) is Subgroup of G ./. M
proof end;

theorem :: GROUP_6:29
for G being Group
for N, M being strict normal Subgroup of G st M is Subgroup of N holds
N ./. ((N,M) *) is normal Subgroup of G ./. M
proof end;

theorem :: GROUP_6:30
for G being strict Group
for N being strict normal Subgroup of G holds
( G ./. N is commutative Group iff G  is Subgroup of N )
proof end;

Lm1: for G, H being non empty unital multMagma
for f being Function of G,H st ( for a being Element of G holds f . a = 1_ H ) holds
for a, b being Element of G holds f . (a * b) = (f . a) * (f . b)

proof end;

definition
let G, H be non empty multMagma ;
let f be Function of G,H;
attr f is multiplicative means :Def6: :: GROUP_6:def 6
for a, b being Element of G holds f . (a * b) = (f . a) * (f . b);
end;

:: deftheorem Def6 defines multiplicative GROUP_6:def 6 :
for G, H being non empty multMagma
for f being Function of G,H holds
( f is multiplicative iff for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) );

registration
let G, H be non empty unital multMagma ;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V22( the carrier of G) quasi_total multiplicative for Element of bool [: the carrier of G, the carrier of H:];
existence
ex b1 being Function of G,H st b1 is multiplicative
proof end;
end;

definition
let G, H be Group;
mode Homomorphism of G,H is multiplicative Function of G,H;
end;

theorem Th31: :: GROUP_6:31
for G, H being Group
for g being Homomorphism of G,H holds g . (1_ G) = 1_ H
proof end;

registration
let G, H be Group;
cluster Function-like quasi_total multiplicative -> unity-preserving for Element of bool [: the carrier of G, the carrier of H:];
coherence
for b1 being Homomorphism of G,H holds b1 is unity-preserving
by Th31;
end;

theorem Th32: :: GROUP_6:32
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a ") = (g . a) "
proof end;

theorem Th33: :: GROUP_6:33
for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)
proof end;

theorem Th34: :: GROUP_6:34
for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).]
proof end;

theorem :: GROUP_6:35
for G, H being Group
for a1, a2, a3 being Element of G
for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]
proof end;

theorem Th36: :: GROUP_6:36
for n being Element of NAT
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
proof end;

theorem :: GROUP_6:37
for i being Integer
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
proof end;

theorem Th38: :: GROUP_6:38
for G being non empty multMagma holds id the carrier of G is multiplicative ;

theorem Th39: :: GROUP_6:39
for G, H, I being non empty unital multMagma
for h being multiplicative Function of G,H
for h1 being multiplicative Function of H,I holds h1 * h is multiplicative
proof end;

registration
let G, H, I be non empty unital multMagma ;
let h be multiplicative Function of G,H;
let h1 be multiplicative Function of H,I;
cluster h * h1 -> multiplicative for Function of G,I;
coherence
for b1 being Function of G,I st b1 = h1 * h holds
b1 is multiplicative
by Th39;
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);
coherence
G --> (1_ H) is Function of G,H
;
end;

:: deftheorem defines 1: GROUP_6:def 7 :
for G, H being non empty multMagma holds 1: (G,H) = G --> (1_ H);

registration
let G, H be non empty unital multMagma ;
cluster 1: (G,H) -> multiplicative ;
coherence
1: (G,H) is multiplicative
proof end;
end;

theorem :: GROUP_6:40
for G, H, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds
( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) )
proof end;

definition
let G be Group;
let N be normal Subgroup of G;
func nat_hom N -> Function of G,(G ./. N) means :Def8: :: GROUP_6:def 8
for a being Element of G holds it . a = a * N;
existence
ex b1 being Function of G,(G ./. N) st
for a being Element of G holds b1 . a = a * N
proof end;
uniqueness
for b1, b2 being Function of G,(G ./. N) st ( for a being Element of G holds b1 . a = a * N ) & ( for a being Element of G holds b2 . a = a * N ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines nat_hom GROUP_6:def 8 :
for G being Group
for N being normal Subgroup of G
for b3 being Function of G,(G ./. N) holds
( b3 = nat_hom N iff for a being Element of G holds b3 . a = a * N );

registration
let G be Group;
let N be normal Subgroup of G;
coherence
proof end;
end;

definition
let G, H be Group;
let g be Homomorphism of G,H;
func Ker g -> strict Subgroup of G means :Def9: :: GROUP_6:def 9
the carrier of it = { a where a is Element of G : g . a = 1_ H } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H }
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H } & the carrier of b2 = { a where a is Element of G : g . a = 1_ H } holds
b1 = b2
by GROUP_2:59;
end;

:: deftheorem Def9 defines Ker GROUP_6:def 9 :
for G, H being Group
for g being Homomorphism of G,H
for b4 being strict Subgroup of G holds
( b4 = Ker g iff the carrier of b4 = { a where a is Element of G : g . a = 1_ H } );

registration
let G, H be Group;
let g be Homomorphism of G,H;
coherence
Ker g is normal
proof end;
end;

theorem Th41: :: GROUP_6:41
for G, H being Group
for a being Element of G
for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )
proof end;

theorem :: GROUP_6:42
for G, H being strict Group holds Ker (1: (G,H)) = G
proof end;

theorem Th43: :: GROUP_6:43
for G being Group
for N being strict normal Subgroup of G holds Ker () = N
proof end;

definition
let G, H be Group;
let g be Homomorphism of G,H;
func Image g -> strict Subgroup of H means :Def10: :: GROUP_6:def 10
the carrier of it = g .: the carrier of G;
existence
ex b1 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G
proof end;
uniqueness
for b1, b2 being strict Subgroup of H st the carrier of b1 = g .: the carrier of G & the carrier of b2 = g .: the carrier of G holds
b1 = b2
by GROUP_2:59;
end;

:: deftheorem Def10 defines Image GROUP_6:def 10 :
for G, H being Group
for g being Homomorphism of G,H
for b4 being strict Subgroup of H holds
( b4 = Image g iff the carrier of b4 = g .: the carrier of G );

theorem Th44: :: GROUP_6:44
for G, H being Group
for g being Homomorphism of G,H holds rng g = the carrier of ()
proof end;

theorem Th45: :: GROUP_6:45
for G, H being Group
for g being Homomorphism of G,H
for x being object holds
( x in Image g iff ex a being Element of G st x = g . a )
proof end;

theorem :: GROUP_6:46
for G, H being Group
for g being Homomorphism of G,H holds Image g = gr (rng g)
proof end;

theorem :: GROUP_6:47
for G, H being Group holds Image (1: (G,H)) = (1). H
proof end;

theorem Th48: :: GROUP_6:48
for G being Group
for N being normal Subgroup of G holds Image () = G ./. N
proof end;

theorem Th49: :: GROUP_6:49
for G, H being Group
for h being Homomorphism of G,H holds h is Homomorphism of G,()
proof end;

theorem Th50: :: GROUP_6:50
for G, H being Group
for g being Homomorphism of G,H st G is finite holds
Image g is finite
proof end;

registration
let G be finite Group;
let H be Group;
let g be Homomorphism of G,H;
coherence
Image g is finite
by Th50;
end;

Lm2: for A being commutative Group
for a, b being Element of A holds a * b = b * a

;

theorem :: GROUP_6:51
for G, H being Group
for g being Homomorphism of G,H st G is commutative Group holds
Image g is commutative
proof end;

theorem Th52: :: GROUP_6:52
for G, H being Group
for g being Homomorphism of G,H holds card () c= card G
proof end;

theorem :: GROUP_6:53
for G being finite Group
for H being Group
for g being Homomorphism of G,H holds card () <= card G
proof end;

theorem :: GROUP_6:54
for G, H being Group
for c being Element of H
for h being Homomorphism of G,H st h is one-to-one & c in Image h holds
h . ((h ") . c) = c
proof end;

theorem :: GROUP_6:55
for G, H being Group
for h being Homomorphism of G,H st h is one-to-one holds
h " is Homomorphism of (),G
proof end;

theorem Th56: :: GROUP_6:56
for G, H being Group
for h being Homomorphism of G,H holds
( h is one-to-one iff Ker h = (1). G )
proof end;

theorem Th57: :: GROUP_6:57
for G being Group
for H being strict Group
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
proof end;

theorem Th58: :: GROUP_6:58
for G, H being non empty set
for h being Function of G,H st h is onto holds
for c being Element of H ex a being Element of G st h . a = c
proof end;

theorem Th59: :: GROUP_6:59
for G being Group
for N being normal Subgroup of G holds nat_hom N is onto
proof end;

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 ) ) by FUNCT_2:def 3;

theorem :: GROUP_6:61
for G being set
for H being non empty set
for h being Function of G,H st h is bijective holds
( dom h = G & rng h = H ) by ;

theorem Th62: :: GROUP_6:62
for G, H being Group
for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G
proof end;

theorem Th63: :: GROUP_6:63
for G being set
for H being non empty set
for h being Function of G,H
for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective
proof end;

theorem Th64: :: GROUP_6:64
for G being set
for H, I being non empty set
for h being Function of G,H
for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective
proof end;

theorem Th65: :: GROUP_6:65
for G being Group holds nat_hom ((1). G) is bijective
proof end;

definition
let G, H be Group;
pred G,H are_isomorphic means :Def11: :: GROUP_6:def 11
ex h being Homomorphism of G,H st h is bijective ;
reflexivity
for G being Group ex h being Homomorphism of G,G st h is bijective
proof end;
end;

:: deftheorem Def11 defines are_isomorphic GROUP_6:def 11 :
for G, H being Group holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

theorem Th66: :: GROUP_6:66
for G, H being Group st G,H are_isomorphic holds
H,G are_isomorphic
proof end;

definition
let G, H be Group;
:: original: are_isomorphic
redefine pred G,H are_isomorphic ;
symmetry
for G, H being Group st (b1,b2) holds
(b2,b1)
by Th66;
end;

theorem :: GROUP_6:67
for G, H, I being Group st G,H are_isomorphic & H,I are_isomorphic holds
G,I are_isomorphic
proof end;

theorem :: GROUP_6:68
for G, H being Group
for h being Homomorphism of G,H st h is one-to-one holds
G, Image h are_isomorphic
proof end;

theorem Th69: :: GROUP_6:69
for G, H being strict Group st G is trivial & H is trivial holds
G,H are_isomorphic
proof end;

theorem :: GROUP_6:70
for G, H being Group holds (1). G, (1). H are_isomorphic by Th69;

theorem :: GROUP_6:71
for G being Group holds G,G ./. ((1). G) are_isomorphic
proof end;

theorem :: GROUP_6:72
for G being Group holds G ./. () is trivial
proof end;

theorem Th73: :: GROUP_6:73
for G, H being strict Group st G,H are_isomorphic holds
card G = card H
proof end;

theorem Th74: :: GROUP_6:74
for G, H being Group st G,H are_isomorphic & G is finite holds
H is finite
proof end;

theorem :: GROUP_6:75
for G, H being strict Group st G,H are_isomorphic holds
card G = card H by Th73;

theorem :: GROUP_6:76
for G being trivial strict Group
for H being strict Group st G,H are_isomorphic holds
H is trivial
proof end;

theorem :: GROUP_6:77
for G, H being Group st G,H are_isomorphic & G is commutative holds
H is commutative
proof end;

Lm3: for G, H being Group
for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),() st
( h is bijective & g = h * (nat_hom (Ker g)) ) )

proof end;

theorem :: GROUP_6:78
for G, H being Group
for g being Homomorphism of G,H holds G ./. (Ker g), Image g are_isomorphic by Lm3;

:: First isomorphism theorem for groups
theorem :: GROUP_6:79
for G, H being Group
for g being Homomorphism of G,H ex h being Homomorphism of (G ./. (Ker g)),() st
( h is bijective & g = h * (nat_hom (Ker g)) ) by Lm3;

:: Third isomorphism theorem for groups
theorem :: GROUP_6:80
for G being Group
for N being normal Subgroup of G
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 end;

:: Second isomorphism theorem for groups
theorem :: GROUP_6:81
for G being Group
for B being Subgroup of G
for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) *`),B ./. (B /\ N) are_isomorphic
proof end;