FORMALIZED MATHEMATICSVol.2,No.5, November–December 1991Universit´e Catholique de Louvain Isomorphisms of Categories Andrzej Trybulec Warsaw University Bialystok Summary. We continue the development of the category theorybasically following [12] (compare also [11]). We deﬁne the concept of iso-morphic categories and prove basic facts related, e.g. that the Cartesianproduct of categories is associative up to the isomorphism. We introducethe composition of a functor and a transformation, and of transforma-tion and a functor, and afterwards we deﬁne again those concepts fornatural transformations. Let us observe, that we have to duplicate thoseconcepts because of the permissiveness: if a functor F is not naturallytransformable to G, then natural transformation from F to G has no ﬁxedmeaning, hence we cannot claim that the composition of it with a func-tor as a transformation results in a natural transformation. We deﬁnealso the so called horizontal composition of transformations ([12], p.140,exercise 4.2,5(C)) and prove interchange law ([11], p.44). We concludewith the deﬁnition of equivalent categories.MML Identiﬁer: ISOCAT 1.The articles [16], [17], [4], [5], [3], [7], [1], [2], [10], [13], [8], [14], [6], [9], and [15]provide the notation and terminology for this paper. We adopt the followingconvention: A, B, C, D will denote categories, F , F1, F2 will denote functorsfrom A to B, and G will denote a functor from B to C. One can prove thefollowing propositions: (1) For all functions F , G such that F is one-to-one and G is one-to-one holds [: F, G :] is one-to-one. (2) rng π1(A × B) = the morphisms of A and rng π2(B × A) = the mor- phisms of A. (3) For every morphism f of A such that f is invertible holds F (f ) is invertible. (4) For every functor F from A to B and for every functor G from B to A holds F · idA = F and idA · G = G. 629 c 1991 Fondation Philippe le Hodey ISSN 0777–4028

630 andrzej trybulec (5) For all objects a, b of A such that hom(a, b) = ∅ and for every morphism f from a to b and for every functor F from A to B and for every functor G from B to C holds (G · F )(f ) = G(F (f )). (6) For all objects a, b, c of A such that hom(a, b) = ∅ and hom(b, c) = ∅ and for every morphism f from a to b and for every morphism g from b to c and for every functor F from A to B holds F (g · f ) = F (g) · F (f ). (7) For all functors F1, F2 from A to B such that F1 is transformable to F2 and for every transformation t from F1 to F2 and for every object a of A holds t(a) ∈ hom(F1(a), F2(a)). (8) For all functors F1, F2 from A to B and for all functors G1, G2 from B to C such that F1 is transformable to F2 and G1 is transformable to G2 holds G1 · F1 is transformable to G2 · F2. (9) For all functors F1, F2 from A to B such that F1 is transformable to F2 and for every transformation t from F1 to F2 such that t is invertible and for every object a of A holds F1(a) and F2(a) are isomorphic. Let us consider C, D. Let us observe that the mode below can be charac- terized by another conditions, which are equivalent to the formulas previously deﬁning them. In accordance the mode Let us note that one can characterize the mode functor from C to D, by the following (equivalent) condition: (Def.1) (i) for every object c of C there exists an object d of D such that it(idc) = idd, (ii) for every morphism f of C holds it(iddom f ) = iddom it(f) and it(idcod f ) = idcod it(f), (iii) for all morphisms f , g of C such that dom g = cod f holds it(g · f ) = it(g) · it(f ). Let us consider A. Then idA is a functor from A to A. Let us consider B, C, and let F be a functor from A to B, and let G be a functor from B to C. Then G · F is a functor from A to C. In the sequel o, m are arbitrary. We now state three propositions: (10) If F is an isomorphism, then for every morphism g of B there exists a morphism f of A such that F (f ) = g. (11) If F is an isomorphism, then for every object b of B there exists an object a of A such that F (a) = b. (12) If F is one-to-one, then Obj F is one-to-one. Let us consider A, B, F . Let us assume that F is an isomorphism. The functor F −1 yields a functor from B to A and is deﬁned by: (Def.2) F −1 = F −1. Let us consider A, B, F . Let us note that one can characterize the predicate F is an isomorphism by the following (equivalent) condition: (Def.3) F is one-to-one and rng F = the morphisms of B. Next we state several propositions: (13) If F is an isomorphism, then F −1 is an isomorphism.

