:: Introduction to Categories and Functors
:: by Czes{\l}aw Byli\'nski
::
:: Received October 25, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct CatStr -> MultiGraphStruct ;
aggr CatStr(# carrier, carrier', Source, Target, Comp #) -> CatStr ;
sel Comp c₁ -> PartFunc of [: the carrier' of c₁, the carrier' of c₁:], the carrier' of c₁;

end;

definition

let C be CatStr ;
mode Object of C is Element of C;
mode Morphism of C is Element of the carrier' of C;

end;

:: Domain and codomain of a Morphism

registration

cluster non empty non void for CatStr ;

existence
ex b₁ being CatStr st
( not b₁ is void & not b₁ is empty )

proof end;

end;

definition

let C be CatStr ;
let f, g be Morphism of C;
assume A1: [g,f] in dom the Comp of C ;

func g (*) f -> Morphism of C equals :Def1: :: CAT_1:def 1
the Comp of C . (g,f);

coherence
the Comp of C . (g,f) is Morphism of C by A1, PARTFUN1:4;

end;

:: deftheorem Def1 defines (*) CAT_1:def 1 :
for C being CatStr
for f, g being Morphism of C st [g,f] in dom the Comp of C holds
g (*) f = the Comp of C . (g,f);

definition

let C be non empty non void CatStr ;
let a, b be Object of C;

func Hom (a,b) -> Subset of the carrier' of C equals :: CAT_1:def 4
{ f where f is Morphism of C : ( dom f = a & cod f = b ) } ;

correctness
coherence
{ f where f is Morphism of C : ( dom f = a & cod f = b ) } is Subset of the carrier' of C;

proof end;

end;

:: deftheorem CAT_1:def 2 :
canceled;

:: deftheorem CAT_1:def 3 :
canceled;

:: deftheorem defines Hom CAT_1:def 4 :
for C being non empty non void CatStr
for a, b being Object of C holds Hom (a,b) = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;

theorem Th1: :: CAT_1:1

for C being non empty non void CatStr
for f being Morphism of C
for a, b being Object of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )

proof end;

theorem :: CAT_1:2

for C being non empty non void CatStr
for f being Morphism of C holds Hom ((dom f),(cod f)) <> {} by Th1;

definition

let C be non empty non void CatStr ;
let a, b be Object of C;
assume A1: Hom (a,b) <> {} ;

mode Morphism of a,b -> Morphism of C means :Def3: :: CAT_1:def 5
it in Hom (a,b);

existence
ex b₁ being Morphism of C st b₁ in Hom (a,b) by A1, SUBSET_1:4;

end;

:: deftheorem Def3 defines Morphism CAT_1:def 5 :
for C being non empty non void CatStr
for a, b being Object of C st Hom (a,b) <> {} holds
for b₄ being Morphism of C holds
( b₄ is Morphism of a,b iff b₄ in Hom (a,b) );

theorem :: CAT_1:3

canceled;

::$CT

theorem Th3: :: CAT_1:4

for C being non empty non void CatStr
for f being Morphism of C holds f is Morphism of dom f, cod f

proof end;

theorem Th4: :: CAT_1:5

for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( dom f = a & cod f = b )

proof end;

theorem :: CAT_1:6

for C being non empty non void CatStr
for a, b, c, d being Object of C
for f being Morphism of a,b
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds
( a = c & b = d )

proof end;

theorem Th6: :: CAT_1:7

for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g

proof end;

theorem Th7: :: CAT_1:8

for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}

proof end;

theorem :: CAT_1:9

for C being non empty non void CatStr
for a, b, c, d being Object of C
for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds
ex h being Morphism of c,d st Hom (c,d) = {h}

proof end;

:: Category

definition

let C be non empty non void CatStr ;

attr C is Category-like means :Def4: :: CAT_1:def 6
for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f );

attr C is transitive means :Def5: :: CAT_1:def 7
for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g );

attr C is associative means :Def6: :: CAT_1:def 8
for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f;

attr C is reflexive means :Def7: :: CAT_1:def 9
for b being Element of C holds Hom (b,b) <> {} ;

attr C is with_identities means :Def8: :: CAT_1:def 10
for a being Element of C ex i being Morphism of a,a st
for b being Element of C holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) );

end;

:: deftheorem Def4 defines Category-like CAT_1:def 6 :
for C being non empty non void CatStr holds
( C is Category-like iff for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f ) );

:: deftheorem Def5 defines transitive CAT_1:def 7 :
for C being non empty non void CatStr holds
( C is transitive iff for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) );

:: deftheorem Def6 defines associative CAT_1:def 8 :
for C being non empty non void CatStr holds
( C is associative iff for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f );

