let C, D be category; :: thesis: for F, F1, F2 being Functor of C,D
for T1 being natural_transformation of F1,F
for T2 being natural_transformation of F,F2 st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
let F, F1, F2 be Functor of C,D; :: thesis: for T1 being natural_transformation of F1,F
for T2 being natural_transformation of F,F2 st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
let T1 be natural_transformation of F1,F; :: thesis: for T2 being natural_transformation of F,F2 st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
let T2 be natural_transformation of F,F2; :: thesis: ( F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant implies ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) ) )
assume A1: ( F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 ) ; :: thesis: ( not F is covariant or not F1 is covariant or not F2 is covariant or ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) ) )
assume A2: ( F is covariant & F1 is covariant & F2 is covariant ) ; :: thesis: ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
per cases ( C is empty or not C is empty ) ;
suppose A3: C is empty ; :: thesis: ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
set T = the natural_transformation of F1,F2;
take the natural_transformation of F1,F2 ; :: thesis: ( the natural_transformation of F1,F2 is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
the natural_transformation of F1,F2 . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
thus ( the natural_transformation of F1,F2 is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
the natural_transformation of F1,F2 . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) ) by A3, CAT_6:1; :: thesis: verum
end;
suppose A4: not C is empty ; :: thesis: ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
then A5: not D is empty by A2, CAT_6:31;
defpred S1[ object , object ] means ex f being morphism of C st
( $1 = f & ( for f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
$2 = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) );
A6: T1 is_natural_transformation_of F1,F by A1, Def26;
A7: T2 is_natural_transformation_of F,F2 by A1, Def26;
A8: for x being object st x in the carrier of C holds
ex y being object st
( y in the carrier of D & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of C implies ex y being object st
( y in the carrier of D & S1[x,y] ) )
assume x in the carrier of C ; :: thesis: ex y being object st
( y in the carrier of D & S1[x,y] )
then reconsider f = x as morphism of C by CAT_6:def 1;
not Ob C is empty by A4;
then ( dom f in Ob C & cod f in Ob C ) ;
then reconsider f1 = dom f, f2 = cod f as morphism of C ;
reconsider y = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) as object ;
take y ; :: thesis: ( y in the carrier of D & S1[x,y] )
not Mor D is empty by A5;
then y in Mor D ;
hence y in the carrier of D by CAT_6:def 1; :: thesis: S1[x,y]
thus S1[x,y] :: thesis: verum
proof
take f ; :: thesis: ( x = f & ( for f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
y = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
thus x = f ; :: thesis: for f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
y = ((T2 . f2) (*) (F . f)) (*) (T1 . f1)
let f1, f2 be morphism of C; :: thesis: ( f1 is identity & f2 is identity & f |> f1 & f2 |> f implies y = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) )
assume ( f1 is identity & f2 is identity & f |> f1 & f2 |> f ) ; :: thesis: y = ((T2 . f2) (*) (F . f)) (*) (T1 . f1)
then ( f1 = dom f & f2 = cod f ) by CAT_6:26, CAT_6:27;
hence y = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ; :: thesis: verum
end;
end;
consider T being Function of the carrier of C, the carrier of D such that
A9: for x being object st x in the carrier of C holds
S1[x,T . x] from FUNCT_2:sch 1(A8);
reconsider T = T as Functor of C,D ;
A10: for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1)
proof
let f, f1, f2 be morphism of C; :: thesis: ( f1 is identity & f2 is identity & f |> f1 & f2 |> f implies T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) )
assume A11: ( f1 is identity & f2 is identity & f |> f1 & f2 |> f ) ; :: thesis: T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1)
not Mor C is empty by A4;
then f in Mor C ;
then A12: f in the carrier of C by CAT_6:def 1;
reconsider x = f as object ;
consider ff being morphism of C such that
A13: ( x = ff & ( for f1, f2 being morphism of C st f1 is identity & f2 is identity & ff |> f1 & f2 |> ff holds
T . x = ((T2 . f2) (*) (F . ff)) (*) (T1 . f1) ) ) by A12, A9;
T . x = ((T2 . f2) (*) (F . ff)) (*) (T1 . f1) by A11, A13;
hence T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) by A4, A13, CAT_6:def 21; :: thesis: verum
end;
A14: for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )
proof
let f, f1, f2 be morphism of C; :: thesis: ( f1 is identity & f2 is identity & f1 |> f & f |> f2 implies ( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )
assume A15: ( f1 is identity & f2 is identity & f1 |> f & f |> f2 ) ; :: thesis: ( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )
A16: ( T1 . f1 |> F1 . f & F . f |> T1 . f2 & T1 . f = (T1 . f1) (*) (F1 . f) & T1 . f = (F . f) (*) (T1 . f2) ) by A2, A15, A6, Th58;
A17: ( T2 . f1 |> F . f & F2 . f |> T2 . f2 & T2 . f = (T2 . f1) (*) (F . f) & T2 . f = (F2 . f) (*) (T2 . f2) ) by A2, A15, A7, Th58;
A18: f1 |> f1 by A4, A15, CAT_6:24;
then A19: T2 . f1 |> F . f1 by A7;
F . f1 |> T1 . f1 by A18, A6;
then dom (F . f1) = cod (T1 . f1) by A5, CAT_7:5;
then dom ((T2 . f1) (*) (F . f1)) = cod (T1 . f1) by A19, CAT_7:4;
then A20: (T2 . f1) (*) (F . f1) |> T1 . f1 by A5, CAT_7:5;
A21: f1 |> f1 by A4, A15, CAT_6:24;
then T . f1 = ((T2 . f1) (*) (F . f1)) (*) (T1 . f1) by A15, A10;
then A22: dom (T . f1) = dom (T1 . f1) by A20, CAT_7:4;
dom (T1 . f1) = cod (F1 . f) by A16, A5, CAT_7:5;
hence T . f1 |> F1 . f by A22, A5, CAT_7:5; :: thesis: ( F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )
A23: f2 |> f2 by A4, A15, CAT_6:24;
then A24: ( T2 . f2 |> F . f2 & F2 . f2 |> T2 . f2 & T2 . f2 = (T2 . f2) (*) (F . f2) & T2 . f2 = (F2 . f2) (*) (T2 . f2) ) by A2, A7, A15, Th58;
A25: ( T1 . f2 |> F1 . f2 & F . f2 |> T1 . f2 & T1 . f2 = (T1 . f2) (*) (F1 . f2) & T1 . f2 = (F . f2) (*) (T1 . f2) ) by A2, A23, A6, A15, Th58;
A26: ( D is left_composable & D is right_composable ) by CAT_6:def 11;
A27: T2 . f2 |> (F . f2) (*) (T1 . f2) by A24, A25, A26, CAT_6:def 9;
A28: f2 |> f2 by A4, A15, CAT_6:24;
then T . f2 = ((T2 . f2) (*) (F . f2)) (*) (T1 . f2) by A15, A10;
then A29: cod (T . f2) = cod (T2 . f2) by A24, A25, A27, CAT_7:4;
F2 . f |> T2 . f2 by A15, A7;
then cod (T2 . f2) = dom (F2 . f) by A5, CAT_7:5;
hence F2 . f |> T . f2 by A29, A5, CAT_7:5; :: thesis: ( T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )
A30: ( F is identity-preserving & F is multiplicative ) by A2, CAT_6:def 25;
A31: F . f = F . (f (*) f2) by A15, CAT_6:def 14, CAT_6:def 5
.= (F . f) (*) (F . f2) by A30, A15, CAT_6:def 23 ;
A32: T2 . f1 |> F . f1 by A18, A7;
A33: F . f1 |> T1 . f1 by A18, A6;
A34: F . f1 |> F . f by A30, A15, CAT_6:def 23;
A35: F . f |> F . f2 by A30, A15, CAT_6:def 23;
A36: F2 . f |> T2 . f2 by A15, A7;
A37: T2 . f2 |> F . f2 by A23, A7;
thus T . f = ((T2 . f1) (*) ((F . f) (*) (F . f2))) (*) (T1 . f2) by A10, A15, A31
.= (((T2 . f1) (*) (F . f1)) (*) (F . f)) (*) (T1 . f2) by A2, A31, A15, A18, A7, Th58
.= ((T2 . f1) (*) (F . f1)) (*) ((F . f) (*) (T1 . f2)) by A32, A34, A16, Th2
.= (((T2 . f1) (*) (F . f1)) (*) (T1 . f1)) (*) (F1 . f) by A32, A33, A16, Th2
.= (T . f1) (*) (F1 . f) by A21, A15, A10 ; :: thesis: T . f = (F2 . f) (*) (T . f2)
thus T . f = ((T2 . f1) (*) ((F . f) (*) (F . f2))) (*) (T1 . f2) by A10, A15, A31
.= (((F2 . f) (*) (T2 . f2)) (*) (F . f2)) (*) (T1 . f2) by A17, A35, A25, Th2
.= (F2 . f) (*) (((T2 . f2) (*) (F . f2)) (*) (T1 . f2)) by A25, A36, A37, Th2
.= (F2 . f) (*) (T . f2) by A28, A15, A10 ; :: thesis: verum
end;
then A38: T is_natural_transformation_of F1,F2 by A2, Th58;
then F1 is_naturally_transformable_to F2 ;
then reconsider T = T as natural_transformation of F1,F2 by A38, Def26;
take T ; :: thesis: ( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )
thus ( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) ) by A2, A14, A10, Th58; :: thesis: verum
end;
end;