let A be Category; for f being morphism of (alter A) holds
( f is identity iff ex o being Object of A st f = id o )
let f be morphism of (alter A); ( f is identity iff ex o being Object of A st f = id o )
hereby ( ex o being Object of A st f = id o implies f is identity )
assume A1:
f is
identity
;
ex o being Element of the carrier of A st f = id oA3:
f is
Object of
(alter A)
by A1, Th22;
then A4:
for
f1 being
morphism of
(alter A) holds
( (
f |> f1 implies
f (*) f1 = f1 ) & (
f1 |> f implies
f1 (*) f = f1 ) &
f |> f )
by Th23;
reconsider a1 =
f as
Morphism of
A ;
[a1,a1] in dom the
Comp of
A
by A4, Def2;
then A5:
dom a1 = cod a1
by CAT_1:15;
set o =
dom a1;
reconsider a1 =
a1 as
Morphism of
dom a1,
dom a1 by A5, CAT_1:4;
take o =
dom a1;
f = id o
for
b being
Object of
A holds
( (
Hom (
o,
b)
<> {} implies for
a being
Morphism of
o,
b holds
a (*) a1 = a ) & (
Hom (
b,
o)
<> {} implies for
a being
Morphism of
b,
o holds
a1 (*) a = a ) )
proof
let b be
Object of
A;
( ( Hom (o,b) <> {} implies for a being Morphism of o,b holds a (*) a1 = a ) & ( Hom (b,o) <> {} implies for a being Morphism of b,o holds a1 (*) a = a ) )
thus
(
Hom (
o,
b)
<> {} implies for
f1 being
Morphism of
o,
b holds
f1 (*) a1 = f1 )
( Hom (b,o) <> {} implies for a being Morphism of b,o holds a1 (*) a = a )proof
assume A6:
Hom (
o,
b)
<> {}
;
for f1 being Morphism of o,b holds f1 (*) a1 = f1
let f1 be
Morphism of
o,
b;
f1 (*) a1 = f1
f1 in Hom (
o,
b)
by A6, CAT_1:def 5;
then
(
dom f1 = o &
cod f1 = b )
by CAT_1:1;
then A7:
[f1,a1] in dom the
Comp of
A
by A5, CAT_1:def 6;
reconsider f2 =
f1 as
morphism of
(alter A) ;
f2 (*) f = f2
by A4, A7, Def2;
hence
f1 (*) a1 = f1
by Th41, A7;
verum
end;
assume A8:
Hom (
b,
o)
<> {}
;
for a being Morphism of b,o holds a1 (*) a = a
let f1 be
Morphism of
b,
o;
a1 (*) f1 = f1
f1 in Hom (
b,
o)
by A8, CAT_1:def 5;
then A9:
(
dom f1 = b &
cod f1 = o )
by CAT_1:1;
then A10:
[a1,f1] in dom the
Comp of
A
by CAT_1:def 6;
reconsider f2 =
f1 as
morphism of
(alter A) ;
f |> f2
by A9, CAT_1:def 6;
then
f (*) f2 = f2
by A3, Th23;
hence
a1 (*) f1 = f1
by Th41, A10;
verum
end; hence
f = id o
by CAT_1:def 12;
verum
end;
given o being Object of A such that A11:
f = id o
; f is identity
A12:
for f1 being morphism of (alter A) st f |> f1 holds
f (*) f1 = f1
for f1 being morphism of (alter A) st f1 |> f holds
f1 (*) f = f1
then
f is right_identity
;
hence
f is identity
by A12, Def4; verum