:: CAT_1 semantic presentation

theorem :: CAT_1:1

canceled;

theorem :: CAT_1:2

canceled;

theorem :: CAT_1:3

canceled;

theorem Th4: :: CAT_1:4

for X, Y, Z being set
for D being non empty set
for f being Function of X,D st Y c= X & f .: Y c= Z holds
f | Y is Function of Y,Z

proof end;

definition

let a, b, c be set ;
func a,b .--> c -> PartFunc of [:{a},{b}:],{c} equals :: CAT_1:def 1
[a,b] .--> c;
correctness

proof end;

end;

:: deftheorem defines .--> CAT_1:def 1 :

theorem :: CAT_1:5

canceled;

theorem :: CAT_1:6

canceled;

theorem Th7: :: CAT_1:7

for a, b, c being set holds
( dom (a,b .--> c) = {[a,b]} & dom (a,b .--> c) = [:{a},{b}:] )

proof end;

theorem Th8: :: CAT_1:8

for a, b, c being set holds (a,b .--> c) . [a,b] = c

proof end;

theorem Th9: :: CAT_1:9

for a, b, c being set
for x being Element of {a}
for y being Element of {b} holds (a,b .--> c) . [x,y] = c

proof end;

definition

attr c₁ is strict;
struct CatStr -> ;
aggr CatStr(# Objects, Morphisms, Dom, Cod, Comp, Id #) -> CatStr ;
sel Objects c₁ -> non empty set ;
sel Morphisms c₁ -> non empty set ;
sel Dom c₁ -> Function of the Morphisms of c₁,the Objects of c₁;
sel Cod c₁ -> Function of the Morphisms of c₁,the Objects of c₁;
sel Comp c₁ -> PartFunc of [:the Morphisms of c₁,the Morphisms of c₁:],the Morphisms of c₁;
sel Id c₁ -> Function of the Objects of c₁,the Morphisms of c₁;

end;

definition

let C be CatStr ;
mode Object of C is Element of the Objects of C;
mode Morphism of C is Element of the Morphisms of C;

end;

definition

let C be CatStr ;
let f be Morphism of C;
func dom f -> Object of C equals :: CAT_1:def 2
the Dom of C . f;
correctness ;
func cod f -> Object of C equals :: CAT_1:def 3
the Cod of C . f;
correctness ;

end;

:: deftheorem defines dom CAT_1:def 2 :

:: deftheorem defines cod CAT_1:def 3 :

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 :Def4: :: CAT_1:def 4
the Comp of C . [g,f];
coherence by A1, PARTFUN1:27;

end;

:: deftheorem Def4 defines * CAT_1:def 4 :

definition

let C be CatStr ;
let a be Object of C;
func id a -> Morphism of C equals :: CAT_1:def 5
the Id of C . a;
correctness ;

end;

:: deftheorem defines id CAT_1:def 5 :

definition

let C be CatStr ;
let a, b be Object of C;
func Hom a,b -> Subset of the Morphisms of C equals :: CAT_1:def 6
{ f where f is Morphism of C : ( dom f = a & cod f = b ) } ;
correctness

proof end;

end;

:: deftheorem defines Hom CAT_1:def 6 :

theorem :: CAT_1:10

canceled;

theorem :: CAT_1:11

canceled;

theorem :: CAT_1:12

canceled;

theorem :: CAT_1:13

canceled;

theorem :: CAT_1:14

canceled;

theorem :: CAT_1:15

canceled;

theorem :: CAT_1:16

canceled;

theorem :: CAT_1:17

canceled;

theorem Th18: :: CAT_1:18

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

proof end;

theorem :: CAT_1:19

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

definition

let C be CatStr ;
let a, b be Object of C;
assume A1: Hom a,b <> {} ;
mode Morphism of a,b -> Morphism of C means :Def7: :: CAT_1:def 7
it in Hom a,b;
existence by A1, SUBSET_1:10;

end;

:: deftheorem Def7 defines Morphism CAT_1:def 7 :

theorem :: CAT_1:20

canceled;

theorem :: CAT_1:21

for C being CatStr
for a, b being Object of C
for f being set st f in Hom a,b holds
f is Morphism of a,b by Def7;

theorem Th22: :: CAT_1:22

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

proof end;

theorem Th23: :: CAT_1:23

for C being 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:24

for C being 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 Th25: :: CAT_1:25

for C being 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 Th26: :: CAT_1:26

for C being 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:27

for C being 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;

definition

let m, o be set ;
:: original: .-->
redefine func m .--> o -> Function of {m},{o};
coherence

proof end;

end;

Lm1: now

let o, m be set ; :: thesis:
let C be CatStr ; :: thesis:
assume A1: C = CatStr(# {o},{m},(m .--> o),(m .--> o),(m,m .--> m),(o .--> m) #) ; :: thesis:
set CP = the Comp of C;
set CD = the Dom of C;
set CC = the Cod of C;
set CI = the Id of C;
thus for f, g being Element of the Morphisms of C holds
( [g,f] in dom the Comp of C iff the Dom of C . g = the Cod of C . f ) :: thesis:

proof

let f, g be Element of the Morphisms of C; :: thesis:
( f = m & g = m & dom the Comp of C = {[m,m]} ) by A1, Th7, TARSKI:def 1;
hence ( [g,f] in dom the Comp of C iff the Dom of C . g = the Cod of C . f ) by A1, TARSKI:def 1; :: thesis:

end;

thus for f, g being Element of the Morphisms of C st the Dom of C . g = the Cod of C . f holds
( the Dom of C . (the Comp of C . [g,f]) = the Dom of C . f & the Cod of C . (the Comp of C . [g,f]) = the Cod of C . g ) :: thesis:

proof

let f, g be Element of the Morphisms of C; :: thesis:
the Comp of C . [g,f] = m by A1, Th9;
then reconsider gf = the Comp of C . [g,f] as Element of the Morphisms of C by A1, TARSKI:def 1;
( the Dom of C . f = o & the Cod of C . g = o & the Dom of C . gf = o & the Cod of C . gf = o ) by A1, FUNCT_2:65;
hence ( the Dom of C . g = the Cod of C . f implies ( the Dom of C . (the Comp of C . [g,f]) = the Dom of C . f & the Cod of C . (the Comp of C . [g,f]) = the Cod of C . g ) ) ; :: thesis:

end;

thus for f, g, h being Element of the Morphisms of C st the Dom of C . h = the Cod of C . g & the Dom of C . g = the Cod of C . f holds
the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] :: thesis:

proof

let f, g, h be Element of the Morphisms of C; :: thesis:
( the Comp of C . [g,f] = m & the Comp of C . [h,g] = m ) by A1, Th9;
then reconsider gf = the Comp of C . [g,f], hg = the Comp of C . [h,g] as Element of the Morphisms of C by A1, TARSKI:def 1;
( the Comp of C . [h,gf] = m & the Comp of C . [hg,f] = m ) by A1, Th9;
hence ( the Dom of C . h = the Cod of C . g & the Dom of C . g = the Cod of C . f implies the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] ) ; :: thesis:

end;

let b be Element of the Objects of C; :: thesis:
b = o by A1, TARSKI:def 1;
hence ( the Dom of C . (the Id of C . b) = b & the Cod of C . (the Id of C . b) = b ) by A1, FUNCT_2:65; :: thesis:
thus for f being Element of the Morphisms of C st the Cod of C . f = b holds
the Comp of C . [(the Id of C . b),f] = f :: thesis:

proof

let f be Element of the Morphisms of C; :: thesis:
f = m by A1, TARSKI:def 1;
hence ( the Cod of C . f = b implies the Comp of C . [(the Id of C . b),f] = f ) by A1, Th9; :: thesis:

end;

let g be Element of the Morphisms of C; :: thesis:
g = m by A1, TARSKI:def 1;
hence the Comp of C . [g,(the Id of C . b)] = g by A1, Th9; :: thesis:

end;

definition

let C be CatStr ;
attr C is Category-like means :Def8: :: CAT_1:def 8
( ( for f, g being Element of the Morphisms of C holds
( [g,f] in dom the Comp of C iff the Dom of C . g = the Cod of C . f ) ) & ( for f, g being Element of the Morphisms of C st the Dom of C . g = the Cod of C . f holds
( the Dom of C . (the Comp of C . [g,f]) = the Dom of C . f & the Cod of C . (the Comp of C . [g,f]) = the Cod of C . g ) ) & ( for f, g, h being Element of the Morphisms of C st the Dom of C . h = the Cod of C . g & the Dom of C . g = the Cod of C . f holds
the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] ) & ( for b being Element of the Objects of C holds
( the Dom of C . (the Id of C . b) = b & the Cod of C . (the Id of C . b) = b & ( for f being Element of the Morphisms of C st the Cod of C . f = b holds
the Comp of C . [(the Id of C . b),f] = f ) & ( for g being Element of the Morphisms of C st the Dom of C . g = b holds
the Comp of C . [g,(the Id of C . b)] = g ) ) ) );

