Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Isomorphisms of Categories

**by****Andrzej Trybulec**- Received November 22, 1991
- MML identifier: ISOCAT_1

- [ Mizar article, MML identifier index ]

environ vocabulary CAT_1, FUNCT_1, RELAT_1, FUNCT_3, NATTRA_1, BOOLE, WELLORD1, PARTFUN1, SEQ_1, ISOCAT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, CAT_1, CAT_2, NATTRA_1; constructors NATTRA_1, MEMBERED, PARTFUN1, XBOOLE_0; clusters RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Auxiliary theorems reserve A,B,C,D for Category, F for Functor of A,B, G for Functor of B,C; theorem :: 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; theorem :: ISOCAT_1:2 rng pr1(A,B) = the Morphisms of A & rng pr2(B,A) = the Morphisms of A; theorem :: ISOCAT_1:3 for f being Morphism of A st f is invertible holds F.f is invertible; theorem :: ISOCAT_1:4 for F being Functor of A,B, G being Functor of B,A holds F*id A = F & id A*G = G; canceled 2; theorem :: ISOCAT_1:7 for F1,F2 being Functor of A,B st F1 is_transformable_to F2 for t being transformation of F1,F2, a being Object of A holds t.a in Hom(F1.a,F2.a); theorem :: ISOCAT_1:8 for F1,F2 being Functor of A,B, 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; theorem :: ISOCAT_1:9 for F1,F2 being Functor of A,B st F1 is_transformable_to F2 for t being transformation of F1,F2 st t is invertible for a being Object of A holds F1.a, F2.a are_isomorphic; definition let C,D; 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; end; definition let A; redefine func id A -> Functor of A,A; let B,C; let F be Functor of A,B, G be Functor of B,C; func G*F -> Functor of A,C; end; reserve o,m for set; theorem :: ISOCAT_1:10 F is_an_isomorphism implies for g being Morphism of B ex f being Morphism of A st F.f = g; theorem :: ISOCAT_1:11 F is_an_isomorphism implies for b being Object of B ex a being Object of A st F.a = b; theorem :: ISOCAT_1:12 F is one-to-one implies Obj F is one-to-one; definition let A,B,F; assume F is_an_isomorphism; func F" -> Functor of B,A equals :: ISOCAT_1:def 2 F"; end; definition let A,B,F; redefine attr F is isomorphic means :: ISOCAT_1:def 3 F is one-to-one & rng F = the Morphisms of B; synonym F is_an_isomorphism; end; theorem :: ISOCAT_1:13 F is_an_isomorphism implies F" is_an_isomorphism; theorem :: ISOCAT_1:14 F is_an_isomorphism implies (Obj F)" = Obj F"; theorem :: ISOCAT_1:15 F is_an_isomorphism implies F"" = F; theorem :: ISOCAT_1:16 F is_an_isomorphism implies F*F" = id B & F"*F = id A; theorem :: ISOCAT_1:17 F is_an_isomorphism & G is_an_isomorphism implies G*F is_an_isomorphism; :: Isomorphism of categories definition let A,B; pred A,B are_isomorphic means :: ISOCAT_1:def 4 ex F being Functor of A,B st F is_an_isomorphism; reflexivity; symmetry; synonym A ~= B; end; canceled 2; theorem :: ISOCAT_1:20 A ~= B & B ~= C implies A ~= C; theorem :: ISOCAT_1:21 [:1Cat(o,m),A:] ~= A; theorem :: ISOCAT_1:22 [:A,B:] ~= [:B,A:]; theorem :: ISOCAT_1:23 [:[:A,B:],C:] ~= [:A,[:B,C:]:]; theorem :: ISOCAT_1:24 A ~= B & C ~= D implies [:A,C:] ~= [:B,D:]; definition let A,B,C; let F1,F2 be Functor of A,B such that 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 :: ISOCAT_1:def 5 G*t; end; definition let A,B,C; let G1,G2 be Functor of B,C such that 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 :: ISOCAT_1:def 6 t*Obj F; end; theorem :: ISOCAT_1:25 for G1,G2 be Functor of B,C st G1 is_transformable_to G2 for F be Functor of A,B, t be transformation of G1,G2, a be Object of A holds (t*F).a = t.(F.a); theorem :: ISOCAT_1:26 for F1,F2 be Functor of A,B st F1 is_transformable_to F2 for t be transformation of F1,F2, G be Functor of B,C, a being Object of A holds (G*t).a = G.(t.a); theorem :: ISOCAT_1:27 for F1,F2 being Functor of A,B, 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; definition let A,B,C; let F1,F2 be Functor of A,B such that 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 :: ISOCAT_1:def 7 G*t; end; theorem :: ISOCAT_1:28 for F1,F2 be Functor of A,B st F1 is_naturally_transformable_to F2 for t be natural_transformation of F1,F2, G be Functor of B,C, a being Object of A holds (G*t).a = G.(t.a); definition let A,B,C; let G1,G2 be Functor of B,C such that 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 :: ISOCAT_1:def 8 t*F; end; theorem :: ISOCAT_1:29 for G1,G2 be Functor of B,C st G1 is_naturally_transformable_to G2 for F be Functor of A,B, t be natural_transformation of G1,G2, a be Object of A holds (t*F).a = t.(F.a); reserve F,F1,F2,F3 for Functor of A,B, G,G1,G2,G3 for Functor of B,C, H,H1,H2 for Functor of C,D, s for natural_transformation of F1,F2, s' for natural_transformation of F2,F3, t for natural_transformation of G1,G2, t' for natural_transformation of G2,G3, u for natural_transformation of H1,H2; theorem :: ISOCAT_1:30 F1 is_naturally_transformable_to F2 implies for a being Object of A holds Hom(F1.a,F2.a) <> {}; theorem :: ISOCAT_1:31 F1 is_naturally_transformable_to F2 implies for t1,t2 being natural_transformation of F1,F2 st for a being Object of A holds t1.a = t2.a holds t1 = t2; theorem :: ISOCAT_1:32 F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies G*(s'`*`s) = (G*s')`*`(G*s); theorem :: ISOCAT_1:33 G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t'`*`t)*F = (t'*F)`*`(t*F); theorem :: ISOCAT_1:34 H1 is_naturally_transformable_to H2 implies u*G*F = u*(G*F); theorem :: ISOCAT_1:35 G1 is_naturally_transformable_to G2 implies H*t*F = H*(t*F); theorem :: ISOCAT_1:36 F1 is_naturally_transformable_to F2 implies H*G*s = H*(G*s); theorem :: ISOCAT_1:37 (id G)*F = id(G*F); theorem :: ISOCAT_1:38 G*id F = id(G*F); theorem :: ISOCAT_1:39 G1 is_naturally_transformable_to G2 implies t*id B = t; theorem :: ISOCAT_1:40 F1 is_naturally_transformable_to F2 implies (id B)*s = s; definition let A,B,C,F1,F2,G1,G2; let s,t; func t(#)s -> natural_transformation of G1*F1,G2*F2 equals :: ISOCAT_1:def 9 (t*F2)`*`(G1*s); end; theorem :: ISOCAT_1:41 F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies t(#)s = (G2*s)`*`(t*F1); theorem :: ISOCAT_1:42 F1 is_naturally_transformable_to F2 implies (id id B)(#)s = s; theorem :: ISOCAT_1:43 G1 is_naturally_transformable_to G2 implies t(#)(id id B) = t; theorem :: ISOCAT_1:44 F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 & H1 is_naturally_transformable_to H2 implies u(#)(t(#)s) = (u(#)t)(#)s; theorem :: ISOCAT_1:45 G1 is_naturally_transformable_to G2 implies t*F = t(#)id F; theorem :: ISOCAT_1:46 F1 is_naturally_transformable_to F2 implies G*s = (id G)(#)s; theorem :: ISOCAT_1:47 F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t'`*`t)(#)(s'`*`s) = (t'(#)s')`*`(t(#)s); theorem :: ISOCAT_1:48 for F being Functor of A,B, 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; theorem :: ISOCAT_1:49 for F being Functor of A,B, G being Functor of B,A for I being Functor of A,A st I ~= id A holds F*I ~= F & I*G ~= G; definition let A,B be Category; pred A is_equivalent_with B means :: ISOCAT_1:def 10 ex F being Functor of A,B, G being Functor of B,A st G*F ~= id A & F*G ~= id B; reflexivity; symmetry; synonym A,B are_equivalent; end; theorem :: ISOCAT_1:50 A ~= B implies A is_equivalent_with B; canceled 2; theorem :: ISOCAT_1:53 A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent; definition let A,B; assume A,B are_equivalent; mode Equivalence of A,B -> Functor of A,B means :: ISOCAT_1:def 11 ex G being Functor of B,A st G*it ~= id A & it*G ~= id B; end; theorem :: ISOCAT_1:54 id A is Equivalence of A,A; theorem :: ISOCAT_1:55 A,B are_equivalent & B,C are_equivalent implies for F being Equivalence of A,B, G being Equivalence of B,C holds G*F is Equivalence of A,C; theorem :: ISOCAT_1:56 A,B are_equivalent implies for F being Equivalence of A,B ex G being Equivalence of B,A st G*F ~= id A & F*G ~= id B; theorem :: ISOCAT_1:57 for F being Functor of A,B, G being Functor of B,A st G*F ~= id A holds F is faithful; theorem :: ISOCAT_1:58 A,B are_equivalent implies 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;

Back to top