:: Isomorphisms of Categories
:: by Andrzej Trybulec
::
:: Received November 22, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

theorem :: ISOCAT_1:1
canceled;

theorem :: ISOCAT_1:2
canceled;

theorem Th3: :: ISOCAT_1:3
for B, A 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
proofend;

theorem Th4: :: 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))
proofend;

theorem Th5: :: 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
proofend;

theorem Th6: :: 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
proofend;

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
 for b1 being M2( bool [: the carrier' of C, the carrier' of D:]) holds
( b1 is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b1 . (id c) = id d ) & ( for f being Morphism of C holds
( b1 . (id (dom f)) = id (dom (b1 . f)) & b1 . (id (cod f)) = id (cod (b1 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b1 . (g (*) f) = (b1 . g) (*) (b1 . f) ) ) ) by CAT_1:61, CAT_1:62, CAT_1:63, CAT_1:64;
end;

:: deftheorem  defines Functor ISOCAT_1:def_1_:_
 for C, D being Category
for b3 being M2( bool [: the carrier' of b1, the carrier' of b2:]) holds
( b3 is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b3 . (id c) = id d ) & ( for f being Morphism of C holds
( b3 . (id (dom f)) = id (dom (b3 . f)) & b3 . (id (cod f)) = id (cod (b3 . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b3 . (g (*) f) = (b3 . g) (*) (b3 . f) ) ) );

theorem Th7: :: ISOCAT_1:7
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
proofend;

theorem Th8: :: ISOCAT_1:8
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
proofend;

theorem Th9: :: ISOCAT_1:9
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
proofend;

definition
let A, B be Category;
let F be Functor of A,B;
assume A1: F is isomorphic ;
funcF "  ->  Functor of B,A equals :Def2: :: ISOCAT_1:def 2
F " ;
coherence
 F " is Functor of B,A
proofend;
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 " ;

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 carrier' of B );
compatibility
 ( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) )
proofend;
end;

:: deftheorem Def3 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 ) );

theorem Th10: :: ISOCAT_1:10
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
F " is isomorphic
proofend;

theorem :: ISOCAT_1:11
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
(Obj F) " = Obj (F ")
proofend;

theorem :: ISOCAT_1:12
for A, B being Category
for F being Functor of A,B st F is isomorphic holds
(F ") " = F
proofend;

theorem Th13: :: ISOCAT_1:13
for B, A being Category
for F being Functor of A,B st F is isomorphic holds
( F * (F ") = id B & (F ") * F = id A )
proofend;

theorem Th14: :: 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
proofend;

:: Isomorphism of categories
definition
let A, B be Category;
predA,B are_isomorphic  means :: ISOCAT_1:def 4
 ex F being Functor of A,B st F is isomorphic ;
reflexivity
 for A being Category ex F being Functor of A,A st F is isomorphic
proofend;
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
proofend;
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 );

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

theorem :: ISOCAT_1:15
for A, B, C being Category st A ~= B & B ~= C holds
A ~= C
proofend;

theorem :: ISOCAT_1:16
for A being Category
for o, m being set holds [:(1Cat (o,m)),A:] ~= A
proofend;

theorem :: ISOCAT_1:17
for A, B being Category holds [:A,B:] ~= [:B,A:]
proofend;

theorem :: ISOCAT_1:18
for A, B, C being Category holds [:[:A,B:],C:] ~= [:A,[:B,C:]:]
proofend;

theorem :: ISOCAT_1:19
for A, B, C, D being Category st A ~= B & C ~= D holds
[:A,C:] ~= [:B,D:]
proofend;

definition
let A, B, C be Category;
let F1, F2 be Functor of A,B;
assume B1: F1 is_transformable_to F2 ;
let t be transformation of F1,F2;
let G be Functor of B,C;
funcG * t ->  transformation of G * F1,G * F2 equals :Def5: :: ISOCAT_1:def 5
G * t;
coherence
 G * t is transformation of G * F1,G * F2
proofend;
correctness
;
end;

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

definition
let A, B, C be Category;
let G1, G2 be Functor of B,C;
assume B1: G1 is_transformable_to G2 ;
let F be Functor of A,B;
let t be transformation of G1,G2;
funct * F ->  transformation of G1 * F,G2 * F equals :Def6: :: ISOCAT_1:def 6
t * (Obj F);
coherence
 t * (Obj F) is transformation of G1 * F,G2 * F
proofend;
correctness
;
end;

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

theorem Th20: :: ISOCAT_1:20
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)
proofend;

theorem Th21: :: 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)
proofend;

theorem Th22: :: 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
proofend;