isomorphisms of categories 631 (14) If F is an isomorphism, then (Obj F )−1 = Obj(F −1). (15) If F is an isomorphism, then (F −1)−1 = F . (16) If F is an isomorphism, then F · F −1 = idB and F −1 · F = idA. (17) If F is an isomorphism and G is an isomorphism, then G · F is an isomorphism. In the sequel t1 denotes a natural transformation from F1 to F2 and t2 denotes a natural transformation from F to F2. We now deﬁne two new predicates. Let us consider A, B. We say that A and B are isomorphic if and only if:(Def.4) there exists a functor F from A to B such that F is an isomorphism. We write A ∼= B if A and B are isomorphic. The following propositions are true: (18) A =∼ A. (19) If A ∼= B, then B ∼= A. (20) If A ∼= B and B ∼= C, then A ∼= C. (21) [: ˙ (o, m), A :] ∼= A. (22) [: A, B :] =∼ [: B, A :]. (23) [: [: A, B :], C :] =∼ [: A, [: B, C :] :]. (24) If A ∼= B and C =∼ D, then [: A, C :] ∼= [: B, D :]. Let us consider A, B, C, and let F1, F2 be functors from A to B satisfying the condition: F1 is transformable to F2. Let t be a transformation from F1 to F2, and let G be a functor from B to C. The functor G·t yields a transformation from G · F1 to G · F2 and is deﬁned as follows:(Def.5) G · t = G · t. Let us consider A, B, C, and let G1, G2 be functors from B to C satisfying the condition: G1 is transformable to G2. Let F be a functor from A to B, and let t be a transformation from G1 to G2. The functor t · F yielding a transformation from G1 · F to G2 · F is deﬁned by:(Def.6) t · F = t · Obj F . We now state three propositions: (25) For all functors G1, G2 from B to C such that G1 is transformable to G2 and for every functor F from A to B and for every transformation t from G1 to G2 and for every object a of A holds (t · F )(a) = t(F (a)). (26) For all functors F1, F2 from A to B such that F1 is transformable to F2 and for every transformation t from F1 to F2 and for every functor G from B to C and for every object a of A holds (G · t)(a) = G(t(a)). (27) For all functors F1, F2 from A to B and for all functors G1, G2 from B to C such that F1 is naturally transformable to F2 and G1 is naturally transformable to G2 holds G1 · F1 is naturally transformable to G2 · F2. Let us consider A, B, C, and let F1, F2 be functors from A to B satisfying the condition: F1 is naturally transformable to F2. Let t be a natural transformation

632 andrzej trybulec from F1 to F2, and let G be a functor from B to C. The functor G · t yielding a natural transformation from G · F1 to G · F2 is deﬁned by: (Def.7) G · t = G · t. Next we state the proposition (28) For all functors F1, F2 from A to B such that F1 is naturally trans- formable to F2 and for every natural transformation t from F1 to F2 and for every functor G from B to C and for every object a of A holds (G · t)(a) = G(t(a)). Let us consider A, B, C, and let G1, G2 be functors from B to C satisfying the condition: G1 is naturally transformable to G2. Let F be a functor from A to B, and let t be a natural transformation from G1 to G2. The functor t · F yields a natural transformation from G1 · F to G2 · F and is deﬁned as follows: (Def.8) t · F = t · F . The following proposition is true (29) For all functors G1, G2 from B to C such that G1 is naturally trans- formable to G2 and for every functor F from A to B and for every nat- ural transformation t from G1 to G2 and for every object a of A holds (t · F )(a) = t(F (a)). For simplicity we follow the rules: F , F1, F2, F3 are functors from A to B, G, G1, G2, G3 are functors from B to C, H, H1, H2 are functors from C to D, s is a natural transformation from F1 to F2, s′ is a natural transformation from F2 to F3, t is a natural transformation from G1 to G2, t′ is a natural transformation from G2 to G3, and u is a natural transformation from H1 to H2. We now state a number of propositions: (30) If F1 is naturally transformable to F2, then for every object a of A holds hom(F1(a), F2(a)) = ∅. (31) If F1 is naturally transformable to F2, then for all natural transfor- mations t1, t2 from F1 to F2 such that for every object a of A holds t1(a) = t2(a) holds t1 = t2. (32) If F1 is naturally transformable to F2 and F2 is naturally transformable to F3, then G · (s′ ◦ s) = G · s′ ◦ G · s. (33) If G1 is naturally transformable to G2 and G2 is naturally transformable to G3, then (t′ ◦ t) · F = t′ · F ◦ t · F . (34) If H1 is naturally transformable to H2, then (u · G) · F = u · (G · F ). (35) If G1 is naturally transformable to G2, then (H · t) · F = H · (t · F ). (36) If F1 is naturally transformable to F2, then (H · G) · s = H · (G · s). (37) idG · F = id(G·F ). (38) G · idF = id(G·F ). (39) If G1 is naturally transformable to G2, then t · idB = t. (40) If F1 is naturally transformable to F2, then idB · s = s.

