let A, B, C be Category; for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F
let G be Functor of A, Functors (B,C); ex F being Functor of [:A,B:],C st G = export F
defpred S1[ object , object ] means for f being Morphism of A
for g being Morphism of B st $1 = [f,g] holds
for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
$2 = (t . (cod g)) (*) (f1 . g);
A1:
now for m being object st m in the carrier' of [:A,B:] holds
ex o being object st
( o in the carrier' of C & S1[m,o] )let m be
object ;
( m in the carrier' of [:A,B:] implies ex o being object st
( o in the carrier' of C & S1[m,o] ) )assume
m in the
carrier' of
[:A,B:]
;
ex o being object st
( o in the carrier' of C & S1[m,o] )then consider m1 being
Morphism of
A,
m2 being
Morphism of
B such that A2:
m = [m1,m2]
by CAT_2:27;
consider F1,
F2 being
Functor of
B,
C,
t1 being
natural_transformation of
F1,
F2 such that
F1 is_naturally_transformable_to F2
and
dom (G . m1) = F1
and
cod (G . m1) = F2
and A3:
G . m1 = [[F1,F2],t1]
by Th6;
reconsider o =
(t1 . (cod m2)) (*) (F1 . m2) as
object ;
take o =
o;
( o in the carrier' of C & S1[m,o] )thus
o in the
carrier' of
C
;
S1[m,o]thus
S1[
m,
o]
verumproof
let f be
Morphism of
A;
for g being Morphism of B st m = [f,g] holds
for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g)let g be
Morphism of
B;
( m = [f,g] implies for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g) )
assume A4:
m = [f,g]
;
for f1, f2 being Functor of B,C
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g)
then A5:
g = m2
by A2, XTUPLE_0:1;
let f1,
f2 be
Functor of
B,
C;
for t being natural_transformation of f1,f2 st G . f = [[f1,f2],t] holds
o = (t . (cod g)) (*) (f1 . g)let t be
natural_transformation of
f1,
f2;
( G . f = [[f1,f2],t] implies o = (t . (cod g)) (*) (f1 . g) )
assume A6:
G . f = [[f1,f2],t]
;
o = (t . (cod g)) (*) (f1 . g)
A7:
f = m1
by A2, A4, XTUPLE_0:1;
then
[F1,F2] = [f1,f2]
by A3, A6, XTUPLE_0:1;
then
(
F1 = f1 &
F2 = f2 )
by XTUPLE_0:1;
hence
o = (t . (cod g)) (*) (f1 . g)
by A3, A7, A5, A6, XTUPLE_0:1;
verum
end; end;
consider F being Function of the carrier' of [:A,B:], the carrier' of C such that
A8:
for m being object st m in the carrier' of [:A,B:] holds
S1[m,F . m]
from FUNCT_2:sch 1(A1);
F is Functor of [:A,B:],C
proof
thus
for
ab being
Object of
[:A,B:] ex
c being
Object of
C st
F . (id ab) = id c
ISOCAT_1:def 1 ( ( for b1 being Element of the carrier' of [:A,B:] holds
( F . (id (dom b1)) = id (dom (F . b1)) & F . (id (cod b1)) = id (cod (F . b1)) ) ) & ( for b1, b2 being Element of the carrier' of [:A,B:] holds
( not dom b2 = cod b1 or F . (b2 (*) b1) = (F . b2) (*) (F . b1) ) ) )proof
let ab be
Object of
[:A,B:];
ex c being Object of C st F . (id ab) = id c
consider a being
Object of
A,
b being
Object of
B such that A9:
ab = [a,b]
by CAT_2:25;
reconsider H =
G . a as
Functor of
B,
C by Th5;
take
H . b
;
F . (id ab) = id (H . b)
A10:
Hom (
(H . b),
(H . b))
<> {}
;
A11:
G . (id a) =
id (G . a)
by CAT_1:71
.=
[[H,H],(id H)]
by NATTRA_1:def 17
;
id ab = [(id a),(id b)]
by A9, CAT_2:31;
hence F . (id ab) =
((id H) . (cod (id b))) (*) (H . (id b))
by A8, A11
.=
((id H) . (cod (id b))) (*) (id (H . b))
by CAT_1:71
.=
((id H) . b) (*) (id (H . b))
.=
(id (H . b)) (*) (id (H . b))
by NATTRA_1:20
.=
(id (H . b)) * (id (H . b))
by A10, CAT_1:def 13
.=
id (H . b)
;
verum
end;
thus
for
f being
Morphism of
[:A,B:] holds
(
F . (id (dom f)) = id (dom (F . f)) &
F . (id (cod f)) = id (cod (F . f)) )
for b1, b2 being Element of the carrier' of [:A,B:] holds
( not dom b2 = cod b1 or F . (b2 (*) b1) = (F . b2) (*) (F . b1) )proof
let f be
Morphism of
[:A,B:];
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )
consider f1 being
Morphism of
A,
f2 being
Morphism of
B such that A12:
f = [f1,f2]
by CAT_2:27;
reconsider H =
G . (dom f1) as
Functor of
B,
C by Th5;
A13:
Hom (
(dom (H . f2)),
(dom (H . f2)))
<> {}
;
A14:
(
id (G . (dom f1)) = [[H,H],(id H)] &
G . (id (dom f1)) = id (G . (dom f1)) )
by CAT_1:71, NATTRA_1:def 17;
consider F1,
F2 being
Functor of
B,
C,
t being
natural_transformation of
F1,
F2 such that A15:
F1 is_naturally_transformable_to F2
and A16:
dom (G . f1) = F1
and A17:
cod (G . f1) = F2
and A18:
G . f1 = [[F1,F2],t]
by Th6;
A19:
F1 . (cod f2) = cod (F1 . f2)
by CAT_1:72;
Hom (
(F1 . (cod f2)),
(F2 . (cod f2)))
<> {}
by A15, ISOCAT_1:25;
then A20:
dom (t . (cod f2)) = cod (F1 . f2)
by A19, CAT_1:5;
A21:
F1 = H
by A16, CAT_1:72;
id (dom f) =
id [(dom f1),(dom f2)]
by A12, CAT_2:28
.=
[(id (dom f1)),(id (dom f2))]
by CAT_2:31
;
hence F . (id (dom f)) =
((id H) . (cod (id (dom f2)))) (*) (H . (id (dom f2)))
by A8, A14
.=
((id H) . (cod (id (dom f2)))) (*) (id (H . (dom f2)))
by CAT_1:71
.=
((id H) . (cod (id (dom f2)))) (*) (id (dom (H . f2)))
by CAT_1:72
.=
((id H) . (dom f2)) (*) (id (dom (H . f2)))
.=
(id (H . (dom f2))) (*) (id (dom (H . f2)))
by NATTRA_1:20
.=
(id (dom (H . f2))) (*) (id (dom (H . f2)))
by CAT_1:72
.=
(id (dom (H . f2))) * (id (dom (H . f2)))
by A13, CAT_1:def 13
.=
id (dom (F1 . f2))
by A21
.=
id (dom ((t . (cod f2)) (*) (F1 . f2)))
by A20, CAT_1:17
.=
id (dom (F . f))
by A8, A12, A18
;
F . (id (cod f)) = id (cod (F . f))
reconsider H =
G . (cod f1) as
Functor of
B,
C by Th5;
A22:
F2 = H
by A17, CAT_1:72;
A23:
Hom (
(cod (H . f2)),
(cod (H . f2)))
<> {}
;
A24:
id (cod f) =
id [(cod f1),(cod f2)]
by A12, CAT_2:28
.=
[(id (cod f1)),(id (cod f2))]
by CAT_2:31
;
A25:
Hom (
(F1 . (cod f2)),
(F2 . (cod f2)))
<> {}
by A15, ISOCAT_1:25;
F1 . (cod f2) = cod (F1 . f2)
by CAT_1:72;
then A26:
dom (t . (cod f2)) = cod (F1 . f2)
by A25, CAT_1:5;
(
id (G . (cod f1)) = [[H,H],(id H)] &
G . (id (cod f1)) = id (G . (cod f1)) )
by CAT_1:71, NATTRA_1:def 17;
hence F . (id (cod f)) =
((id H) . (cod (id (cod f2)))) (*) (H . (id (cod f2)))
by A8, A24
.=
((id H) . (cod (id (cod f2)))) (*) (id (H . (cod f2)))
by CAT_1:71
.=
((id H) . (cod (id (cod f2)))) (*) (id (cod (H . f2)))
by CAT_1:72
.=
((id H) . (cod f2)) (*) (id (cod (H . f2)))
.=
(id (H . (cod f2))) (*) (id (cod (H . f2)))
by NATTRA_1:20
.=
(id (cod (H . f2))) (*) (id (cod (H . f2)))
by CAT_1:72
.=
(id (cod (H . f2))) * (id (cod (H . f2)))
by A23, CAT_1:def 13
.=
id (cod (H . f2))
.=
id (F2 . (cod f2))
by A22, CAT_1:72
.=
id (cod (t . (cod f2)))
by A25, CAT_1:5
.=
id (cod ((t . (cod f2)) (*) (F1 . f2)))
by A26, CAT_1:17
.=
id (cod (F . f))
by A8, A12, A18
;
verum
end;
let f,
g be
Morphism of
[:A,B:];
( not dom g = cod f or F . (g (*) f) = (F . g) (*) (F . f) )
assume A27:
dom g = cod f
;
F . (g (*) f) = (F . g) (*) (F . f)
consider g1 being
Morphism of
A,
g2 being
Morphism of
B such that A28:
g = [g1,g2]
by CAT_2:27;
reconsider g29 =
g2 as
Morphism of
dom g2,
cod g2 by CAT_1:4;
consider f1 being
Morphism of
A,
f2 being
Morphism of
B such that A29:
f = [f1,f2]
by CAT_2:27;
A30:
[(cod f1),(cod f2)] = cod f
by A29, CAT_2:28;
consider G1,
G2 being
Functor of
B,
C,
s being
natural_transformation of
G1,
G2 such that A31:
G1 is_naturally_transformable_to G2
and A32:
dom (G . g1) = G1
and
cod (G . g1) = G2
and A33:
G . g1 = [[G1,G2],s]
by Th6;
consider F1,
F2 being
Functor of
B,
C,
t being
natural_transformation of
F1,
F2 such that A34:
F1 is_naturally_transformable_to F2
and
dom (G . f1) = F1
and A35:
cod (G . f1) = F2
and A36:
G . f1 = [[F1,F2],t]
by Th6;
A37:
F . f = (t . (cod f2)) (*) (F1 . f2)
by A8, A29, A36;
A38:
[(dom g1),(dom g2)] = dom g
by A28, CAT_2:28;
then A39:
cod f1 = dom g1
by A27, A30, XTUPLE_0:1;
then reconsider s =
s as
natural_transformation of
F2,
G2 by A35, A32, CAT_1:64;
A40:
cod f2 = dom g2
by A27, A30, A38, XTUPLE_0:1;
then A41:
g (*) f = [(g1 (*) f1),(g2 (*) f2)]
by A29, A28, A39, CAT_2:29;
reconsider f29 =
f2 as
Morphism of
dom f2,
dom g2 by A40, CAT_1:4;
A42:
cod (g2 (*) f2) = cod g2
by A40, CAT_1:17;
A43:
Hom (
(dom f2),
(dom g2))
<> {}
by A40, CAT_1:2;
then A44:
Hom (
(F1 . (dom f2)),
(F1 . (dom g2)))
<> {}
by CAT_1:84;
A45:
Hom (
(F1 . (dom g2)),
(F2 . (dom g2)))
<> {}
by A34, ISOCAT_1:25;
then A46:
Hom (
(F1 . (dom f2)),
(F2 . (dom g2)))
<> {}
by A44, CAT_1:24;
A47:
Hom (
(dom g2),
(cod g2))
<> {}
by CAT_1:2;
then A48:
F1 /. g2 = F1 /. g29
by CAT_3:def 10;
A49:
F2 = G1
by A35, A32, A39, CAT_1:64;
then A50:
Hom (
(F2 . (cod g2)),
(G2 . (cod g2)))
<> {}
by A31, ISOCAT_1:25;
A51:
G1 /. g2 = F2 /. g29
by A49, A47, CAT_3:def 10;
A52:
Hom (
(F2 . (dom g2)),
(F2 . (cod g2)))
<> {}
by A47, CAT_1:84;
then A53:
Hom (
(F2 . (dom g2)),
(G2 . (cod g2)))
<> {}
by A50, CAT_1:24;
A54:
Hom (
(F1 . (dom g2)),
(F1 . (cod g2)))
<> {}
by A47, CAT_1:84;
then A55:
Hom (
(F1 . (dom f2)),
(F1 . (cod g2)))
<> {}
by A44, CAT_1:24;
A56:
Hom (
(F1 . (cod g2)),
(F2 . (cod g2)))
<> {}
by A34, ISOCAT_1:25;
then A57:
Hom (
(F1 . (cod g2)),
(G2 . (cod g2)))
<> {}
by A50, CAT_1:24;
A58:
F1 /. f2 = F1 /. f29
by A43, CAT_3:def 10;
G . (g1 (*) f1) =
(G . g1) (*) (G . f1)
by A39, CAT_1:64
.=
[[F1,G2],(s `*` t)]
by A36, A33, A49, NATTRA_1:36
;
hence F . (g (*) f) =
((s `*` t) . (cod (g2 (*) f2))) (*) (F1 . (g2 (*) f2))
by A8, A41
.=
((s . (cod g2)) * (t . (cod g2))) (*) (F1 . (g2 (*) f2))
by A34, A31, A49, A42, NATTRA_1:25
.=
((s . (cod g2)) * (t . (cod g2))) (*) ((F1 /. g2) (*) (F1 /. f2))
by A40, CAT_1:64
.=
((s . (cod g2)) * (t . (cod g2))) (*) ((F1 /. g29) * (F1 /. f29))
by A44, A54, A48, A58, CAT_1:def 13
.=
((s . (cod g2)) * (t . (cod g2))) * ((F1 /. g29) * (F1 /. f29))
by A55, A57, CAT_1:def 13
.=
(s . (cod g2)) * ((t . (cod g2)) * ((F1 /. g29) * (F1 /. f29)))
by A50, A56, A55, CAT_1:25
.=
(s . (cod g2)) * (((t . (cod g2)) * (F1 /. g29)) * (F1 /. f29))
by A56, A44, A54, CAT_1:25
.=
(s . (cod g2)) * (((F2 /. g29) * (t . (dom g2))) * (F1 /. f29))
by A34, A47, NATTRA_1:def 8
.=
(s . (cod g2)) * ((F2 /. g29) * ((t . (dom g2)) * (F1 /. f29)))
by A44, A52, A45, CAT_1:25
.=
((s . (cod g2)) * (F2 /. g29)) * ((t . (dom g2)) * (F1 /. f29))
by A50, A52, A46, CAT_1:25
.=
((s . (cod g2)) * (F2 /. g29)) (*) ((t . (dom g2)) * (F1 /. f29))
by A46, A53, CAT_1:def 13
.=
((s . (cod g2)) * (F2 /. g29)) (*) ((t . (cod f2)) (*) (F1 . f2))
by A40, A44, A45, A58, CAT_1:def 13
.=
((s . (cod g2)) (*) (G1 /. g2)) (*) ((t . (cod f2)) (*) (F1 . f2))
by A50, A52, A51, CAT_1:def 13
.=
(F . g) (*) (F . f)
by A8, A28, A33, A49, A37
;
verum
end;
then reconsider F = F as Functor of [:A,B:],C ;
take
F
; G = export F
now for f being Morphism of A holds G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]let f be
Morphism of
A;
G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]consider f1,
f2 being
Functor of
B,
C,
t being
natural_transformation of
f1,
f2 such that A59:
f1 is_naturally_transformable_to f2
and A60:
dom (G . f) = f1
and A61:
cod (G . f) = f2
and A62:
G . f = [[f1,f2],t]
by Th6;
then A66:
f1 = F ?- (dom f)
by FUNCT_2:63;
then A70:
f2 = F ?- (cod f)
by FUNCT_2:63;
hence
G . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]
by A59, A62, A66, A70, ISOCAT_1:26;
verum end;
hence
G = export F
by Def4; verum