:: deftheorem Def7 defines reflexive CAT_1:def 9 :
for C being non empty non void CatStr holds
( C is reflexive iff for b being Element of C holds Hom (b,b) <> {} );

:: deftheorem Def8 defines with_identities CAT_1:def 10 :
for C being non empty non void CatStr holds
( C is with_identities iff for a being Element of C ex i being Morphism of a,a st
for b being Element of C holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) );

definition

let o, m be object ;

func 1Cat (o,m) -> strict CatStr equals :: CAT_1:def 11
CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

correctness
coherence
CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) is strict CatStr ;
;

end;

:: deftheorem defines 1Cat CAT_1:def 11 :
for o, m being object holds 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

registration

let o, m be object ;

cluster 1Cat (o,m) -> non empty trivial non void trivial' strict ;

coherence
( not 1Cat (o,m) is empty & 1Cat (o,m) is trivial & not 1Cat (o,m) is void & 1Cat (o,m) is trivial' ) ;

end;

registration

cluster non empty trivial non void -> non empty non void transitive reflexive for CatStr ;

coherence
for b₁ being non empty non void CatStr st not b₁ is empty & b₁ is trivial holds
( b₁ is transitive & b₁ is reflexive )

proof end;

end;

registration

cluster non empty non void trivial' -> non empty non void associative with_identities for CatStr ;

coherence
for b₁ being non empty non void CatStr st not b₁ is void & b₁ is trivial' holds
( b₁ is associative & b₁ is with_identities )

proof end;

end;

registration

let o, m be object ;

cluster 1Cat (o,m) -> strict Category-like ;

coherence
1Cat (o,m) is Category-like

proof end;

end;

registration

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

existence
ex b₁ being non empty non void CatStr st
( b₁ is reflexive & b₁ is transitive & b₁ is associative & b₁ is with_identities & b₁ is Category-like & not b₁ is void & not b₁ is empty & b₁ is strict )

proof end;

end;

definition

mode Category is non empty non void Category-like transitive associative reflexive with_identities CatStr ;

end;

registration

let C be non empty non void reflexive CatStr ;
let a be Object of C;

cluster Hom (a,a) -> non empty ;

coherence
not Hom (a,a) is empty by Def7;

end;

theorem :: CAT_1:10

canceled;

theorem Th9: :: CAT_1:11

for o, m being set
for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)

proof end;

theorem :: CAT_1:12

for o, m being set
for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b

proof end;

theorem :: CAT_1:13

for o, m being set
for a, b being Object of (1Cat (o,m)) holds Hom (a,b) <> {} by Th9;

theorem :: CAT_1:14

for o, m being set
for a, b, c, d being Object of (1Cat (o,m))
for f being Morphism of a,b
for g being Morphism of c,d holds f = g

proof end;

theorem :: CAT_1:15

for C being Category
for f, g being Morphism of C holds
( dom g = cod f iff [g,f] in dom the Comp of C ) by Def4;

theorem Th14: :: CAT_1:16

for C being Category
for f, g being Morphism of C st dom g = cod f holds
g (*) f = the Comp of C . (g,f)

proof end;

theorem :: CAT_1:17

for C being Category
for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by Def5;

theorem :: CAT_1:18

for C being Category
for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f by Def6;

definition

let C be non empty non void reflexive with_identities CatStr ;
let a be Object of C;

func id a -> Morphism of a,a means :Def10: :: CAT_1:def 12
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) it = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds it (*) f = f ) );

existence
ex b₁ being Morphism of a,a st
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b₁ = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b₁ (*) f = f ) ) by Def8;
uniqueness
for b₁, b₂ being Morphism of a,a st ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b₁ = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b₁ (*) f = f ) ) ) & ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b₂ = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b₂ (*) f = f ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines id CAT_1:def 12 :
for C being non empty non void reflexive with_identities CatStr
for a being Object of C
for b₃ being Morphism of a,a holds
( b₃ = id a iff for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b₃ = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b₃ (*) f = f ) ) );

theorem :: CAT_1:19

canceled;

theorem :: CAT_1:20

canceled;

::$CT 2

theorem :: CAT_1:21

for C being Category
for b being Object of C
for f being Morphism of C st cod f = b holds
(id b) (*) f = f

proof end;

theorem :: CAT_1:22

for C being Category
for b being Object of C
for g being Morphism of C st dom g = b holds
g (*) (id b) = g

proof end;

theorem Th19: :: CAT_1:23

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)

proof end;

definition

let C be Category;
let a, b, c be Object of C;
let f be Morphism of a,b;
let g be Morphism of b,c;
assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ;

