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