let C1, C2 be category; for F1, F2, T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 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) ) )
let F1, F2 be Functor of C1,C2; for T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 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) ) )
let T be Functor of C1,C2; ( F1 is covariant & F2 is covariant implies ( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 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) ) ) )
assume A1:
( F1 is covariant & F2 is covariant )
; ( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 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) ) )
hereby ( ( for f, f1, f2 being morphism of C1 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) ) ) implies T is_natural_transformation_of F1,F2 )
assume A2:
T is_natural_transformation_of F1,
F2
;
for f, f1, f2 being morphism of C1 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) )let f,
f1,
f2 be
morphism of
C1;
( 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 A3:
(
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 A4:
(
f1 |> f &
f |> f2 )
;
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )hence
(
T . f1 |> F1 . f &
F2 . f |> T . f2 )
by A2;
( T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) )thus T . f =
T . (f1 (*) f)
by A3, A4, Th4
.=
(T . f1) (*) (F1 . f)
by A4, A2
;
T . f = (F2 . f) (*) (T . f2)thus T . f =
T . (f (*) f2)
by A3, A4, Th4
.=
(F2 . f) (*) (T . f2)
by A4, A2
;
verum
end;
assume A5:
for f, f1, f2 being morphism of C1 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) )
; T is_natural_transformation_of F1,F2
for g1, g2 being morphism of C1 st g1 |> g2 holds
( T . g1 |> F1 . g2 & F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )
proof
let g1,
g2 be
morphism of
C1;
( g1 |> g2 implies ( T . g1 |> F1 . g2 & F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) ) )
assume A6:
g1 |> g2
;
( T . g1 |> F1 . g2 & F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )
then A7:
not
C1 is
empty
by CAT_6:1;
then consider f1,
f2 being
morphism of
C1 such that A8:
(
f1 is
identity &
f2 is
identity )
and A9:
(
f1 |> g1 (*) g2 &
g1 (*) g2 |> f2 )
by Th5;
consider g11 being
morphism of
C1 such that A10:
(
dom g1 = g11 &
g1 |> g11 &
g11 is
identity )
by A7, CAT_6:def 18;
f1 |> g1
by A6, A9, Th3;
then A11:
(
T . f1 |> F1 . g1 &
T . g1 = (T . f1) (*) (F1 . g1) )
by A8, A10, A5;
A12:
F1 . g1 |> F1 . g2
by A1, A6, Th13;
hence
T . g1 |> F1 . g2
by A11, Th3;
( F2 . g1 |> T . g2 & T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )
consider g22 being
morphism of
C1 such that A13:
(
cod g2 = g22 &
g22 |> g2 &
g22 is
identity )
by A7, CAT_6:def 19;
g2 |> f2
by A6, A9, Th3;
then A14:
(
F2 . g2 |> T . f2 &
T . g2 = (F2 . g2) (*) (T . f2) )
by A13, A8, A5;
A15:
F2 . g1 |> F2 . g2
by A1, A6, Th13;
hence
F2 . g1 |> T . g2
by A14, Th3;
( T . (g1 (*) g2) = (T . g1) (*) (F1 . g2) & T . (g1 (*) g2) = (F2 . g1) (*) (T . g2) )
thus T . (g1 (*) g2) =
(T . f1) (*) (F1 . (g1 (*) g2))
by A8, A9, A5
.=
(T . f1) (*) ((F1 . g1) (*) (F1 . g2))
by A1, A6, Th13
.=
(T . g1) (*) (F1 . g2)
by A11, A12, Th1
;
T . (g1 (*) g2) = (F2 . g1) (*) (T . g2)
thus T . (g1 (*) g2) =
(F2 . (g1 (*) g2)) (*) (T . f2)
by A8, A9, A5
.=
((F2 . g1) (*) (F2 . g2)) (*) (T . f2)
by A1, A6, Th13
.=
(F2 . g1) (*) (T . g2)
by A14, A15, Th1
;
verum
end;
hence
T is_natural_transformation_of F1,F2
; verum