func g * f -> Morphism of a,c equals :Def11: :: CAT_1:def 13
g (*) f;

correctness
coherence
g (*) f is Morphism of a,c;

proof end;

end;

:: deftheorem Def11 defines * CAT_1:def 13 :
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g * f = g (*) f;

theorem :: CAT_1:24

for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
Hom (a,c) <> {} by Th19;

theorem Th21: :: CAT_1:25

for C being Category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)

proof end;

theorem :: CAT_1:26

canceled;

::$CT

theorem :: CAT_1:27

for C being Category
for a being Object of C holds id a in Hom (a,a) by Def3;

theorem Th23: :: CAT_1:28

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

proof end;

theorem Th24: :: CAT_1:29

for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
g * (id b) = g

proof end;

registration

let C be Category;
let a be Object of C;
let f be Morphism of a,a;
A1: Hom (a,a) <> {} ;

reduce f * (id a) to f;

reducibility
f * (id a) = f by A1, Th24;

reduce (id a) * f to f;

reducibility
(id a) * f = f by A1, Th23;

end;

theorem :: CAT_1:30

for C being Category
for a being Object of C holds (id a) * (id a) = id a ;

:: Monics, Epis

definition

let C be Category;
let b, c be Object of C;
let g be Morphism of b,c;

attr g is monic means :: CAT_1:def 14
( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 ) );

end;

:: deftheorem defines monic CAT_1:def 14 :
for C being Category
for b, c being Object of C
for g being Morphism of b,c holds
( g is monic iff ( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 ) ) );

definition

let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;

attr f is epi means :: CAT_1:def 15
( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ) );

end;

:: deftheorem defines epi CAT_1:def 15 :
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is epi iff ( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ) ) );

definition

let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;

attr f is invertible means :: CAT_1:def 16
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) );

end;

:: deftheorem defines invertible CAT_1:def 16 :
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is invertible iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) );

theorem :: CAT_1:31

for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) ;

theorem :: CAT_1:32

for C being Category
for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st g is monic & h is monic holds
h * g is monic

proof end;

theorem :: CAT_1:33

for C being Category
for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds
g is monic

proof end;

theorem :: CAT_1:34

for C being Category
for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
g is monic

proof end;

theorem :: CAT_1:35

for C being Category
for b being Object of C holds id b is monic

proof end;

theorem :: CAT_1:36

for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) ;

theorem :: CAT_1:37

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is epi & g is epi holds
g * f is epi

proof end;

theorem :: CAT_1:38

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi

proof end;

theorem :: CAT_1:39

for C being Category
for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
h is epi

proof end;

theorem :: CAT_1:40

for C being Category
for b being Object of C holds id b is epi

proof end;

theorem :: CAT_1:41

for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) ) ;

theorem Th37: :: CAT_1:42

for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds
for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2

proof end;

definition

let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;
assume A1: f is invertible ;

func f " -> Morphism of b,a means :Def15: :: CAT_1:def 17
( f * it = id b & it * f = id a );

existence
ex b₁ being Morphism of b,a st
( f * b₁ = id b & b₁ * f = id a ) by A1;
uniqueness
for b₁, b₂ being Morphism of b,a st f * b₁ = id b & b₁ * f = id a & f * b₂ = id b & b₂ * f = id a holds
b₁ = b₂ by A1, Th37;

end;

:: deftheorem Def15 defines " CAT_1:def 17 :
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
for b₅ being Morphism of b,a holds
( b₅ = f " iff ( f * b₅ = id b & b₅ * f = id a ) );

theorem :: CAT_1:43

for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
( f is monic & f is epi )

proof end;

theorem :: CAT_1:44

for C being Category
for a being Object of C holds id a is invertible

proof end;

theorem Th40: :: CAT_1:45

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible

proof end;

theorem :: CAT_1:46

for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
f " is invertible

proof end;

theorem :: CAT_1:47

for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
(g * f) " = (f ") * (g ")

proof end;

definition

let C be Category;
let a be Object of C;

attr a is terminal means :: CAT_1:def 18
for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g );

attr a is initial means :: CAT_1:def 19
for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g );

let b be Object of C;

pred a,b are_isomorphic means :: CAT_1:def 20
ex f being Morphism of a,b st f is invertible ;

reflexivity
for a being Object of C ex f being Morphism of a,a st f is invertible

proof end;

symmetry
for a, b being Object of C st ex f being Morphism of a,b st f is invertible holds
ex f being Morphism of b,a st f is invertible

proof end;

end;

:: deftheorem defines terminal CAT_1:def 18 :
for C being Category
for a being Object of C holds
( a is terminal iff for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g ) );