end;

:: deftheorem Def8 defines Category-like CAT_1:def 8 :

registration

cluster Category-like CatStr ;
existence

proof end;

end;

definition

mode Category is Category-like CatStr ;

end;

registration

cluster strict CatStr ;
existence

proof end;

end;

theorem :: CAT_1:28

canceled;

theorem :: CAT_1:29

for C being CatStr st ( for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f ) ) & ( for f, g being Morphism of C st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g ) ) & ( for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f ) & ( for b being Object of C holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of C st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of C st dom g = b holds
g * (id b) = g ) ) ) holds
C is Category-like

proof end;

definition

let o, m be set ;
func 1Cat o,m -> strict Category equals :: CAT_1:def 9
CatStr(# {o},{m},(m .--> o),(m .--> o),(m,m .--> m),(o .--> m) #);
correctness

proof end;

end;

:: deftheorem defines 1Cat CAT_1:def 9 :

theorem :: CAT_1:30

canceled;

theorem :: CAT_1:31

canceled;

theorem :: CAT_1:32

for o, m being set holds o is Object of (1Cat o,m) by TARSKI:def 1;

theorem :: CAT_1:33

for m, o being set holds m is Morphism of (1Cat o,m) by TARSKI:def 1;

theorem Th34: :: CAT_1:34

for o, m being set
for a being Object of (1Cat o,m) holds a = o by TARSKI:def 1;

theorem Th35: :: CAT_1:35

for o, m being set
for f being Morphism of (1Cat o,m) holds f = m by TARSKI:def 1;

theorem Th36: :: CAT_1:36

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

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

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

theorem :: CAT_1:39

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 Th40: :: CAT_1:40

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

theorem Th41: :: CAT_1:41

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

proof end;

theorem Th42: :: CAT_1:42

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 )

proof end;

theorem Th43: :: CAT_1:43

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

proof end;

theorem Th44: :: CAT_1:44

for C being Category
for b being Object of C holds
( dom (id b) = b & cod (id b) = b ) by Def8;

theorem Th45: :: CAT_1:45

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

proof end;

theorem Th46: :: CAT_1:46

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 Th47: :: CAT_1:47

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;

definition

let C be Category;
let g be Morphism of C;
attr g is monic means :: CAT_1:def 10
for f1, f2 being Morphism of C st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g * f1 = g * f2 holds
f1 = f2;

end;

:: deftheorem defines monic CAT_1:def 10 :

definition

let C be Category;
let f be Morphism of C;
attr f is epi means :: CAT_1:def 11
for g1, g2 being Morphism of C st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1 * f = g2 * f holds
g1 = g2;

end;

:: deftheorem defines epi CAT_1:def 11 :

definition

let C be Category;
let f be Morphism of C;
attr f is invertible means :: CAT_1:def 12
ex g being Morphism of C st
( dom g = cod f & cod g = dom f & f * g = id (cod f) & g * f = id (dom f) );

end;

:: deftheorem defines invertible CAT_1:def 12 :

theorem :: CAT_1:48

canceled;

theorem :: CAT_1:49

canceled;

theorem :: CAT_1:50

canceled;

theorem Th51: :: CAT_1:51

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;

theorem :: CAT_1:52

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

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 :Def13: :: CAT_1:def 13
g * f;
correctness

proof end;

end;

:: deftheorem Def13 defines * CAT_1:def 13 :

theorem :: CAT_1:53

canceled;

theorem Th54: :: CAT_1:54

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 Th55: :: CAT_1:55

