:: by Andrzej Trybulec

::

:: Received November 22, 1991

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

::$CT 2

theorem Th1: :: ISOCAT_1:3

for A, B being Category

for F being Functor of A,B

for a, b being Object of A

for f being Morphism of a,b st f is invertible holds

F /. f is invertible

for F being Functor of A,B

for a, b being Object of A

for f being Morphism of a,b st f is invertible holds

F /. f is invertible

proof end;

theorem Th2: :: ISOCAT_1:4

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

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 Th3: :: ISOCAT_1:5

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

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 Th4: :: ISOCAT_1:6

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

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;

for b_{1} being M3( bool [: the carrier' of C, the carrier' of D:]) holds

( b_{1} is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b_{1} . (id c) = id d ) & ( for f being Morphism of C holds

( b_{1} . (id (dom f)) = id (dom (b_{1} . f)) & b_{1} . (id (cod f)) = id (cod (b_{1} . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

b_{1} . (g (*) f) = (b_{1} . g) (*) (b_{1} . f) ) ) )
by CAT_1:61, CAT_1:62, CAT_1:63, CAT_1:64;

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

for b

( b

( b

b

:: deftheorem defines Functor ISOCAT_1:def 1 :

for C, D being Category

for b_{3} being M3( bool [: the carrier' of b_{1}, the carrier' of b_{2}:]) holds

( b_{3} is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b_{3} . (id c) = id d ) & ( for f being Morphism of C holds

( b_{3} . (id (dom f)) = id (dom (b_{3} . f)) & b_{3} . (id (cod f)) = id (cod (b_{3} . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds

b_{3} . (g (*) f) = (b_{3} . g) (*) (b_{3} . f) ) ) );

for C, D being Category

for b

( b

( b

b

theorem Th5: :: ISOCAT_1:7

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

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 Th6: :: ISOCAT_1:8

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

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;

definition

let A, B be Category;

let F be Functor of A,B;

assume A1: F is isomorphic ;

coherence

F " is Functor of B,A

end;
let F be Functor of A,B;

assume A1: F is isomorphic ;

coherence

F " is Functor of B,A

proof end;

:: deftheorem Def2 defines " ISOCAT_1:def 2 :

for A, B being Category

for F being Functor of A,B st F is isomorphic holds

F " = F " ;

for A, B being Category

for F being Functor of A,B st F is isomorphic holds

F " = F " ;

definition

let A, B be Category;

let F be Functor of A,B;

( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) )

end;
let F be Functor of A,B;

redefine attr F is isomorphic means :: ISOCAT_1:def 3

( F is one-to-one & rng F = the carrier' of B );

compatibility ( F is one-to-one & rng F = the carrier' of B );

( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) )

proof end;

:: deftheorem defines isomorphic ISOCAT_1:def 3 :

for A, B being Category

for F being Functor of A,B holds

( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) );

for A, B being Category

for F being Functor of A,B holds

( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) );

theorem Th11: :: ISOCAT_1:13

for A, B being Category

for F being Functor of A,B st F is isomorphic holds

( F * (F ") = id B & (F ") * F = id A )

for F being Functor of A,B st F is isomorphic holds

( F * (F ") = id B & (F ") * F = id A )

proof end;

theorem Th12: :: ISOCAT_1:14

for A, B, C being Category

for F being Functor of A,B

for G being Functor of B,C st F is isomorphic & G is isomorphic holds

G * F is isomorphic

for F being Functor of A,B

for G being Functor of B,C st F is isomorphic & G is isomorphic holds

G * F is isomorphic

proof end;

:: Isomorphism of categories

definition

let A, B be Category;

reflexivity

for A being Category ex F being Functor of A,A st F is isomorphic

for A, B being Category st ex F being Functor of A,B st F is isomorphic holds

ex F being Functor of B,A st F is isomorphic

end;
reflexivity

for A being Category ex F being Functor of A,A st F is isomorphic

proof end;

symmetry for A, B being Category st ex F being Functor of A,B st F is isomorphic holds

ex F being Functor of B,A st F is isomorphic

proof end;

:: deftheorem defines are_isomorphic ISOCAT_1:def 4 :

for A, B being Category holds

( A,B are_isomorphic iff ex F being Functor of A,B st F is isomorphic );

for A, B being Category holds

( A,B are_isomorphic iff ex F being Functor of A,B st F is isomorphic );

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;

coherence

G * t is transformation of G * F1,G * F2

;

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

coherence

G * t is transformation of G * F1,G * F2

proof end;

correctness ;

:: deftheorem Def5 defines * ISOCAT_1:def 5 :

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 holds G * t = G * t;

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 holds G * t = G * t;

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;

coherence

t * (Obj F) is transformation of G1 * F,G2 * F

;

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

coherence

t * (Obj F) is transformation of G1 * F,G2 * F

proof end;

correctness ;

:: deftheorem Def6 defines * ISOCAT_1:def 6 :

for A, B, C 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 holds t * F = t * (Obj F);

for A, B, C 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 holds t * F = t * (Obj F);

theorem Th18: :: ISOCAT_1:20

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

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 Th19: :: ISOCAT_1:21

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)

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 Th20: :: ISOCAT_1:22

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

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;

coherence

G * t is natural_transformation of G * F1,G * F2

;

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

coherence

G * t is natural_transformation of G * F1,G * F2

proof end;

correctness ;

:: deftheorem Def7 defines * ISOCAT_1:def 7 :

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 holds G * t = G * t;

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 holds G * t = G * t;

theorem Th21: :: ISOCAT_1:23

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)

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;

coherence

t * F is natural_transformation of G1 * F,G2 * F

;

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

coherence

t * F is natural_transformation of G1 * F,G2 * F

proof end;

correctness ;

:: deftheorem Def8 defines * ISOCAT_1:def 8 :

for A, B, C 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 holds t * F = t * F;

for A, B, C 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 holds t * F = t * F;

theorem Th22: :: ISOCAT_1:24

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

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 Th23: :: ISOCAT_1:25

for A, B 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)) <> {} by NATTRA_1:def 2;

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)) <> {} by NATTRA_1:def 2;

