:: by Andrzej Trybulec

::

:: Received May 15, 1991

:: Copyright (c) 1991-2018 Association of Mizar Users

::$CT 4

theorem Th4: :: NATTRA_1:8

for A being Category

for C being Subcategory of A holds

( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

for C being Subcategory of A holds

( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

proof end;

theorem Th5: :: NATTRA_1:9

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 st ( for o being Element of A st o in O holds

id o in M ) holds

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

CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A

for O being non empty Subset of the carrier of A

for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds

id o in M ) holds

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

CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A

proof end;

theorem Th6: :: NATTRA_1:10

for C being strict Category

for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds

A = C

for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds

A = C

proof end;

definition
end;

theorem :: NATTRA_1:11

for A, B, C 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)

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;

:: The following theorems are analogues of theorems from CAT_1, with

:: the new concept of the application of a functor to a morphism

:: the new concept of the application of a functor to a morphism

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

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 Th9: :: NATTRA_1:13

for A, B 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)

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

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 Th11: :: NATTRA_1:15

for A, B being Category

for F being Functor of A,B

for a being Object of A holds F /. (id a) = id (F . a)

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

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

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;

for F1 being Functor of A,B

for a being Object of A holds Hom ((F1 . a),(F1 . a)) <> {} ;

end;
let F1, F2 be Functor of A,B;

pred F1 is_transformable_to F2 means :Def1: :: NATTRA_1:def 2

for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ;

reflexivity for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} ;

for F1 being Functor of A,B

for a being Object of A holds Hom ((F1 . a),(F1 . a)) <> {} ;

:: deftheorem Def1 defines is_transformable_to NATTRA_1:def 2 :

for A, B being Category

for F1, F2 being Functor of A,B holds

( F1 is_transformable_to F2 iff for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} );

for A, B being Category

for F1, F2 being Functor of A,B holds

( F1 is_transformable_to F2 iff for a being Object of A holds Hom ((F1 . a),(F2 . a)) <> {} );

theorem Th14: :: NATTRA_1:18

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

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 ;

ex b_{1} being Function of the carrier of A, the carrier' of B st

for a being Object of A holds b_{1} . a is Morphism of F1 . a,F2 . a

end;
let F1, F2 be Functor of A,B;

assume A1: F1 is_transformable_to F2 ;

mode transformation of F1,F2 -> Function of the carrier of A, the carrier' of B means :Def2: :: NATTRA_1:def 3

for a being Object of A holds it . a is Morphism of F1 . a,F2 . a;

existence for a being Object of A holds it . a is Morphism of F1 . a,F2 . a;

ex b

for a being Object of A holds b

proof end;

:: deftheorem Def2 defines transformation NATTRA_1:def 3 :

for A, B being Category

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

for b_{5} being Function of the carrier of A, the carrier' of B holds

( b_{5} is transformation of F1,F2 iff for a being Object of A holds b_{5} . a is Morphism of F1 . a,F2 . a );

for A, B being Category

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

for b

