let R be Ring; for S being R -homomorphic Ring
for f being Homomorphism of R,S st f is onto holds
R / (ker f),S are_isomorphic
let S be R -homomorphic Ring; for f being Homomorphism of R,S st f is onto holds
R / (ker f),S are_isomorphic
let f be Homomorphism of R,S; ( f is onto implies R / (ker f),S are_isomorphic )
set B = R / (ker f);
set I = ker f;
set T = Image f;
assume AS:
f is onto
; R / (ker f),S are_isomorphic
then A:
rng f = the carrier of S
by FUNCT_2:def 3;
B: rng (canHom f) =
the carrier of (Image f)
by FUNCT_2:def 3
.=
rng f
by defim
;
then reconsider g = canHom f as Function of (R / (ker f)),S by FUNCT_2:6;
g . (1. (R / (ker f))) =
(canHom f) . (1_ (R / (ker f)))
.=
1_ (Image f)
by GROUP_1:def 13
.=
1. S
by defim
;
then C:
( g is additive & g is multiplicative & g is unity-preserving )
by C1, C2;
rng g = the carrier of S
by B, AS, FUNCT_2:def 3;
then
g is onto
by FUNCT_2:def 3;
hence
R / (ker f),S are_isomorphic
by C; verum