:: NATTRA_1 semantic presentation

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
let c₄ be Subset of c₁;
redefine func | as c₃ | c₄ -> Function of a₄,a₂;
coherence by FUNCT_2:38;

end;

theorem Th1: :: NATTRA_1:1

for b₁, b₂, b₃, b₄ being non empty set
for b₅ being Function of b₃,b₁
for b₆ being Function of b₄,b₂
for b₇ being non empty Subset of b₃
for b₈ being non empty Subset of b₄ holds [:b₅,b₆:] | [:b₇,b₈:] = [:(b₅ | b₇),(b₆ | b₈):]

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Subset of c₁;
let c₄ be non empty Subset of c₂;
let c₅ be PartFunc of [:c₃,c₃:],c₃;
let c₆ be PartFunc of [:c₄,c₄:],c₄;
redefine func |: as |:c₅,c₆:| -> PartFunc of [:[:a₃,a₄:],[:a₃,a₄:]:],[:a₃,a₄:];
coherence by FUNCT_4:62;

end;

theorem Th2: :: NATTRA_1:2

for b₁, b₂ being non empty set
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂
for b₅ being PartFunc of [:b₁,b₁:],b₁
for b₆ being PartFunc of [:b₂,b₂:],b₂
for b₇ being PartFunc of [:b₃,b₃:],b₃ st b₇ = b₅ || b₃ holds
for b₈ being PartFunc of [:b₄,b₄:],b₄ st b₈ = b₆ || b₄ holds
|:b₇,b₈:| = |:b₅,b₆:| || [:b₃,b₄:]

proof end;

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

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

provided

E3: for b₁ being Element of F₁() holds F₂() meets F₃(b₁)

proof end;

theorem Th3: :: NATTRA_1:3

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Morphism of b₂,b₂ holds b₃ in Hom b₂,b₂

proof end;

theorem Th4: :: NATTRA_1:4

for b₁, b₂ being set
for b₃, b₄ being Morphism of (1Cat b₁,b₂) holds b₃ = b₄

proof end;

theorem Th5: :: NATTRA_1:5

for b₁ being Category
for b₂ being Object of b₁ holds [[(id b₂),(id b₂)],(id b₂)] in the Comp of b₁

proof end;

theorem Th6: :: NATTRA_1:6

for b₁, b₂ being set holds the Comp of (1Cat b₁,b₂) = {[[b₂,b₂],b₂]}

proof end;

theorem Th7: :: NATTRA_1:7

for b₁ being Category
for b₂ being Object of b₁ holds 1Cat b₂,(id b₂) is Subcategory of b₁

proof end;

theorem Th8: :: NATTRA_1:8

for b₁ being Category
for b₂ being Subcategory of b₁ holds
( the Dom of b₂ = the Dom of b₁ | the Morphisms of b₂ & the Cod of b₂ = the Cod of b₁ | the Morphisms of b₂ & the Comp of b₂ = the Comp of b₁ || the Morphisms of b₂ & the Id of b₂ = the Id of b₁ | the Objects of b₂ )

proof end;

theorem Th9: :: NATTRA_1:9

