let C be Category; :: thesis: for c being Object of C holds
( c opp is initial iff c is terminal )
let c be Object of C; :: thesis: ( c opp is initial iff c is terminal )
thus
( c opp is initial implies c is terminal )
:: thesis: ( c is terminal implies c opp is initial )proof
assume A1:
c opp is
initial
;
:: thesis: c is terminal
let b be
Object of
C;
:: according to CAT_1:def 15 :: thesis: ( not Hom b,c = {} & ex b1 being Morphism of b,c st
for b2 being Morphism of b,c holds b1 = b2 )
A2:
Hom (c opp ),
(b opp ) <> {}
by A1, CAT_1:def 16;
then consider f being
Morphism of
(C opp ) such that A3:
f in Hom (c opp ),
(b opp )
by SUBSET_1:10;
A4:
(
opp (b opp ) = b &
opp (c opp ) = c )
;
hence A5:
Hom b,
c <> {}
by A3, Th14;
:: thesis: ex b1 being Morphism of b,c st
for b2 being Morphism of b,c holds b1 = b2
consider f being
Morphism of
c opp ,
b opp such that A6:
for
g being
Morphism of
c opp ,
b opp holds
f = g
by A1, CAT_1:def 16;
reconsider f' =
opp f as
Morphism of
b,
c by A2, A4, Th16;
take
f'
;
:: thesis: for b1 being Morphism of b,c holds f' = b1
let g be
Morphism of
b,
c;
:: thesis: f' = g
g opp is
Morphism of
c opp ,
b opp
by A5, Th15;
hence
f' = g
by A6;
:: thesis: verum
end;
assume A7:
c is terminal
; :: thesis: c opp is initial
let b be Object of (C opp ); :: according to CAT_1:def 16 :: thesis: ( not Hom (c opp ),b = {} & ex b1 being Morphism of c opp ,b st
for b2 being Morphism of c opp ,b holds b1 = b2 )
A8:
Hom (opp b),c <> {}
by A7, CAT_1:def 15;
then consider f being Morphism of C such that
A9:
f in Hom (opp b),c
by SUBSET_1:10;
A10:
(opp b) opp = b
;
hence A11:
Hom (c opp ),b <> {}
by A9, Th13; :: thesis: ex b1 being Morphism of c opp ,b st
for b2 being Morphism of c opp ,b holds b1 = b2
consider f being Morphism of opp b,c such that
A12:
for g being Morphism of opp b,c holds f = g
by A7, CAT_1:def 15;
reconsider f' = f opp as Morphism of c opp ,b by A8, A10, Th15;
take
f'
; :: thesis: for b1 being Morphism of c opp ,b holds f' = b1
let g be Morphism of c opp ,b; :: thesis: f' = g
opp g is Morphism of opp b, opp (c opp )
by A11, Th16;
hence
f' = g
by A12; :: thesis: verum