( b

definition

let A, B be Category;

let F be Functor of A,B;

ex b_{1} being transformation of F,F st

for a being Object of A holds b_{1} . a = id (F . a)

for b_{1}, b_{2} being transformation of F,F st ( for a being Object of A holds b_{1} . a = id (F . a) ) & ( for a being Object of A holds b_{2} . a = id (F . a) ) holds

b_{1} = b_{2}

end;
let F be Functor of A,B;

func id F -> transformation of F,F means :Def3: :: NATTRA_1:def 4

for a being Object of A holds it . a = id (F . a);

existence for a being Object of A holds it . a = id (F . a);

ex b

for a being Object of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines id NATTRA_1:def 4 :

for A, B being Category

for F being Functor of A,B

for b_{4} being transformation of F,F holds

( b_{4} = id F iff for a being Object of A holds b_{4} . a = id (F . a) );

for A, B being Category

for F being Functor of A,B

for b

( b

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;

coherence

t . a is Morphism of F1 . a,F2 . a by A1, Def2;

end;
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;

coherence

t . a is Morphism of F1 . a,F2 . a by A1, Def2;

:: deftheorem Def4 defines . NATTRA_1:def 5 :

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

for a being Object of A holds t . a = t . a;

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

for a being Object of A holds t . a = t . a;

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;

ex b_{1} being transformation of F,F2 st

for a being Object of A holds b_{1} . a = (t2 . a) * (t1 . a)

for b_{1}, b_{2} being transformation of F,F2 st ( for a being Object of A holds b_{1} . a = (t2 . a) * (t1 . a) ) & ( for a being Object of A holds b_{2} . a = (t2 . a) * (t1 . a) ) holds

b_{1} = b_{2}

end;
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 :Def5: :: NATTRA_1:def 6

for a being Object of A holds it . a = (t2 . a) * (t1 . a);

existence for a being Object of A holds it . a = (t2 . a) * (t1 . a);

ex b

for a being Object of A holds b

proof end;

uniqueness for b

b

proof end;

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

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

for t1 being transformation of F,F1

for t2 being transformation of F1,F2

for b_{8} being transformation of F,F2 holds

( b_{8} = t2 `*` t1 iff for a being Object of A holds b_{8} . a = (t2 . a) * (t1 . a) );

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

for t1 being transformation of F,F1

for t2 being transformation of F1,F2

for b

( b

theorem Th15: :: NATTRA_1:19

for A, B 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

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 Th16: :: NATTRA_1:20

for A, B being Category

for F being Functor of A,B

for a being Object of A holds (id F) . a = id (F . a)

for F being Functor of A,B

for a being Object of A holds (id F) . a = id (F . a)

proof end;

theorem Th17: :: NATTRA_1:21

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 )

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 Th18: :: NATTRA_1:22

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)

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 A, B 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;

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;
let F1, F2 be Functor of A,B;

pred F1 is_naturally_transformable_to F2 means :: 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 ( 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) );

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

proof end;

:: deftheorem defines is_naturally_transformable_to NATTRA_1:def 7 :

for A, B being Category

for F1, F2 being Functor of A,B holds

( F1 is_naturally_transformable_to F2 iff ( 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) ) );

for A, B being Category

for F1, F2 being Functor of A,B holds

( F1 is_naturally_transformable_to F2 iff ( 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) ) );

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

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 Th19: :: NATTRA_1:23

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

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 ;

ex b_{1} 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 (b_{1} . b) * (F1 /. f) = (F2 /. f) * (b_{1} . a)
by A1;

end;
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 :Def7: :: 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 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);

ex b

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (b

:: deftheorem Def7 defines natural_transformation NATTRA_1:def 8 :

for A, B being Category

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

for b_{5} being transformation of F1,F2 holds

( b_{5} is natural_transformation of F1,F2 iff for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (b_{5} . b) * (F1 /. f) = (F2 /. f) * (b_{5} . a) );

for A, B being Category

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

for b

( b

for f being Morphism of a,b holds (b

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

id F is natural_transformation of F,F

end;
let F be Functor of A,B;

:: original: id

redefine func id F -> natural_transformation of F,F;

coherence

id F is natural_transformation of F,F

proof 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;

coherence

t2 `*` t1 is natural_transformation of F,F2

end;
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;

coherence

t2 `*` t1 is natural_transformation of F,F2

proof end;

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

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

for t1 being natural_transformation of F,F1

for t2 being natural_transformation of F1,F2 holds t2 `*` t1 = t2 `*` t1;

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

for t1 being natural_transformation of F,F1

for t2 being natural_transformation of F1,F2 holds t2 `*` t1 = t2 `*` t1;

theorem Th20: :: NATTRA_1:24

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 )

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

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)

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 Th22: :: NATTRA_1:26

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)

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;

:: Natural equivalences

definition
end;

:: deftheorem defines invertible NATTRA_1:def 10 :

for A, B being Category

for F1, F2 being Functor of A,B

for IT being transformation of F1,F2 holds

( IT is invertible iff for a being Object of A holds IT . a is invertible );

for A, B being Category

for F1, F2 being Functor of A,B

for IT being transformation of F1,F2 holds

( IT is invertible iff for a being Object of A holds IT . a is invertible );

definition

