begin
theorem
for
C being
category for
o1,
o2,
o3,
o4 being
object of
for
a being
Morphism of ,
for
b being
Morphism of ,
for
c being
Morphism of ,
for
d being
Morphism of , st
b * a = d * c &
a * (a " ) = idm o2 &
(d " ) * d = idm o4 &
<^o1,o2^> <> {} &
<^o2,o1^> <> {} &
<^o2,o3^> <> {} &
<^o3,o4^> <> {} &
<^o4,o3^> <> {} holds
c * (a " ) = (d " ) * b
theorem
for
A being non
empty transitive AltCatStr for
B,
C being non
empty with_units AltCatStr for
F being
feasible Covariant FunctorStr of
A,
B for
G being
FunctorStr of
B,
C for
o,
o1 being
object of holds
Morph-Map (G * F),
o,
o1 = (Morph-Map G,(F . o),(F . o1)) * (Morph-Map F,o,o1)
theorem
for
A being non
empty transitive AltCatStr for
B,
C being non
empty with_units AltCatStr for
F being
feasible Contravariant FunctorStr of
A,
B for
G being
FunctorStr of
B,
C for
o,
o1 being
object of holds
Morph-Map (G * F),
o,
o1 = (Morph-Map G,(F . o1),(F . o)) * (Morph-Map F,o,o1)
Lm1:
for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
begin
definition
let A,
B,
C be non
empty transitive with_units AltCatStr ;
let F1,
F2 be
covariant Functor of
A,
B;
let t be
transformation of
F1,
F2;
let G be
covariant Functor of
B,
C;
assume A1:
F1 is_transformable_to F2
;
func G * t -> transformation of
G * F1,
G * F2 means :
Def1:
for
o being
object of holds
it . o = G . (t ! o);
existence
ex b1 being transformation of G * F1,G * F2 st
for o being object of holds b1 . o = G . (t ! o)
uniqueness
for b1, b2 being transformation of G * F1,G * F2 st ( for o being object of holds b1 . o = G . (t ! o) ) & ( for o being object of holds b2 . o = G . (t ! o) ) holds
b1 = b2
end;
:: deftheorem Def1 defines * FUNCTOR3:def 1 :
theorem Th11:
definition
let A,
B,
C be non
empty transitive with_units AltCatStr ;
let G1,
G2 be
covariant Functor of
B,
C;
let F be
covariant Functor of
A,
B;
let s be
transformation of
G1,
G2;
assume A1:
G1 is_transformable_to G2
;
func s * F -> transformation of
G1 * F,
G2 * F means :
Def2:
for
o being
object of holds
it . o = s ! (F . o);
existence
ex b1 being transformation of G1 * F,G2 * F st
for o being object of holds b1 . o = s ! (F . o)
uniqueness
for b1, b2 being transformation of G1 * F,G2 * F st ( for o being object of holds b1 . o = s ! (F . o) ) & ( for o being object of holds b2 . o = s ! (F . o) ) holds
b1 = b2
end;
:: deftheorem Def2 defines * FUNCTOR3:def 2 :
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
definition
let A,
B,
C be non
empty transitive with_units AltCatStr ;
let F1,
F2 be
covariant Functor of
A,
B;
let G1,
G2 be
covariant Functor of
B,
C;
let t be
transformation of
F1,
F2;
let s be
transformation of
G1,
G2;
func s (#) t -> transformation of
G1 * F1,
G2 * F2 equals
(s * F2) `*` (G1 * t);
coherence
(s * F2) `*` (G1 * t) is transformation of G1 * F1,G2 * F2
;
end;
:: deftheorem defines (#) FUNCTOR3:def 3 :
theorem Th22:
theorem
theorem
theorem
theorem
theorem
for
A,
B,
C,
D being
category for
F1,
F2 being
covariant Functor of
A,
B for
G1,
G2 being
covariant Functor of
B,
C for
H1,
H2 being
covariant Functor of
C,
D for
t being
transformation of
F1,
F2 for
s being
transformation of
G1,
G2 for
u being
transformation of
H1,
H2 st
F1 is_transformable_to F2 &
G1 is_transformable_to G2 &
H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
Lm2:
now
let A,
B,
C be
category;
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )let F1,
F2 be
covariant Functor of
A,
B;
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )let G1,
G2 be
covariant Functor of
B,
C;
for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )let s be
natural_transformation of
G1,
G2;
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )let t be
natural_transformation of
F1,
F2;
( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )set k =
s (#) t;
assume A1:
F1 is_naturally_transformable_to F2
;
( G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )then A2:
F1 is_transformable_to F2
by FUNCTOR2:def 6;
assume A3:
G1 is_naturally_transformable_to G2
;
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )then A4:
G1 is_transformable_to G2
by FUNCTOR2:def 6;
A5:
now
let a,
b be
object of ;
( <^a,b^> <> {} implies for f being Morphism of , holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a) )assume A6:
<^a,b^> <> {}
;
for f being Morphism of , holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a)A7:
<^((G1 * F1) . a),((G1 * F1) . b)^> <> {}
by A6, FUNCTOR0:def 19;
A8:
(G2 * F2) . a = G2 . (F2 . a)
by FUNCTOR0:34;
then reconsider sF2a =
s ! (F2 . a) as
Morphism of ,
by FUNCTOR0:34;
A9:
(G2 * F2) . b = G2 . (F2 . b)
by FUNCTOR0:34;
then reconsider sF2b =
s ! (F2 . b) as
Morphism of ,
by FUNCTOR0:34;
<^(G1 . (F2 . b)),(G2 . (F2 . b))^> <> {}
by A4, FUNCTOR2:def 1;
then A10:
<^((G1 * F2) . b),((G2 * F2) . b)^> <> {}
by A9, FUNCTOR0:34;
let f be
Morphism of ,;
((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a)A11:
(G1 * F1) . a = G1 . (F1 . a)
by FUNCTOR0:34;
then reconsider G1tbF1f =
G1 . ((t ! b) * (F1 . f)) as
Morphism of ,
by FUNCTOR0:34;
reconsider G1ta =
G1 . (t ! a) as
Morphism of ,
by A11, FUNCTOR0:34;
A12:
<^(G1 . (F1 . a)),(G2 . (F1 . a))^> <> {}
by A4, FUNCTOR2:def 1;
A13:
(G1 * F1) . b = G1 . (F1 . b)
by FUNCTOR0:34;
then reconsider G1tb =
G1 . (t ! b) as
Morphism of ,
by FUNCTOR0:34;
A14:
<^(F1 . b),(F2 . b)^> <> {}
by A2, FUNCTOR2:def 1;
then
<^(G1 . (F1 . b)),(G1 . (F2 . b))^> <> {}
by FUNCTOR0:def 19;
then A15:
<^((G1 * F1) . b),((G1 * F2) . b)^> <> {}
by A13, FUNCTOR0:34;
A16:
<^(F1 . a),(F1 . b)^> <> {}
by A6, FUNCTOR0:def 19;
then A17:
<^(F1 . a),(F2 . b)^> <> {}
by A14, ALTCAT_1:def 4;
reconsider G1F1f =
G1 . (F1 . f) as
Morphism of ,
by A13, FUNCTOR0:34;
A18:
s ! (F2 . a) = (s * F2) . a
by A4, Def2;
A19:
G1 . ((t ! b) * (F1 . f)) =
(G1 . (t ! b)) * (G1 . (F1 . f))
by A14, A16, FUNCTOR0:def 24
.=
G1tb * G1F1f
by A11, A13, FUNCTOR0:34
;
reconsider G2F2f =
G2 . (F2 . f) as
Morphism of ,
by A8, FUNCTOR0:34;
A20:
s ! (F2 . b) = (s * F2) . b
by A4, Def2;
A21:
G1 * F2 is_transformable_to G2 * F2
by A4, Th10;
A22:
<^(F2 . a),(F2 . b)^> <> {}
by A6, FUNCTOR0:def 19;
then A23:
<^(G2 . (F2 . a)),(G2 . (F2 . b))^> <> {}
by FUNCTOR0:def 19;
A24:
<^(F1 . a),(F2 . a)^> <> {}
by A2, FUNCTOR2:def 1;
then A25:
<^(G2 . (F1 . a)),(G2 . (F2 . a))^> <> {}
by FUNCTOR0:def 19;
A26:
G1 * F1 is_transformable_to G1 * F2
by A2, Th10;
hence ((s (#) t) ! b) * ((G1 * F1) . f) =
(((s * F2) ! b) * ((G1 * t) ! b)) * ((G1 * F1) . f)
by A21, FUNCTOR2:def 5
.=
(sF2b * ((G1 * t) ! b)) * ((G1 * F1) . f)
by A21, A20, FUNCTOR2:def 4
.=
(sF2b * G1tb) * ((G1 * F1) . f)
by A2, Th11
.=
(sF2b * G1tb) * G1F1f
by A6, Th6
.=
sF2b * G1tbF1f
by A7, A15, A10, A19, ALTCAT_1:25
.=
(s ! (F2 . b)) * (G1 . ((t ! b) * (F1 . f)))
by A11, A9, FUNCTOR0:34
.=
(G2 . ((t ! b) * (F1 . f))) * (s ! (F1 . a))
by A3, A17, FUNCTOR2:def 7
.=
(G2 . ((F2 . f) * (t ! a))) * (s ! (F1 . a))
by A1, A6, FUNCTOR2:def 7
.=
((G2 . (F2 . f)) * (G2 . (t ! a))) * (s ! (F1 . a))
by A22, A24, FUNCTOR0:def 24
.=
(G2 . (F2 . f)) * ((G2 . (t ! a)) * (s ! (F1 . a)))
by A12, A25, A23, ALTCAT_1:25
.=
(G2 . (F2 . f)) * ((s ! (F2 . a)) * (G1 . (t ! a)))
by A3, A24, FUNCTOR2:def 7
.=
G2F2f * (sF2a * G1ta)
by A11, A8, A9, FUNCTOR0:34
.=
((G2 * F2) . f) * (sF2a * G1ta)
by A6, Th6
.=
((G2 * F2) . f) * (((s * F2) ! a) * G1ta)
by A21, A18, FUNCTOR2:def 4
.=
((G2 * F2) . f) * (((s * F2) ! a) * ((G1 * t) ! a))
by A2, Th11
.=
((G2 * F2) . f) * ((s (#) t) ! a)
by A21, A26, FUNCTOR2:def 5
;
verum
end;
thus
G1 * F1 is_naturally_transformable_to G2 * F2
s (#) t is natural_transformation of G1 * F1,G2 * F2
proof
thus
G1 * F1 is_transformable_to G2 * F2
by A2, A4, Th10;
FUNCTOR2:def 6 ex b1 being transformation of G1 * F1,G2 * F2 st
for b2, b3 being M2(the carrier of A) holds
( <^b2,b3^> = {} or for b4 being M2(<^b2,b3^>) holds (b1 ! b3) * ((G1 * F1) . b4) = ((G2 * F2) . b4) * (b1 ! b2) )
take
s (#) t
;
for b1, b2 being M2(the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) )
thus
for
b1,
b2 being
M2(the
carrier of
A) holds
(
<^b1,b2^> = {} or for
b3 being
M2(
<^b1,b2^>) holds
((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) )
by A5;
verum
end;
hence
s (#) t is
natural_transformation of
G1 * F1,
G2 * F2
by A5, FUNCTOR2:def 7;
verum
end;
theorem Th28:
theorem Th29:
theorem
theorem
for
A,
B,
C being
category for
F1,
F2,
F3 being
covariant Functor of
A,
B for
G1,
G2,
G3 being
covariant Functor of
B,
C for
s being
natural_transformation of
G1,
G2 for
s1 being
natural_transformation of
G2,
G3 for
t being
transformation of
F1,
F2 for
t1 being
transformation of
F2,
F3 st
F1 is_naturally_transformable_to F2 &
F2 is_naturally_transformable_to F3 &
G1 is_naturally_transformable_to G2 &
G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
begin
theorem Th32:
definition
let A,
B be
category;
let F1,
F2 be
covariant Functor of
A,
B;
pred F1,
F2 are_naturally_equivalent means :
Def4:
(
F1 is_naturally_transformable_to F2 &
F2 is_transformable_to F1 & ex
t being
natural_transformation of
F1,
F2 st
for
a being
object of holds
t ! a is
iso );
reflexivity
for F1 being covariant Functor of A,B holds
( F1 is_naturally_transformable_to F1 & F1 is_transformable_to F1 & ex t being natural_transformation of F1,F1 st
for a being object of holds t ! a is iso )
symmetry
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being natural_transformation of F1,F2 st
for a being object of holds t ! a is iso holds
( F2 is_naturally_transformable_to F1 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being object of holds t ! a is iso )
end;
:: deftheorem Def4 defines are_naturally_equivalent FUNCTOR3:def 4 :
:: deftheorem Def5 defines natural_equivalence FUNCTOR3:def 5 :
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
for
A,
B,
C being
category for
F1,
F2 being
covariant Functor of
A,
B for
G1,
G2 being
covariant Functor of
B,
C for
e being
natural_equivalence of
F1,
F2 for
f being
natural_equivalence of
G1,
G2 st
F1,
F2 are_naturally_equivalent &
G1,
G2 are_naturally_equivalent holds
(
G1 * F1,
G2 * F2 are_naturally_equivalent &
f (#) e is
natural_equivalence of
G1 * F1,
G2 * F2 )
:: deftheorem Def6 defines " FUNCTOR3:def 6 :
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem