begin
theorem Th1:
definition
let A,
B be non
empty set ;
let A1 be non
empty Subset of
A;
let B1 be non
empty Subset of
B;
let f be
PartFunc of
[:A1,A1:],
A1;
let g be
PartFunc of
[:B1,B1:],
B1;
|:redefine func |:f,g:| -> PartFunc of
[:[:A1,B1:],[:A1,B1:]:],
[:A1,B1:];
coherence
|:f,g:| is PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:]
by FUNCT_4:62;
end;
theorem Th2:
for
A1,
A2 being non
empty set for
Y1 being non
empty Subset of
A1 for
Y2 being non
empty Subset of
A2 for
f being
PartFunc of
[:A1,A1:],
A1 for
g being
PartFunc of
[:A2,A2:],
A2 for
F being
PartFunc of
[:Y1,Y1:],
Y1 st
F = f || Y1 holds
for
G being
PartFunc of
[:Y2,Y2:],
Y2 st
G = g || Y2 holds
|:F,G:| = |:f,g:| || [:Y1,Y2:]
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
for
A being
Category for
O being non
empty Subset of the
carrier of
A for
M being non
empty Subset of the
carrier' of
A for
DOM,
COD being
Function of
M,
O st
DOM = the
Source of
A | M &
COD = the
Target of
A | M holds
for
COMP being
PartFunc of
[:M,M:],
M st
COMP = the
Comp of
A || M holds
for
ID being
Function of
O,
M st
ID = the
Id of
A | O holds
CatStr(#
O,
M,
DOM,
COD,
COMP,
ID #) is
Subcategory of
A
theorem Th10:
begin
:: deftheorem Def1 defines . NATTRA_1:def 1 :
theorem
theorem
theorem Th13:
theorem
theorem Th15:
theorem
theorem Th17:
begin
:: deftheorem Def2 defines is_transformable_to NATTRA_1:def 2 :
theorem
canceled;
theorem Th19:
:: deftheorem Def3 defines transformation NATTRA_1:def 3 :
:: deftheorem Def4 defines id NATTRA_1:def 4 :
:: deftheorem Def5 defines . NATTRA_1:def 5 :
definition
let A,
B be
Category;
let F,
F1,
F2 be
Functor of
A,
B;
assume that A1:
F is_transformable_to F1
and A2:
F1 is_transformable_to F2
;
let t1 be
transformation of
F,
F1;
let t2 be
transformation of
F1,
F2;
func t2 `*` t1 -> transformation of
F,
F2 means :
Def6:
for
a being
Object of
A holds
it . a = (t2 . a) * (t1 . a);
existence
ex b1 being transformation of F,F2 st
for a being Object of A holds b1 . a = (t2 . a) * (t1 . a)
uniqueness
for b1, b2 being transformation of F,F2 st ( for a being Object of A holds b1 . a = (t2 . a) * (t1 . a) ) & ( for a being Object of A holds b2 . a = (t2 . a) * (t1 . a) ) holds
b1 = b2
end;
:: deftheorem Def6 defines `*` NATTRA_1:def 6 :
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
begin
Lm1:
for B, A being Category
for F being Functor of A,B
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F . f) = (F . f) * ((id F) . a)
definition
let A,
B be
Category;
let F1,
F2 be
Functor of
A,
B;
pred F1 is_naturally_transformable_to F2 means :
Def7:
(
F1 is_transformable_to F2 & ex
t being
transformation of
F1,
F2 st
for
a,
b being
Object of
A st
Hom a,
b <> {} holds
for
f being
Morphism of
a,
b holds
(t . b) * (F1 . f) = (F2 . f) * (t . a) );
reflexivity
for F1 being Functor of A,B holds
( F1 is_transformable_to F1 & ex t being transformation of F1,F1 st
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 . f) = (F1 . f) * (t . a) )
end;
:: deftheorem Def7 defines is_naturally_transformable_to NATTRA_1:def 7 :
Lm2:
for B, A being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F . f) = (F1 . f) * (t1 . a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a) ) holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
theorem
canceled;
theorem Th25:
definition
let A,
B be
Category;
let F1,
F2 be
Functor of
A,
B;
assume A1:
F1 is_naturally_transformable_to F2
;
mode natural_transformation of
F1,
F2 -> transformation of
F1,
F2 means :
Def8:
for
a,
b being
Object of
A st
Hom a,
b <> {} holds
for
f being
Morphism of
a,
b holds
(it . b) * (F1 . f) = (F2 . f) * (it . a);
existence
ex b1 being transformation of F1,F2 st
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (b1 . b) * (F1 . f) = (F2 . f) * (b1 . a)
by A1, Def7;
end;
:: deftheorem Def8 defines natural_transformation NATTRA_1:def 8 :
:: deftheorem Def9 defines `*` NATTRA_1:def 9 :
theorem Th26:
theorem Th27:
theorem Th28:
:: deftheorem Def10 defines invertible NATTRA_1:def 10 :
:: deftheorem Def11 defines are_naturally_equivalent NATTRA_1:def 11 :
Lm3:
for A, B being Category
for F1, F2 being Functor of A,B
for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is invertible holds
F2 is_transformable_to F1
:: deftheorem Def12 defines " NATTRA_1:def 12 :
Lm4:
now
let A,
B be
Category;
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 " ) . a)let F1,
F2 be
Functor of
A,
B;
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 " ) . a)let t1 be
natural_transformation of
F1,
F2;
( F1 is_naturally_transformable_to F2 & t1 is invertible implies for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 " ) . a) )assume that A1:
F1 is_naturally_transformable_to F2
and A2:
t1 is
invertible
;
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 " ) . a)let a,
b be
Object of
A;
( Hom a,b <> {} implies for f being Morphism of a,b holds ((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 " ) . a) )assume A3:
Hom a,
b <> {}
;
for f being Morphism of a,b holds ((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 " ) . a)A4:
Hom (F1 . a),
(F1 . b) <> {}
by A3, CAT_1:126;
let f be
Morphism of
a,
b;
((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 " ) . a)A5:
Hom (F2 . a),
(F2 . b) <> {}
by A3, CAT_1:126;
A6:
F1 is_transformable_to F2
by A1, Def7;
then A7:
Hom (F1 . b),
(F2 . b) <> {}
by Def2;
A8:
t1 . b is
invertible
by A2, Def10;
then A9:
Hom (F2 . b),
(F1 . b) <> {}
by A7, CAT_1:70;
A10:
Hom (F1 . a),
(F2 . a) <> {}
by A6, Def2;
(F2 . f) * (t1 . a) = (t1 . b) * (F1 . f)
by A1, A3, Def8;
then A11:
(((t1 . b) " ) * (F2 . f)) * (t1 . a) =
((t1 . b) " ) * ((t1 . b) * (F1 . f))
by A10, A9, A5, CAT_1:54
.=
(((t1 . b) " ) * (t1 . b)) * (F1 . f)
by A4, A7, A9, CAT_1:54
.=
(id (F1 . b)) * (F1 . f)
by A8, A7, CAT_1:def 14
.=
F1 . f
by A4, CAT_1:57
;
A12:
t1 . a is
invertible
by A2, Def10;
then A13:
Hom (F2 . a),
(F1 . a) <> {}
by A10, CAT_1:70;
then A14:
Hom (F2 . a),
(F1 . b) <> {}
by A4, CAT_1:52;
then ((t1 . b) " ) * (F2 . f) =
(((t1 . b) " ) * (F2 . f)) * (id (F2 . a))
by CAT_1:58
.=
(((t1 . b) " ) * (F2 . f)) * ((t1 . a) * ((t1 . a) " ))
by A12, A10, CAT_1:def 14
.=
(F1 . f) * ((t1 . a) " )
by A10, A13, A14, A11, CAT_1:54
;
hence ((t1 " ) . b) * (F2 . f) =
(F1 . f) * ((t1 . a) " )
by A2, A6, Def12
.=
(F1 . f) * ((t1 " ) . a)
by A2, A6, Def12
;
verum
end;
Lm5:
for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & t1 is invertible holds
F2 is_naturally_transformable_to F1
:: deftheorem Def13 defines " NATTRA_1:def 13 :
theorem
canceled;
theorem Th30:
theorem
theorem Th32:
:: deftheorem Def14 defines natural_equivalence NATTRA_1:def 14 :
theorem
theorem
begin
definition
let A,
B be
Category;
mode NatTrans-DOMAIN of
A,
B -> non
empty set means :
Def15:
for
x being
set st
x in it holds
ex
F1,
F2 being
Functor of
A,
B ex
t being
natural_transformation of
F1,
F2 st
(
x = [[F1,F2],t] &
F1 is_naturally_transformable_to F2 );
existence
ex b1 being non empty set st
for x being set st x in b1 holds
ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 )
end;
:: deftheorem Def15 defines NatTrans-DOMAIN NATTRA_1:def 15 :
definition
let A,
B be
Category;
func NatTrans A,
B -> NatTrans-DOMAIN of
A,
B means :
Def16:
for
x being
set holds
(
x in it iff ex
F1,
F2 being
Functor of
A,
B ex
t being
natural_transformation of
F1,
F2 st
(
x = [[F1,F2],t] &
F1 is_naturally_transformable_to F2 ) );
existence
ex b1 being NatTrans-DOMAIN of A,B st
for x being set holds
( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )
uniqueness
for b1, b2 being NatTrans-DOMAIN of A,B st ( for x being set holds
( x in b1 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds
( x in b2 iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) holds
b1 = b2
end;
:: deftheorem Def16 defines NatTrans NATTRA_1:def 16 :
theorem Th35:
definition
canceled;let A,
B be
Category;
func Functors A,
B -> strict Category means :
Def18:
( the
carrier of
it = Funct A,
B & the
carrier' of
it = NatTrans A,
B & ( for
f being
Morphism of
it holds
(
dom f = (f `1 ) `1 &
cod f = (f `1 ) `2 ) ) & ( for
f,
g being
Morphism of
it st
dom g = cod f holds
[g,f] in dom the
Comp of
it ) & ( for
f,
g being
Morphism of
it st
[g,f] in dom the
Comp of
it holds
ex
F,
F1,
F2 being
Functor of
A,
B ex
t being
natural_transformation of
F,
F1 ex
t1 being
natural_transformation of
F1,
F2 st
(
f = [[F,F1],t] &
g = [[F1,F2],t1] & the
Comp of
it . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for
a being
Object of
it for
F being
Functor of
A,
B st
F = a holds
id a = [[F,F],(id F)] ) );
existence
ex b1 being strict Category st
( the carrier of b1 = Funct A,B & the carrier' of b1 = NatTrans A,B & ( for f being Morphism of b1 holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds
[g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
uniqueness
for b1, b2 being strict Category st the carrier of b1 = Funct A,B & the carrier' of b1 = NatTrans A,B & ( for f being Morphism of b1 holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) ) & ( for f, g being Morphism of b1 st dom g = cod f holds
[g,f] in dom the Comp of b1 ) & ( for f, g being Morphism of b1 st [g,f] in dom the Comp of b1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) & the carrier of b2 = Funct A,B & the carrier' of b2 = NatTrans A,B & ( for f being Morphism of b2 holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) ) & ( for f, g being Morphism of b2 st dom g = cod f holds
[g,f] in dom the Comp of b2 ) & ( for f, g being Morphism of b2 st [g,f] in dom the Comp of b2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b2 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) holds
b1 = b2
end;
:: deftheorem NATTRA_1:def 17 :
canceled;
:: deftheorem Def18 defines Functors NATTRA_1:def 18 :
for
A,
B being
Category for
b3 being
strict Category holds
(
b3 = Functors A,
B iff ( the
carrier of
b3 = Funct A,
B & the
carrier' of
b3 = NatTrans A,
B & ( for
f being
Morphism of
b3 holds
(
dom f = (f `1 ) `1 &
cod f = (f `1 ) `2 ) ) & ( for
f,
g being
Morphism of
b3 st
dom g = cod f holds
[g,f] in dom the
Comp of
b3 ) & ( for
f,
g being
Morphism of
b3 st
[g,f] in dom the
Comp of
b3 holds
ex
F,
F1,
F2 being
Functor of
A,
B ex
t being
natural_transformation of
F,
F1 ex
t1 being
natural_transformation of
F1,
F2 st
(
f = [[F,F1],t] &
g = [[F1,F2],t1] & the
Comp of
b3 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for
a being
Object of
b3 for
F being
Functor of
A,
B st
F = a holds
id a = [[F,F],(id F)] ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th39:
theorem
for
A,
B being
Category for
a,
b being
Object of
(Functors A,B) for
f being
Morphism of
a,
b st
Hom a,
b <> {} holds
ex
F,
F1 being
Functor of
A,
B ex
t being
natural_transformation of
F,
F1 st
(
a = F &
b = F1 &
f = [[F,F1],t] )
theorem Th41:
for
A,
B being
Category for
F2,
F3,
F,
F1 being
Functor of
A,
B for
t being
natural_transformation of
F,
F1 for
t' being
natural_transformation of
F2,
F3 for
f,
g being
Morphism of
(Functors A,B) st
f = [[F,F1],t] &
g = [[F2,F3],t'] holds
(
[g,f] in dom the
Comp of
(Functors A,B) iff
F1 = F2 )
theorem
for
A,
B being
Category for
F,
F1,
F2 being
Functor of
A,
B for
t being
natural_transformation of
F,
F1 for
t1 being
natural_transformation of
F1,
F2 for
f,
g being
Morphism of
(Functors A,B) st
f = [[F,F1],t] &
g = [[F1,F2],t1] holds
g * f = [[F,F2],(t1 `*` t)]
begin
:: deftheorem Def19 defines discrete NATTRA_1:def 19 :
theorem
canceled;
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
theorem Th49:
theorem Th50:
theorem
:: deftheorem Def20 defines IdCat NATTRA_1:def 20 :
theorem Th52:
theorem
theorem
theorem