let A, B be Category;

let F1, F2 be Functor of A,B;

for F1 being Functor of A,B holds

( F1 is_naturally_transformable_to F1 & ex t being natural_transformation of F1,F1 st t is invertible )

end;
let F1, F2 be Functor of A,B;

pred F1,F2 are_naturally_equivalent means :: NATTRA_1:def 11

( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible );

reflexivity ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible );

for F1 being Functor of A,B holds

( F1 is_naturally_transformable_to F1 & ex t being natural_transformation of F1,F1 st t is invertible )

proof end;

:: deftheorem defines are_naturally_equivalent NATTRA_1:def 11 :

for A, B being Category

for F1, F2 being Functor of A,B holds

( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible ) );

for A, B being Category

for F1, F2 being Functor of A,B holds

( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible ) );

notation

let A, B be Category;

let F1, F2 be Functor of A,B;

synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ;

end;
let F1, F2 be Functor of A,B;

synonym F1 ~= F2 for F1,F2 are_naturally_equivalent ;

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 ;

ex b_{1} being transformation of F2,F1 st

for a being Object of A holds b_{1} . a = (t1 . a) "

for b_{1}, b_{2} being transformation of F2,F1 st ( for a being Object of A holds b_{1} . a = (t1 . a) " ) & ( for a being Object of A holds b_{2} . a = (t1 . a) " ) holds

b_{1} = b_{2}

end;
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 :Def11: :: NATTRA_1:def 12

for a being Object of A holds it . a = (t1 . a) " ;

existence for a being Object of A holds it . a = (t1 . a) " ;

ex b

for a being Object of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines " NATTRA_1:def 12 :

for A, B being Category

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

for t1 being transformation of F1,F2 st t1 is invertible holds

for b_{6} being transformation of F2,F1 holds

( b_{6} = t1 " iff for a being Object of A holds b_{6} . a = (t1 . a) " );

for A, B being Category

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

for t1 being transformation of F1,F2 st t1 is invertible holds

for b

( b

Lm4: now :: thesis: 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, 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)

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 A, B be Category; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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) <> {} ; :: thesis: 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:84;

let f be Morphism of a,b; :: thesis: ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)

A5: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;

A6: F1 is_transformable_to F2 by A1;

A7: Hom ((F1 . b),(F2 . b)) <> {} by Def1, A1;

A8: t1 . b is invertible by A2;

then A9: Hom ((F2 . b),(F1 . b)) <> {} ;

A10: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def1;

(F2 /. f) * (t1 . a) = (t1 . b) * (F1 /. f) by A1, A3, Def7;