for C being Category
for a being Object of C holds id a in Hom a,a

proof end;

theorem :: CAT_1:56

for C being Category
for a being Object of C holds Hom a,a <> {} by Th55;

definition

let C be Category;
let a be Object of C;
:: original: id
redefine func id a -> Morphism of a,a;
coherence

proof end;

end;

theorem Th57: :: 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 <> {} holds
(id b) * f = f

proof end;

theorem Th58: :: CAT_1:58

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;

theorem Th59: :: CAT_1:59

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

proof end;

theorem Th60: :: CAT_1:60

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 )

proof end;

theorem :: CAT_1:61

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 <> {} & g is monic & h is monic holds
h * g is monic

proof end;

theorem :: CAT_1:62

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

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

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

proof end;

theorem Th65: :: CAT_1:65

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 )

proof end;

theorem :: CAT_1:66

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 <> {} & f is epi & g is epi holds
g * f is epi

proof end;

theorem :: CAT_1:67

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

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

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

proof end;

theorem Th70: :: CAT_1:70

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

proof end;

theorem Th71: :: CAT_1:71

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 that
A1: Hom a,b <> {} and
A2: f is invertible ;
func f " -> Morphism of b,a means :Def14: :: CAT_1:def 14
( f * it = id b & it * f = id a );
existence by A1, A2, Th70;
uniqueness

proof end;

end;

:: deftheorem Def14 defines " CAT_1:def 14 :

theorem :: CAT_1:72

canceled;

theorem :: CAT_1:73

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

proof end;

theorem :: CAT_1:74

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

proof end;

theorem Th75: :: CAT_1:75

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 <> {} & f is invertible & g is invertible holds
g * f is invertible

proof end;

theorem :: CAT_1:76

for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom a,b <> {} & f is invertible holds
f " is invertible

proof end;

theorem :: CAT_1:77

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 <> {} & 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 :Def15: :: CAT_1:def 15
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 :Def16: :: CAT_1:def 16
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 :Def17: :: CAT_1:def 17
( Hom a,b <> {} & ex f being Morphism of a,b st f is invertible );

end;

:: deftheorem Def15 defines terminal CAT_1:def 15 :

:: deftheorem Def16 defines initial CAT_1:def 16 :

:: deftheorem Def17 defines are_isomorphic CAT_1:def 17 :

theorem :: CAT_1:78

canceled;

theorem :: CAT_1:79

canceled;

theorem :: CAT_1:80

canceled;

theorem Th81: :: CAT_1:81

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 f' being Morphism of b,a st
( f * f' = id b & f' * f = id a ) ) )

proof end;

theorem :: CAT_1:82

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 Th83: :: CAT_1:83

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

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

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

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 Th87: :: CAT_1:87

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

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

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

proof end;

theorem :: CAT_1:90

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;

theorem :: CAT_1:91

for C being Category
for a being Object of C holds a,a are_isomorphic

proof end;

theorem :: CAT_1:92

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

proof end;

theorem :: CAT_1:93

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;

definition

let C, D be Category;
mode Functor of C,D -> Function of the Morphisms of C,the Morphisms of D means :Def18: :: CAT_1:def 18
( ( for c being Element of the Objects of C ex d being Element of the Objects of D st it . (the Id of C . c) = the Id of D . d ) & ( for f being Element of the Morphisms of C holds
( it . (the Id of C . (the Dom of C . f)) = the Id of D . (the Dom of D . (it . f)) & it . (the Id of C . (the Cod of C . f)) = the Id of D . (the Cod of D . (it . f)) ) ) & ( for f, g being Element of the Morphisms of C st [g,f] in dom the Comp of C holds
it . (the Comp of C . [g,f]) = the Comp of D . [(it . g),(it . f)] ) );
existence

proof end;

end;

:: deftheorem Def18 defines Functor CAT_1:def 18 :

theorem :: CAT_1:94

canceled;

theorem :: CAT_1:95

canceled;

theorem Th96: :: CAT_1:96

for C, D being Category
for T being Function of the Morphisms of C,the Morphisms 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 Th97: :: CAT_1:97

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

proof end;

theorem Th98: :: CAT_1:98

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

theorem Th99: :: CAT_1:99

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 Th100: :: CAT_1:100

