let C be Category; for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
let a, b be Object of C; ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
thus
( a,b are_isomorphic implies ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) implies a,b are_isomorphic )proof
given f being
Morphism of
a,
b such that A1:
f is
invertible
;
CAT_1:def 20 ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) )
thus
(
Hom (
a,
b)
<> {} &
Hom (
b,
a)
<> {} )
by A1;
ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a )
take
f
;
ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a )
thus
ex
f9 being
Morphism of
b,
a st
(
f * f9 = id b &
f9 * f = id a )
by A1;
verum
end;
assume that
A2:
Hom (a,b) <> {}
and
A3:
Hom (b,a) <> {}
; ( for f being Morphism of a,b
for f9 being Morphism of b,a holds
( not f * f9 = id b or not f9 * f = id a ) or a,b are_isomorphic )
given f being Morphism of a,b such that A4:
ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a )
; a,b are_isomorphic
take
f
; CAT_1:def 20 f is invertible
thus
f is invertible
by A2, A3, A4; verum