then A11: (((t1 . b) ") * (F2 /. f)) * (t1 . a) = ((t1 . b) ") * ((t1 . b) * (F1 /. f)) by A10, A9, A5, CAT_1:25

.= (((t1 . b) ") * (t1 . b)) * (F1 /. f) by A4, A7, A9, CAT_1:25

.= (id (F1 . b)) * (F1 /. f) by A8, CAT_1:def 17

.= F1 /. f by A4, CAT_1:28 ;

A12: t1 . a is invertible by A2;

then A13: Hom ((F2 . a),(F1 . a)) <> {} ;

then A14: Hom ((F2 . a),(F1 . b)) <> {} by A4, CAT_1:24;

then ((t1 . b) ") * (F2 /. f) = (((t1 . b) ") * (F2 /. f)) * (id (F2 . a)) by CAT_1:29

.= (((t1 . b) ") * (F2 /. f)) * ((t1 . a) * ((t1 . a) ")) by A12, CAT_1:def 17

.= (F1 /. f) * ((t1 . a) ") by A10, A13, A14, A11, CAT_1:25 ;

hence ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 . a) ") by A2, A6, Def11

.= (F1 /. f) * ((t1 ") . a) by A2, A6, Def11 ;

:: thesis: verum

end;
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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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) <> {} ; :: thesis: 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:84;

let f be Morphism of a,b; :: thesis: ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a)

A5: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;

A6: F1 is_transformable_to F2 by A1;

A7: Hom ((F1 . b),(F2 . b)) <> {} by Def1, A1;

A8: t1 . b is invertible by A2;

then A9: Hom ((F2 . b),(F1 . b)) <> {} ;

A10: Hom ((F1 . a),(F2 . a)) <> {} by A1, Def1;

(F2 /. f) * (t1 . a) = (t1 . b) * (F1 /. f) by A1, A3, Def7;

then A11: (((t1 . b) ") * (F2 /. f)) * (t1 . a) = ((t1 . b) ") * ((t1 . b) * (F1 /. f)) by A10, A9, A5, CAT_1:25

.= (((t1 . b) ") * (t1 . b)) * (F1 /. f) by A4, A7, A9, CAT_1:25

.= (id (F1 . b)) * (F1 /. f) by A8, CAT_1:def 17

.= F1 /. f by A4, CAT_1:28 ;

A12: t1 . a is invertible by A2;

then A13: Hom ((F2 . a),(F1 . a)) <> {} ;

then A14: Hom ((F2 . a),(F1 . b)) <> {} by A4, CAT_1:24;

then ((t1 . b) ") * (F2 /. f) = (((t1 . b) ") * (F2 /. f)) * (id (F2 . a)) by CAT_1:29

.= (((t1 . b) ") * (F2 /. f)) * ((t1 . a) * ((t1 . a) ")) by A12, CAT_1:def 17

.= (F1 /. f) * ((t1 . a) ") by A10, A13, A14, A11, CAT_1:25 ;

hence ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 . a) ") by A2, A6, Def11

.= (F1 /. f) * ((t1 ") . a) by A2, A6, Def11 ;

:: thesis: verum

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 ;

coherence

t1 " is natural_transformation of F2,F1

end;
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 ;

coherence

t1 " is natural_transformation of F2,F1

proof end;

:: deftheorem Def12 defines " NATTRA_1:def 13 :

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

t1 " = t1 " ;

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

t1 " = t1 " ;

theorem Th23: :: NATTRA_1:27

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

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;

definition

let A, B be Category;

let F1, F2 be Functor of A,B;

assume A1: F1,F2 are_naturally_equivalent ;

ex b_{1} being natural_transformation of F1,F2 st b_{1} is invertible
by A1;

end;
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 :Def13: :: NATTRA_1:def 14

it is invertible ;

existence it is invertible ;

ex b

:: deftheorem Def13 defines natural_equivalence NATTRA_1:def 14 :

for A, B being Category

for F1, F2 being Functor of A,B st F1,F2 are_naturally_equivalent holds

for b_{5} being natural_transformation of F1,F2 holds

( b_{5} is natural_equivalence of F1,F2 iff b_{5} is invertible );

for A, B being Category

for F1, F2 being Functor of A,B st F1,F2 are_naturally_equivalent holds

for b

( b

theorem :: NATTRA_1:31

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 t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3

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

for t being natural_equivalence of F1,F2

for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3

proof end;

definition

let A, B be Category;

ex b_{1} being non empty set st

for x being set st x in b_{1} 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;
mode NatTrans-DOMAIN of A,B -> non empty set means :Def14: :: 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 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 );

ex b

for x being set st x in b

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 )

proof end;

:: deftheorem Def14 defines NatTrans-DOMAIN NATTRA_1:def 15 :

for A, B being Category

for b_{3} being non empty set holds

( b_{3} is NatTrans-DOMAIN of A,B iff for x being set st x in b_{3} 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 ) );

for A, B being Category

for b

( b

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

definition

let A, B be Category;

ex b_{1} being NatTrans-DOMAIN of A,B st

for x being set holds

( x in b_{1} 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 b_{1}, b_{2} being NatTrans-DOMAIN of A,B st ( for x being set holds

( x in b_{1} 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 b_{2} 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

b_{1} = b_{2}

end;
func NatTrans (A,B) -> NatTrans-DOMAIN of A,B means :Def15: :: 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 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 ) );

ex b

for x being set holds

( x in b

( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) )

proof end;

uniqueness for b

( x in b

( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) & ( for x being set holds

( x in b

( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) ) holds

b

proof end;

:: deftheorem Def15 defines NatTrans NATTRA_1:def 16 :

for A, B being Category

for b_{3} being NatTrans-DOMAIN of A,B holds

( b_{3} = NatTrans (A,B) iff for x being set holds

( x in b_{3} 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 A, B being Category

for b

( b

( x in b

( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) );

theorem Th28: :: NATTRA_1:32

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

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;

ex b_{1} being strict Category st

( the carrier of b_{1} = Funct (A,B) & the carrier' of b_{1} = NatTrans (A,B) & ( for f being Morphism of b_{1} holds

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b_{1} st dom g = cod f holds

[g,f] in dom the Comp of b_{1} ) & ( for f, g being Morphism of b_{1} st [g,f] in dom the Comp of b_{1} 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 b_{1} . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b_{1}

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) )

for b_{1}, b_{2} being strict Category st the carrier of b_{1} = Funct (A,B) & the carrier' of b_{1} = NatTrans (A,B) & ( for f being Morphism of b_{1} holds

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b_{1} st dom g = cod f holds

[g,f] in dom the Comp of b_{1} ) & ( for f, g being Morphism of b_{1} st [g,f] in dom the Comp of b_{1} 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 b_{1} . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b_{1}

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) & the carrier of b_{2} = Funct (A,B) & the carrier' of b_{2} = NatTrans (A,B) & ( for f being Morphism of b_{2} holds

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b_{2} st dom g = cod f holds

[g,f] in dom the Comp of b_{2} ) & ( for f, g being Morphism of b_{2} st [g,f] in dom the Comp of b_{2} 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 b_{2} . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b_{2}

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) holds

b_{1} = b_{2}

end;
func Functors (A,B) -> strict Category means :Def16: :: NATTRA_1:def 17

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

ex b

( the carrier of b

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b

[g,f] in dom the Comp of b

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 b

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) )

proof end;

uniqueness for b

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b

[g,f] in dom the Comp of b

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 b

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) & the carrier of b

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b

[g,f] in dom the Comp of b

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 b

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) holds

b

proof end;

:: deftheorem Def16 defines Functors NATTRA_1:def 17 :

for A, B being Category

for b_{3} being strict Category holds

( b_{3} = Functors (A,B) iff ( the carrier of b_{3} = Funct (A,B) & the carrier' of b_{3} = NatTrans (A,B) & ( for f being Morphism of b_{3} holds

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b_{3} st dom g = cod f holds

[g,f] in dom the Comp of b_{3} ) & ( for f, g being Morphism of b_{3} st [g,f] in dom the Comp of b_{3} 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 b_{3} . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b_{3}

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) ) );

for A, B being Category

for b

( b

( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b

[g,f] in dom the Comp of b

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 b

for F being Functor of A,B st F = a holds

id a = [[F,F],(id F)] ) ) );

:: As immediate consequences of the definition we get

theorem Th29: :: NATTRA_1:33

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 )

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

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

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 Th31: :: NATTRA_1:35

for A, B being Category

for F, F1, F2, F3 being Functor of A,B

for t being natural_transformation of F,F1

for t9 being natural_transformation of F2,F3

for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds

( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )

for F, F1, F2, F3 being Functor of A,B

for t being natural_transformation of F,F1

for t9 being natural_transformation of F2,F3

for f, g being Morphism of (Functors (A,B)) st f = [[F,F1],t] & g = [[F2,F3],t9] holds

( [g,f] in dom the Comp of (Functors (A,B)) iff F1 = F2 )

proof end;

theorem :: NATTRA_1:36

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

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;

end;
attr C is quasi-discrete means :Def17: :: NATTRA_1:def 18

for a, b being Element of C st Hom (a,b) <> {} holds

a = b;

for a, b being Element of C st Hom (a,b) <> {} holds

a = b;

attr C is pseudo-discrete means :Def18: :: NATTRA_1:def 19

for a being Element of C holds Hom (a,a) is trivial ;

for a being Element of C holds Hom (a,a) is trivial ;

:: deftheorem Def17 defines quasi-discrete NATTRA_1:def 18 :

for C being Category holds

( C is quasi-discrete iff for a, b being Element of C st Hom (a,b) <> {} holds

a = b );

for C being Category holds

( C is quasi-discrete iff for a, b being Element of C st Hom (a,b) <> {} holds

a = b );

:: deftheorem Def18 defines pseudo-discrete NATTRA_1:def 19 :

for C being Category holds

( C is pseudo-discrete iff for a being Element of C holds Hom (a,a) is trivial );

for C being Category holds

( C is pseudo-discrete iff for a being Element of C holds Hom (a,a) is trivial );

Lm6: for C being Category st C is quasi-discrete holds

the carrier' of C = union { (Hom (a,a)) where a is Element of C : verum }

proof end;

Lm7: for C being Category

for a being Element of C st C is pseudo-discrete holds

Hom (a,a) = {(id a)}

proof end;

:: deftheorem defines discrete NATTRA_1:def 20 :

for C being Category holds

( C is discrete iff ( C is quasi-discrete & C is pseudo-discrete ) );

for C being Category holds

( C is discrete iff ( C is quasi-discrete & C is pseudo-discrete ) );

registration

for b_{1} being Category st b_{1} is discrete holds

( b_{1} is quasi-discrete & b_{1} is pseudo-discrete )
;

for b_{1} being Category st b_{1} is quasi-discrete & b_{1} is pseudo-discrete holds

b_{1} is discrete
;

end;

cluster non empty non void Category-like transitive associative reflexive with_identities discrete -> quasi-discrete pseudo-discrete for Category;

coherence for b

( b

cluster non empty non void Category-like transitive associative reflexive with_identities quasi-discrete pseudo-discrete -> discrete for Category;

coherence for b

b

Lm8: for C being Category st C is discrete holds

the carrier' of C c= { (id a) where a is Element of C : verum }

proof end;

registration
end;

registration

ex b_{1} being Category st b_{1} is discrete
end;

cluster non empty non void V58() Category-like transitive associative reflexive with_identities discrete for Category;

existence ex b

proof end;

registration
end;

registration

let A be discrete Category;

coherence

for b_{1} being Subcategory of A holds b_{1} is discrete

end;
coherence

for b

proof end;

::$CT 3

theorem Th34: :: NATTRA_1:41

for A being discrete Category

for B being Category

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

F1 = F2

for B being Category

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

F1 = F2

proof end;

theorem Th35: :: NATTRA_1:42

for A being discrete Category

for B being Category

for F being Functor of B,A

for t being transformation of F,F holds t = id F

for B being Category

for F being Functor of B,A

for t being transformation of F,F holds t = id F

proof end;

registration
end;

registration

let C be Category;

ex b_{1} being Subcategory of C st

( b_{1} is strict & b_{1} is discrete )

end;
cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities discrete for Subcategory of C;

existence ex b

( b

proof end;

definition

let C be Category;

ex b_{1} being strict Subcategory of C st

( the carrier of b_{1} = the carrier of C & the carrier' of b_{1} = { (id a) where a is Object of C : verum } )

for b_{1}, b_{2} being strict Subcategory of C st the carrier of b_{1} = the carrier of C & the carrier' of b_{1} = { (id a) where a is Object of C : verum } & the carrier of b_{2} = the carrier of C & the carrier' of b_{2} = { (id a) where a is Object of C : verum } holds

b_{1} = b_{2}

end;
func IdCat C -> strict Subcategory of C means :Def20: :: NATTRA_1:def 21

( the carrier of it = the carrier of C & the carrier' of it = { (id a) where a is Object of C : verum } );

existence ( the carrier of it = the carrier of C & the carrier' of it = { (id a) where a is Object of C : verum } );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def20 defines IdCat NATTRA_1:def 21 :

for C being Category

for b_{2} being strict Subcategory of C holds

( b_{2} = IdCat C iff ( the carrier of b_{2} = the carrier of C & the carrier' of b_{2} = { (id a) where a is Object of C : verum } ) );

for C being Category

for b

( b

registration
end;

registration

ex b_{1} being Category st

( b_{1} is strict & b_{1} is discrete )
end;

cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities discrete for Category;

existence ex b

( b

proof end;

registration
end;

::$CT 4