let C, D, E be with_identities CategoryStr ; for F being Functor of C,D
for G being Functor of D,E st F is covariant & G is covariant holds
G (*) F is covariant
let F be Functor of C,D; for G being Functor of D,E st F is covariant & G is covariant holds
G (*) F is covariant
let G be Functor of D,E; ( F is covariant & G is covariant implies G (*) F is covariant )
assume A1:
F is covariant
; ( not G is covariant or G (*) F is covariant )
assume A2:
G is covariant
; G (*) F is covariant
set GF = G (*) F;
for f being morphism of C st f is identity holds
(G (*) F) . f is identity
then A10:
G (*) F is identity-preserving
;
for f1, f2 being morphism of C st f1 |> f2 holds
( (G (*) F) . f1 |> (G (*) F) . f2 & (G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2) )
proof
let f1,
f2 be
morphism of
C;
( f1 |> f2 implies ( (G (*) F) . f1 |> (G (*) F) . f2 & (G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2) ) )
assume A11:
f1 |> f2
;
( (G (*) F) . f1 |> (G (*) F) . f2 & (G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2) )
then A12:
not
C is
empty
;
A15:
(G (*) F) . f1 = G . (F . f1)
by A12, A1, A2, Th34;
A16:
G is
multiplicative
by A2;
F is
multiplicative
by A1;
then A17:
(
F . f1 |> F . f2 &
F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
by A11;
then
(
G . (F . f1) |> G . (F . f2) &
G . ((F . f1) (*) (F . f2)) = (G . (F . f1)) (*) (G . (F . f2)) )
by A16;
hence
(G (*) F) . f1 |> (G (*) F) . f2
by A15, A12, A1, A2, Th34;
(G (*) F) . (f1 (*) f2) = ((G (*) F) . f1) (*) ((G (*) F) . f2)
thus (G (*) F) . (f1 (*) f2) =
G . (F . (f1 (*) f2))
by A12, A1, A2, Th34
.=
(G . (F . f1)) (*) (G . (F . f2))
by A17, A16
.=
((G (*) F) . f1) (*) ((G (*) F) . f2)
by A15, A12, A1, A2, Th34
;
verum
end;
hence
G (*) F is covariant
by A10, Def23; verum