:: Isomorphisms of Categories
:: by Andrzej Trybulec
::
:: Copyright (c) 1991-2018 Association of Mizar Users

theorem :: ISOCAT_1:1
canceled;

theorem :: ISOCAT_1:2
canceled;

::$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 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)) 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 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 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 for b1 being M3( 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 ; end; :: deftheorem defines Functor ISOCAT_1:def 1 : for C, D being Category for b3 being M3( 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 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 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 proof end; theorem Th7: :: 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 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 F " is Functor of B,A proof end; 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 :: 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 ) ) proof end; 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 ) ); theorem Th8: :: ISOCAT_1:10 for A, B being Category for F being Functor of A,B st F is isomorphic holds F " is isomorphic proof end; 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 ") proof end; theorem :: ISOCAT_1:12 for A, B being Category for F being Functor of A,B st F is isomorphic holds (F ") " = F proof end; 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 ) 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 proof end; :: Isomorphism of categories 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 isomorphic ; 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; 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 proof end; theorem :: ISOCAT_1:16 for A being Category for o, m being set holds [:(1Cat (o,m)),A:] ~= A proof end; theorem :: ISOCAT_1:17 for A, B being Category holds [:A,B:] ~= [:B,A:] proof end; theorem :: ISOCAT_1:18 for A, B, C being Category holds [:[:A,B:],C:] ~= [:A,[:B,C:]:] proof end; theorem :: ISOCAT_1:19 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 G * t is transformation of G * F1,G * F2 proof end; 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 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 t * (Obj F) is transformation of G1 * F,G2 * F proof end; 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 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) 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) 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 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 G * t is natural_transformation of G * F1,G * F2 proof end; 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 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) 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 t * F is natural_transformation of G1 * F,G2 * F proof end; 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 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) 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; 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; 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) 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) 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) 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) 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) 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) 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) 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 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 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 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 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) 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 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 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 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) 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 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) 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 ) 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 ) proof end; definition let A, B be Category; 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 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 ) ; end; :: 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 ) ); 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 proof end; theorem Th44: :: ISOCAT_1:46 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 ex b1 being Functor of A,B ex G being Functor of B,A st ( G * b1 ~= id A & b1 * G ~= id B ) by A1; 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 & b3 * G ~= id B ) ); theorem :: ISOCAT_1:47 for A being Category holds id A is Equivalence of A,A proof end; 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 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 ) 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 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 ) ) 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.) 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
proof end;
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 ) & ( for o being Object of C holds b2 . o = id o ) holds
b1 = b2
proof end;
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 );