:: Isomorphisms of Categories :: by Andrzej Trybulec :: :: Received November 22, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies CAT_1, FUNCT_1, ZFMISC_1, RELAT_1, MCART_1, STRUCT_0, ALGSTR_0, GRAPH_1, PZFMISC1, NATTRA_1, XBOOLE_0, WELLORD1, TARSKI, PARTFUN1, VALUED_1, REWRITE1, ISOCAT_1, MONOID_0; notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, STRUCT_0, GRAPH_1, CAT_1, CAT_2, CAT_3, NATTRA_1; constructors NATTRA_1, FUNCOP_1, RELSET_1, CAT_3, FUNCT_4; registrations RELSET_1, FUNCT_2, STRUCT_0, CAT_1, FUNCT_3; 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; ::$CT 2 theorem :: ISOCAT_1:3 for a,b being Object of A for f being Morphism of a,b st f is invertible holds F/.f is invertible; theorem :: ISOCAT_1:4 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:5 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:6 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; reserve o,m for set; theorem :: ISOCAT_1:7 F is isomorphic implies for g being Morphism of B ex f being Morphism of A st F.f = g; theorem :: ISOCAT_1:8 F is isomorphic implies for b being Object of B ex a being Object of A st F.a = b; theorem :: ISOCAT_1:9 F is one-to-one implies Obj F is one-to-one; definition let A,B,F; assume F is isomorphic; 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 carrier' of B; end; theorem :: ISOCAT_1:10 F is isomorphic implies F" is isomorphic; theorem :: ISOCAT_1:11 F is isomorphic implies (Obj F)" = Obj F"; theorem :: ISOCAT_1:12 F is isomorphic implies F"" = F; theorem :: ISOCAT_1:13 F is isomorphic implies F*F" = id B & F"*F = id A; theorem :: ISOCAT_1:14 F is isomorphic & G is isomorphic implies G*F is isomorphic; :: 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 isomorphic; reflexivity; symmetry; end; notation let A,B; synonym A ~= B for A,B are_isomorphic; end; theorem :: ISOCAT_1:15 A ~= B & B ~= C implies A ~= C; theorem :: ISOCAT_1:16 [:1Cat(o,m),A:] ~= A; theorem :: ISOCAT_1:17 [:A,B:] ~= [:B,A:]; theorem :: ISOCAT_1:18 [:[:A,B:],C:] ~= [:A,[:B,C:]:]; theorem :: ISOCAT_1:19 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:20 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:21 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:22 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:23 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:24 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, s9 for natural_transformation of F2,F3, t for natural_transformation of G1,G2, t9 for natural_transformation of G2,G3, u for natural_transformation of H1,H2; theorem :: ISOCAT_1:25 F1 is_naturally_transformable_to F2 implies for a being Object of A holds Hom(F1.a,F2.a) <> {}; theorem :: ISOCAT_1:26 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:27 F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies G*(s9`*`s) = (G*s9)`*`(G*s); theorem :: ISOCAT_1:28 G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t9`*`t)*F = (t9*F)`*`(t*F); theorem :: ISOCAT_1:29 H1 is_naturally_transformable_to H2 implies u*G*F = u*(G*F); theorem :: ISOCAT_1:30 G1 is_naturally_transformable_to G2 implies H*t*F = H*(t*F); theorem :: ISOCAT_1:31 F1 is_naturally_transformable_to F2 implies H*G*s = H*(G*s); theorem :: ISOCAT_1:32 (id G)*F = id(G*F); theorem :: ISOCAT_1:33 G*id F = id(G*F); theorem :: ISOCAT_1:34 G1 is_naturally_transformable_to G2 implies t*id B = t; theorem :: ISOCAT_1:35 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:36 F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies t(#)s = (G2*s)`*`(t*F1); theorem :: ISOCAT_1:37 F1 is_naturally_transformable_to F2 implies (id id B)(#)s = s; theorem :: ISOCAT_1:38 G1 is_naturally_transformable_to G2 implies t(#)(id id B) = t; theorem :: ISOCAT_1:39 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:40 G1 is_naturally_transformable_to G2 implies t*F = t(#)id F; theorem :: ISOCAT_1:41 F1 is_naturally_transformable_to F2 implies G*s = (id G)(#)s; theorem :: ISOCAT_1:42 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 (t9`*`t)(#)(s9`*`s) = (t9(#)s9)`*`(t(#)s); theorem :: ISOCAT_1:43 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:44 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; end; notation let A,B be Category; synonym A,B are_equivalent for A is_equivalent_with B; end; theorem :: ISOCAT_1:45 A ~= B implies A is_equivalent_with B; theorem :: ISOCAT_1:46 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:47 id A is Equivalence of A,A; theorem :: ISOCAT_1:48 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:49 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:50 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:51 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; :: 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; 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; end;