:: Isomorphisms of Categories
:: by Andrzej Trybulec
::
:: Received November 22, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: ISOCAT_1:1
theorem :: ISOCAT_1:2
theorem Th3: :: ISOCAT_1:3
theorem :: ISOCAT_1:4
canceled;
theorem :: ISOCAT_1:5
canceled;
theorem :: ISOCAT_1:6
canceled;
theorem Th7: :: ISOCAT_1:7
theorem Th8: :: ISOCAT_1:8
theorem Th9: :: ISOCAT_1:9
:: deftheorem defines Functor ISOCAT_1:def 1 :
theorem Th10: :: ISOCAT_1:10
theorem Th11: :: ISOCAT_1:11
theorem Th12: :: ISOCAT_1:12
:: deftheorem Def2 defines " ISOCAT_1:def 2 :
:: deftheorem Def3 defines isomorphic ISOCAT_1:def 3 :
theorem Th13: :: ISOCAT_1:13
theorem :: ISOCAT_1:14
theorem :: ISOCAT_1:15
theorem Th16: :: ISOCAT_1:16
theorem Th17: :: ISOCAT_1:17
:: deftheorem defines are_isomorphic ISOCAT_1:def 4 :
theorem :: ISOCAT_1:18
canceled;
theorem :: ISOCAT_1:19
canceled;
theorem :: ISOCAT_1:20
theorem :: ISOCAT_1:21
theorem :: ISOCAT_1:22
theorem :: ISOCAT_1:23
theorem :: ISOCAT_1:24
:: deftheorem Def5 defines * ISOCAT_1:def 5 :
:: deftheorem Def6 defines * ISOCAT_1:def 6 :
theorem Th25: :: ISOCAT_1:25
theorem Th26: :: ISOCAT_1:26
theorem Th27: :: ISOCAT_1:27
:: deftheorem Def7 defines * ISOCAT_1:def 7 :
theorem Th28: :: ISOCAT_1:28
:: deftheorem Def8 defines * ISOCAT_1:def 8 :
theorem Th29: :: ISOCAT_1:29
theorem Th30: :: ISOCAT_1:30
theorem Th31: :: ISOCAT_1:31
theorem Th32: :: ISOCAT_1:32
theorem Th33: :: ISOCAT_1:33
theorem Th34: :: ISOCAT_1:34
theorem Th35: :: ISOCAT_1:35
theorem Th36: :: ISOCAT_1:36
theorem Th37: :: ISOCAT_1:37
theorem Th38: :: ISOCAT_1:38
theorem Th39: :: ISOCAT_1:39
theorem Th40: :: ISOCAT_1:40
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
coherence
(t * F2) `*` (G1 * s) is natural_transformation of G1 * F1,G2 * F2;
;
end;
:: deftheorem defines (#) ISOCAT_1:def 9 :
theorem Th41: :: ISOCAT_1:41
theorem :: ISOCAT_1:42
theorem :: ISOCAT_1:43
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
theorem :: ISOCAT_1:45
theorem :: ISOCAT_1:46
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)
theorem Th48: :: ISOCAT_1:48
theorem Th49: :: ISOCAT_1:49
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
for A being Category ex F, G being Functor of A,A st
( G * F ~= id A & F * G ~= id A )
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 )
;
end;
:: deftheorem Def10 defines is_equivalent_with ISOCAT_1:def 10 :
theorem :: ISOCAT_1:50
theorem :: ISOCAT_1:51
canceled;
theorem :: ISOCAT_1:52
canceled;
theorem Th53: :: ISOCAT_1:53
:: deftheorem Def11 defines Equivalence ISOCAT_1:def 11 :
theorem :: ISOCAT_1:54
theorem :: ISOCAT_1:55
theorem Th56: :: ISOCAT_1:56
theorem Th57: :: ISOCAT_1:57
theorem :: ISOCAT_1:58