let G1, G2 be Group; for N1 being normal Subgroup of G1
for N2 being normal Subgroup of G2
for phi being Homomorphism of G1,G2 st phi is bijective & phi .: the carrier of N1 = the carrier of N2 holds
G1 ./. N1,G2 ./. N2 are_isomorphic
let N1 be normal Subgroup of G1; for N2 being normal Subgroup of G2
for phi being Homomorphism of G1,G2 st phi is bijective & phi .: the carrier of N1 = the carrier of N2 holds
G1 ./. N1,G2 ./. N2 are_isomorphic
let N2 be normal Subgroup of G2; for phi being Homomorphism of G1,G2 st phi is bijective & phi .: the carrier of N1 = the carrier of N2 holds
G1 ./. N1,G2 ./. N2 are_isomorphic
let phi be Homomorphism of G1,G2; ( phi is bijective & phi .: the carrier of N1 = the carrier of N2 implies G1 ./. N1,G2 ./. N2 are_isomorphic )
assume A1:
phi is bijective
; ( not phi .: the carrier of N1 = the carrier of N2 or G1 ./. N1,G2 ./. N2 are_isomorphic )
assume A2:
phi .: the carrier of N1 = the carrier of N2
; G1 ./. N1,G2 ./. N2 are_isomorphic
for g being Element of G1 st g in N1 holds
g in Ker ((nat_hom N2) * phi)
then
N1 is Subgroup of Ker ((nat_hom N2) * phi)
by GROUP_2:58;
then consider phiBar being Homomorphism of (G1 ./. N1),(G2 ./. N2) such that
A3:
(nat_hom N2) * phi = phiBar * (nat_hom N1)
by UniversalPropertyQuotientGroups;
for y being Element of (G2 ./. N2) ex x being Element of (G1 ./. N1) st phiBar . x = y
proof
let y be
Element of
(G2 ./. N2);
ex x being Element of (G1 ./. N1) st phiBar . x = y
consider g2 being
Element of
G2 such that B1:
(
y = g2 * N2 &
y = N2 * g2 )
by GROUP_6:21;
B2:
phi " is
Homomorphism of
G2,
G1
by A1, GROUP_6:62;
then
(phi ") . g2 in G1
by FUNCT_2:5;
then
(nat_hom N1) . ((phi ") . g2) in G1 ./. N1
by FUNCT_2:5;
then consider x being
Element of
(G1 ./. N1) such that B3:
x = (nat_hom N1) . ((phi ") . g2)
;
take
x
;
phiBar . x = y
B4:
(
phi is
one-to-one &
rng phi = the
carrier of
G2 )
by A1, FUNCT_2:def 3;
g2 in G2
;
then
g2 in dom (phi ")
by B2, FUNCT_2:def 1;
then B5:
phi . ((phi ") . g2) =
(phi * (phi ")) . g2
by FUNCT_1:13
.=
(id the carrier of G2) . g2
by B4, FUNCT_2:29
.=
g2
;
thus phiBar . x =
(phiBar * (nat_hom N1)) . ((phi ") . g2)
by B2, B3, FUNCT_2:5, FUNCT_2:15
.=
(nat_hom N2) . (phi . ((phi ") . g2))
by A3, B2, FUNCT_2:5, FUNCT_2:15
.=
y
by B1, B5, GROUP_6:def 8
;
verum
end;
then A4:
phiBar is onto
by GROUP_6:58;
for a, b being Element of (G1 ./. N1) st phiBar . a = phiBar . b holds
a = b
proof
let a,
b be
Element of
(G1 ./. N1);
( phiBar . a = phiBar . b implies a = b )
assume B1:
phiBar . a = phiBar . b
;
a = b
consider x1 being
Element of
G1 such that B2:
(
a = x1 * N1 &
a = N1 * x1 )
by GROUP_6:21;
consider x2 being
Element of
G1 such that B3:
(
b = x2 * N1 &
b = N1 * x2 )
by GROUP_6:21;
B4:
phiBar . a =
phiBar . ((nat_hom N1) . x1)
by B2, GROUP_6:def 8
.=
((nat_hom N2) * phi) . x1
by A3, FUNCT_2:15
.=
(nat_hom N2) . (phi . x1)
by FUNCT_2:15
;
phiBar . b =
phiBar . ((nat_hom N1) . x2)
by B3, GROUP_6:def 8
.=
(phiBar * (nat_hom N1)) . x2
by FUNCT_2:15
.=
(nat_hom N2) . (phi . x2)
by A3, FUNCT_2:15
;
then (phi . x1) * N2 =
(nat_hom N2) . (phi . x2)
by B1, B4, GROUP_6:def 8
.=
(phi . x2) * N2
by GROUP_6:def 8
;
then consider n being
Element of
G2 such that B5:
(
n in N2 &
phi . x1 = (phi . x2) * n )
by Th52;
consider n1 being
object such that B6:
(
n1 in the
carrier of
G1 &
n1 in the
carrier of
N1 &
n = phi . n1 )
by A2, B5, FUNCT_2:64;
reconsider n1 =
n1 as
Element of
G1 by B6;
phi . x1 = phi . (x2 * n1)
by B5, B6, GROUP_6:def 6;
then (x2 ") * x1 =
(x2 ") * (x2 * n1)
by A1, GROUP_6:1
.=
((x2 ") * x2) * n1
by GROUP_1:def 3
.=
(1_ G1) * n1
by GROUP_1:def 5
.=
n1
by GROUP_1:def 4
;
then
(x2 ") * x1 in N1
by B6;
hence
a = b
by B2, B3, GROUP_2:114;
verum
end;
then
phiBar is one-to-one
by GROUP_6:1;
hence
G1 ./. N1,G2 ./. N2 are_isomorphic
by A4, GROUP_6:def 11; verum