let C be Category; for a, b being Object of C
for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )
let a, b be Object of C; for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )
let f be Morphism of a,b; ( f opp is invertible iff f is invertible )
thus
( f opp is invertible implies f is invertible )
( f is invertible implies f opp is invertible )proof
assume A1:
(
Hom (
(b opp),
(a opp))
<> {} &
Hom (
(a opp),
(b opp))
<> {} )
;
CAT_1:def 16 ( for b1 being Morphism of a opp ,b opp holds
( not (f opp) * b1 = id (a opp) or not b1 * (f opp) = id (b opp) ) or f is invertible )
given gg being
Morphism of
a opp ,
b opp such that A2:
(
(f opp) * gg = id (a opp) &
gg * (f opp) = id (b opp) )
;
f is invertible
thus A3:
(
Hom (
a,
b)
<> {} &
Hom (
b,
a)
<> {} )
by A1, Th4;
CAT_1:def 16 ex b1 being Morphism of b,a st
( f * b1 = id b & b1 * f = id a )
reconsider g =
opp gg as
Morphism of
b,
a ;
take
g
;
( f * g = id b & g * f = id a )
A4:
g opp =
g
by Def6, A3
.=
gg
by Def7, A1
;
thus f * g =
(g opp) * (f opp)
by A3, Lm3
.=
id (b opp)
by A2, A4
.=
id b
by Lm2
;
g * f = id a
thus g * f =
(f opp) * (g opp)
by A3, Lm3
.=
id a
by A2, A4, Lm2
;
verum
end;
assume A5:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; CAT_1:def 16 ( for b1 being Morphism of b,a holds
( not f * b1 = id b or not b1 * f = id a ) or f opp is invertible )
given g being Morphism of b,a such that A6:
( f * g = id b & g * f = id a )
; f opp is invertible
thus
( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} )
by A5, Th4; CAT_1:def 16 ex b1 being Morphism of a opp ,b opp st
( (f opp) * b1 = id (a opp) & b1 * (f opp) = id (b opp) )
take
g opp
; ( (f opp) * (g opp) = id (a opp) & (g opp) * (f opp) = id (b opp) )
thus (f opp) * (g opp) =
g * f
by A5, Lm3
.=
id (a opp)
by A6, Lm2
; (g opp) * (f opp) = id (b opp)
thus (g opp) * (f opp) =
f * g
by A5, Lm3
.=
id (b opp)
by A6, Lm2
; verum