let C, B, D be Category; :: thesis: for L being Function of the carrier of C,(Funct B,D)
for M being Function of the carrier of B,(Funct C,D) st ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g) ) holds
ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . f,g = ((L . (cod g)) . f) * ((M . (dom f)) . g)
let L be Function of the carrier of C,(Funct B,D); :: thesis: for M being Function of the carrier of B,(Funct C,D) st ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g) ) holds
ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . f,g = ((L . (cod g)) . f) * ((M . (dom f)) . g)
let M be Function of the carrier of B,(Funct C,D); :: thesis: ( ( for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g) ) implies ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . f,g = ((L . (cod g)) . f) * ((M . (dom f)) . g) )
assume that
A1:
for c being Object of C
for b being Object of B holds (M . b) . (id c) = (L . c) . (id b)
and
A2:
for f being Morphism of B
for g being Morphism of C holds ((M . (cod f)) . g) * ((L . (dom g)) . f) = ((L . (cod g)) . f) * ((M . (dom f)) . g)
; :: thesis: ex S being Functor of [:B,C:],D st
for f being Morphism of B
for g being Morphism of C holds S . f,g = ((L . (cod g)) . f) * ((M . (dom f)) . g)
deffunc H1( Category) -> set = the carrier' of $1;
deffunc H2( Element of H1(B), Element of H1(C)) -> Element of the carrier' of D = ((L . (cod $2)) . $1) * ((M . (dom $1)) . $2);
consider S being Function of [:H1(B),H1(C):],H1(D) such that
A3:
for f being Morphism of B
for g being Morphism of C holds S . f,g = H2(f,g)
from BINOP_1:sch 4();
reconsider T = S as Function of H1([:B,C:]),H1(D) ;
now thus
for
bc being
Object of
[:B,C:] ex
d being
Object of
D st
T . (id bc) = id d
:: thesis: ( ( for fg being Morphism of [:B,C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds
T . (fg2 * fg1) = (T . fg2) * (T . fg1) ) )proof
let bc be
Object of
[:B,C:];
:: thesis: ex d being Object of D st T . (id bc) = id d
consider b being
Object of
B,
c being
Object of
C such that A4:
bc = [b,c]
by DOMAIN_1:9;
consider d being
Object of
D such that A5:
(L . c) . (id b) = id d
by CAT_1:97;
take
d
;
:: thesis: T . (id bc) = id d
Hom d,
d <> {}
by CAT_1:56;
then
(
(id d) * (id d) = (id d) * (id d) &
cod (id c) = c &
dom (id b) = b &
(L . c) . (id b) = (M . b) . (id c) )
by A1, CAT_1:44, CAT_1:def 13;
then
(
((L . (cod (id c))) . (id b)) * ((M . (dom (id b))) . (id c)) = id d &
id bc = [(id b),(id c)] )
by A4, A5, Th41, CAT_1:59;
then
T . (id b),
(id c) = id d
by A3;
hence
T . (id bc) = id d
by A4, Th41;
:: thesis: verum
end; thus
for
fg being
Morphism of
[:B,C:] holds
(
T . (id (dom fg)) = id (dom (T . fg)) &
T . (id (cod fg)) = id (cod (T . fg)) )
:: thesis: for fg1, fg2 being Morphism of [:B,C:] st dom fg2 = cod fg1 holds
T . (fg2 * fg1) = (T . fg2) * (T . fg1)proof
let fg be
Morphism of
[:B,C:];
:: thesis: ( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being
Morphism of
B,
g being
Morphism of
C such that A6:
fg = [f,g]
by DOMAIN_1:9;
set b =
dom f;
set c =
dom g;
set g' =
id (dom g);
set f' =
id (dom f);
A7:
Hom (dom ((M . (dom f)) . g)),
(dom ((M . (dom f)) . g)) <> {}
by CAT_1:56;
id (dom ((L . (cod g)) . f)) =
(L . (cod g)) . (id (dom f))
by CAT_1:98
.=
(M . (dom f)) . (id (cod g))
by A1
.=
id (cod ((M . (dom f)) . g))
by CAT_1:98
;
then A8:
dom ((L . (cod g)) . f) = cod ((M . (dom f)) . g)
by CAT_1:45;
thus T . (id (dom fg)) =
S . (id [(dom f),(dom g)])
by A6, Th38
.=
S . (id (dom f)),
(id (dom g))
by Th41
.=
((L . (cod (id (dom g)))) . (id (dom f))) * ((M . (dom (id (dom f)))) . (id (dom g)))
by A3
.=
((L . (dom g)) . (id (dom f))) * ((M . (dom (id (dom f)))) . (id (dom g)))
by CAT_1:44
.=
((L . (dom g)) . (id (dom f))) * ((M . (dom f)) . (id (dom g)))
by CAT_1:44
.=
((M . (dom f)) . (id (dom g))) * ((M . (dom f)) . (id (dom g)))
by A1
.=
(id (dom ((M . (dom f)) . g))) * ((M . (dom f)) . (id (dom g)))
by CAT_1:98
.=
(id (dom ((M . (dom f)) . g))) * (id (dom ((M . (dom f)) . g)))
by CAT_1:98
.=
(id (dom ((M . (dom f)) . g))) * (id (dom ((M . (dom f)) . g)))
by A7, CAT_1:def 13
.=
id (dom ((M . (dom f)) . g))
by CAT_1:59
.=
id (dom (((L . (cod g)) . f) * ((M . (dom f)) . g)))
by A8, CAT_1:42
.=
id (dom (S . f,g))
by A3
.=
id (dom (T . fg))
by A6
;
:: thesis: T . (id (cod fg)) = id (cod (T . fg))
set b =
cod f;
set c =
cod g;
set g' =
id (cod g);
set f' =
id (cod f);
A9:
Hom (cod ((L . (cod g)) . f)),
(cod ((L . (cod g)) . f)) <> {}
by CAT_1:56;
thus T . (id (cod fg)) =
S . (id [(cod f),(cod g)])
by A6, Th38
.=
S . (id (cod f)),
(id (cod g))
by Th41
.=
((L . (cod (id (cod g)))) . (id (cod f))) * ((M . (dom (id (cod f)))) . (id (cod g)))
by A3
.=
((L . (cod g)) . (id (cod f))) * ((M . (dom (id (cod f)))) . (id (cod g)))
by CAT_1:44
.=
((L . (cod g)) . (id (cod f))) * ((M . (cod f)) . (id (cod g)))
by CAT_1:44
.=
((L . (cod g)) . (id (cod f))) * ((L . (cod g)) . (id (cod f)))
by A1
.=
(id (cod ((L . (cod g)) . f))) * ((L . (cod g)) . (id (cod f)))
by CAT_1:98
.=
(id (cod ((L . (cod g)) . f))) * (id (cod ((L . (cod g)) . f)))
by CAT_1:98
.=
(id (cod ((L . (cod g)) . f))) * (id (cod ((L . (cod g)) . f)))
by A9, CAT_1:def 13
.=
id (cod ((L . (cod g)) . f))
by CAT_1:59
.=
id (cod (((L . (cod g)) . f) * ((M . (dom f)) . g)))
by A8, CAT_1:42
.=
id (cod (S . f,g))
by A3
.=
id (cod (T . fg))
by A6
;
:: thesis: verum
end; let fg1,
fg2 be
Morphism of
[:B,C:];
:: thesis: ( dom fg2 = cod fg1 implies T . (fg2 * fg1) = (T . fg2) * (T . fg1) )assume A10:
dom fg2 = cod fg1
;
:: thesis: T . (fg2 * fg1) = (T . fg2) * (T . fg1)consider f1 being
Morphism of
B,
g1 being
Morphism of
C such that A11:
fg1 = [f1,g1]
by DOMAIN_1:9;
consider f2 being
Morphism of
B,
g2 being
Morphism of
C such that A12:
fg2 = [f2,g2]
by DOMAIN_1:9;
(
[(dom f2),(dom g2)] = dom fg2 &
[(cod f1),(cod g1)] = cod fg1 )
by A11, A12, Th38;
then A13:
(
dom f2 = cod f1 &
dom g2 = cod g1 )
by A10, ZFMISC_1:33;
set f =
f2 * f1;
set g =
g2 * g1;
set L1 =
L . (cod g1);
set L2 =
L . (cod g2);
set M1 =
M . (dom f1);
set M2 =
M . (dom f2);
A14:
(
dom ((L . (cod g2)) . f2) = cod ((L . (cod g2)) . f1) &
dom ((M . (dom f1)) . g2) = cod ((M . (dom f1)) . g1) )
by A13, CAT_1:99;
then A15:
cod (((M . (dom f1)) . g2) * ((M . (dom f1)) . g1)) = cod ((M . (dom f1)) . g2)
by CAT_1:42;
id (dom ((L . (cod g2)) . f1)) =
(L . (cod g2)) . (id (dom f1))
by CAT_1:98
.=
(M . (dom f1)) . (id (cod g2))
by A1
.=
id (cod ((M . (dom f1)) . g2))
by CAT_1:98
;
then A16:
dom ((L . (cod g2)) . f1) = cod ((M . (dom f1)) . g2)
by CAT_1:45;
id (dom ((L . (cod g1)) . f1)) =
(L . (cod g1)) . (id (dom f1))
by CAT_1:98
.=
(M . (dom f1)) . (id (cod g1))
by A1
.=
id (cod ((M . (dom f1)) . g1))
by CAT_1:98
;
then A17:
dom ((L . (cod g1)) . f1) = cod ((M . (dom f1)) . g1)
by CAT_1:45;
id (dom ((M . (dom f2)) . g2)) =
(M . (dom f2)) . (id (dom g2))
by CAT_1:98
.=
(L . (cod g1)) . (id (cod f1))
by A1, A13
.=
id (cod ((L . (cod g1)) . f1))
by CAT_1:98
;
then A18:
dom ((M . (dom f2)) . g2) = cod ((L . (cod g1)) . f1)
by CAT_1:45;
id (dom ((L . (cod g2)) . f2)) =
(L . (cod g2)) . (id (dom f2))
by CAT_1:98
.=
(M . (dom f2)) . (id (cod g2))
by A1
.=
id (cod ((M . (dom f2)) . g2))
by CAT_1:98
;
then A19:
dom ((L . (cod g2)) . f2) = cod ((M . (dom f2)) . g2)
by CAT_1:45;
A20:
cod (((L . (cod g1)) . f1) * ((M . (dom f1)) . g1)) = cod ((L . (cod g1)) . f1)
by A17, CAT_1:42;
thus T . (fg2 * fg1) =
S . (f2 * f1),
(g2 * g1)
by A10, A11, A12, Th40
.=
((L . (cod (g2 * g1))) . (f2 * f1)) * ((M . (dom (f2 * f1))) . (g2 * g1))
by A3
.=
((L . (cod g2)) . (f2 * f1)) * ((M . (dom (f2 * f1))) . (g2 * g1))
by A13, CAT_1:42
.=
((L . (cod g2)) . (f2 * f1)) * ((M . (dom f1)) . (g2 * g1))
by A13, CAT_1:42
.=
(((L . (cod g2)) . f2) * ((L . (cod g2)) . f1)) * ((M . (dom f1)) . (g2 * g1))
by A13, CAT_1:99
.=
(((L . (cod g2)) . f2) * ((L . (cod g2)) . f1)) * (((M . (dom f1)) . g2) * ((M . (dom f1)) . g1))
by A13, CAT_1:99
.=
((L . (cod g2)) . f2) * (((L . (cod g2)) . f1) * (((M . (dom f1)) . g2) * ((M . (dom f1)) . g1)))
by A14, A15, A16, CAT_1:43
.=
((L . (cod g2)) . f2) * ((((L . (cod g2)) . f1) * ((M . (dom f1)) . g2)) * ((M . (dom f1)) . g1))
by A14, A16, CAT_1:43
.=
((L . (cod g2)) . f2) * ((((M . (dom f2)) . g2) * ((L . (cod g1)) . f1)) * ((M . (dom f1)) . g1))
by A2, A13
.=
((L . (cod g2)) . f2) * (((M . (dom f2)) . g2) * (((L . (cod g1)) . f1) * ((M . (dom f1)) . g1)))
by A17, A18, CAT_1:43
.=
(((L . (cod g2)) . f2) * ((M . (dom f2)) . g2)) * (((L . (cod g1)) . f1) * ((M . (dom f1)) . g1))
by A18, A19, A20, CAT_1:43
.=
(((L . (cod g2)) . f2) * ((M . (dom f2)) . g2)) * (S . f1,g1)
by A3
.=
(S . f2,g2) * (T . fg1)
by A3, A11
.=
(T . fg2) * (T . fg1)
by A12
;
:: thesis: verum end;
then reconsider T = T as Functor of [:B,C:],D by CAT_1:96;
take
T
; :: thesis: for f being Morphism of B
for g being Morphism of C holds T . f,g = ((L . (cod g)) . f) * ((M . (dom f)) . g)
thus
for f being Morphism of B
for g being Morphism of C holds T . f,g = ((L . (cod g)) . f) * ((M . (dom f)) . g)
by A3; :: thesis: verum