:: deftheorem defines initial CAT_1:def 19 :
for C being Category
for a being Object of C holds
( a is initial iff for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g ) );

:: deftheorem defines are_isomorphic CAT_1:def 20 :
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ex f being Morphism of a,b st f is invertible );

theorem :: CAT_1:48

for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )

proof end;

theorem :: CAT_1:49

for C being Category
for a being Object of C holds
( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

proof end;

theorem Th45: :: CAT_1:50

for C being Category
for a being Object of C st a is initial holds
for h being Morphism of a,a holds id a = h

proof end;

theorem :: CAT_1:51

for C being Category
for a, b being Object of C st a is initial & b is initial holds
a,b are_isomorphic

proof end;

theorem :: CAT_1:52

for C being Category
for a, b being Object of C st a is initial & a,b are_isomorphic holds
b is initial

proof end;

theorem :: CAT_1:53

for C being Category
for b being Object of C holds
( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

proof end;

theorem Th49: :: CAT_1:54

for C being Category
for a being Object of C st a is terminal holds
for h being Morphism of a,a holds id a = h

proof end;

theorem :: CAT_1:55

for C being Category
for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic

proof end;

theorem :: CAT_1:56

for C being Category
for a, b being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal

proof end;

theorem :: CAT_1:57

for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds
f is monic

proof end;

registration

let C be Category;
let a be Object of C;

reduce dom (id a) to a;

reducibility
dom (id a) = a

proof end;

reduce cod (id a) to a;

reducibility
cod (id a) = a

proof end;

end;

theorem Th53: :: CAT_1:58

for C being Category
for a being Object of C holds
( dom (id a) = a & cod (id a) = a ) ;

theorem Th54: :: CAT_1:59

for C being Category
for a, b being Object of C st id a = id b holds
a = b

proof end;

theorem :: CAT_1:60

for C being Category
for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds
a,c are_isomorphic

proof end;

:: Functors (Covariant Functors)

definition

let C, D be Category;

mode Functor of C,D -> Function of the carrier' of C, the carrier' of D means :Def19: :: CAT_1:def 21
( ( for c being Element of C ex d being Element of D st it . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
it . (g (*) f) = (it . g) (*) (it . f) ) );

existence
ex b₁ being Function of the carrier' of C, the carrier' of D st
( ( for c being Element of C ex d being Element of D st b₁ . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( b₁ . (id (dom f)) = id (dom (b₁ . f)) & b₁ . (id (cod f)) = id (cod (b₁ . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b₁ . (g (*) f) = (b₁ . g) (*) (b₁ . f) ) )

proof end;

end;

:: deftheorem Def19 defines Functor CAT_1:def 21 :
for C, D being Category
for b₃ being Function of the carrier' of C, the carrier' of D holds
( b₃ is Functor of C,D iff ( ( for c being Element of C ex d being Element of D st b₃ . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( b₃ . (id (dom f)) = id (dom (b₃ . f)) & b₃ . (id (cod f)) = id (cod (b₃ . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b₃ . (g (*) f) = (b₃ . g) (*) (b₃ . f) ) ) );

theorem Th56: :: CAT_1:61

for C, D being Category
for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D

proof end;

theorem :: CAT_1:62

for C, D being Category
for T being Functor of C,D
for c being Object of C ex d being Object of D st T . (id c) = id d by Def19;

theorem :: CAT_1:63

for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def19;

theorem Th59: :: CAT_1:64

for C, D being Category
for T being Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )

proof end;

theorem Th60: :: CAT_1:65

for C, D being Category
for T being Function of the carrier' of C, the carrier' of D
for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D

proof end;

:: Object Function of a Functor

definition

let C, D be Category;
let F be Function of the carrier' of C, the carrier' of D;
assume A1: for c being Element of C ex d being Element of D st F . (id c) = id d ;

func Obj F -> Function of the carrier of C, the carrier of D means :Def20: :: CAT_1:def 22
for c being Element of C
for d being Element of D st F . (id c) = id d holds
it . c = d;

existence
ex b₁ being Function of the carrier of C, the carrier of D st
for c being Element of C
for d being Element of D st F . (id c) = id d holds
b₁ . c = d

proof end;

uniqueness
for b₁, b₂ being Function of the carrier of C, the carrier of D st ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
b₁ . c = d ) & ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
b₂ . c = d ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines Obj CAT_1:def 22 :
for C, D being Category
for F being Function of the carrier' of C, the carrier' of D st ( for c being Element of C ex d being Element of D st F . (id c) = id d ) holds
for b₄ being Function of the carrier of C, the carrier of D holds
( b₄ = Obj F iff for c being Element of C
for d being Element of D st F . (id c) = id d holds
b₄ . c = d );

theorem :: CAT_1:66

for C, D being Category
for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) holds
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d by Def20;

theorem Th62: :: CAT_1:67

for C, D being Category
for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d

proof end;

theorem Th63: :: CAT_1:68

for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . (id c) = id ((Obj T) . c)

proof end;

theorem Th64: :: CAT_1:69

for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )

proof end;

definition

let C, D be Category;
let T be Functor of C,D;
let c be Object of C;

func T . c -> Object of D equals :: CAT_1:def 23
(Obj T) . c;

correctness
coherence
(Obj T) . c is Object of D;
;

end;

:: deftheorem defines . CAT_1:def 23 :
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . c = (Obj T) . c;

theorem :: CAT_1:70

for C, D being Category
for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
T . c = d by Th62;

theorem :: CAT_1:71

for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . (id c) = id (T . c) by Th63;

theorem :: CAT_1:72

for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( T . (dom f) = dom (T . f) & T . (cod f) = cod (T . f) ) by Th64;

theorem Th68: :: CAT_1:73

for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D holds S * T is Functor of B,D

proof end;

:: Composition of Functors

definition

let B, C, D be Category;
let T be Functor of B,C;
let S be Functor of C,D;
:: original: *
redefine func S * T -> Functor of B,D;
coherence
T * S is Functor of B,D by Th68;

end;

theorem Th69: :: CAT_1:74

for C being Category holds id the carrier' of C is Functor of C,C

proof end;

theorem Th70: :: CAT_1:75

for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)

proof end;

theorem :: CAT_1:76

for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (S * T) . b = S . (T . b) by Th70;

:: Identity Functor

definition

let C be Category;

func id C -> Functor of C,C equals :: CAT_1:def 24
id the carrier' of C;

coherence
id the carrier' of C is Functor of C,C by Th69;

end;

:: deftheorem defines id CAT_1:def 24 :
for C being Category holds id C = id the carrier' of C;

theorem Th72: :: CAT_1:77

for C being Category
for c being Object of C holds (Obj (id C)) . c = c

proof end;

theorem Th73: :: CAT_1:78

for C being Category holds Obj (id C) = id the carrier of C

proof end;

theorem :: CAT_1:79

for C being Category
for c being Object of C holds (id C) . c = c by Th72;

definition

let C, D be Category;
let T be Functor of C,D;

attr T is isomorphic means :: CAT_1:def 25
( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D );

attr T is full means :: CAT_1:def 26
for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds
for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f );

attr T is faithful means :: CAT_1:def 27
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2;

end;

:: deftheorem defines isomorphic CAT_1:def 25 :
for C, D being Category
for T being Functor of C,D holds
( T is isomorphic iff ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ) );

:: deftheorem defines full CAT_1:def 26 :
for C, D being Category
for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds
for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

:: deftheorem defines faithful CAT_1:def 27 :
for C, D being Category
for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2 );

