:: Products and Coproducts in Categories :: by Czes{\l}aw Byli\'nski :: :: Received May 11, 1992 :: Copyright (c) 1992-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 XBOOLE_0, CAT_1, SUBSET_1, FUNCT_1, PARTFUN1, FUNCOP_1, STRUCT_0, FUNCT_6, RELAT_1, GRAPH_1, FUNCT_4, ARYTM_0, FVSUM_1, ALGSTR_0, WELLORD1, TARSKI, CARD_1, CAT_3, MONOID_0; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_4, ORDINAL1, NUMBERS, FUNCT_2, STRUCT_0, GRAPH_1, CAT_1, OPPCAT_1; constructors PARTFUN1, OPPCAT_1, FUNCOP_1, RELSET_1, NUMBERS, FUNCT_4; registrations XBOOLE_0, RELSET_1, STRUCT_0, CAT_1, OPPCAT_1; requirements SUBSET, BOOLE; begin :: Indexed families reserve I for set, x,x1,x2,y,z for set, A for non empty set; reserve C,D for Category; reserve a,b,c,d for Object of C; reserve f,g,h,i,j,k,p1,p2,q1,q2,i1,i2,j1,j2 for Morphism of C; scheme :: CAT_3:sch 1 LambdaIdx{I()->set,A()->non empty set,F(object)->Element of A()}: ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x); theorem :: CAT_3:1 for F1,F2 being Function of I,A st for x st x in I holds F1/.x = F2/.x holds F1 = F2; scheme :: CAT_3:sch 2 FuncIdxcorrectness{I()->set,A()->non empty set,F(set)->Element of A()}: (ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x)) & for F1,F2 being Function of I(),A() st (for x st x in I() holds F1/.x = F(x)) & (for x st x in I() holds F2/.x = F(x)) holds F1 = F2; definition let A,x; let a be Element of A; redefine func x .--> a -> Function of {x},A; end; theorem :: CAT_3:2 for a being Element of A st x in I holds (I --> a)/.x = a; theorem :: CAT_3:3 x1 <> x2 implies for y1,y2 being Element of A holds ((x1,x2) --> (y1,y2))/.x1 = y1 & ((x1,x2) --> (y1,y2))/.x2 = y2; begin :: Indexed families of morphisms definition let C,I; let F be Function of I,the carrier' of C; func doms F -> Function of I, the carrier of C means :: CAT_3:def 1 for x st x in I holds it/.x = dom(F/.x); func cods F -> Function of I, the carrier of C means :: CAT_3:def 2 for x st x in I holds it/.x = cod(F/.x); end; theorem :: CAT_3:4 doms(I-->f) = I-->(dom f); theorem :: CAT_3:5 cods(I-->f) = I-->(cod f); theorem :: CAT_3:6 doms((x1,x2)-->(p1,p2)) = (x1,x2)-->(dom p1,dom p2); theorem :: CAT_3:7 cods((x1,x2)-->(p1,p2)) = (x1,x2)-->(cod p1,cod p2); definition let C,I; let F be Function of I,the carrier' of C; func F opp -> Function of I,the carrier' of C opp means :: CAT_3:def 3 for x st x in I holds it/.x = (F/.x) opp; end; theorem :: CAT_3:8 (I --> f) opp = I --> f opp; theorem :: CAT_3:9 x1 <> x2 implies ((x1,x2)-->(p1,p2)) opp = (x1,x2)-->(p1 opp,p2 opp); theorem :: CAT_3:10 for F being Function of I,the carrier' of C holds F opp opp = F; definition let C,I; let F be Function of I,the carrier' of C opp; func opp F -> Function of I,the carrier' of C means :: CAT_3:def 4 for x st x in I holds it/.x = opp (F/.x); end; theorem :: CAT_3:11 for f being Morphism of C opp holds opp(I --> f) = I --> (opp f); theorem :: CAT_3:12 x1 <> x2 implies for p1,p2 being Morphism of C opp holds opp ((x1,x2) -->(p1,p2)) = (x1,x2)-->(opp p1,opp p2); theorem :: CAT_3:13 for F being Function of I,the carrier' of C holds opp(F opp) = F; definition let C,I; let F be Function of I,the carrier' of C, f; func F*f -> Function of I,the carrier' of C means :: CAT_3:def 5 for x st x in I holds it/.x = (F/.x)(*)f; func f*F -> Function of I,the carrier' of C means :: CAT_3:def 6 for x st x in I holds it/.x = f(*)(F/.x); end; theorem :: CAT_3:14 x1 <> x2 implies ((x1,x2)-->(p1,p2))*f = (x1,x2)-->(p1(*)f,p2(*)f); theorem :: CAT_3:15 x1 <> x2 implies f*((x1,x2)-->(p1,p2)) = (x1,x2)-->(f(*)p1,f(*)p2); theorem :: CAT_3:16 for F being Function of I,the carrier' of C st doms F = I-->cod f holds doms(F*f) = I-->dom f & cods(F*f) = cods F; theorem :: CAT_3:17 for F being Function of I,the carrier' of C st cods F = I-->dom f holds doms(f*F) = doms F & cods(f*F) = I-->cod f; definition let C,I; let F,G be Function of I,the carrier' of C; func F"*"G -> Function of I,the carrier' of C means :: CAT_3:def 7 for x st x in I holds it/.x = (F/.x)(*)(G/.x); end; theorem :: CAT_3:18 for F,G being Function of I,the carrier' of C st doms F = cods G holds doms(F"*"G) = doms G & cods(F"*"G) = cods F; theorem :: CAT_3:19 x1 <> x2 implies ((x1,x2)-->(p1,p2))"*"((x1,x2)-->(q1,q2)) = (x1,x2) -->(p1(*)q1,p2(*)q2); theorem :: CAT_3:20 for F being Function of I,the carrier' of C holds F*f = F"*"(I-->f); theorem :: CAT_3:21 for F being Function of I,the carrier' of C holds f*F = (I-->f)"*"F; begin :: Retractions and Coretractions reserve f for Morphism of a,b, g for Morphism of b,a; definition let C,a,b; let IT be Morphism of a,b; attr IT is retraction means :: CAT_3:def 8 Hom(a,b) <> {} & Hom(b,a) <> {} & ex g st IT*g = id b; attr IT is coretraction means :: CAT_3:def 9 Hom(a,b) <> {} & Hom(b,a) <> {} & ex g st g*IT = id a; end; theorem :: CAT_3:22 f is retraction implies f is epi; theorem :: CAT_3:23 f is coretraction implies f is monic; reserve g for Morphism of b,c; theorem :: CAT_3:24 f is retraction & g is retraction implies g*f is retraction; theorem :: CAT_3:25 f is coretraction & g is coretraction implies g*f is coretraction; theorem :: CAT_3:26 Hom(a,b) <> {} & Hom(b,a) <> {} & g*f is retraction implies g is retraction; theorem :: CAT_3:27 Hom(b,c) <> {} & Hom(c,b) <> {} & g*f is coretraction implies f is coretraction; theorem :: CAT_3:28 f is retraction & f is monic implies f is invertible; theorem :: CAT_3:29 f is coretraction & f is epi implies f is invertible; theorem :: CAT_3:30 f is invertible iff f is retraction & f is coretraction; definition let C,a,b such that Hom(a,b) <> {}; let D; let T be Functor of C,D, f be Morphism of a,b; func T/.f -> Morphism of T.a, T.b equals :: CAT_3:def 10 T.f; end; theorem :: CAT_3:31 for T being Functor of C,D st f is retraction holds T/.f is retraction; theorem :: CAT_3:32 for T being Functor of C,D st f is coretraction holds T/.f is coretraction; theorem :: CAT_3:33 f is retraction iff f opp is coretraction; theorem :: CAT_3:34 f is coretraction iff f opp is retraction; begin :: carrier' determined by a terminal Object reserve f,g for Morphism of C; definition let C,a,b; assume b is terminal; func term(a,b) -> Morphism of a,b means :: CAT_3:def 11 not contradiction; end; theorem :: CAT_3:35 b is terminal implies dom(term(a,b)) = a & cod(term(a,b)) = b; theorem :: CAT_3:36 b is terminal & dom f = a & cod f = b implies term(a,b) = f; theorem :: CAT_3:37 for f being Morphism of a,b st b is terminal holds term(a,b) = f; begin :: carrier' determined by an iniatial object definition let C,a,b; assume a is initial; func init(a,b) -> Morphism of a,b means :: CAT_3:def 12 not contradiction; end; theorem :: CAT_3:38 a is initial implies dom(init(a,b)) = a & cod(init(a,b)) = b; theorem :: CAT_3:39 a is initial & dom f = a & cod f = b implies init(a,b) = f; theorem :: CAT_3:40 for f being Morphism of a,b st a is initial holds init(a,b) = f; begin :: Products definition let C,a,I; mode Projections_family of a,I -> Function of I,the carrier' of C means :: CAT_3:def 13 doms it = I --> a; end; theorem :: CAT_3:41 for F being Projections_family of a,I st x in I holds dom(F/.x) = a; theorem :: CAT_3:42 for F being Function of {},the carrier' of C holds F is Projections_family of a,{}; theorem :: CAT_3:43 dom f = a implies y .--> f is Projections_family of a,{y}; theorem :: CAT_3:44 dom p1 = a & dom p2 = a implies (x1,x2)-->(p1,p2) is Projections_family of a,{x1,x2}; theorem :: CAT_3:45 for F being Projections_family of a,I st cod f = a holds F*f is Projections_family of dom f,I; theorem :: CAT_3:46 for F being Function of I,the carrier' of C, G being Projections_family of a,I st doms F = cods G holds F"*"G is Projections_family of a,I; theorem :: CAT_3:47 for F being Projections_family of cod f,I holds (f opp)*(F opp) = (F*f ) opp; definition let C,a,I; let F be Function of I,the carrier' of C; pred a is_a_product_wrt F means :: CAT_3:def 14 F is Projections_family of a,I & for b for F9 being Projections_family of b,I st cods F = cods F9 ex h st h in Hom(b,a) & for k st k in Hom(b,a) holds (for x st x in I holds (F/.x)(*)k = F9/.x) iff h = k; end; theorem :: CAT_3:48 for F being Projections_family of c,I, F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds c,d are_isomorphic; theorem :: CAT_3:49 for F being Projections_family of c,I st c is_a_product_wrt F & for x1,x2 st x1 in I & x2 in I holds Hom(cod(F/.x1),cod(F/.x2)) <> {} for x st x in I for d being Object of C st d = cod(F/.x) & Hom(c,d) <> {} for f being Morphism of c,d st f = F/.x holds f is retraction; theorem :: CAT_3:50 for F being Function of {},the carrier' of C holds a is_a_product_wrt F iff a is terminal; theorem :: CAT_3:51 for F being Projections_family of a,I st a is_a_product_wrt F for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds b is_a_product_wrt F*f; theorem :: CAT_3:52 a is_a_product_wrt y .--> id a; theorem :: CAT_3:53 for F being Projections_family of a,I st a is_a_product_wrt F & for x st x in I holds cod(F/.x) is terminal holds a is terminal; definition let C,c,p1,p2; pred c is_a_product_wrt p1,p2 means :: CAT_3:def 15 dom p1 = c & dom p2 = c & for d, f,g st f in Hom(d,cod p1) & g in Hom(d,cod p2) ex h st h in Hom(d,c) & for k st k in Hom(d,c) holds p1(*)k = f & p2(*)k = g iff h = k; end; theorem :: CAT_3:54 x1 <> x2 implies (c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2)-->(p1,p2)); theorem :: CAT_3:55 Hom(c,a) <> {} & Hom(c,b) <> {} implies for p1 being Morphism of c,a, p2 being Morphism of c,b holds c is_a_product_wrt p1,p2 iff for d st Hom(d,a)<> {} & Hom(d,b)<>{} holds Hom(d,c) <> {} & for f being Morphism of d,a, g being Morphism of d,b ex h being Morphism of d,c st for k being Morphism of d,c holds p1*k = f & p2*k = g iff h = k; theorem :: CAT_3:56 c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 implies c,d are_isomorphic; theorem :: CAT_3:57 for p1 being Morphism of c,a, p2 being Morphism of c,b st Hom(c,a) <> {} & Hom(c,b) <> {} & c is_a_product_wrt p1,p2 & Hom(a,b) <> {} & Hom(b,a) <> {} holds p1 is retraction & p2 is retraction; theorem :: CAT_3:58 c is_a_product_wrt p1,p2 & h in Hom(c,c) & p1(*)h = p1 & p2(*)h = p2 implies h = id c; theorem :: CAT_3:59 for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds d is_a_product_wrt p1(*)f,p2(*)f; theorem :: CAT_3:60 c is_a_product_wrt p1,p2 & cod p2 is terminal implies c,cod p1 are_isomorphic ; theorem :: CAT_3:61 c is_a_product_wrt p1,p2 & cod p1 is terminal implies c,cod p2 are_isomorphic ; begin :: Coproducts definition let C,c,I; mode Injections_family of c,I -> Function of I,the carrier' of C means :: CAT_3:def 16 cods it = I --> c; end; theorem :: CAT_3:62 for F being Injections_family of c,I st x in I holds cod(F/.x) = c; theorem :: CAT_3:63 for F being Function of {},the carrier' of C holds F is Injections_family of a,{}; theorem :: CAT_3:64 cod f = a implies y .--> f is Injections_family of a,{y}; theorem :: CAT_3:65 cod p1 = c & cod p2 = c implies (x1,x2)-->(p1,p2) is Injections_family of c,{x1,x2}; theorem :: CAT_3:66 for F being Injections_family of b,I st dom f = b holds f*F is Injections_family of cod f,I; theorem :: CAT_3:67 for F being Injections_family of b,I, G being Function of I,the carrier' of C st doms F = cods G holds F"*"G is Injections_family of b,I; theorem :: CAT_3:68 for F be Function of I,the carrier' of C holds F is Projections_family of c,I iff F opp is Injections_family of c opp,I; theorem :: CAT_3:69 for F be Function of I,the carrier' of C opp, c being Object of C opp holds F is Injections_family of c,I iff opp F is Projections_family of opp c,I; theorem :: CAT_3:70 for F being Injections_family of dom f,I holds (F opp)*(f opp) = (f*F) opp; definition let C,c,I; let F be Function of I,the carrier' of C; pred c is_a_coproduct_wrt F means :: CAT_3:def 17 F is Injections_family of c,I & for d for F9 being Injections_family of d,I st doms F = doms F9 ex h st h in Hom(c,d) & for k st k in Hom(c,d) holds (for x st x in I holds k(*)(F/.x) = F9/.x ) iff h = k; end; theorem :: CAT_3:71 for F being Function of I,the carrier' of C holds c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp; theorem :: CAT_3:72 for F being Injections_family of c,I, F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds c,d are_isomorphic; theorem :: CAT_3:73 for F being Injections_family of c,I st c is_a_coproduct_wrt F & for x1,x2 st x1 in I & x2 in I holds Hom(dom(F/.x1),dom(F/.x2)) <> {} for x st x in I for d being Object of C st d = dom(F/.x) & Hom(d,c) <> {} for f being Morphism of d,c st f = F/.x holds f is coretraction; theorem :: CAT_3:74 for f being Morphism of a,b for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds b is_a_coproduct_wrt f*F; theorem :: CAT_3:75 for F being Injections_family of a,{} holds a is_a_coproduct_wrt F iff a is initial; theorem :: CAT_3:76 a is_a_coproduct_wrt y .--> id a; theorem :: CAT_3:77 for F being Injections_family of a,I st a is_a_coproduct_wrt F & for x st x in I holds dom(F/.x) is initial holds a is initial; definition let C,c,i1,i2; pred c is_a_coproduct_wrt i1,i2 means :: CAT_3:def 18 cod i1 = c & cod i2 = c & for d,f,g st f in Hom(dom i1,d) & g in Hom(dom i2,d) ex h st h in Hom(c,d) & for k st k in Hom(c,d) holds k(*)i1 = f & k(*)i2 = g iff h = k; end; theorem :: CAT_3:78 c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp, p2 opp; theorem :: CAT_3:79 x1 <> x2 implies (c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2)-->(i1,i2)); theorem :: CAT_3:80 c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 implies c,d are_isomorphic; theorem :: CAT_3:81 Hom(a,c) <> {} & Hom(b,c) <> {} implies for i1 being Morphism of a,c, i2 being Morphism of b,c holds c is_a_coproduct_wrt i1,i2 iff for d st Hom(a,d) <>{} & Hom(b,d)<>{} holds Hom(c,d) <> {} & for f being Morphism of a,d, g being Morphism of b,d ex h being Morphism of c,d st for k being Morphism of c,d holds k*i1 = f & k*i2 = g iff h = k; theorem :: CAT_3:82 for i1 being Morphism of a,c, i2 being Morphism of b,c st Hom(a,c) <> {} & Hom(b,c) <> {} holds c is_a_coproduct_wrt i1,i2 & Hom(a,b) <> {} & Hom(b,a) <> {} implies i1 is coretraction & i2 is coretraction; theorem :: CAT_3:83 c is_a_coproduct_wrt i1,i2 & h in Hom(c,c) & h(*)i1 = i1 & h(*)i2 = i2 implies h = id c; theorem :: CAT_3:84 for f being Morphism of c,d holds c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible implies d is_a_coproduct_wrt f(*)i1,f(*)i2; theorem :: CAT_3:85 c is_a_coproduct_wrt i1,i2 & dom i2 is initial implies dom i1,c are_isomorphic; theorem :: CAT_3:86 c is_a_coproduct_wrt i1,i2 & dom i1 is initial implies dom i2,c are_isomorphic;