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