isomorphisms of categories 633 Let us consider A, B, C, F1, F2, G1, G2, s, t. The functor t s yields a natural transformation from G1 · F1 to G2 · F2 and is deﬁned as follows: (Def.9) t s = t · F2 ◦ G1 · s. We now state several propositions: (41) If F1 is naturally transformable to F2 and G1 is naturally transformable to G2, then t s = G2 · s ◦ t · F1. (42) If F1 is naturally transformable to F2, then id(idB) s = s. (43) If G1 is naturally transformable to G2, then t id(idB) = t. (44) If F1 is naturally transformable to F2 and G1 is naturally transformable to G2 and H1 is naturally transformable to H2, then u (t s) = (u t) s. (45) If G1 is naturally transformable to G2, then t · F = t idF . (46) If F1 is naturally transformable to F2, then G · s = idG s. (47) If F1 is naturally transformable to F2 and F2 is naturally transformable to F3 and G1 is naturally transformable to G2 and G2 is naturally trans- formable to G3, then (t′ ◦ t) (s′ ◦ s) = t′ s′ ◦ t s. (48) For every functor F from A to B and for every functor G from C to D and for all functors I, J from B to C such that I ∼= J holds G · I ∼= G · J and I · F =∼ J · F . (49) For every functor F from A to B and for every functor G from B to A and for every functor I from A to A such that I ∼= idA holds F · I ∼= F and I · G =∼ G. We now deﬁne two new predicates. Let A, B be categories. We say that A is equivalent with B if and only if:(Def.10) there exists a functor F from A to B and there exists a functor G from B to A such that G · F =∼ idA and F · G ∼= idB. A and B are equivalent stands for A is equivalent with B. We now state four propositions: (50) If A =∼ B, then A is equivalent with B. (51) A is equivalent with A. (52) If A and B are equivalent, then B and A are equivalent. (53) If A and B are equivalent and B and C are equivalent, then A and C are equivalent. Let us consider A, B. Let us assume that A and B are equivalent. A functor from A to B is called an equivalence of A and B if:(Def.11) there exists a functor G from B to A such that G · it ∼= idA and it · G =∼ idB . Next we state several propositions: (54) idA is an equivalence of A and A. (55) If A and B are equivalent and B and C are equivalent, then for every equivalence F of A and B and for every equivalence G of B and C holds G · F is an equivalence of A and C.

634 andrzej trybulec (56) If A and B are equivalent, then for every equivalence F of A and B there exists an equivalence G of B and A such that G · F ∼= idA and F · G =∼ idB. (57) For every functor F from A to B and for every functor G from B to A such that G · F =∼ idA holds F is faithful. (58) If A and B are equivalent, then for every equivalence F of A and B holds F is full and F is faithful and for every object b of B there exists an object a of A such that b and F (a) are isomorphic. References [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. [2] Grzegorz Bancerek. Curried and uncurried functions. Formalized Mathematics, 1(3):537–541, 1990. [3] Czeslaw Bylin´ski. Basic functions and operations on functions. Formalized Mathematics, 1(1):245–254, 1990. [4] Czeslaw Bylin´ski. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990. [5] Czeslaw Bylin´ski. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. [6] Czeslaw Bylin´ski. Introduction to categories and functors. Formalized Mathematics, 1(2):409–420, 1990. [7] Czeslaw Bylin´ski. The modiﬁcation of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521–527, 1990. [8] Czeslaw Bylin´ski. Partial functions. Formalized Mathematics, 1(2):357–367, 1990. [9] Czeslaw Bylin´ski. Subcategories and products of categories. Formalized Mathematics, 1(4):725–732, 1990. [10] Agata Darmochwal. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. [11] Saunders Mac Lane. Categories for the Working Mathematician. Volume 5 of Graduate Texts in Mathemaics, Springer Verlag, New York, Heidelberg, Berlin, 1971. [12] Zbigniew Semadeni and Antoni Wiweger. Wste¸p do teorii kategorii i funktoro´w. Vol- ume 45 of Biblioteka Matematyczna, PWN, Warszawa, 1978. [13] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990. [14] Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990. [15] Andrzej Trybulec. Natural transformations. Discrete categories. Formalized Mathemat- ics, 2(4):467–474, 1991. [16] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990. [17] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990. Received November 22, 1991

# Isomorphisms of Categories - Formalized Mathematics, eISSN ...

##
**Description: ** FORMALIZED MATHEMATICS Vol.2,No.5, November–December 1991 Universit´e Catholique de Louvain Isomorphisms of Categories Andrzej Trybulec Warsaw University

### Read the Text Version

No Text Content!

- 1 - 6

Pages: