:: NATTRA_1 semantic presentation

definition

let A1 be set ;
let B1 be non empty set ;
let f be Function of A1,B1;
let Y1 be Subset of A1;
:: original: |
redefine func f | Y1 -> Function of Y1,B1;
coherence by FUNCT_2:38;

end;

theorem Th1: :: NATTRA_1:1

for B1, B2, A1, A2 being non empty set
for f being Function of A1,B1
for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]

proof end;

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;
:: original: |:
redefine func |:f,g:| -> PartFunc of [:[:A1,B1:],[:A1,B1:]:],[:A1,B1:];
coherence by FUNCT_4:62;

end;

theorem Th2: :: NATTRA_1:2

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:]

proof end;

scheme :: NATTRA_1:sch 1
MChoice{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> set } :

ex t being Function of F₁(),F₂() st
for a being Element of F₁() holds t . a in F₃(a)

provided

A1: for a being Element of F₁() holds F₂() meets F₃(a)

proof end;

theorem Th3: :: NATTRA_1:3

for A being Category
for a being Object of A
for m being Morphism of a,a holds m in Hom a,a

proof end;

theorem Th4: :: NATTRA_1:4

for o, m being set
for f, g being Morphism of (1Cat o,m) holds f = g

proof end;

theorem Th5: :: NATTRA_1:5

for A being Category
for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A

proof end;

theorem Th6: :: NATTRA_1:6

for o, m being set holds the Comp of (1Cat o,m) = {[[m,m],m]}

proof end;

theorem Th7: :: NATTRA_1:7

for A being Category
for a being Object of A holds 1Cat a,(id a) is Subcategory of A

proof end;

theorem Th8: :: NATTRA_1:8

for A being Category
for C being Subcategory of A holds
( the Dom of C = the Dom of A | the Morphisms of C & the Cod of C = the Cod of A | the Morphisms of C & the Comp of C = the Comp of A || the Morphisms of C & the Id of C = the Id of A | the Objects of C )

proof end;

theorem Th9: :: NATTRA_1:9

for A being Category
for O being non empty Subset of the Objects of A
for M being non empty Subset of the Morphisms of A
for DOM, COD being Function of M,O st DOM = the Dom of A | M & COD = the Cod 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

proof end;

theorem Th10: :: NATTRA_1:10

for C being strict Category
for A being strict Subcategory of C st the Objects of A = the Objects of C & the Morphisms of A = the Morphisms of C holds
A = C

proof end;

definition

let A, B be Category;
let F be Functor of A,B;
let a, b be Object of A;
assume A1: Hom a,b <> {} ;
let f be Morphism of a,b;
func F . f -> Morphism of F . a,F . b equals :Def1: :: NATTRA_1:def 1
F . f;
coherence by A1, CAT_1:125;

end;

:: deftheorem Def1 defines . NATTRA_1:def 1 :

theorem :: NATTRA_1:11

for B, C, A being Category
for F being Functor of A,B
for G being Functor of B,C
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (G * F) . f = G . (F . f)

proof end;

theorem :: NATTRA_1:12

for A, B being Category
for F1, F2 being Functor of A,B st ( for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds F1 . f = F2 . f ) holds
F1 = F2

proof end;

theorem Th13: :: NATTRA_1:13

for B, A being Category
for F being Functor of A,B
for a, b, c being Object of A st Hom a,b <> {} & Hom b,c <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds F . (g * f) = (F . g) * (F . f)

proof end;

theorem :: NATTRA_1:14

for A, B being Category
for F being Functor of A,B
for c being Object of A
for d being Object of B st F . (id c) = id d holds
F . c = d

proof end;

theorem Th15: :: NATTRA_1:15

for B, A being Category
for F being Functor of A,B
for a being Object of A holds F . (id a) = id (F . a)

proof end;

theorem :: NATTRA_1:16

for A being Category
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (id A) . f = f

proof end;

theorem Th17: :: NATTRA_1:17

for A being Category
for a, b, c, d being Object of A st Hom a,b meets Hom c,d holds
( a = c & b = d )

proof end;

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
pred F1 is_transformable_to F2 means :Def2: :: NATTRA_1:def 2
for a being Object of A holds Hom (F1 . a),(F2 . a) <> {} ;
reflexivity by CAT_1:56;

end;

:: deftheorem Def2 defines is_transformable_to NATTRA_1:def 2 :

theorem :: NATTRA_1:18

canceled;

theorem Th19: :: NATTRA_1:19

for A, B being Category
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2

proof end;

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
mode transformation of F1,F2 -> Function of the Objects of A,the Morphisms of B means :Def3: :: NATTRA_1:def 3
for a being Object of A holds it . a is Morphism of F1 . a,F2 . a;
existence

proof end;

end;

:: deftheorem Def3 defines transformation NATTRA_1:def 3 :

definition

let A, B be Category;
let F be Functor of A,B;
func id F -> transformation of F,F means :Def4: :: NATTRA_1:def 4
for a being Object of A holds it . a = id (F . a);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines id NATTRA_1:def 4 :

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
let t be transformation of F1,F2;
let a be Object of A;
func t . a -> Morphism of F1 . a,F2 . a equals :Def5: :: NATTRA_1:def 5
t . a;
coherence by A1, Def3;

end;

:: 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: :: NATTRA_1:def 6
for a being Object of A holds it . a = (t2 . a) * (t1 . a);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines `*` NATTRA_1:def 6 :

theorem Th20: :: NATTRA_1:20

for B, A being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2

proof end;

theorem Th21: :: NATTRA_1:21

for B, A being Category
for F being Functor of A,B
for a being Object of A holds (id F) . a = id (F . a)

proof end;

theorem Th22: :: NATTRA_1:22

for A, B being Category
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )

proof end;

theorem Th23: :: NATTRA_1:23

for A, B being Category
for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)

proof end;

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)

proof end;

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
pred F1 is_naturally_transformable_to F2 means :Def7: :: NATTRA_1:def 7
( 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

proof end;

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)

proof end;

theorem :: NATTRA_1:24

canceled;

theorem Th25: :: NATTRA_1:25

for A, B being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2

proof end;

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: :: NATTRA_1:def 8
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 by A1, Def7;

end;

:: deftheorem Def8 defines natural_transformation NATTRA_1:def 8 :

definition

let A, B be Category;
let F be Functor of A,B;
:: original: id
redefine func id F -> natural_transformation of F,F;
coherence

proof end;

end;

definition

let A, B be Category;
let F, F1, F2 be Functor of A,B;
assume that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2 ;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
func t2 `*` t1 -> natural_transformation of F,F2 equals :Def9: :: NATTRA_1:def 9
t2 `*` t1;
coherence

proof end;

end;

:: deftheorem Def9 defines `*` NATTRA_1:def 9 :

theorem Th26: :: NATTRA_1:26

for A, B being Category
for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (id F2) `*` t = t & t `*` (id F1) = t )

proof end;

theorem Th27: :: NATTRA_1:27

for B, A being Category
for F, F1, F2 being Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being Object of A holds (t2 `*` t1) . a = (t2 . a) * (t1 . a)

proof end;

theorem Th28: :: NATTRA_1:28

for A, B being Category
for F, F1, F2, F3 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

proof end;

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
let IT be transformation of F1,F2;
attr IT is invertible means :Def10: :: NATTRA_1:def 10
for a being Object of A holds IT . a is invertible;

end;

:: deftheorem Def10 defines invertible NATTRA_1:def 10 :

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
pred F1,F2 are_naturally_equivalent means :Def11: :: NATTRA_1:def 11
( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible );
reflexivity

proof end;

end;

:: deftheorem Def11 defines are_naturally_equivalent NATTRA_1:def 11 :

notation

let A, B be Category;
let F1, F2 be Functor of A,B;
synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ;

end;

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

proof end;

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
let t1 be transformation of F1,F2;
assume A2: t1 is invertible ;
func t1 " -> transformation of F2,F1 means :Def12: :: NATTRA_1:def 12
for a being Object of A holds it . a = (t1 . a) " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines " NATTRA_1:def 12 :

Lm4: now

let A, B be Category;
let F1, F2 be Functor of A,B;
let t1 be natural_transformation of F1,F2; :: thesis:
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible ; :: thesis:
A3: F1 is_transformable_to F2 by A1, Def7;
let a, b be Object of A; :: thesis:
assume A4: Hom a,b <> {} ; :: thesis:
A5: t1 . b is invertible by A2, Def10;
A6: t1 . a is invertible by A2, Def10;
A7: Hom (F1 . a),(F1 . b) <> {} by A4, CAT_1:126;
A8: Hom (F1 . a),(F2 . a) <> {} by A3, Def2;
A9: Hom (F1 . b),(F2 . b) <> {} by A3, Def2;
then A10: Hom (F2 . b),(F1 . b) <> {} by A5, CAT_1:70;
A11: Hom (F2 . a),(F2 . b) <> {} by A4, CAT_1:126;
A12: Hom (F2 . a),(F1 . a) <> {} by A6, A8, CAT_1:70;
then A13: Hom (F2 . a),(F1 . b) <> {} by A7, CAT_1:52;
let f be Morphism of a,b; :: thesis:
(F2 . f) * (t1 . a) = (t1 . b) * (F1 . f) by A1, A4, Def8;
then A14: (((t1 . b) " ) * (F2 . f)) * (t1 . a) = ((t1 . b) " ) * ((t1 . b) * (F1 . f)) by A8, A10, A11, CAT_1:54
.= (((t1 . b) " ) * (t1 . b)) * (F1 . f) by A7, A9, A10, CAT_1:54
.= (id (F1 . b)) * (F1 . f) by A5, A9, CAT_1:def 14
.= F1 . f by A7, CAT_1:57 ;
((t1 . b) " ) * (F2 . f) = (((t1 . b) " ) * (F2 . f)) * (id (F2 . a)) by A13, CAT_1:58
.= (((t1 . b) " ) * (F2 . f)) * ((t1 . a) * ((t1 . a) " )) by A6, A8, CAT_1:def 14
.= (F1 . f) * ((t1 . a) " ) by A8, A12, A13, A14, CAT_1:54 ;
hence ((t1 " ) . b) * (F2 . f) = (F1 . f) * ((t1 . a) " ) by A2, A3, Def12
.= (F1 . f) * ((t1 " ) . a) by A2, A3, Def12 ;
:: thesis:

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

proof end;

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
let t1 be natural_transformation of F1,F2;
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible ;
func t1 " -> natural_transformation of F2,F1 equals :Def13: :: NATTRA_1:def 13
t1 " ;
coherence

proof end;

end;

:: deftheorem Def13 defines " NATTRA_1:def 13 :

theorem :: NATTRA_1:29

canceled;

theorem Th30: :: NATTRA_1:30

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
for a being Object of A holds (t1 " ) . a = (t1 . a) "

proof end;

theorem :: NATTRA_1:31

for A, B being Category
for F1, F2 being Functor of A,B st F1 ~= F2 holds
F2 ~= F1

proof end;

theorem Th32: :: NATTRA_1:32

for A, B being Category
for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
F1 ~= F3

proof end;

definition

let A, B be Category;
let F1, F2 be Functor of A,B;
assume A1: F1,F2 are_naturally_equivalent ;
mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means :Def14: :: NATTRA_1:def 14
it is invertible;
existence by A1, Def11;

end;

:: deftheorem Def14 defines natural_equivalence NATTRA_1:def 14 :

theorem :: NATTRA_1:33

for A, B being Category
for F being Functor of A,B holds id F is natural_equivalence of F,F

proof end;

theorem :: NATTRA_1:34

for A, B being Category
for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
for t being natural_equivalence of F1,F2
for t' being natural_equivalence of F2,F3 holds t' `*` t is natural_equivalence of F1,F3

proof end;

definition

let A, B be Category;
mode NatTrans-DOMAIN of A,B -> non empty set means :Def15: :: NATTRA_1:def 15
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

proof end;

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: :: NATTRA_1:def 16
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines NatTrans NATTRA_1:def 16 :

definition

let A1, B1, A2, B2 be non empty set ;
let f1 be Function of A1,B1;
let f2 be Function of A2,B2;
:: original: =
redefine pred f1 = f2 means :: NATTRA_1:def 17
( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) );
compatibility

proof end;

end;

:: deftheorem defines = NATTRA_1:def 17 :

theorem Th35: :: NATTRA_1:35

for A, B being Category
for F1, F2 being Functor of A,B
for t1 being natural_transformation of F1,F2 holds
( F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans A,B )

proof end;

definition

let A, B be Category;
func Functors A,B -> strict Category means :Def18: :: NATTRA_1:def 18
( the Objects of it = Funct A,B & the Morphisms 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Functors NATTRA_1:def 18 :

theorem :: NATTRA_1:36

canceled;

theorem :: NATTRA_1:37

canceled;

theorem :: NATTRA_1:38

canceled;

theorem Th39: :: NATTRA_1:39

for A, B being Category
for F, F1 being Functor of A,B
for t being natural_transformation of F,F1
for f being Morphism of (Functors A,B) st f = [[F,F1],t] holds
( dom f = F & cod f = F1 )

proof end;

theorem :: NATTRA_1:40

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] )

proof end;

theorem Th41: :: NATTRA_1:41

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 )

proof end;

theorem :: NATTRA_1:42

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)]

proof end;

definition

let C be Category;
attr C is discrete means :Def19: :: NATTRA_1:def 19
for f being Morphism of C ex a being Object of C st f = id a;

end;

:: deftheorem Def19 defines discrete NATTRA_1:def 19 :

registration

cluster discrete CatStr ;
existence

proof end;

end;

theorem :: NATTRA_1:43

canceled;

theorem Th44: :: NATTRA_1:44

for A being discrete Category
for a being Object of A holds Hom a,a = {(id a)}

proof end;

theorem Th45: :: NATTRA_1:45

for A being Category holds
( A is discrete iff ( ( for a being Object of A ex B being finite set st
( B = Hom a,a & card B = 1 ) ) & ( for a, b being Object of A st a <> b holds
Hom a,b = {} ) ) )

proof end;

theorem Th46: :: NATTRA_1:46

for o, m being set holds 1Cat o,m is discrete

proof end;

theorem :: NATTRA_1:47

for A being discrete Category
for C being Subcategory of A holds C is discrete

proof end;

theorem :: NATTRA_1:48