for b₁ being Category
for b₂ being non empty Subset of the Objects of b₁
for b₃ being non empty Subset of the Morphisms of b₁
for b₄, b₅ being Function of b₃,b₂ st b₄ = the Dom of b₁ | b₃ & b₅ = the Cod of b₁ | b₃ holds
for b₆ being PartFunc of [:b₃,b₃:],b₃ st b₆ = the Comp of b₁ || b₃ holds
for b₇ being Function of b₂,b₃ st b₇ = the Id of b₁ | b₂ holds
CatStr(# b₂,b₃,b₄,b₅,b₆,b₇ #) is Subcategory of b₁

proof end;

theorem Th10: :: NATTRA_1:10

for b₁ being strict Category
for b₂ being strict Subcategory of b₁ st the Objects of b₂ = the Objects of b₁ & the Morphisms of b₂ = the Morphisms of b₁ holds
b₂ = b₁

proof end;

definition

let c₁, c₂ be Category;
let c₃ be Functor of c₁,c₂;
let c₄, c₅ be Object of c₁;
assume E11: Hom c₄,c₅ <> {} ;
let c₆ be Morphism of c₄,c₅;
func c₃ . c₆ -> Morphism of a₃ . a₄,a₃ . a₅ equals :Def1: :: NATTRA_1:def 1
a₃ . a₆;
coherence by E11, CAT_1:125;

end;

:: deftheorem Def1 defines . NATTRA_1:def 1 :

theorem Th11: :: NATTRA_1:11

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₃,b₁
for b₅ being Functor of b₁,b₂
for b₆, b₇ being Object of b₃ st Hom b₆,b₇ <> {} holds
for b₈ being Morphism of b₆,b₇ holds (b₅ * b₄) . b₈ = b₅ . (b₄ . b₈)

proof end;

theorem Th12: :: NATTRA_1:12

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂ st ( for b₅, b₆ being Object of b₁ st Hom b₅,b₆ <> {} holds
for b₇ being Morphism of b₅,b₆ holds b₃ . b₇ = b₄ . b₇ ) holds
b₃ = b₄

proof end;

theorem Th13: :: NATTRA_1:13

for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁
for b₄, b₅, b₆ being Object of b₂ st Hom b₄,b₅ <> {} & Hom b₅,b₆ <> {} holds
for b₇ being Morphism of b₄,b₅
for b₈ being Morphism of b₅,b₆ holds b₃ . (b₈ * b₇) = (b₃ . b₈) * (b₃ . b₇)

proof end;

theorem Th14: :: NATTRA_1:14

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂
for b₄ being Object of b₁
for b₅ being Object of b₂ st b₃ . (id b₄) = id b₅ holds
b₃ . b₄ = b₅

proof end;

theorem Th15: :: NATTRA_1:15

for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁
for b₄ being Object of b₂ holds b₃ . (id b₄) = id (b₃ . b₄)

proof end;

theorem Th16: :: NATTRA_1:16

for b₁ being Category
for b₂, b₃ being Object of b₁ st Hom b₂,b₃ <> {} holds
for b₄ being Morphism of b₂,b₃ holds (id b₁) . b₄ = b₄

proof end;

theorem Th17: :: NATTRA_1:17

for b₁ being Category
for b₂, b₃, b₄, b₅ being Object of b₁ st Hom b₂,b₃ meets Hom b₄,b₅ holds
( b₂ = b₄ & b₃ = b₅ )

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
pred c₃ is_transformable_to c₄ means :Def2: :: NATTRA_1:def 2
for b₁ being Object of a₁ holds Hom (a₃ . b₁),(a₄ . b₁) <> {} ;
reflexivity by CAT_1:56;

end;

:: deftheorem Def2 defines is_transformable_to NATTRA_1:def 2 :

theorem Th18: :: NATTRA_1:18

canceled;

theorem Th19: :: NATTRA_1:19

for b₁, b₂ being Category
for b₃, b₄, b₅ being Functor of b₁,b₂ st b₃ is_transformable_to b₄ & b₄ is_transformable_to b₅ holds
b₃ is_transformable_to b₅

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
assume E17: c₃ is_transformable_to c₄ ;
mode transformation of c₃,c₄ -> Function of the Objects of a₁,the Morphisms of a₂ means :Def3: :: NATTRA_1:def 3
for b₁ being Object of a₁ holds a₅ . b₁ is Morphism of a₃ . b₁,a₄ . b₁;
existence

proof end;

end;

:: deftheorem Def3 defines transformation NATTRA_1:def 3 :

definition

let c₁, c₂ be Category;
let c₃ be Functor of c₁,c₂;
func id c₃ -> transformation of a₃,a₃ means :Def4: :: NATTRA_1:def 4
for b₁ being Object of a₁ holds a₄ . b₁ = id (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines id NATTRA_1:def 4 :

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
assume E19: c₃ is_transformable_to c₄ ;
let c₅ be transformation of c₃,c₄;
let c₆ be Object of c₁;
func c₅ . c₆ -> Morphism of a₃ . a₆,a₄ . a₆ equals :Def5: :: NATTRA_1:def 5
a₅ . a₆;
coherence by E19, Def3;

end;

:: deftheorem Def5 defines . NATTRA_1:def 5 :

definition

let c₁, c₂ be Category;
let c₃, c₄, c₅ be Functor of c₁,c₂;
assume that
E20: c₃ is_transformable_to c₄ and
E21: c₄ is_transformable_to c₅ ;
let c₆ be transformation of c₃,c₄;
let c₇ be transformation of c₄,c₅;
func c₇ `*` c₆ -> transformation of a₃,a₅ means :Def6: :: NATTRA_1:def 6
for b₁ being Object of a₁ holds a₈ . b₁ = (a₇ . b₁) * (a₆ . b₁);
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th20: :: NATTRA_1:20

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₂,b₁ st b₃ is_transformable_to b₄ holds
for b₅, b₆ being transformation of b₃,b₄ st ( for b₇ being Object of b₂ holds b₅ . b₇ = b₆ . b₇ ) holds
b₅ = b₆

proof end;

theorem Th21: :: NATTRA_1:21

for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁
for b₄ being Object of b₂ holds (id b₃) . b₄ = id (b₃ . b₄)

proof end;

theorem Th22: :: NATTRA_1:22

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂ st b₃ is_transformable_to b₄ holds
for b₅ being transformation of b₃,b₄ holds
( (id b₄) `*` b₅ = b₅ & b₅ `*` (id b₃) = b₅ )

proof end;

theorem Th23: :: NATTRA_1:23

for b₁, b₂ being Category
for b₃, b₄, b₅, b₆ being Functor of b₁,b₂ st b₃ is_transformable_to b₄ & b₄ is_transformable_to b₅ & b₅ is_transformable_to b₆ holds
for b₇ being transformation of b₃,b₄
for b₈ being transformation of b₄,b₅
for b₉ being transformation of b₅,b₆ holds (b₉ `*` b₈) `*` b₇ = b₉ `*` (b₈ `*` b₇)

proof end;

Lemma25: for b₁, b₂ being Category
for b₃ being Functor of b₂,b₁
for b₄, b₅ being Object of b₂ st Hom b₄,b₅ <> {} holds
for b₆ being Morphism of b₄,b₅ holds ((id b₃) . b₅) * (b₃ . b₆) = (b₃ . b₆) * ((id b₃) . b₄)

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
pred c₃ is_naturally_transformable_to c₄ means :Def7: :: NATTRA_1:def 7
( a₃ is_transformable_to a₄ & ex b₁ being transformation of a₃,a₄ st
for b₂, b₃ being Object of a₁ st Hom b₂,b₃ <> {} holds
for b₄ being Morphism of b₂,b₃ holds (b₁ . b₃) * (a₃ . b₄) = (a₄ . b₄) * (b₁ . b₂) );
reflexivity

proof end;

end;

:: deftheorem Def7 defines is_naturally_transformable_to NATTRA_1:def 7 :

Lemma27: for b₁, b₂ being Category
for b₃, b₄, b₅ being Functor of b₂,b₁ st b₃ is_transformable_to b₄ & b₄ is_transformable_to b₅ holds
for b₆ being transformation of b₃,b₄ st ( for b₇, b₈ being Object of b₂ st Hom b₇,b₈ <> {} holds
for b₉ being Morphism of b₇,b₈ holds (b₆ . b₈) * (b₃ . b₉) = (b₄ . b₉) * (b₆ . b₇) ) holds
for b₇ being transformation of b₄,b₅ st ( for b₈, b₉ being Object of b₂ st Hom b₈,b₉ <> {} holds
for b₁₀ being Morphism of b₈,b₉ holds (b₇ . b₉) * (b₄ . b₁₀) = (b₅ . b₁₀) * (b₇ . b₈) ) holds
for b₈, b₉ being Object of b₂ st Hom b₈,b₉ <> {} holds
for b₁₀ being Morphism of b₈,b₉ holds ((b₇ `*` b₆) . b₉) * (b₃ . b₁₀) = (b₅ . b₁₀) * ((b₇ `*` b₆) . b₈)

proof end;

theorem Th24: :: NATTRA_1:24

canceled;

theorem Th25: :: NATTRA_1:25

for b₁, b₂ being Category
for b₃, b₄, b₅ being Functor of b₁,b₂ st b₃ is_naturally_transformable_to b₄ & b₄ is_naturally_transformable_to b₅ holds
b₃ is_naturally_transformable_to b₅

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
assume E29: c₃ is_naturally_transformable_to c₄ ;
mode natural_transformation of c₃,c₄ -> transformation of a₃,a₄ means :Def8: :: NATTRA_1:def 8
for b₁, b₂ being Object of a₁ st Hom b₁,b₂ <> {} holds
for b₃ being Morphism of b₁,b₂ holds (a₅ . b₂) * (a₃ . b₃) = (a₄ . b₃) * (a₅ . b₁);
existence by E29, Def7;

end;

:: deftheorem Def8 defines natural_transformation NATTRA_1:def 8 :

definition

let c₁, c₂ be Category;
let c₃ be Functor of c₁,c₂;
redefine func id as id c₃ -> natural_transformation of a₃,a₃;
coherence

proof end;

end;

definition

let c₁, c₂ be Category;
let c₃, c₄, c₅ be Functor of c₁,c₂;
assume that
E30: c₃ is_naturally_transformable_to c₄ and
E31: c₄ is_naturally_transformable_to c₅ ;
let c₆ be natural_transformation of c₃,c₄;
let c₇ be natural_transformation of c₄,c₅;
func c₇ `*` c₆ -> natural_transformation of a₃,a₅ equals :Def9: :: NATTRA_1:def 9
a₇ `*` a₆;
coherence

proof end;

end;

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

theorem Th26: :: NATTRA_1:26

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂ st b₃ is_naturally_transformable_to b₄ holds
for b₅ being natural_transformation of b₃,b₄ holds
( (id b₄) `*` b₅ = b₅ & b₅ `*` (id b₃) = b₅ )

proof end;

theorem Th27: :: NATTRA_1:27

for b₁, b₂ being Category
for b₃, b₄, b₅ being Functor of b₂,b₁ st b₃ is_naturally_transformable_to b₄ & b₄ is_naturally_transformable_to b₅ holds
for b₆ being natural_transformation of b₃,b₄
for b₇ being natural_transformation of b₄,b₅
for b₈ being Object of b₂ holds (b₇ `*` b₆) . b₈ = (b₇ . b₈) * (b₆ . b₈)

proof end;

theorem Th28: :: NATTRA_1:28

for b₁, b₂ being Category
for b₃, b₄, b₅, b₆ being Functor of b₁,b₂
for b₇ being natural_transformation of b₃,b₄
for b₈ being natural_transformation of b₄,b₅ st b₃ is_naturally_transformable_to b₄ & b₄ is_naturally_transformable_to b₅ & b₅ is_naturally_transformable_to b₆ holds
for b₉ being natural_transformation of b₅,b₆ holds (b₉ `*` b₈) `*` b₇ = b₉ `*` (b₈ `*` b₇)

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
let c₅ be transformation of c₃,c₄;
attr a₅ is invertible means :Def10: :: NATTRA_1:def 10
for b₁ being Object of a₁ holds a₅ . b₁ is invertible;

end;

:: deftheorem Def10 defines invertible NATTRA_1:def 10 :

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
pred c₃,c₄ are_naturally_equivalent means :Def11: :: NATTRA_1:def 11
( a₃ is_naturally_transformable_to a₄ & ex b₁ being natural_transformation of a₃,a₄ st b₁ is invertible );
reflexivity

proof end;

end;

:: deftheorem Def11 defines are_naturally_equivalent NATTRA_1:def 11 :

notation

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
synonym c₃ ~= c₄ for c₃,c₄ are_naturally_equivalent ;

end;

Lemma36: for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂
for b₅ being transformation of b₃,b₄ st b₃ is_transformable_to b₄ & b₅ is invertible holds
b₄ is_transformable_to b₃

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
assume E37: c₃ is_transformable_to c₄ ;
let c₅ be transformation of c₃,c₄;
assume E38: c₅ is invertible ;
func c₅ " -> transformation of a₄,a₃ means :Def12: :: NATTRA_1:def 12
for b₁ being Object of a₁ holds a₆ . b₁ = (a₅ . b₁) " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines " NATTRA_1:def 12 :

E38: now

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
let c₅ be natural_transformation of c₃,c₄;
assume that
E39: c₃ is_naturally_transformable_to c₄ and
E40: c₅ is invertible ;
E41: c₃ is_transformable_to c₄ by E39, Def7;
let c₆, c₇ be Object of c₁;
assume E42: Hom c₆,c₇ <> {} ;
E43: c₅ . c₇ is invertible by E40, Def10;
E44: c₅ . c₆ is invertible by E40, Def10;
E45: Hom (c₃ . c₆),(c₃ . c₇) <> {} by E42, CAT_1:126;
E46: Hom (c₃ . c₆),(c₄ . c₆) <> {} by E41, Def2;
E47: Hom (c₃ . c₇),(c₄ . c₇) <> {} by E41, Def2;
then E48: Hom (c₄ . c₇),(c₃ . c₇) <> {} by E43, CAT_1:70;
E49: Hom (c₄ . c₆),(c₄ . c₇) <> {} by E42, CAT_1:126;
E50: Hom (c₄ . c₆),(c₃ . c₆) <> {} by E44, E46, CAT_1:70;
then E51: Hom (c₄ . c₆),(c₃ . c₇) <> {} by E45, CAT_1:52;
let c₈ be Morphism of c₆,c₇;
(c₄ . c₈) * (c₅ . c₆) = (c₅ . c₇) * (c₃ . c₈) by E39, E42, Def8;
then E52: (((c₅ . c₇) " ) * (c₄ . c₈)) * (c₅ . c₆) = ((c₅ . c₇) " ) * ((c₅ . c₇) * (c₃ . c₈)) by E46, E48, E49, CAT_1:54
.= (((c₅ . c₇) " ) * (c₅ . c₇)) * (c₃ . c₈) by E45, E47, E48, CAT_1:54
.= (id (c₃ . c₇)) * (c₃ . c₈) by E43, E47, CAT_1:def 14
.= c₃ . c₈ by E45, CAT_1:57 ;
((c₅ . c₇) " ) * (c₄ . c₈) = (((c₅ . c₇) " ) * (c₄ . c₈)) * (id (c₄ . c₆)) by E51, CAT_1:58
.= (((c₅ . c₇) " ) * (c₄ . c₈)) * ((c₅ . c₆) * ((c₅ . c₆) " )) by E44, E46, CAT_1:def 14
.= (c₃ . c₈) * ((c₅ . c₆) " ) by E46, E50, E51, E52, CAT_1:54 ;
hence ((c₅ " ) . c₇) * (c₄ . c₈) = (c₃ . c₈) * ((c₅ . c₆) " ) by E40, E41, Def12
.= (c₃ . c₈) * ((c₅ " ) . c₆) by E40, E41, Def12 ;

end;

Lemma39: for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂
for b₅ being natural_transformation of b₃,b₄ st b₃ is_naturally_transformable_to b₄ & b₅ is invertible holds
b₄ is_naturally_transformable_to b₃

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
let c₅ be natural_transformation of c₃,c₄;
assume that
E40: c₃ is_naturally_transformable_to c₄ and
E41: c₅ is invertible ;
func c₅ " -> natural_transformation of a₄,a₃ equals :Def13: :: NATTRA_1:def 13
a₅ " ;
coherence

proof end;

end;

:: deftheorem Def13 defines " NATTRA_1:def 13 :

theorem Th29: :: NATTRA_1:29

canceled;

theorem Th30: :: NATTRA_1:30

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂
for b₅ being natural_transformation of b₃,b₄ st b₃ is_naturally_transformable_to b₄ & b₅ is invertible holds
for b₆ being Object of b₁ holds (b₅ " ) . b₆ = (b₅ . b₆) "

proof end;

theorem Th31: :: NATTRA_1:31

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂ st b₃ ~= b₄ holds
b₄ ~= b₃

proof end;

theorem Th32: :: NATTRA_1:32

for b₁, b₂ being Category
for b₃, b₄, b₅ being Functor of b₁,b₂ st b₃ ~= b₄ & b₄ ~= b₅ holds
b₃ ~= b₅

proof end;

definition

let c₁, c₂ be Category;
let c₃, c₄ be Functor of c₁,c₂;
assume E43: c₃,c₄ are_naturally_equivalent ;
mode natural_equivalence of c₃,c₄ -> natural_transformation of a₃,a₄ means :Def14: :: NATTRA_1:def 14
a₅ is invertible;
existence by E43, Def11;

end;

:: deftheorem Def14 defines natural_equivalence NATTRA_1:def 14 :

theorem Th33: :: NATTRA_1:33

for b₁, b₂ being Category
for b₃ being Functor of b₁,b₂ holds id b₃ is natural_equivalence of b₃,b₃

proof end;

theorem Th34: :: NATTRA_1:34

for b₁, b₂ being Category
for b₃, b₄, b₅ being Functor of b₁,b₂ st b₃ ~= b₄ & b₄ ~= b₅ holds
for b₆ being natural_equivalence of b₃,b₄
for b₇ being natural_equivalence of b₄,b₅ holds b₇ `*` b₆ is natural_equivalence of b₃,b₅

proof end;

definition

let c₁, c₂ be Category;
mode NatTrans-DOMAIN of c₁,c₂ -> non empty set means :Def15: :: NATTRA_1:def 15
for b₁ being set st b₁ in a₃ holds
ex b₂, b₃ being Functor of a₁,a₂ex b₄ being natural_transformation of b₂,b₃ st
( b₁ = [[b₂,b₃],b₄] & b₂ is_naturally_transformable_to b₃ );
existence

proof end;

end;

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

definition

let c₁, c₂ be Category;
func NatTrans c₁,c₂ -> NatTrans-DOMAIN of a₁,a₂ means :Def16: :: NATTRA_1:def 16
for b₁ being set holds
( b₁ in a₃ iff ex b₂, b₃ being Functor of a₁,a₂ex b₄ being natural_transformation of b₂,b₃ st
( b₁ = [[b₂,b₃],b₄] & b₂ is_naturally_transformable_to b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines NatTrans NATTRA_1:def 16 :

definition

let c₁, c₂, c₃, c₄ be non empty set ;
let c₅ be Function of c₁,c₂;
let c₆ be Function of c₃,c₄;
redefine pred = as c₅ = c₆ means :: NATTRA_1:def 17
( a₁ = a₃ & ( for b₁ being Element of a₁ holds a₅ . b₁ = a₆ . b₁ ) );
compatibility

proof end;

end;

:: deftheorem Def17 defines = NATTRA_1:def 17 :

theorem Th35: :: NATTRA_1:35

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂
for b₅ being natural_transformation of b₃,b₄ holds
( b₃ is_naturally_transformable_to b₄ iff [[b₃,b₄],b₅] in NatTrans b₁,b₂ )

proof end;

definition

let c₁, c₂ be Category;
func Functors c₁,c₂ -> strict Category means :Def18: :: NATTRA_1:def 18
( the Objects of a₃ = Funct a₁,a₂ & the Morphisms of a₃ = NatTrans a₁,a₂ & ( for b₁ being Morphism of a₃ holds
( dom b₁ = (b₁ `1 ) `1 & cod b₁ = (b₁ `1 ) `2 ) ) & ( for b₁, b₂ being Morphism of a₃ st dom b₂ = cod b₁ holds
[b₂,b₁] in dom the Comp of a₃ ) & ( for b₁, b₂ being Morphism of a₃ st [b₂,b₁] in dom the Comp of a₃ holds
ex b₃, b₄, b₅ being Functor of a₁,a₂ex b₆ being natural_transformation of b₃,b₄ex b₇ being natural_transformation of b₄,b₅ st
( b₁ = [[b₃,b₄],b₆] & b₂ = [[b₄,b₅],b₇] & the Comp of a₃ . [b₂,b₁] = [[b₃,b₅],(b₇ `*` b₆)] ) ) & ( for b₁ being Object of a₃
for b₂ being Functor of a₁,a₂ st b₂ = b₁ holds
id b₁ = [[b₂,b₂],(id b₂)] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Functors NATTRA_1:def 18 :

theorem Th36: :: NATTRA_1:36

canceled;

theorem Th37: :: NATTRA_1:37

canceled;

theorem Th38: :: NATTRA_1:38

canceled;

theorem Th39: :: NATTRA_1:39

for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂
for b₅ being natural_transformation of b₃,b₄
for b₆ being Morphism of (Functors b₁,b₂) st b₆ = [[b₃,b₄],b₅] holds
( dom b₆ = b₃ & cod b₆ = b₄ )

proof end;

theorem Th40: :: NATTRA_1:40

for b₁, b₂ being Category
for b₃, b₄ being Object of (Functors b₁,b₂)
for b₅ being Morphism of b₃,b₄ st Hom b₃,b₄ <> {} holds
ex b₆, b₇ being Functor of b₁,b₂ex b₈ being natural_transformation of b₆,b₇ st
( b₃ = b₆ & b₄ = b₇ & b₅ = [[b₆,b₇],b₈] )

proof end;

theorem Th41: :: NATTRA_1:41

for b₁, b₂ being Category
for b₃, b₄, b₅, b₆ being Functor of b₁,b₂
for b₇ being natural_transformation of b₅,b₆
for b₈ being natural_transformation of b₃,b₄
for b₉, b₁₀ being Morphism of (Functors b₁,b₂) st b₉ = [[b₅,b₆],b₇] & b₁₀ = [[b₃,b₄],b₈] holds
( [b₁₀,b₉] in dom the Comp of (Functors b₁,b₂) iff b₆ = b₃ )

proof end;

theorem Th42: :: NATTRA_1:42

for b₁, b₂ being Category
for b₃, b₄, b₅ being Functor of b₁,b₂
for b₆ being natural_transformation of b₃,b₄
for b₇ being natural_transformation of b₄,b₅
for b₈, b₉ being Morphism of (Functors b₁,b₂) st b₈ = [[b₃,b₄],b₆] & b₉ = [[b₄,b₅],b₇] holds
b₉ * b₈ = [[b₃,b₅],(b₇ `*` b₆)]

proof end;

definition

let c₁ be Category;
attr a₁ is discrete means :Def19: :: NATTRA_1:def 19
for b₁ being Morphism of a₁ ex b₂ being Object of a₁ st b₁ = id b₂;

end;

:: deftheorem Def19 defines discrete NATTRA_1:def 19 :

registration

cluster discrete CatStr ;
existence

proof end;

end;

theorem Th43: :: NATTRA_1:43

canceled;

theorem Th44: :: NATTRA_1:44

for b₁ being discrete Category
for b₂ being Object of b₁ holds Hom b₂,b₂ = {(id b₂)}

proof end;

theorem Th45: :: NATTRA_1:45

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

proof end;

theorem Th46: :: NATTRA_1:46

for b₁, b₂ being set holds 1Cat b₁,b₂ is discrete

proof end;

theorem Th47: :: NATTRA_1:47

for b₁ being discrete Category
for b₂ being Subcategory of b₁ holds b₂ is discrete

proof end;

theorem Th48: :: NATTRA_1:48

for b₁, b₂ being Category st b₁ is discrete & b₂ is discrete holds
[:b₁,b₂:] is discrete

proof end;

theorem Th49: :: NATTRA_1:49

for b₁ being discrete Category
for b₂ being Category
for b₃, b₄ being Functor of b₂,b₁ st b₃ is_transformable_to b₄ holds
b₃ = b₄

proof end;

theorem Th50: :: NATTRA_1:50

for b₁ being discrete Category
for b₂ being Category
for b₃ being Functor of b₂,b₁
for b₄ being transformation of b₃,b₃ holds b₄ = id b₃

proof end;

theorem Th51: :: NATTRA_1:51

for b₁, b₂ being Category st b₁ is discrete holds
Functors b₂,b₁ is discrete

proof end;

registration

let c₁ be Category;
cluster strict discrete Subcategory of a₁;
existence

proof end;

end;

definition

let c₁ be Category;
func IdCat c₁ -> strict discrete Subcategory of a₁ means :Def20: :: NATTRA_1:def 20
( the Objects of a₂ = the Objects of a₁ & the Morphisms of a₂ = { (id b₁) where B is Object of a₁ : verum } );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines IdCat NATTRA_1:def 20 :

theorem Th52: :: NATTRA_1:52

for b₁ being strict Category st b₁ is discrete holds
IdCat b₁ = b₁

proof end;

theorem Th53: :: NATTRA_1:53

for b₁ being Category holds IdCat (IdCat b₁) = IdCat b₁ by Th52;

theorem Th54: :: NATTRA_1:54

for b₁, b₂ being set holds IdCat (1Cat b₁,b₂) = 1Cat b₁,b₂

proof end;

theorem Th55: :: NATTRA_1:55

for b₁, b₂ being Category holds IdCat [:b₁,b₂:] = [:(IdCat b₁),(IdCat b₂):]

proof end;