let C, D be Category; for F being covariant Functor of (alter C),(alter D) holds F is Functor of C,D
let F be covariant Functor of (alter C),(alter D); F is Functor of C,D
reconsider F1 = F as Function of the carrier' of C, the carrier' of D ;
A1:
( F is identity-preserving & F is multiplicative )
by Def25;
A2:
for a being Object of C ex b being Object of D st F1 . (id a) = id b
A4:
for f being Morphism of C holds
( F1 . (id (dom f)) = id (dom (F1 . f)) & F1 . (id (cod f)) = id (cod (F1 . f)) )
proof
let f be
Morphism of
C;
( F1 . (id (dom f)) = id (dom (F1 . f)) & F1 . (id (cod f)) = id (cod (F1 . f)) )
reconsider f1 =
f as
morphism of
(alter C) ;
reconsider d1 =
id (dom f) as
morphism of
(alter C) ;
dom f = cod (id (dom f))
;
then A5:
f1 |> d1
by CAT_1:15;
A6:
F . d1 is
identity
by Th42, A1;
reconsider d2 =
id (dom (F1 . f)) as
morphism of
(alter D) ;
dom (F1 . f) = cod (id (dom (F1 . f)))
;
then
[(F1 . f),(id (dom (F1 . f)))] in dom the
Comp of
D
by CAT_1:15;
then A7:
F . f1 |> d2
by Def21;
F . d1 =
dom (F . f1)
by A1, A5, A6, Th26
.=
d2
by Th42, A7, Th26
;
hence
F1 . (id (dom f)) = id (dom (F1 . f))
by Def21;
F1 . (id (cod f)) = id (cod (F1 . f))
reconsider c1 =
id (cod f) as
morphism of
(alter C) ;
cod f = dom (id (cod f))
;
then A8:
c1 |> f1
by CAT_1:15;
A9:
F . c1 is
identity
by Th42, A1;
reconsider c2 =
id (cod (F1 . f)) as
morphism of
(alter D) ;
cod (F1 . f) = dom (id (cod (F1 . f)))
;
then
[(id (cod (F1 . f))),(F1 . f)] in dom the
Comp of
D
by CAT_1:15;
then A10:
c2 |> F . f1
by Def21;
F . c1 =
cod (F . f1)
by A1, A8, A9, Th27
.=
c2
by Th42, A10, Th27
;
hence
F1 . (id (cod f)) = id (cod (F1 . f))
by Def21;
verum
end;
for f, g being Morphism of C st dom g = cod f holds
F1 . (g (*) f) = (F1 . g) (*) (F1 . f)
proof
let f,
g be
Morphism of
C;
( dom g = cod f implies F1 . (g (*) f) = (F1 . g) (*) (F1 . f) )
assume A11:
dom g = cod f
;
F1 . (g (*) f) = (F1 . g) (*) (F1 . f)
reconsider f1 =
f,
g1 =
g as
morphism of
(alter C) ;
A12:
[g1,f1] in dom the
composition of
(alter C)
by A11, CAT_1:15;
A13:
g1 |> f1
by A11, CAT_1:15;
A14:
the
composition of
(alter C) . (
g1,
f1)
= g1 (*) f1
by A12, Def2, Def3;
A15:
(
F . g1 = F1 . g &
F . f1 = F1 . f )
by Def21;
A16:
[(F1 . g),(F1 . f)] in dom the
Comp of
D
by A15, Def2, A13, A1;
thus F1 . (g (*) f) =
F1 . ( the Comp of C . (g,f))
by A11, CAT_1:16
.=
F . (g1 (*) f1)
by A14, Def21
.=
(F . g1) (*) (F . f1)
by A13, A1
.=
the
Comp of
D . (
(F1 . g),
(F1 . f))
by A15, Def3, A13, A1
.=
(F1 . g) (*) (F1 . f)
by A16, CAT_1:def 1
;
verum
end;
hence
F is Functor of C,D
by A2, A4, CAT_1:61; verum