definition
let A, B, C be Category;
let F1, F2 be Functor of A,B;
assume B1: F1 is_naturally_transformable_to F2 ;
let t be natural_transformation of F1,F2;
let G be Functor of B,C;
funcG * t ->  natural_transformation of G * F1,G * F2 equals :Def7: :: ISOCAT_1:def 7
G * t;
coherence
 G * t is natural_transformation of G * F1,G * F2
proofend;
correctness
;
end;

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

theorem Th23: :: 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)
proofend;

definition
let A, B, C be Category;
let G1, G2 be Functor of B,C;
assume B1: G1 is_naturally_transformable_to G2 ;
let F be Functor of A,B;
let t be natural_transformation of G1,G2;
funct * F ->  natural_transformation of G1 * F,G2 * F equals :Def8: :: ISOCAT_1:def 8
t * F;
coherence
 t * F is natural_transformation of G1 * F,G2 * F
proofend;
correctness
;
end;

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

theorem Th24: :: ISOCAT_1:24
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)
proofend;

theorem Th25: :: ISOCAT_1:25
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)) <> {}
proofend;

theorem Th26: :: ISOCAT_1:26
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
proofend;

theorem Th27: :: ISOCAT_1:27
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 s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 &amp; F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
proofend;

theorem Th28: :: 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 &amp; G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
proofend;

theorem Th29: :: 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)
proofend;

theorem Th30: :: ISOCAT_1:30
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)
proofend;

theorem Th31: :: ISOCAT_1:31
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)
proofend;

theorem Th32: :: 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)
proofend;

theorem Th33: :: 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)
proofend;

theorem Th34: :: ISOCAT_1:34
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
proofend;

theorem Th35: :: 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
proofend;

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;
funct (#) 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_:_
 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 Th36: :: 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 &amp; G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
proofend;

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

theorem :: ISOCAT_1:38
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
proofend;

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 &amp; G1 is_naturally_transformable_to G2 &amp; H1 is_naturally_transformable_to H2 holds
u (#) (t (#) s) = (u (#) t) (#) s
proofend;

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

theorem :: ISOCAT_1:41
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
proofend;

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 &amp; F2 is_naturally_transformable_to F3 &amp; G1 is_naturally_transformable_to G2 &amp; G2 is_naturally_transformable_to G3 holds
(t9 `*` t) (#) (s9 `*` s) = (t9 (#) s9) `*` (t (#) s)
proofend;

theorem Th43: :: 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 &amp; I * F ~= J * F )
proofend;

theorem Th44: :: 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 &amp; I * G ~= G )
proofend;

definition
let A, B be Category;
predA 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 &amp; F * G ~= id B );
reflexivity
 for A being Category ex F, G being Functor of A,A st
( G * F ~= id A &amp; F * G ~= id A )
proofend;
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 &amp; F * G ~= id B ) holds
ex F being Functor of B,A ex G being Functor of A,B st
( G * F ~= id B &amp; F * G ~= id A ) ;
end;

:: deftheorem Def10 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 &amp; F * G ~= id B ) );

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

theorem :: ISOCAT_1:45
for A, B being Category st A ~= B holds
A is_equivalent_with B
proofend;

theorem Th46: :: ISOCAT_1:46
for A, B, C being Category st A,B are_equivalent &amp; B,C are_equivalent holds
A,C are_equivalent
proofend;

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 &amp; it * G ~= id B );
existence
 ex b1 being Functor of A,B ex G being Functor of B,A st
( G * b1 ~= id A &amp; b1 * G ~= id B ) by A1, Def10;
end;

:: deftheorem Def11 defines Equivalence ISOCAT_1:def_11_:_
 for A, B being Category st A,B are_equivalent holds
for b3 being Functor of A,B holds
( b3 is Equivalence of A,B iff ex G being Functor of B,A st
( G * b3 ~= id A &amp; b3 * G ~= id B ) );

theorem :: ISOCAT_1:47
for A being Category holds id A is Equivalence of A,A
proofend;

theorem :: ISOCAT_1:48
for A, B, C being Category st A,B are_equivalent &amp; 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
proofend;

theorem Th49: :: 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 &amp; F * G ~= id B )
proofend;

theorem Th50: :: 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
proofend;

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 &amp; F is faithful &amp; ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )
proofend;

:: 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.)
definition
let C be Category;
deffunc H1( Object of C) ->  Morphism of $1,$1 = id $1;
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
 ex b1 being Function of the carrier of C, the carrier' of C st
for o being Object of C holds b1 . o = id o
proofend;
uniqueness
 for b1, b2 being Function of the carrier of C, the carrier' of C st ( for o being Object of C holds b1 . o = id o ) &amp; ( for o being Object of C holds b2 . o = id o ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines IdMap ISOCAT_1:def_12_:_
 for C being Category
for b2 being Function of the carrier of C, the carrier' of C holds
( b2 = IdMap C iff for o being Object of C holds b2 . o = id o );