theorem Th24: :: ISOCAT_1:26

for A, B 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 by NATTRA_1:19;

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 by NATTRA_1:19;

theorem Th25: :: ISOCAT_1:27

for A, B, C 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 s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

G * (s9 `*` s) = (G * s9) `*` (G * s)

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 s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

G * (s9 `*` s) = (G * s9) `*` (G * s)

proof end;

theorem Th26: :: ISOCAT_1:28

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 t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds

(t9 `*` t) * F = (t9 * F) `*` (t * F)

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 t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds

(t9 `*` t) * F = (t9 * F) `*` (t * F)

proof end;

theorem Th27: :: ISOCAT_1:29

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)

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 Th28: :: ISOCAT_1:30

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

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 Th29: :: ISOCAT_1:31

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

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 Th30: :: ISOCAT_1:32

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)

for F being Functor of A,B

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

proof end;

theorem Th31: :: ISOCAT_1:33

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)

for F being Functor of A,B

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

proof end;

theorem Th32: :: ISOCAT_1:34

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

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 Th33: :: ISOCAT_1:35

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

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;

coherence

(t * F2) `*` (G1 * s) is natural_transformation of G1 * F1,G2 * F2;

;

end;
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 (t * F2) `*` (G1 * s);

coherence

(t * F2) `*` (G1 * s) is natural_transformation of G1 * F1,G2 * F2;

;

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

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 holds t (#) s = (t * F2) `*` (G1 * s);

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 holds t (#) s = (t * F2) `*` (G1 * s);

theorem Th34: :: ISOCAT_1:36

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)

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

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

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

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

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

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

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

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)

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

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

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

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 s9 being natural_transformation of F2,F3

for t being natural_transformation of G1,G2

for t9 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

(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)

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 s9 being natural_transformation of F2,F3

for t being natural_transformation of G1,G2

for t9 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

(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)

proof end;

theorem Th41: :: ISOCAT_1:43

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 )

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 Th42: :: ISOCAT_1:44

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 )

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;

for A being Category ex F, G being Functor of A,A st

( G * F ~= id A & F * G ~= id A )

for A, B being Category st ex F being Functor of A,B ex G being Functor of B,A st

( G * F ~= id A & F * G ~= id B ) holds

ex F being Functor of B,A ex G being Functor of A,B st

( G * F ~= id B & F * G ~= id A ) ;

end;
pred A is_equivalent_with B means :: 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 ex F being Functor of A,B ex G being Functor of B,A st

( G * F ~= id A & F * G ~= id B );

for A being Category ex F, G being Functor of A,A st

( G * F ~= id A & F * G ~= id A )

proof end;

symmetry for A, B being Category st ex F being Functor of A,B ex G being Functor of B,A st

( G * F ~= id A & F * G ~= id B ) holds

ex F being Functor of B,A ex G being Functor of A,B st

( G * F ~= id B & F * G ~= id A ) ;

:: deftheorem defines is_equivalent_with ISOCAT_1:def 10 :

for A, B being Category holds

( A is_equivalent_with B iff ex F being Functor of A,B ex G being Functor of B,A st

( G * F ~= id A & F * G ~= id B ) );

for A, B being Category holds

( A is_equivalent_with B iff ex F being Functor of A,B ex G being Functor of B,A st

( G * F ~= id A & F * G ~= id B ) );

definition

let A, B be Category;

assume A1: A,B are_equivalent ;

ex b_{1} being Functor of A,B ex G being Functor of B,A st

( G * b_{1} ~= id A & b_{1} * G ~= id B )
by A1;

end;
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 ex G being Functor of B,A st

( G * it ~= id A & it * G ~= id B );

ex b

( G * b

:: deftheorem Def11 defines Equivalence ISOCAT_1:def 11 :

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

for b_{3} being Functor of A,B holds

( b_{3} is Equivalence of A,B iff ex G being Functor of B,A st

( G * b_{3} ~= id A & b_{3} * G ~= id B ) );

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

for b

( b

( G * b

theorem :: ISOCAT_1:48

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

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 Th47: :: ISOCAT_1:49

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 )

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 Th48: :: ISOCAT_1:50

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

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

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

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;

:: The elimination of the Id selector caused the necessity to

:: introduce corresponding functor because 'the Id of C' is sometimes

:: separately used, not applied to an object (2012.01.25, A.T.)

:: introduce corresponding functor because 'the Id of C' is sometimes

:: separately used, not applied to an object (2012.01.25, A.T.)

definition

let C be Category;

deffunc H_{1}( Object of C) -> Morphism of $1,$1 = id $1;

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

for o being Object of C holds b_{1} . o = id o

for b_{1}, b_{2} being Function of the carrier of C, the carrier' of C st ( for o being Object of C holds b_{1} . o = id o ) & ( for o being Object of C holds b_{2} . o = id o ) holds

b_{1} = b_{2}

end;
deffunc H

func IdMap C -> Function of the carrier of C, the carrier' of C means :: ISOCAT_1:def 12

for o being Object of C holds it . o = id o;

existence for o being Object of C holds it . o = id o;

ex b

for o being Object of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines IdMap ISOCAT_1:def 12 :

for C being Category

for b_{2} being Function of the carrier of C, the carrier' of C holds

( b_{2} = IdMap C iff for o being Object of C holds b_{2} . o = id o );

for C being Category

for b

( b