theorem :: CAT_1:80

for C being Category holds id C is isomorphic

proof end;

theorem Th76: :: CAT_1:81

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C
for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))

proof end;

theorem Th77: :: CAT_1:82

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))

proof end;

theorem Th78: :: CAT_1:83

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9

proof end;

theorem Th79: :: CAT_1:84

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
Hom ((T . c),(T . c9)) <> {}

proof end;

theorem :: CAT_1:85

for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D st T is full & S is full holds
S * T is full

proof end;

theorem :: CAT_1:86

for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D st T is faithful & S is faithful holds
S * T is faithful

proof end;

theorem Th82: :: CAT_1:87

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))

proof end;

definition

let C, D be Category;
let T be Functor of C,D;
let c, c9 be Object of C;

func hom (T,c,c9) -> Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))) equals :: CAT_1:def 28
T | (Hom (c,c9));

correctness
coherence
T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9)));

proof end;

end;

:: deftheorem defines hom CAT_1:def 28 :
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds hom (T,c,c9) = T | (Hom (c,c9));

theorem Th83: :: CAT_1:88

for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f

proof end;

theorem :: CAT_1:89

for C, D being Category
for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )

proof end;

theorem :: CAT_1:90

for C, D being Category
for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )

proof end;

theorem :: CAT_1:91

for C being Category
for a, b being Element of C st Hom (a,b) <> {} holds
ex m being Morphism of a,b st m in Hom (a,b)

proof end;

theorem :: CAT_1:92

for C being Category holds the carrier' of C = union { (Hom (a,b)) where a, b is Object of C : verum }

proof end;