let C, D be Category; for c being Object of C
for d being Object of D holds id [c,d] = [(id c),(id d)]
let c be Object of C; for d being Object of D holds id [c,d] = [(id c),(id d)]
let d be Object of D; id [c,d] = [(id c),(id d)]
A1: dom [(id c),(id d)] =
[(dom (id c)),(dom (id d))]
by Th22
.=
[c,(dom (id d))]
.=
[c,d]
;
cod [(id c),(id d)] =
[(cod (id c)),(cod (id d))]
by Th22
.=
[c,(cod (id d))]
.=
[c,d]
;
then reconsider m = [(id c),(id d)] as Morphism of [c,d],[c,d] by A1, CAT_1:4;
for b being Object of [:C,D:] holds
( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) )
proof
let b be
Object of
[:C,D:];
( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) )
thus
(
Hom (
[c,d],
b)
<> {} implies for
f being
Morphism of
[c,d],
b holds
f (*) [(id c),(id d)] = f )
( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f )proof
assume A2:
Hom (
[c,d],
b)
<> {}
;
for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f
let f be
Morphism of
[c,d],
b;
f (*) [(id c),(id d)] = f
consider fc being
Morphism of
C,
fd being
Morphism of
D such that A3:
f = [fc,fd]
by DOMAIN_1:1;
A4:
[c,d] =
dom f
by A2, CAT_1:5
.=
[(dom fc),(dom fd)]
by A3, Th22
;
then A5:
c = dom fc
by XTUPLE_0:1;
then A6:
cod (id c) = dom fc
;
A7:
d = dom fd
by A4, XTUPLE_0:1;
then
cod (id d) = dom fd
;
hence f (*) [(id c),(id d)] =
[(fc (*) (id c)),(fd (*) (id d))]
by A3, A6, Th23
.=
[fc,(fd (*) (id d))]
by A5, CAT_1:22
.=
f
by A3, A7, CAT_1:22
;
verum
end;
assume A8:
Hom (
b,
[c,d])
<> {}
;
for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f
let f be
Morphism of
b,
[c,d];
[(id c),(id d)] (*) f = f
consider fc being
Morphism of
C,
fd being
Morphism of
D such that A9:
f = [fc,fd]
by DOMAIN_1:1;
A10:
[c,d] =
cod f
by A8, CAT_1:5
.=
[(cod fc),(cod fd)]
by A9, Th22
;
then A11:
c = cod fc
by XTUPLE_0:1;
then A12:
dom (id c) = cod fc
;
A13:
d = cod fd
by A10, XTUPLE_0:1;
then
dom (id d) = cod fd
;
hence [(id c),(id d)] (*) f =
[((id c) (*) fc),((id d) (*) fd)]
by A9, A12, Th23
.=
[fc,((id d) (*) fd)]
by A11, CAT_1:21
.=
f
by A9, A13, CAT_1:21
;
verum
end;
then
m = id [c,d]
by CAT_1:def 12;
hence
id [c,d] = [(id c),(id d)]
; verum