let C1, C2 be non empty category; for f being morphism of (Functors (C1,C2)) holds
( f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F] )
set C = Functors (C1,C2);
let f be morphism of (Functors (C1,C2)); ( f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F] )
thus
( f is identity implies ex F being covariant Functor of C1,C2 st f = [[F,F],F] )
( ex F being covariant Functor of C1,C2 st f = [[F,F],F] implies f is identity )proof
assume A1:
f is
identity
;
ex F being covariant Functor of C1,C2 st f = [[F,F],F]
consider F,
F1,
F2 being
covariant Functor of
C1,
C2,
T1 being
natural_transformation of
F1,
F,
T2 being
natural_transformation of
F,
F2 such that A2:
(
f = [[F,F2],T2] &
f = [[F1,F],T1] &
f (*) f = [[F1,F2],(T2 `*` T1)] & ( for
g1,
g2 being
morphism of
C1 st
g2 |> g1 holds
(
T2 . g2 |> T1 . g1 &
(T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) )
by A1, CAT_6:24, Th63;
A3:
(
[F,F2] = [F1,F] &
T1 = T2 )
by A2, XTUPLE_0:1;
then A4:
(
F = F1 &
F = F2 )
by XTUPLE_0:1;
set f1 =
[[F,F],F];
A5:
F is_natural_transformation_of F,
F
by Th61;
A6:
F is_naturally_transformable_to F
by Th61;
then
F is
natural_transformation of
F,
F
by A5, Def26;
then
[[F,F],F] in { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) }
by A6;
then
[[F,F],F] in the
carrier of
(Functors (C1,C2))
by Def28;
then reconsider f1 =
[[F,F],F] as
morphism of
(Functors (C1,C2)) by CAT_6:def 1;
reconsider x2 =
f1 as
Element of the
carrier of
(Functors (C1,C2)) by CAT_6:def 1;
reconsider x3 =
f as
Element of the
carrier of
(Functors (C1,C2)) by CAT_6:def 1;
reconsider x1 =
f as
Element of the
carrier of
(Functors (C1,C2)) by CAT_6:def 1;
ex
F1,
F2,
F3 being
Functor of
C1,
C2 ex
T1 being
natural_transformation of
F1,
F2 ex
T2 being
natural_transformation of
F2,
F3 st
(
x1 = [[F1,F2],T1] &
x2 = [[F2,F3],T2] &
x3 = [[F1,F3],(T2 `*` T1)] )
proof
set F1 =
F;
set F2 =
F;
set F3 =
F;
reconsider T1 =
T1 as
natural_transformation of
F,
F by A3, XTUPLE_0:1;
reconsider T2 =
F as
natural_transformation of
F,
F by A6, A5, Def26;
take
F
;
ex F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F,F3],(T2 `*` T1)] )
take
F
;
ex F3 being Functor of C1,C2 ex T1 being natural_transformation of F,F ex T2 being natural_transformation of F,F3 st
( x1 = [[F,F],T1] & x2 = [[F,F3],T2] & x3 = [[F,F3],(T2 `*` T1)] )
take
F
;
ex T1, T2 being natural_transformation of F,F st
( x1 = [[F,F],T1] & x2 = [[F,F],T2] & x3 = [[F,F],(T2 `*` T1)] )
take
T1
;
ex T2 being natural_transformation of F,F st
( x1 = [[F,F],T1] & x2 = [[F,F],T2] & x3 = [[F,F],(T2 `*` T1)] )
take
T2
;
( x1 = [[F,F],T1] & x2 = [[F,F],T2] & x3 = [[F,F],(T2 `*` T1)] )
thus
x1 = [[F,F],T1]
by A2, A3, XTUPLE_0:1;
( x2 = [[F,F],T2] & x3 = [[F,F],(T2 `*` T1)] )
thus
x2 = [[F,F],T2]
;
x3 = [[F,F],(T2 `*` T1)]
for
x being
object st
x in the
carrier of
C1 holds
T1 . x = (T2 `*` T1) . x
hence
x3 = [[F,F],(T2 `*` T1)]
by A2, A4, FUNCT_2:12;
verum
end;
then
[(KuratowskiPair (f1,f)),f] in { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of (Functors (C1,C2)) : ex F1, F2, F3 being Functor of C1,C2 ex t1 being natural_transformation of F1,F2 ex t2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],t1] & x2 = [[F2,F3],t2] & x3 = [[F1,F3],(t2 `*` t1)] ) }
;
then A9:
[(KuratowskiPair (f1,f)),f] in the
composition of
(Functors (C1,C2))
by Def28;
then A10:
KuratowskiPair (
f1,
f)
in dom the
composition of
(Functors (C1,C2))
by XTUPLE_0:def 12;
then A11:
f1 |> f
by CAT_6:def 2;
A12:
f1 (*) f =
the
composition of
(Functors (C1,C2)) . (
f1,
f)
by A10, CAT_6:def 3, CAT_6:def 2
.=
the
composition of
(Functors (C1,C2)) . (KuratowskiPair (f1,f))
by BINOP_1:def 1
.=
f
by A9, A10, FUNCT_1:def 2
;
take
F
;
f = [[F,F],F]
thus
f = [[F,F],F]
by A12, A11, A1, Th4;
verum
end;
assume
ex F being covariant Functor of C1,C2 st f = [[F,F],F]
; f is identity
then consider F being covariant Functor of C1,C2 such that
A13:
f = [[F,F],F]
;
A14:
for f1 being morphism of (Functors (C1,C2)) st f |> f1 holds
f (*) f1 = f1
proof
let f1 be
morphism of
(Functors (C1,C2));
( f |> f1 implies f (*) f1 = f1 )
assume
f |> f1
;
f (*) f1 = f1
then consider F3,
F1,
F2 being
covariant Functor of
C1,
C2,
T1 being
natural_transformation of
F1,
F3,
T2 being
natural_transformation of
F3,
F2 such that A15:
(
f = [[F3,F2],T2] &
f1 = [[F1,F3],T1] &
f (*) f1 = [[F1,F2],(T2 `*` T1)] & ( for
g1,
g2 being
morphism of
C1 st
g2 |> g1 holds
(
T2 . g2 |> T1 . g1 &
(T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) )
by Th63;
A16:
(
[F,F] = [F3,F2] &
F = T2 )
by A13, A15, XTUPLE_0:1;
then A17:
(
F = F3 &
F = F2 )
by XTUPLE_0:1;
for
x being
object st
x in the
carrier of
C1 holds
T1 . x = (T2 `*` T1) . x
hence
f (*) f1 = f1
by A15, A17, FUNCT_2:12;
verum
end;
then
f is left_identity
by CAT_6:def 4;
then
f is right_identity
by CAT_6:9;
hence
f is identity
by A14, CAT_6:def 4, CAT_6:def 14; verum