:: ISOCAT_1 semantic presentation

theorem Th1: :: ISOCAT_1:1

for F, G being Function st F is one-to-one & G is one-to-one holds
[:F,G:] is one-to-one

proof end;

theorem Th2: :: ISOCAT_1:2

for A, B being Category holds
( rng (pr1 A,B) = the Morphisms of A & rng (pr2 B,A) = the Morphisms of A )

proof end;

theorem Th3: :: ISOCAT_1:3

for B, A being Category
for F being Functor of A,B
for f being Morphism of A st f is invertible holds
F . f is invertible

proof end;

theorem Th4: :: ISOCAT_1:4

for A, B being Category
for F being Functor of A,B
for G being Functor of B,A holds
( F * (id A) = F & (id A) * G = G ) by FUNCT_2:23;

theorem :: ISOCAT_1:5

canceled;

theorem :: ISOCAT_1:6

canceled;

theorem Th7: :: ISOCAT_1:7

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 in Hom (F1 . a),(F2 . a)

proof end;

theorem Th8: :: ISOCAT_1:8

for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_transformable_to F2 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2

proof end;

theorem Th9: :: ISOCAT_1:9

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 st t is invertible holds
for a being Object of A holds F1 . a,F2 . a are_isomorphic

proof end;

definition

let C, D be Category;
redefine mode Functor of C,D means :: ISOCAT_1:def 1
( ( for c being Object of C ex d being Object of D st it . (id c) = id d ) & ( for f being Morphism of C holds
( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
it . (g * f) = (it . g) * (it . f) ) );
compatibility by CAT_1:96, CAT_1:97, CAT_1:98, CAT_1:99;

end;

:: deftheorem defines Functor ISOCAT_1:def 1 :

definition

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

proof end;

end;

theorem Th10: :: ISOCAT_1:10

for B, A being Category
for F being Functor of A,B st F is isomorphic holds
for g being Morphism of B ex f being Morphism of A st F . f = g

proof end;

theorem Th11: :: ISOCAT_1:11

for B, A being Category
for F being Functor of A,B st F is isomorphic holds
for b being Object of B ex a being Object of A st F . a = b

proof end;

theorem Th12: :: ISOCAT_1:12

for A, B being Category
for F being Functor of A,B st F is one-to-one holds
Obj F is one-to-one

proof end;

definition

let A, B be Category;
let F be Functor of A,B;
assume A1: F is isomorphic ;
func F " -> Functor of B,A equals :Def2: :: ISOCAT_1:def 2
F " ;
coherence

proof end;

end;

:: deftheorem Def2 defines " ISOCAT_1:def 2 :

notation

let A, B be Category;
let F be Functor of A,B;
synonym F is_an_isomorphism for isomorphic FF is_an_isomorphism ;

end;

definition

let A, B be Category;
let F be Functor of A,B;
redefine attr F is isomorphic means :Def3: :: ISOCAT_1:def 3
( F is one-to-one & rng F = the Morphisms of B );
compatibility

proof end;

end;

:: deftheorem Def3 defines is_an_isomorphism ISOCAT_1:def 3 :

theorem Th13: :: ISOCAT_1:13

for A, B being Category
for F being Functor of A,B st F is_an_isomorphism holds
F " is_an_isomorphism

proof end;

theorem :: ISOCAT_1:14

for A, B being Category
for F being Functor of A,B st F is_an_isomorphism holds
(Obj F) " = Obj (F " )

proof end;

theorem :: ISOCAT_1:15