for C, D being Category
for T being Function of the Morphisms of C,the Morphisms of D
for F being Function of the Objects of C,the Objects 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;

definition

let C, D be Category;
let F be Function of the Morphisms of C,the Morphisms of D;
assume A1: for c being Element of the Objects of C ex d being Element of the Objects of D st F . (the Id of C . c) = the Id of D . d ;
func Obj F -> Function of the Objects of C,the Objects of D means :Def19: :: CAT_1:def 19
for c being Element of the Objects of C
for d being Element of the Objects of D st F . (the Id of C . c) = the Id of D . d holds
it . c = d;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines Obj CAT_1:def 19 :

theorem :: CAT_1:101

canceled;

theorem Th102: :: CAT_1:102

for C, D being Category
for T being Function of the Morphisms of C,the Morphisms 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

proof end;

theorem Th103: :: CAT_1:103

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 Th104: :: CAT_1:104

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 Th105: :: CAT_1:105

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 20
(Obj T) . c;
correctness ;

end;

:: deftheorem defines . CAT_1:def 20 :

theorem :: CAT_1:106

canceled;

theorem :: CAT_1:107

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

theorem Th108: :: CAT_1:108

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

theorem Th109: :: CAT_1:109

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

theorem Th110: :: CAT_1:110

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;

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 by Th110;

end;

theorem Th111: :: CAT_1:111

for C being Category holds id the Morphisms of C is Functor of C,C

proof end;

theorem Th112: :: CAT_1:112

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 Th113: :: CAT_1:113

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

definition

let C be Category;
func id C -> Functor of C,C equals :: CAT_1:def 21
id the Morphisms of C;
coherence by Th111;

end;

:: deftheorem defines id CAT_1:def 21 :

theorem :: CAT_1:114

canceled;

theorem Th115: :: CAT_1:115

for C being Category
for f being Morphism of C holds (id C) . f = f by FUNCT_1:35;

theorem Th116: :: CAT_1:116

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

proof end;

theorem Th117: :: CAT_1:117

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

proof end;

theorem :: CAT_1:118

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

definition

let C, D be Category;
let T be Functor of C,D;
attr T is isomorphic means :: CAT_1:def 22
( T is one-to-one & rng T = the Morphisms of D & rng (Obj T) = the Objects of D );
attr T is full means :Def23: :: CAT_1:def 23
for c, c' being Object of C st Hom (T . c),(T . c') <> {} holds
for g being Morphism of T . c,T . c' holds
( Hom c,c' <> {} & ex f being Morphism of c,c' st g = T . f );
attr T is faithful means :Def24: :: CAT_1:def 24
for c, c' being Object of C st Hom c,c' <> {} holds
for f1, f2 being Morphism of c,c' st T . f1 = T . f2 holds
f1 = f2;

end;

:: deftheorem defines isomorphic CAT_1:def 22 :

:: deftheorem Def23 defines full CAT_1:def 23 :

:: deftheorem Def24 defines faithful CAT_1:def 24 :

notation

let C, D be Category;
let T be Functor of C,D;
synonym T is_an_isomorphism for isomorphic T;

end;

theorem :: CAT_1:119

canceled;

theorem :: CAT_1:120

canceled;

theorem :: CAT_1:121

canceled;

theorem :: CAT_1:122

for C being Category holds id C is_an_isomorphism

proof end;

theorem Th123: :: CAT_1:123

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

proof end;

theorem Th124: :: CAT_1:124

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

proof end;

theorem Th125: :: CAT_1:125

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

proof end;

theorem Th126: :: CAT_1:126

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

proof end;

theorem :: CAT_1:127

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

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 Th129: :: CAT_1:129

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

proof end;

definition

let C, D be Category;
let T be Functor of C,D;
let c, c' be Object of C;
func hom T,c,c' -> Function of Hom c,c', Hom (T . c),(T . c') equals :: CAT_1:def 25
T | (Hom c,c');
correctness

proof end;

end;

:: deftheorem defines hom CAT_1:def 25 :

theorem :: CAT_1:130

canceled;

theorem Th131: :: CAT_1:131

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

proof end;

theorem :: CAT_1:132

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

proof end;

theorem :: CAT_1:133

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

proof end;