for A, B being Category
for F being Functor of A,B st F is_an_isomorphism holds
(F " ) " = F

proof end;

theorem Th16: :: ISOCAT_1:16

for B, A being Category
for F being Functor of A,B st F is_an_isomorphism holds
( F * (F " ) = id B & (F " ) * F = id A )

proof end;

theorem Th17: :: ISOCAT_1:17

for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st F is_an_isomorphism & G is_an_isomorphism holds
G * F is_an_isomorphism

proof end;

definition

let A, B be Category;
pred A,B are_isomorphic means :: ISOCAT_1:def 4
ex F being Functor of A,B st F is_an_isomorphism ;
reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem defines are_isomorphic ISOCAT_1:def 4 :

notation

let A, B be Category;
synonym A ~= B for A,B are_isomorphic ;

end;

theorem :: ISOCAT_1:18

canceled;

theorem :: ISOCAT_1:19

canceled;

theorem :: ISOCAT_1:20

for A, B, C being Category st A ~= B & B ~= C holds
A ~= C

proof end;

theorem :: ISOCAT_1:21

for A being Category
for o, m being set holds [:(1Cat o,m),A:] ~= A

proof end;

theorem :: ISOCAT_1:22

for A, B being Category holds [:A,B:] ~= [:B,A:]

proof end;

theorem :: ISOCAT_1:23

for A, B, C being Category holds [:[:A,B:],C:] ~= [:A,[:B,C:]:]

proof end;

theorem :: ISOCAT_1:24

for A, B, C, D being Category st A ~= B & C ~= D holds
[:A,C:] ~= [:B,D:]

proof end;

definition

let A, B, C 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 G be Functor of B,C;
func G * t -> transformation of G * F1,G * F2 equals :Def5: :: ISOCAT_1:def 5
G * t;
coherence

proof end;

correctness ;

end;

:: deftheorem Def5 defines * ISOCAT_1:def 5 :

definition

let A, B, C be Category;
let G1, G2 be Functor of B,C;
assume A1: G1 is_transformable_to G2 ;
let F be Functor of A,B;
let t be transformation of G1,G2;
func t * F -> transformation of G1 * F,G2 * F equals :Def6: :: ISOCAT_1:def 6
t * (Obj F);
coherence

proof end;

correctness ;

end;

:: deftheorem Def6 defines * ISOCAT_1:def 6 :

theorem Th25: :: ISOCAT_1:25

for B, C, A being Category
for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds
for F being Functor of A,B
for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)

proof end;

theorem Th26: :: ISOCAT_1:26

for A, B, C 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 G being Functor of B,C
for a being Object of A holds (G * t) . a = G . (t . a)

proof end;

theorem Th27: :: ISOCAT_1:27

for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
G1 * F1 is_naturally_transformable_to G2 * F2

proof end;

definition

let A, B, C be Category;
let F1, F2 be Functor of A,B;
assume A1: F1 is_naturally_transformable_to F2 ;
let t be natural_transformation of F1,F2;
let G be Functor of B,C;
func G * t -> natural_transformation of G * F1,G * F2 equals :Def7: :: ISOCAT_1:def 7
G * t;
coherence

proof end;

correctness ;

end;

:: deftheorem Def7 defines * ISOCAT_1:def 7 :

theorem Th28: :: ISOCAT_1:28

for A, B, C 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
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G . (t . a)

proof end;

definition

let A, B, C be Category;
let G1, G2 be Functor of B,C;
assume A1: G1 is_naturally_transformable_to G2 ;
let F be Functor of A,B;
let t be natural_transformation of G1,G2;
func t * F -> natural_transformation of G1 * F,G2 * F equals :Def8: :: ISOCAT_1:def 8
t * F;
coherence

proof end;

correctness ;

end;

:: deftheorem Def8 defines * ISOCAT_1:def 8 :

theorem Th29: :: ISOCAT_1:29

for B, C, A being Category
for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds
for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)

proof end;

theorem Th30: :: ISOCAT_1:30

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

proof end;

theorem Th31: :: ISOCAT_1:31

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

proof end;

theorem Th32: :: ISOCAT_1:32

for C, A, B being Category
for F1, F2, F3 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2
for s' being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s' `*` s) = (G * s') `*` (G * s)

proof end;

theorem Th33: :: ISOCAT_1:33

for A, B, C being Category
for F being Functor of A,B
for G1, G2, G3 being Functor of B,C
for t being natural_transformation of G1,G2
for t' being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t' `*` t) * F = (t' * F) `*` (t * F)

proof end;

theorem Th34: :: ISOCAT_1:34

for A, B, C, D being Category
for F being Functor of A,B
for G being Functor of B,C
for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)

proof end;

theorem Th35: :: ISOCAT_1:35

for A, D, B, C being Category
for F being Functor of A,B
for G1, G2 being Functor of B,C
for H being Functor of C,D
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
(H * t) * F = H * (t * F)

proof end;

theorem Th36: :: ISOCAT_1:36

for C, D, A, B being Category
for F1, F2 being Functor of A,B
for G being Functor of B,C
for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)

proof end;

theorem Th37: :: ISOCAT_1:37

for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C holds (id G) * F = id (G * F)

proof end;

theorem Th38: :: ISOCAT_1:38

for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C holds G * (id F) = id (G * F)

proof end;

theorem Th39: :: ISOCAT_1:39

for C, B being Category
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * (id B) = t

proof end;

theorem Th40: :: ISOCAT_1:40

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

proof end;

definition

let A, B, C be Category;
let F1, F2 be Functor of A,B;
let G1, G2 be Functor of B,C;
let s be natural_transformation of F1,F2;
let t be natural_transformation of G1,G2;
func t (#) s -> natural_transformation of G1 * F1,G2 * F2 equals :: ISOCAT_1:def 9
(t * F2) `*` (G1 * s);
correctness ;

end;

:: deftheorem defines (#) ISOCAT_1:def 9 :

theorem Th41: :: ISOCAT_1:41

for A, B, C being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)

proof end;

theorem :: ISOCAT_1:42

for A, B being Category
for F1, F2 being Functor of A,B
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(id (id B)) (#) s = s

proof end;

theorem :: ISOCAT_1:43

for C, B being Category
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t (#) (id (id B)) = t

proof end;

theorem :: ISOCAT_1:44

for A, B, C, D being Category
for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for H1, H2 being Functor of C,D
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2
for u being natural_transformation of H1,H2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s

proof end;

theorem :: ISOCAT_1:45

for A, B, C being Category
for F being Functor of A,B
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * F = t (#) (id F)

proof end;

theorem :: ISOCAT_1:46

for C, A, B being Category
for F1, F2 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s

proof end;

theorem :: ISOCAT_1:47

for A, B, C being Category
for F1, F2, F3 being Functor of A,B
for G1, G2, G3 being Functor of B,C
for s being natural_transformation of F1,F2
for s' being natural_transformation of F2,F3
for t being natural_transformation of G1,G2
for t' being natural_transformation of G2,G3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t' `*` t) (#) (s' `*` s) = (t' (#) s') `*` (t (#) s)

proof end;

theorem Th48: :: ISOCAT_1:48

for A, B, C, D being Category
for F being Functor of A,B
for G being Functor of C,D
for I, J being Functor of B,C st I ~= J holds
( G * I ~= G * J & I * F ~= J * F )

proof end;

theorem Th49: :: ISOCAT_1:49

for A, B being Category
for F being Functor of A,B
for G being Functor of B,A
for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )

proof end;

definition

let A, B be Category;
pred A is_equivalent_with B means :Def10: :: ISOCAT_1:def 10
ex F being Functor of A,B ex G being Functor of B,A st
( G * F ~= id A & F * G ~= id B );
reflexivity

proof end;

symmetry ;

end;

:: deftheorem Def10 defines is_equivalent_with ISOCAT_1:def 10 :

notation

let A, B be Category;
synonym A,B are_equivalent for A is_equivalent_with B;

end;

theorem :: ISOCAT_1:50

for A, B being Category st A ~= B holds
A is_equivalent_with B

proof end;

theorem :: ISOCAT_1:51

canceled;

theorem :: ISOCAT_1:52

canceled;

theorem Th53: :: ISOCAT_1:53

for A, B, C being Category st A,B are_equivalent & B,C are_equivalent holds
A,C are_equivalent

proof end;

definition

let A, B be Category;
assume A1: A,B are_equivalent ;
mode Equivalence of A,B -> Functor of A,B means :Def11: :: ISOCAT_1:def 11
ex G being Functor of B,A st
( G * it ~= id A & it * G ~= id B );
existence by A1, Def10;

end;

:: deftheorem Def11 defines Equivalence ISOCAT_1:def 11 :

theorem :: ISOCAT_1:54

for A being Category holds id A is Equivalence of A,A

proof end;

theorem :: ISOCAT_1:55

for A, B, C being Category st A,B are_equivalent & B,C are_equivalent holds
for F being Equivalence of A,B
for G being Equivalence of B,C holds G * F is Equivalence of A,C

proof end;

theorem Th56: :: ISOCAT_1:56

for A, B being Category st A,B are_equivalent holds
for F being Equivalence of A,B ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B )

proof end;

theorem Th57: :: ISOCAT_1:57

for A, B being Category
for F being Functor of A,B
for G being Functor of B,A st G * F ~= id A holds
F is faithful

proof end;

theorem :: ISOCAT_1:58

for A, B being Category st A,B are_equivalent holds
for F being Equivalence of A,B holds
( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )

proof end;