Copyright (c) 1992 Association of Mizar Users
environ vocabulary FUNCT_1, CAT_1, WELLORD1, BOOLE, FINSET_1, CAT_3, RELAT_1, FUNCOP_1, FINSEQ_4, CARD_1, ARYTM_1, FUNCT_4, FUNCT_6, PARTFUN1, FUNCT_3, ALGSTR_1, DIRAF, EQREL_1, CAT_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ALGSTR_1, REAL_1, NAT_1, CARD_1, FUNCT_4, CAT_1, CAT_3; constructors DOMAIN_1, ALGSTR_1, REAL_1, NAT_1, CAT_3, FINSEQ_4, PARTFUN1, XREAL_0, XBOOLE_0; clusters SUBSET_1, FINSET_1, RELSET_1, RELAT_1, FUNCT_1, NAT_1, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE; definitions CAT_1, CAT_3; theorems TARSKI, ZFMISC_1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, CARD_2, CAT_1, CAT_3, FUNCT_1, RELSET_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1; begin reserve o,m,r for set; definition let o,m,r; func (o,m) :-> r -> Function of [:{o},{m}:],{r} means not contradiction; existence; uniqueness by FUNCT_2:66; end; definition let C be Category, a,b be Object of C; redefine pred a,b are_isomorphic means Hom(a,b)<>{} & Hom(b,a)<>{} & ex f being Morphism of a,b, f' being Morphism of b,a st f*f' = id b & f'*f = id a; compatibility by CAT_1:81; end; begin :: Cartesian Categories definition let C be Category; attr C is with_finite_product means for I being finite set, F being Function of I,the Objects of C ex a being Object of C, F' being Projections_family of a,I st cods F' = F & a is_a_product_wrt F'; synonym C has_finite_product; end; theorem Th1: for C being Category holds C has_finite_product iff (ex a being Object of C st a is terminal) & for a,b being Object of C ex c being Object of C, p1,p2 being Morphism of C st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 proof let C be Category; thus C has_finite_product implies (ex a being Object of C st a is terminal) & for a,b being Object of C ex c being Object of C, p1,p2 being Morphism of C st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 proof assume A1: for I being finite set, F being Function of I,the Objects of C ex a being Object of C, F' being Projections_family of a,I st cods F' = F & a is_a_product_wrt F'; reconsider F = {} as Function of {},the Objects of C by FUNCT_2:55,RELAT_1: 60; consider a being Object of C, F' being Projections_family of a,{} such that cods F' = F and A2: a is_a_product_wrt F' by A1; a is terminal by A2,CAT_3:55; hence ex a being Object of C st a is terminal; let a,b be Object of C; set F = (0,1)-->(a,b); consider c being Object of C, F' being Projections_family of c,{0,1} such that A3: cods F' = F and A4: c is_a_product_wrt F' by A1; take c, p1 = F'/.0, p2 = F'/.1; A5: 0 in {0,1} & 1 in {0,1} by TARSKI:def 2; hence dom p1 = c & dom p2 = c by CAT_3:45; F/.0 = a & F/.1 = b by CAT_3:7; hence cod p1 = a & cod p2 = b by A3,A5,CAT_3:def 4; A6: dom F' = {0,1} by FUNCT_2:def 1; p1 = F'.0 & p2 = F'.1 by A5,CAT_3:def 1; then 0 <> 1 & F' = (0,1)-->(p1,p2) by A6,FUNCT_4:69; hence c is_a_product_wrt p1,p2 by A4,CAT_3:59; end; given a being Object of C such that A7: a is terminal; assume A8:for a,b being Object of C ex c being Object of C, p1,p2 being Morphism of C st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2; defpred Q[Nat] means for I being finite set, F being Function of I,the Objects of C st card I = $1 ex a being Object of C, F' being Projections_family of a,I st cods F' = F & a is_a_product_wrt F'; A9: Q[ 0 ] proof let I be finite set, F be Function of I,the Objects of C; assume A10: card I = 0; then A11: I = {} by CARD_2:59; {} is Function of {}, the Morphisms of C by FUNCT_2:55,RELAT_1:60; then reconsider F' = {} as Projections_family of a,I by A11,CAT_3:46; take a,F'; for x being set st x in I holds (cods F')/.x = F/.x by A10,CARD_2:59; hence cods F' = F by CAT_3:1; thus thesis by A7,A11,CAT_3:55; end; A12: for n being Nat st Q[n] holds Q[n+1] proof let n be Nat such that A13: Q[n]; let I be finite set, F be Function of I,the Objects of C such that A14: card I = n+1; consider x being Element of I; reconsider Ix = I \ {x} as finite set; A15: {x} c= I by A14,CARD_1:47,ZFMISC_1:37; reconsider sx = {x} as finite set; A16: card(Ix) = card(I) - card(sx) by A15,CARD_2:63 .= card(I) - 1 by CARD_1:79 .= n by A14,XCMPLX_1:26; A17: I\{x} c= I & the Objects of C <> {} by XBOOLE_1:36; then reconsider G = F|(I\{x}) as Function of I\{x},the Objects of C by FUNCT_2:38; consider a being Object of C, G' being Projections_family of a,I\{x} such that A18: cods G' = G and A19: a is_a_product_wrt G' by A13,A16; consider c being Object of C, p1,p2 being Morphism of C such that A20: dom p1 = c & dom p2 = c and A21: cod p1 = a & cod p2 = F/.x and A22: c is_a_product_wrt p1,p2 by A8; set F' = (G'*p1) +* ({x} -->p2); A23: dom(G'*p1) = I\{x} & dom({x} -->p2) = {x} by FUNCT_2:def 1; then A24: dom(G'*p1) \/ dom({x} -->p2) = I \/ {x} by XBOOLE_1:39 .= I by A14,CARD_1:47,ZFMISC_1:46; then A25: dom F' = I by FUNCT_4:def 1; A26: rng F' c= rng(G'*p1) \/ rng({x} -->p2) by FUNCT_4:18; rng(G'*p1) c= the Morphisms of C & rng({x} -->p2) c= the Morphisms of C by RELSET_1:12; then rng(G'*p1) \/ rng({x} -->p2) c= the Morphisms of C by XBOOLE_1:8; then rng F' c= the Morphisms of C by A26,XBOOLE_1:1; then reconsider F' as Function of I, the Morphisms of C by A25,FUNCT_2:def 1,RELSET_1:11; A27: doms G' = (I\{x})-->a by CAT_3:def 14; now let y be set; assume A28: y in I; now per cases; suppose y = x; then A29: y in {x} by TARSKI:def 1; F'/.y = F'.y by A28,CAT_3:def 1 .= ({x} -->p2).y by A23,A29,FUNCT_4:14 .= p2 by A29,FUNCOP_1:13; hence (I --> c).y = dom(F'/.y) by A20,A28,FUNCOP_1:13 .= (doms F')/.y by A28,CAT_3:def 3; suppose A30: y <> x; then A31: not y in {x} by TARSKI:def 1; A32: y in I\{x} by A28,A30,ZFMISC_1:64; F'/.y = F'.y by A28,CAT_3:def 1 .= (G'*p1).y by A23,A24,A28,A31,FUNCT_4:def 1 .= (G'*p1)/.y by A32,CAT_3:def 1; hence (doms F')/.y = dom((G'*p1)/.y) by A28,CAT_3:def 3 .= (doms(G'*p1))/.y by A32,CAT_3:def 3 .= ((I\{x})-->c)/.y by A20,A21,A27,CAT_3:20 .= c by A32,CAT_3:2 .= (I --> c).y by A28,FUNCOP_1:13; end; hence (doms F').y = (I --> c).y by A28,CAT_3:def 1; end; then doms F' = I --> c by FUNCT_2:18; then reconsider F' as Projections_family of c,I by CAT_3:def 14; take c,F'; now let y be set; assume A33: y in I; now per cases; suppose A34: y = x; then A35: y in {x} by TARSKI:def 1; F'/.y = F'.y by A33,CAT_3:def 1 .= ({x} -->p2).y by A23,A35,FUNCT_4:14 .= p2 by A35,FUNCOP_1:13; hence (cods F')/.y = F/.y by A21,A33,A34,CAT_3:def 4; suppose A36: y <> x; then A37: not y in {x} by TARSKI:def 1; A38: y in I\{x} by A33,A36,ZFMISC_1:64; F'/.y = F'.y by A33,CAT_3:def 1 .= (G'*p1).y by A23,A24,A33,A37,FUNCT_4:def 1 .= (G'*p1)/.y by A38,CAT_3:def 1; hence (cods F')/.y = cod((G'*p1)/.y) by A33,CAT_3:def 4 .= (cods(G'*p1))/.y by A38,CAT_3:def 4 .= G/.y by A18,A21,A27,CAT_3:20 .= G.y by A38,CAT_3:def 1 .= F.y by A38,FUNCT_1:72 .= F/.y by A33,CAT_3:def 1; end; hence (cods F')/.y = F/.y; end; hence A39: cods F' = F by CAT_3:1; thus F' is Projections_family of c,I; let d be Object of C; let F'' be Projections_family of d,I such that A40: cods F' = cods F''; reconsider G'' = F''|(I\{x}) as Function of I\{x},the Morphisms of C by A17,FUNCT_2:38; now let y be set; assume A41: y in I\{x}; then A42: y in I by XBOOLE_0:def 4; G''/.y = G''.y by A41,CAT_3:def 1 .= F''.y by A41,FUNCT_1:72 .= F''/.y by A42,CAT_3:def 1; hence doms(G'')/.y = dom(F''/.y) by A41,CAT_3:def 3 .= d by A42,CAT_3:45 .= ((I\{x})-->d)/.y by A41,CAT_3:2; end; then doms G'' = I\{x} --> d by CAT_3:1; then reconsider G'' as Projections_family of d,I\{x} by CAT_3:def 14; now let y be set; assume A43: y in I\{x}; then A44: y in I by XBOOLE_0:def 4; then A45: F''/.y = F''.y by CAT_3:def 1 .= G''.y by A43,FUNCT_1:72 .= G''/.y by A43,CAT_3:def 1; G/.y = G.y by A43,CAT_3:def 1 .= F.y by A43,FUNCT_1:72 .= F/.y by A44,CAT_3:def 1; hence (cods G')/.y = cod(G''/.y) by A18,A39,A40,A44,A45,CAT_3:def 4 .= (cods G'')/.y by A43,CAT_3:def 4; end; then cods G' = cods G'' by CAT_3:1; then consider h' being Morphism of C such that A46: h' in Hom(d,a) and A47: for k being Morphism of C st k in Hom(d,a) holds (for y being set st y in I\{x} holds (G'/.y)*k = G''/.y) iff h' = k by A19,CAT_3:def 15; set g = F''/.x; A48: dom g = d by A14,CARD_1:47,CAT_3:45; A49: x in {x} by TARSKI:def 1; A50: F'/.x = F'.x by A14,CARD_1:47,CAT_3:def 1 .= ({x} -->p2).x by A23,A49,FUNCT_4:14 .= p2 by A49,FUNCOP_1:13; then cod p2 = (cods F')/.x by A14,CARD_1:47,CAT_3:def 4 .= cod g by A14,A40,CARD_1:47,CAT_3:def 4; then g in Hom(d,cod p2) by A48,CAT_1:18; then consider h being Morphism of C such that A51: h in Hom(d,c) and A52: for k being Morphism of C st k in Hom(d,c) holds p1*k = h' & p2*k = g iff h = k by A21,A22,A46,CAT_3:def 16; take h; thus h in Hom(d,c) by A51; let k be Morphism of C such that A53: k in Hom(d,c); thus (for y being set st y in I holds (F'/.y)*k = F''/.y) implies h = k proof assume A54: for y being set st y in I holds (F'/.y)*k = F''/.y; then A55: p2*k = g by A14,A50,CARD_1:47; A56: dom k = d & cod k = c by A53,CAT_1:18; then dom(p1*k) = d & cod(p1*k) = a by A20,A21,CAT_1:42; then A57: p1*k in Hom(d,a) by CAT_1:18; for y being set st y in I\{x} holds (G'/.y)*(p1*k) = G''/.y proof let y be set; assume A58: y in I\{x}; then A59: y in I & not y in {x} by XBOOLE_0:def 4; then A60: F'/.y = F'.y by CAT_3:def 1 .= (G'*p1).y by A23,A24,A59,FUNCT_4:def 1 .= (G'*p1)/.y by A58,CAT_3:def 1; dom(G'/.y) = a by A58,CAT_3:45; hence (G'/.y)*(p1*k) = ((G'/.y)*p1)*k by A20,A21,A56,CAT_1:43 .= ((G'*p1)/.y)*k by A58,CAT_3:def 7 .= F''/.y by A54,A59,A60 .= F''.y by A59,CAT_3:def 1 .= G''.y by A58,FUNCT_1:72 .= G''/.y by A58,CAT_3:def 1; end; then p1*k = h' by A47,A57; hence h = k by A52,A53,A55; end; assume A61: h = k; let y be set such that A62: y in I; now per cases; suppose A63: y = x; then A64: y in {x} by TARSKI:def 1; F'/.y = F'.y by A62,CAT_3:def 1 .= ({x} -->p2).y by A23,A64,FUNCT_4:14 .= p2 by A64,FUNCOP_1:13; hence thesis by A52,A53,A61,A63; suppose A65: y <> x; then A66: not y in {x} by TARSKI:def 1; A67: y in I\{x} by A62,A65,ZFMISC_1:64; then A68: cod k = c & dom(G'/.y) = a by A53,CAT_1:18,CAT_3:45; F'/.y = F'.y by A62,CAT_3:def 1 .= (G'*p1).y by A23,A24,A62,A66,FUNCT_4:def 1 .= (G'*p1)/.y by A67,CAT_3:def 1 .= (G'/.y)*p1 by A67,CAT_3:def 7; hence (F'/.y)*k = (G'/.y)*(p1*k) by A20,A21,A68,CAT_1:43 .= (G'/.y)*h' by A52,A53,A61 .= G''/.y by A46,A47,A67 .= G''.y by A67,CAT_3:def 1 .= F''.y by A67,FUNCT_1:72 .= F''/.y by A62,CAT_3:def 1; end; hence thesis; end; A69: for n being Nat holds Q[n] from Ind(A9,A12); let I be finite set, F be Function of I,the Objects of C; card I = card I; hence thesis by A69; end; definition struct (CatStr)ProdCatStr (# Objects,Morphisms -> non empty set, Dom,Cod -> Function of the Morphisms, the Objects, Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms, Id -> Function of the Objects, the Morphisms, TerminalObj -> Element of the Objects, CatProd -> Function of [:the Objects,the Objects:],the Objects, Proj1,Proj2 -> Function of [:the Objects,the Objects:],the Morphisms #); end; definition let C be ProdCatStr; func [1]C -> Object of C equals :Def4: the TerminalObj of C; correctness; let a,b be Object of C; func a[x]b -> Object of C equals :Def5: (the CatProd of C).[a,b]; correctness; func pr1(a,b) -> Morphism of C equals :Def6: (the Proj1 of C).[a,b]; correctness; func pr2(a,b) -> Morphism of C equals :Def7: (the Proj2 of C).[a,b]; correctness; end; definition let o,m; func c1Cat(o,m) -> strict ProdCatStr equals :Def8: ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #); correctness; end; theorem the CatStr of c1Cat(o,m) = 1Cat(o,m) proof c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8; hence thesis by CAT_1:def 9; end; Lm1: c1Cat(o,m) is Category-like proof set C = c1Cat(o,m); A1: C = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8; set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C, CI = the Id of C; thus for f,g being Morphism of C holds [g,f] in dom CP iff CD.g=CC.f proof let f,g be Morphism of C; f = m & g = m & dom CP = {[m,m]} by A1,CAT_1:7,TARSKI:def 1; hence thesis by A1,TARSKI:def 1; end; thus for f,g being Morphism of C st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g proof let f,g be Morphism of C; CP.[g,f] = m by A1,CAT_1:9; then reconsider gf = CP.[g,f] as Morphism of C by A1,TARSKI:def 1; CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65; hence thesis; end; thus for f,g,h being Morphism of C st CD.h = CC.g & CD.g = CC.f holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f] proof let f,g,h be Morphism of C; CP.[g,f] = m & CP.[h,g] = m by A1,CAT_1:9; then reconsider gf = CP.[g,f],hg = CP.[h,g] as Morphism of C by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,CAT_1:9; hence thesis; end; let b be Object of C; b = o by A1,TARSKI:def 1; hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65; thus for f being Morphism of C st CC.f = b holds CP.[CI.b,f] = f proof let f be Morphism of C; f = m by A1,TARSKI:def 1; hence thesis by A1,CAT_1:9; end; let g be Morphism of C; assume CD.g = b; g = m by A1,TARSKI:def 1; hence CP.[g,CI.b] = g by A1,CAT_1:9; end; definition cluster strict Category-like ProdCatStr; existence proof c1Cat(0,1) is Category-like by Lm1; hence thesis; end; end; definition let o,m be set; cluster c1Cat(o,m) -> Category-like; coherence by Lm1; end; theorem Th3: for a being Object of c1Cat(o,m) holds a = o proof let a be Object of c1Cat(o,m); c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8; hence thesis by TARSKI:def 1; end; theorem Th4: for a,b being Object of c1Cat(o,m) holds a = b proof let a,b be Object of c1Cat(o,m); a = o & b = o by Th3; hence thesis; end; theorem Th5: for f being Morphism of c1Cat(o,m) holds f = m proof let f be Morphism of c1Cat(o,m); c1Cat(o,m) = ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def8; hence thesis by TARSKI:def 1; end; theorem Th6: for f,g being Morphism of c1Cat(o,m) holds f = g proof let f,g be Morphism of c1Cat(o,m); f = m & g = m by Th5; hence thesis; end; theorem Th7: for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m) holds f in Hom(a,b) proof let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m); dom f = o & cod f = o by Th3; then dom f = a & cod f = b by Th3; hence f in Hom(a,b) by CAT_1:18; end; theorem for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m) holds f is Morphism of a,b proof let a,b be Object of c1Cat(o,m), f be Morphism of c1Cat(o,m); f in Hom(a,b) by Th7; hence thesis by CAT_1:def 7; end; theorem for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {} by Th7; theorem Th10: for a being Object of c1Cat(o,m) holds a is terminal proof let a be Object of c1Cat(o,m); let b be Object of c1Cat(o,m); thus Hom(b,a)<>{} by Th7; consider f being Morphism of b,a; take f; thus thesis by Th6; end; theorem Th11: for c being Object of c1Cat(o,m), p1,p2 being Morphism of c1Cat(o,m) holds c is_a_product_wrt p1,p2 proof let c be Object of c1Cat(o,m), p1,p2 be Morphism of c1Cat(o,m); thus dom p1 = c & dom p2 = c by Th4; let d be Object of c1Cat(o,m),f,g be Morphism of c1Cat(o,m) such that f in Hom(d,cod p1) & g in Hom(d,cod p2); take h = p1; thus h in Hom(d,c) by Th7; thus thesis by Th6; end; definition let IT be Category-like ProdCatStr; attr IT is Cartesian means :Def9: the TerminalObj of IT is terminal & for a,b being Object of IT holds cod((the Proj1 of IT).[a,b]) = a & cod((the Proj2 of IT).[a,b]) = b & (the CatProd of IT).[a,b] is_a_product_wrt (the Proj1 of IT).[a,b],(the Proj2 of IT).[a,b]; end; theorem Th12: for o,m being set holds c1Cat(o,m) is Cartesian proof let o,m be set; set 1PCat = c1Cat(o,m); thus the TerminalObj of 1PCat is terminal by Th10; let a,b be Object of 1PCat; thus cod((the Proj1 of 1PCat).[a,b]) = a by Th4; thus cod((the Proj2 of 1PCat).[a,b]) = b by Th4; thus (the CatProd of 1PCat).[a,b] is_a_product_wrt (the Proj1 of 1PCat).[a,b],(the Proj2 of 1PCat).[a,b] by Th11; end; definition cluster strict Cartesian (Category-like ProdCatStr); existence proof c1Cat(0,1) is Cartesian by Th12; hence thesis; end; end; definition mode Cartesian_category is Cartesian (Category-like ProdCatStr); end; reserve C for Cartesian_category; reserve a,b,c,d,e,s for Object of C; theorem Th13: [1]C is terminal proof [1]C = the TerminalObj of C by Def4; hence thesis by Def9; end; theorem Th14: for f1,f2 being Morphism of a,[1]C holds f1 = f2 proof let f1,f2 be Morphism of a,[1]C; [1]C is terminal by Th13; then consider f being Morphism of a,[1]C such that A1: for g being Morphism of a,[1]C holds f = g by CAT_1:def 15; thus f1 = f by A1 .= f2 by A1; end; theorem Th15: Hom(a,[1]C) <> {} proof [1]C is terminal by Th13; hence thesis by CAT_1:def 15; end; definition let C,a; func term(a) -> Morphism of a,[1]C means not contradiction; existence; uniqueness by Th14; end; theorem Th16: term a = term(a,[1]C) proof [1]C is terminal by Th13; hence thesis by CAT_3:41; end; theorem dom(term a) = a & cod(term a) = [1]C proof [1]C is terminal & term a = term(a,[1]C) by Th13,Th16; hence thesis by CAT_3:39; end; theorem Hom(a,[1]C) = {term a} proof A1: Hom(a,[1]C) <> {} by Th15; for f2 being Morphism of a,[1]C holds term a = f2 by Th14; hence thesis by A1,CAT_1:26; end; theorem Th19: dom pr1(a,b) = a[x]b & cod pr1(a,b) = a proof set p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b]; (the CatProd of C).[a,b] is_a_product_wrt p1,p2 by Def9; then a[x]b is_a_product_wrt p1,p2 by Def5; then dom p1 = a[x]b & cod p1 = a by Def9,CAT_3:def 16; hence thesis by Def6; end; theorem Th20: dom pr2(a,b) = a[x]b & cod pr2(a,b) = b proof set p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b]; (the CatProd of C).[a,b] is_a_product_wrt p1,p2 by Def9; then a[x]b is_a_product_wrt p1,p2 by Def5; then dom p2 = a[x]b & cod p2 = b by Def9,CAT_3:def 16; hence thesis by Def7; end; definition let C,a,b; redefine func pr1(a,b) -> Morphism of a[x]b,a; coherence proof dom pr1(a,b) = a[x]b & cod pr1(a,b) = a by Th19; hence thesis by CAT_1:22; end; func pr2(a,b) -> Morphism of a[x]b,b; coherence proof dom pr2(a,b) = a[x]b & cod pr2(a,b) = b by Th20; hence thesis by CAT_1:22; end; end; theorem Th21: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} proof set c = (the CatProd of C).[a,b], p1 = (the Proj1 of C).[a,b], p2 = (the Proj2 of C).[a,b]; c is_a_product_wrt p1,p2 by Def9; then dom p1 = c & dom p2 = c & cod(p1) = a & cod(p2) = b by Def9,CAT_3:def 16 ; then Hom(c,a) <> {} & Hom(c,b) <> {} by CAT_1:18; hence thesis by Def5; end; theorem Th22: a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) proof (the CatProd of C).[a,b] = a[x]b & (the Proj1 of C).[a,b] = pr1(a,b) & (the Proj2 of C).[a,b] = pr2(a,b) by Def5,Def6,Def7; hence thesis by Def9; end; theorem C has_finite_product proof A1: [1]C is terminal by Th13; for a,b ex c being Object of C, p1,p2 being Morphism of C st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 proof let a,b; take a[x]b, pr1(a,b), pr2(a,b); thus thesis by Th19,Th20,Th22; end; hence thesis by A1,Th1; end; theorem Hom(a,b) <> {} & Hom(b,a) <> {} implies pr1(a,b) is retraction & pr2(a,b) is retraction proof a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) & cod pr1(a,b) = a & cod pr2(a,b) = b by Th19,Th20,Th22; hence thesis by CAT_3:62; end; definition let C,a,b,c; let f be Morphism of c,a, g be Morphism of c,b; assume A1: Hom(c,a) <> {} & Hom(c,b) <> {}; func <:f,g:> -> Morphism of c,a[x]b means :Def11: pr1(a,b)*it = f & pr2(a,b)*it = g; existence proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} & a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22; then consider h being Morphism of c,a[x]b such that A2: for h1 being Morphism of c,a[x]b holds pr1(a,b)*h1 = f & pr2(a,b)*h1 = g iff h = h1 by A1,CAT_3:60; take h; thus thesis by A2; end; uniqueness proof let h1,h2 be Morphism of c,a[x]b such that A3: pr1(a,b)*h1 = f & pr2(a,b)*h1 = g and A4: pr1(a,b)*h2 = f & pr2(a,b)*h2 = g; Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} & a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22; then consider h being Morphism of c,a[x]b such that A5: for h1 being Morphism of c,a[x]b holds pr1(a,b)*h1 = f & pr2(a,b)*h1 = g iff h = h1 by A1,CAT_3:60; h1 = h & h2 = h by A3,A4,A5; hence thesis; end; end; theorem Th25: Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {} proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} & a[x]b is_a_product_wrt pr1(a,b),pr2(a,b) by Th21,Th22; hence thesis by CAT_3:60; end; theorem Th26: <:pr1(a,b),pr2(a,b):> = id(a[x]b) proof A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21; then pr1(a,b)*(id(a[x]b)) = pr1(a,b) & pr2(a,b)*(id(a[x]b)) = pr2(a,b) by CAT_1:58; hence thesis by A1,Def11; end; theorem Th27: for f being Morphism of c,a, g being Morphism of c,b, h being Morphism of d,c st Hom(c,a)<>{} & Hom(c,b)<>{} & Hom(d,c)<>{} holds <:f*h,g*h:> = <:f,g:>*h proof let f be Morphism of c,a, g be Morphism of c,b, h be Morphism of d,c; assume that A1: Hom(c,a)<>{} and A2: Hom(c,b)<>{} and A3: Hom(d,c)<>{}; Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} & Hom(c,a[x]b) <> {} & (pr1(a,b)*<:f,g:>)*h = f*h & (pr2(a,b)*<:f,g:>)*h = g*h by A1,A2,Def11,Th21,Th25; then pr1(a,b)*(<:f,g:>*h) = f*h & pr2(a,b)*(<:f,g:>*h) = g*h & Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A3,CAT_1:52,54; hence thesis by Def11; end; theorem Th28: for f,k being Morphism of c,a, g,h being Morphism of c,b st Hom(c,a) <> {} & Hom(c,b) <> {} & <:f,g:> = <:k,h:> holds f = k & g = h proof let f,k be Morphism of c,a, g,h be Morphism of c,b; assume Hom(c,a) <> {} & Hom(c,b) <> {}; then pr1(a,b)*<:f,g:> = f & pr1(a,b)*<:k,h:> = k & pr2(a,b)*<:f,g:> = g & pr2(a,b)*<:k,h:> = h by Def11; hence thesis; end; theorem for f being Morphism of c,a, g being Morphism of c,b st Hom(c,a) <> {} & Hom(c,b) <> {} & (f is monic or g is monic) holds <:f,g:> is monic proof let f be Morphism of c,a, g be Morphism of c,b; assume that A1: Hom(c,a) <> {} and A2: Hom(c,b) <> {} and A3: f is monic or g is monic; A4: now assume A5: f is monic; let d; let f1,f2 be Morphism of d,c such that A6: Hom(d,c)<>{} and A7: <:f,g:>*f1 = <:f,g:>*f2; <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 & Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A6,Th27,CAT_1:52; then f*f1 = f*f2 by A7,Th28; hence f1 = f2 by A1,A5,A6,CAT_1:60; end; A8: Hom(c,a[x]b) <> {} by A1,A2,Th25; now assume A9: g is monic; let d be Object of C, f1,f2 be Morphism of d,c such that A10: Hom(d,c)<>{} and A11: <:f,g:>*f1 = <:f,g:>*f2; <:f*f1,g*f1:> = <:f,g:>*f1 & <:f*f2,g*f2:> = <:f,g:>*f2 & Hom(d,a) <> {} & Hom(d,b) <> {} by A1,A2,A10,Th27,CAT_1:52; then g*f1 = g*f2 by A11,Th28; hence f1 = f2 by A2,A9,A10,CAT_1:60; end; hence thesis by A3,A4,A8,CAT_1:60; end; theorem Th30: Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {} proof Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th15,CAT_1:56; hence thesis by Th25; end; definition let C,a; func lambda(a) -> Morphism of [1]C[x]a,a equals :Def12: pr2([1]C,a); correctness; func lambda'(a) -> Morphism of a,[1]C[x]a equals :Def13: <:term a,id a:>; correctness; func rho(a) -> Morphism of a[x][1]C,a equals :Def14: pr1(a,[1]C); correctness; func rho'(a) -> Morphism of a,a[x][1]C equals :Def15: <:id a,term a:>; correctness; end; theorem Th31: lambda(a)*lambda'(a) = id a & lambda'(a)*lambda(a) = id([1]C[x]a) & rho(a)*rho'(a) = id a & rho'(a)*rho(a) = id(a[x][1]C) proof A1: Hom(a,[1]C) <> {} & Hom(a,a) <> {} by Th15,CAT_1:56; A2: Hom([1]C[x]a,a) <> {} by Th21; then (id a)*pr2([1]C,a) = pr2([1]C,a) & (term a)*pr2([1]C,a) = pr1([1]C,a) & Hom([1]C[x]a,[1]C)<>{} by Th14,Th21,CAT_1:57; then A3:<:term a,id a:>*pr2([1]C,a) = <:pr1([1]C,a),pr2([1]C,a):> by A1,A2, Th27; pr2([1]C,a)*<:term a,id a:> = id a by A1,Def11; hence id a = lambda(a)*<:term a,id a:> by Def12 .= lambda(a)*lambda'(a) by Def13; <:term a,id a:>*pr2([1]C,a) = id([1]C[x]a) by A3,Th26; hence id([1]C[x]a) = <:term a,id a:>*lambda(a) by Def12 .= lambda'(a)*lambda(a) by Def13; A4: Hom(a[x][1]C,a) <> {} by Th21; then (id a)*pr1(a,[1]C) = pr1(a,[1]C) & (term a)*pr1(a,[1]C) = pr2(a,[1]C) & Hom(a[x][1]C,[1]C)<>{} by Th14,Th21,CAT_1:57; then A5: <:id a,term a:>*pr1(a,[1]C) = <:pr1(a,[1]C),pr2(a,[1]C):> by A1,A4, Th27; pr1(a,[1]C)*<:id a,term a:> = id a by A1,Def11; hence id a = rho(a)*<:id a,term a:> by Def14 .= rho(a)*rho'(a) by Def15; <:id a,term a:>*pr1(a,[1]C) = id(a[x][1]C) by A5,Th26; hence id(a[x][1]C) = <:id a,term a:>*rho(a) by Def14 .= rho'(a)*rho(a) by Def15; end; theorem a, a[x][1]C are_isomorphic & a,[1]C[x]a are_isomorphic proof thus a,a[x][1]C are_isomorphic proof thus Hom(a,a[x][1]C) <> {} & Hom(a[x][1]C,a) <> {} by Th21,Th30; take rho'(a), rho(a); thus thesis by Th31; end; thus Hom(a,[1]C[x]a) <> {} & Hom([1]C[x]a,a) <> {} by Th21,Th30; take lambda'(a), lambda(a); thus thesis by Th31; end; definition let C,a,b; func Switch(a,b) -> Morphism of a[x]b,b[x]a equals :Def16: <:pr2(a,b),pr1(a,b):>; correctness; end; theorem Th33: Hom(a[x]b,b[x]a)<>{} proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21; hence thesis by Th25; end; theorem Th34: Switch(a,b)*Switch(b,a) = id(b[x]a) proof A1: Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21; A2: Hom(b[x]a,b) <> {} & Hom(b[x]a,a) <> {} by Th21; then A3: Hom(b[x]a,a[x]b)<>{} by Th25; thus Switch(a,b)*Switch(b,a) = <:pr2(a,b),pr1(a,b):>*Switch(b,a) by Def16 .= <:pr2(a,b),pr1(a,b):>*<:pr2(b,a),pr1(b,a):> by Def16 .= <:pr2(a,b)*<:pr2(b,a),pr1(b,a):>,pr1(a,b)*<:pr2(b,a),pr1(b,a):>:> by A1,A3,Th27 .= <:pr1(b,a),pr1(a,b)*<:pr2(b,a),pr1(b,a):>:> by A2,Def11 .= <:pr1(b,a),pr2(b,a):> by A2,Def11 .= id(b[x]a) by Th26; end; theorem a[x]b,b[x]a are_isomorphic proof thus Hom(a[x]b,b[x]a)<>{} & Hom(b[x]a,a[x]b)<>{} by Th33; take Switch(a,b), Switch(b,a); thus thesis by Th34; end; definition let C,a; func Delta a -> Morphism of a,a[x]a equals :Def17: <:id a,id a:>; correctness; end; theorem Hom(a,a[x]a) <> {} proof Hom(a,a) <> {} by CAT_1:56; hence thesis by Th25; end; theorem for f being Morphism of a,b st Hom(a,b) <> {} holds <:f,f:> = Delta(b)*f proof let f be Morphism of a,b such that A1: Hom(a,b) <> {}; A2: Hom(b,b) <> {} by CAT_1:56; (id b)*f = f by A1,CAT_1:57; hence <:f,f:> = <:id b, id b:>*f by A1,A2,Th27 .= Delta(b)*f by Def17; end; definition let C,a,b,c; func Alpha(a,b,c) -> Morphism of (a[x]b)[x]c,a[x](b[x]c) equals :Def18: <:pr1(a,b)*pr1(a[x]b,c),<:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>:>; correctness; func Alpha'(a,b,c) -> Morphism of a[x](b[x]c),(a[x]b)[x]c equals :Def19: <:<:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>; correctness; end; theorem Th38: Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} proof A1: Hom(a[x]b,a) <> {} by Th21; A2: Hom((a[x]b)[x]c,a[x]b) <> {} by Th21; then A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:52; Hom(a[x]b,b) <> {} by Th21; then A4: Hom((a[x]b)[x]c,b) <> {} by A2,CAT_1:52; Hom((a[x]b)[x]c,c) <> {} by Th21; then Hom((a[x]b)[x]c,b[x]c) <> {} by A4,Th25; hence Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by A3,Th25; A5: Hom(b[x]c,b) <> {} by Th21; A6: Hom(a[x](b[x]c),b[x]c) <> {} by Th21; then A7: Hom(a[x](b[x]c),b) <> {} by A5,CAT_1:52; Hom(b[x]c,c) <> {} by Th21; then A8: Hom(a[x](b[x]c),c) <> {} by A6,CAT_1:52; Hom(a[x](b[x]c),a) <> {} by Th21; then Hom(a[x](b[x]c),a[x]b) <> {} by A7,Th25; hence Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by A8,Th25; end; theorem Th39: Alpha(a,b,c)*Alpha'(a,b,c) = id(a[x](b[x]c)) & Alpha'(a,b,c)*Alpha(a,b,c) = id((a[x]b)[x]c) proof A1: Hom(a[x]b,a) <> {} by Th21; A2: Hom((a[x]b)[x]c,a[x]b) <> {} by Th21; then A3: Hom((a[x]b)[x]c,a) <> {} by A1,CAT_1:52; A4: Hom(a[x]b,b) <> {} by Th21; then A5: Hom((a[x]b)[x]c,b) <> {} by A2,CAT_1:52; A6: Hom((a[x]b)[x]c,c) <> {} by Th21; then A7: Hom((a[x]b)[x]c,b[x]c) <> {} by A5,Th25; A8: Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} by Th38; A9: Hom(b[x]c,b) <> {} by Th21; A10: Hom(a[x](b[x]c),b[x]c) <> {} by Th21; then A11: Hom(a[x](b[x]c),b) <> {} by A9,CAT_1:52; A12: Hom(b[x]c,c) <> {} by Th21; then A13: Hom(a[x](b[x]c),c) <> {} by A10,CAT_1:52; A14: Hom(a[x](b[x]c),a) <> {} by Th21; then A15: Hom(a[x](b[x]c),a[x]b) <> {} by A11,Th25; A16: Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by Th38; set k = <:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>; set l = <:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>; set f = <:pr1(a,b)*pr1(a[x]b,c),k:>; set g = <:l,pr2(b,c)*pr2(a,b[x]c):>; A17: pr1(a,b)*pr1(a[x]b,c)*g = pr1(a,b)*(pr1(a[x]b,c)*g) by A1,A2,A16,CAT_1:54 .= pr1(a,b)*l by A13,A15,Def11 .= pr1(a,b[x]c) by A11,A14,Def11; pr2(a,b)*pr1(a[x]b,c)*g = pr2(a,b)*(pr1(a[x]b,c)*g) by A2,A4,A16,CAT_1:54 .= pr2(a,b)*l by A13,A15,Def11 .= pr1(b,c)*pr2(a,b[x]c) by A11,A14,Def11; then A18: k*g = <:pr1(b,c)*pr2(a,b[x]c),pr2(a[x]b,c)*g:> by A5,A6,A16,Th27 .= <:pr1(b,c)*pr2(a,b[x]c),pr2(b,c)*pr2(a,b[x]c):> by A13,A15,Def11 .= <:pr1(b,c),pr2(b,c):>*pr2(a,b[x]c) by A9,A10,A12,Th27 .= id(b[x]c)*pr2(a,b[x]c) by Th26 .= pr2(a,b[x]c) by A10,CAT_1:57; thus Alpha(a,b,c)*Alpha'(a,b,c) = Alpha(a,b,c)*g by Def19 .= f*g by Def18 .= <:pr1(a,b[x]c),pr2(a,b[x]c):> by A3,A7,A16,A17,A18,Th27 .= id(a[x](b[x]c)) by Th26; pr1(b,c)*pr2(a,b[x]c)*f = pr1(b,c)*(pr2(a,b[x]c)*f) by A8,A9,A10,CAT_1:54 .= pr1(b,c)*k by A3,A7,Def11 .= pr2(a,b)*pr1(a[x]b,c) by A5,A6,Def11; then A19: l*f = <:pr1(a,b[x]c)*f,pr2(a,b)*pr1(a[x]b,c):> by A8,A11,A14,Th27 .= <:pr1(a,b)*pr1(a[x]b,c),pr2(a,b)*pr1(a[x]b,c):> by A3,A7,Def11 .= <:pr1(a,b),pr2(a,b):>*pr1(a[x]b,c) by A1,A2,A4,Th27 .= id(a[x]b)*pr1(a[x]b,c) by Th26 .= pr1(a[x]b,c) by A2,CAT_1:57; A20: pr2(b,c)*pr2(a,b[x]c)*f = pr2(b,c)*(pr2(a,b[x]c)*f) by A8,A10,A12,CAT_1:54 .= pr2(b,c)*k by A3,A7,Def11 .= pr2(a[x]b,c) by A5,A6,Def11; thus Alpha'(a,b,c)*Alpha(a,b,c) = Alpha'(a,b,c)*f by Def18 .= g*f by Def19 .= <:pr1(a[x]b,c),pr2(a[x]b,c):> by A8,A13,A15,A19,A20,Th27 .= id((a[x]b)[x]c) by Th26; end; theorem (a[x]b)[x]c,a[x](b[x]c) are_isomorphic proof thus Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {} by Th38; take Alpha(a,b,c), Alpha'(a,b,c); thus thesis by Th39; end; definition let C,a,b,c,d; let f be Morphism of a,b, g be Morphism of c,d; func f[x]g -> Morphism of a[x]c,b[x]d equals :Def20: <:f*pr1(a,c),g*pr2(a,c):>; correctness; end; theorem Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a[x]b,c[x]d) <> {} proof assume A1: Hom(a,c) <> {} & Hom(b,d) <> {}; Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21; then Hom(a[x]b,c) <> {} & Hom(a[x]b,d) <> {} by A1,CAT_1:52; hence thesis by Th25; end; theorem (id a)[x](id b) = id(a[x]b) proof Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {} by Th21; then (id a)*pr1(a,b) = pr1(a,b) & (id b)*pr2(a,b) = pr2(a,b) by CAT_1:57; then (id a)[x](id b) = <:pr1(a,b),pr2(a,b):> by Def20; hence thesis by Th26; end; theorem Th43: for f being Morphism of a,b, h being Morphism of c,d, g being Morphism of e,a, k being Morphism of e,c st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(e,c) <> {} holds (f[x]h)*<:g,k:> = <:f*g,h*k:> proof let f be Morphism of a,b, h be Morphism of c,d; let g be Morphism of e,a, k be Morphism of e,c; assume that A1: Hom(a,b) <> {} and A2: Hom(c,d) <> {} and A3: Hom(e,a) <> {} and A4: Hom(e,c) <> {}; A5: Hom(e,a[x]c) <> {} by A3,A4,Th25; Hom(a[x]c,a) <> {} & Hom(a[x]c,c) <> {} & pr1(a,c)*<:g,k:> = g & pr2(a,c)*<:g,k:> = k by A3,A4,Def11,Th21; then Hom(a[x]c,b) <> {} & Hom(a[x]c,d) <> {} & f*g = (f*pr1(a,c))*<:g,k:> & h*k = (h*pr2(a,c))*<:g,k:> by A1,A2,A5,CAT_1:52,54; then <:f*g,h*k:> = <:f*pr1(a,c),h*pr2(a,c):>*<:g,k:> by A5,Th27; hence thesis by Def20; end; theorem for f being Morphism of c,a, g being Morphism of c,b st Hom(c,a) <> {} & Hom(c,b) <> {} holds <:f,g:> = (f[x]g)*Delta(c) proof let f be Morphism of c,a, g be Morphism of c,b such that A1: Hom(c,a) <> {} and A2: Hom(c,b) <> {}; A3: Hom(c,c) <> {} by CAT_1:56; thus (f[x]g)*Delta(c) = (f[x]g)*<:id c,id c:> by Def17 .= <:f*(id c),g*(id c):> by A1,A2,A3,Th43 .= <:f,g*(id c):> by A1,CAT_1:58 .= <:f,g:> by A2,CAT_1:58; end; theorem for f being Morphism of a,b, h being Morphism of c,d, g being Morphism of e,a, k being Morphism of s,c st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(s,c) <> {} holds (f[x]h)*(g[x]k) = (f*g)[x](h*k) proof let f be Morphism of a,b, h be Morphism of c,d; let g be Morphism of e,a, k be Morphism of s,c; assume that A1: Hom(a,b) <> {} and A2: Hom(c,d) <> {} and A3: Hom(e,a) <> {} and A4: Hom(s,c) <> {}; A5: Hom(e[x]s,e) <> {} & Hom(e[x]s,s) <> {} by Th21; then f*(g*pr1(e,s)) = (f*g)*pr1(e,s) & h*(k*pr2(e,s)) = (h*k)*pr2(e,s) by A1,A2,A3,A4,CAT_1:54; then Hom(e[x]s,a) <> {} & Hom(e[x]s,c) <> {} & (f*g)[x](h*k) = <:f*(g*pr1(e,s)),h*(k*pr2(e,s)):> & g[x]k = <:g*pr1(e,s),k*pr2(e,s):> by A3,A4,A5,Def20,CAT_1:52; hence thesis by A1,A2,Th43; end; begin :: Categories with Finite Coproducts definition let C be Category; attr C is with_finite_coproduct means for I being finite set, F being Function of I,the Objects of C ex a being Object of C, F' being Injections_family of a,I st doms F' = F & a is_a_coproduct_wrt F'; synonym C has_finite_coproduct; end; theorem Th46: for C being Category holds C has_finite_coproduct iff (ex a being Object of C st a is initial) & for a,b being Object of C ex c being Object of C, i1,i2 being Morphism of C st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 proof let C be Category; thus C has_finite_coproduct implies (ex a being Object of C st a is initial) & for a,b being Object of C ex c being Object of C, i1,i2 being Morphism of C st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 proof assume A1: for I being finite set, F being Function of I,the Objects of C ex a being Object of C, F' being Injections_family of a,I st doms F' = F & a is_a_coproduct_wrt F'; reconsider F = {} as Function of {},the Objects of C by FUNCT_2:55,RELAT_1: 60; consider a being Object of C, F' being Injections_family of a,{} such that doms F' = F and A2: a is_a_coproduct_wrt F' by A1; a is initial by A2,CAT_3:81; hence ex a being Object of C st a is initial; let a,b be Object of C; set F = (0,1)-->(a,b); consider c being Object of C, F' being Injections_family of c,{0,1} such that A3: doms F' = F and A4: c is_a_coproduct_wrt F' by A1; take c, i1 = F'/.0, i2 = F'/.1; A5: 0 in {0,1} & 1 in {0,1} by TARSKI:def 2; F/.0 = a & F/.1 = b by CAT_3:7; hence dom i1 = a & dom i2 = b by A3,A5,CAT_3:def 3; thus cod i1 = c & cod i2 = c by A5,CAT_3:67; A6: dom F' = {0,1} by FUNCT_2:def 1; i1 = F'.0 & i2 = F'.1 by A5,CAT_3:def 1; then 0 <> 1 & F' = (0,1)-->(i1,i2) by A6,FUNCT_4:69; hence c is_a_coproduct_wrt i1,i2 by A4,CAT_3:85; end; given a being Object of C such that A7: a is initial; assume A8: for a,b being Object of C ex c being Object of C, i1,i2 being Morphism of C st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2; defpred Q[Nat] means for I being finite set, F being Function of I,the Objects of C st card I = $1 ex a being Object of C, F' being Injections_family of a,I st doms F' = F & a is_a_coproduct_wrt F'; A9: Q[ 0 ] proof let I be finite set, F be Function of I,the Objects of C; assume A10: card I = 0; then A11: I = {} by CARD_2:59; {} is Function of {}, the Morphisms of C by FUNCT_2:55,RELAT_1:60; then reconsider F' = {} as Injections_family of a,I by A11,CAT_3:68; take a,F'; for x being set st x in I holds (doms F')/.x = F/.x by A10,CARD_2:59; hence doms F' = F by CAT_3:1; thus thesis by A7,A11,CAT_3:81; end; A12: for n being Nat st Q[n] holds Q[n+1] proof let n be Nat such that A13: Q[n]; let I be finite set, F be Function of I,the Objects of C such that A14: card I = n+1; consider x being Element of I; reconsider Ix = I \ {x} as finite set; A15: {x} c= I by A14,CARD_1:47,ZFMISC_1:37; reconsider sx = {x} as finite set; A16: card(Ix) = card(I) - card(sx) by A15,CARD_2:63 .= card(I) - 1 by CARD_1:79 .= n by A14,XCMPLX_1:26; A17: I\{x} c= I & the Objects of C <> {} by XBOOLE_1:36; then reconsider G = F|(I\{x}) as Function of I\{x},the Objects of C by FUNCT_2:38; consider a being Object of C, G' being Injections_family of a,I\{x} such that A18: doms G' = G and A19: a is_a_coproduct_wrt G' by A13,A16; set b = F/.x; consider c being Object of C, i1,i2 being Morphism of C such that A20: dom i1 = a & dom i2 = b and A21: cod i1 = c & cod i2 = c and A22: c is_a_coproduct_wrt i1,i2 by A8; set F' = (i1*G') +* ({x} -->i2); A23: dom(i1*G') = I\{x} & dom({x} -->i2) = {x} by FUNCT_2:def 1; then A24: dom(i1*G') \/ dom({x} -->i2) = I \/ {x} by XBOOLE_1:39 .= I by A14,CARD_1:47,ZFMISC_1:46; then A25: dom F' = I by FUNCT_4:def 1; A26: rng F' c= rng(i1*G') \/ rng({x} -->i2) by FUNCT_4:18; rng(i1*G') c= the Morphisms of C & rng({x} -->i2) c= the Morphisms of C by RELSET_1:12; then rng(i1*G') \/ rng({x} -->i2) c= the Morphisms of C by XBOOLE_1:8; then rng F' c= the Morphisms of C by A26,XBOOLE_1:1; then reconsider F' as Function of I, the Morphisms of C by A25,FUNCT_2:def 1,RELSET_1:11; A27: cods G' = (I\{x})-->a by CAT_3:def 17; now let y be set; assume A28: y in I; now per cases; suppose y = x; then A29: y in {x} by TARSKI:def 1; F'/.y = F'.y by A28,CAT_3:def 1 .= ({x} -->i2).y by A23,A29,FUNCT_4:14 .= i2 by A29,FUNCOP_1:13; hence (I --> c).y = cod(F'/.y) by A21,A28,FUNCOP_1:13 .= (cods F')/.y by A28,CAT_3:def 4; suppose A30: y <> x; then A31: not y in {x} by TARSKI:def 1; A32: y in I\{x} by A28,A30,ZFMISC_1:64; F'/.y = F'.y by A28,CAT_3:def 1 .= (i1*G').y by A23,A24,A28,A31,FUNCT_4:def 1 .= (i1*G')/.y by A32,CAT_3:def 1; hence (cods F')/.y = cod((i1*G')/.y) by A28,CAT_3:def 4 .= (cods(i1*G'))/.y by A32,CAT_3:def 4 .= ((I\{x})-->c)/.y by A20,A21,A27,CAT_3:21 .= c by A32,CAT_3:2 .= (I --> c).y by A28,FUNCOP_1:13; end; hence (cods F').y = (I --> c).y by A28,CAT_3:def 1; end; then cods F' = I --> c by FUNCT_2:18; then reconsider F' as Injections_family of c,I by CAT_3:def 17; take c,F'; now let y be set; assume A33: y in I; now per cases; suppose A34: y = x; then A35: y in {x} by TARSKI:def 1; F'/.y = F'.y by A33,CAT_3:def 1 .= ({x} -->i2).y by A23,A35,FUNCT_4:14 .= i2 by A35,FUNCOP_1:13; hence (doms F')/.y = F/.y by A20,A33,A34,CAT_3:def 3; suppose A36: y <> x; then A37: not y in {x} by TARSKI:def 1; A38: y in I\{x} by A33,A36,ZFMISC_1:64; F'/.y = F'.y by A33,CAT_3:def 1 .= (i1*G').y by A23,A24,A33,A37,FUNCT_4:def 1 .= (i1*G')/.y by A38,CAT_3:def 1; hence (doms F')/.y = dom((i1*G')/.y) by A33,CAT_3:def 3 .= (doms(i1*G'))/.y by A38,CAT_3:def 3 .= G/.y by A18,A20,A27,CAT_3:21 .= G.y by A38,CAT_3:def 1 .= F.y by A38,FUNCT_1:72 .= F/.y by A33,CAT_3:def 1; end; hence (doms F')/.y = F/.y; end; hence A39: doms F' = F by CAT_3:1; thus F' is Injections_family of c,I; let d be Object of C; let F'' be Injections_family of d,I such that A40: doms F' = doms F''; reconsider G'' = F''|(I\{x}) as Function of I\{x},the Morphisms of C by A17,FUNCT_2:38; now let y be set; assume A41: y in I\{x}; then A42: y in I by XBOOLE_0:def 4; G''/.y = G''.y by A41,CAT_3:def 1 .= F''.y by A41,FUNCT_1:72 .= F''/.y by A42,CAT_3:def 1; hence cods(G'')/.y = cod(F''/.y) by A41,CAT_3:def 4 .= d by A42,CAT_3:67 .= ((I\{x})-->d)/.y by A41,CAT_3:2; end; then cods G'' = I\{x} --> d by CAT_3:1; then reconsider G'' as Injections_family of d,I\{x} by CAT_3:def 17; now let y be set; assume A43: y in I\{x}; then A44: y in I by XBOOLE_0:def 4; then A45: F''/.y = F''.y by CAT_3:def 1 .= G''.y by A43,FUNCT_1:72 .= G''/.y by A43,CAT_3:def 1; G/.y = G.y by A43,CAT_3:def 1 .= F.y by A43,FUNCT_1:72 .= F/.y by A44,CAT_3:def 1; hence (doms G')/.y = dom(G''/.y) by A18,A39,A40,A44,A45,CAT_3:def 3 .= (doms G'')/.y by A43,CAT_3:def 3; end; then doms G' = doms G'' by CAT_3:1; then consider h' being Morphism of C such that A46: h' in Hom(a,d) and A47: for k being Morphism of C st k in Hom(a,d) holds (for y being set st y in I\{x} holds k*(G'/.y) = G''/.y) iff h' = k by A19,CAT_3:def 18; set g = F''/.x; A48: cod g = d by A14,CARD_1:47,CAT_3:67; A49: x in {x} by TARSKI:def 1; A50: F'/.x = F'.x by A14,CARD_1:47,CAT_3:def 1 .= ({x} -->i2).x by A23,A49,FUNCT_4:14 .= i2 by A49,FUNCOP_1:13; then dom i2 = (doms F')/.x by A14,CARD_1:47,CAT_3:def 3 .= dom g by A14,A40,CARD_1:47,CAT_3:def 3; then g in Hom(dom i2,d) by A48,CAT_1:18; then consider h being Morphism of C such that A51: h in Hom(c,d) and A52: for k being Morphism of C st k in Hom(c,d) holds k*i1 = h' & k*i2 = g iff h = k by A20,A22,A46,CAT_3:def 19; take h; thus h in Hom(c,d) by A51; let k be Morphism of C such that A53: k in Hom(c,d); thus (for y being set st y in I holds k*(F'/.y) = F''/.y) implies h = k proof assume A54: for y being set st y in I holds k*(F'/.y) = F''/.y; then A55: k*i2 = g by A14,A50,CARD_1:47; A56: cod k = d & dom k = c by A53,CAT_1:18; then cod(k*i1) = d & dom(k*i1) = a by A20,A21,CAT_1:42; then A57: k*i1 in Hom(a,d) by CAT_1:18; for y being set st y in I\{x} holds k*i1*(G'/.y) = G''/.y proof let y be set; assume A58: y in I\{x}; then A59: y in I & not y in {x} by XBOOLE_0:def 4; then A60: F'/.y = F'.y by CAT_3:def 1 .= (i1*G').y by A23,A24,A59,FUNCT_4:def 1 .= (i1*G')/.y by A58,CAT_3:def 1; cod(G'/.y) = a by A58,CAT_3:67; hence k*i1*(G'/.y) = k*(i1*(G'/.y)) by A20,A21,A56,CAT_1:43 .= k*((i1*G')/.y) by A58,CAT_3:def 8 .= F''/.y by A54,A59,A60 .= F''.y by A59,CAT_3:def 1 .= G''.y by A58,FUNCT_1:72 .= G''/.y by A58,CAT_3:def 1; end; then k*i1 = h' by A47,A57; hence h = k by A52,A53,A55; end; assume A61: h = k; let y be set such that A62: y in I; now per cases; suppose A63: y = x; then A64: y in {x} by TARSKI:def 1; F'/.y = F'.y by A62,CAT_3:def 1 .= ({x} -->i2).y by A23,A64,FUNCT_4:14 .= i2 by A64,FUNCOP_1:13; hence thesis by A52,A53,A61,A63; suppose A65: y <> x; then A66: not y in {x} by TARSKI:def 1; A67: y in I\{x} by A62,A65,ZFMISC_1:64; then A68: dom k = c & cod(G'/.y) = a by A53,CAT_1:18,CAT_3:67; F'/.y = F'.y by A62,CAT_3:def 1 .= (i1*G').y by A23,A24,A62,A66,FUNCT_4:def 1 .= (i1*G')/.y by A67,CAT_3:def 1 .= i1*(G'/.y) by A67,CAT_3:def 8; hence k*(F'/.y) = k*i1*(G'/.y) by A20,A21,A68,CAT_1:43 .= h'*(G'/.y) by A52,A53,A61 .= G''/.y by A46,A47,A67 .= G''.y by A67,CAT_3:def 1 .= F''.y by A67,FUNCT_1:72 .= F''/.y by A62,CAT_3:def 1; end; hence thesis; end; A69: for n being Nat holds Q[n] from Ind(A9,A12); let I be finite set, F be Function of I,the Objects of C; card I = card I; hence thesis by A69; end; definition struct (CatStr)CoprodCatStr (# Objects,Morphisms -> non empty set, Dom,Cod -> Function of the Morphisms, the Objects, Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms, Id -> Function of the Objects, the Morphisms, Initial -> Element of the Objects, Coproduct -> Function of [:the Objects,the Objects:],the Objects, Incl1,Incl2 -> Function of [:the Objects,the Objects:],the Morphisms #); end; definition let C be CoprodCatStr; func [0]C -> Object of C equals :Def22: the Initial of C; correctness; let a,b be Object of C; func a+b -> Object of C equals :Def23: (the Coproduct of C).[a,b]; correctness; func in1(a,b) -> Morphism of C equals :Def24: (the Incl1 of C).[a,b]; correctness; func in2(a,b) -> Morphism of C equals :Def25: (the Incl2 of C).[a,b]; correctness; end; definition let o,m; func c1Cat*(o,m) -> strict CoprodCatStr equals :Def26: CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #); correctness; end; theorem the CatStr of c1Cat*(o,m) = 1Cat(o,m) proof c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26; hence thesis by CAT_1:def 9; end; Lm2: c1Cat*(o,m) is Category-like proof set C = c1Cat*(o,m); A1: C = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26; set CP = the Comp of C, CD = the Dom of C, CC = the Cod of C, CI = the Id of C; thus for f,g being Morphism of C holds [g,f] in dom CP iff CD.g=CC.f proof let f,g be Morphism of C; f = m & g = m & dom CP = {[m,m]} by A1,CAT_1:7,TARSKI:def 1; hence thesis by A1,TARSKI:def 1; end; thus for f,g being Morphism of C st CD.g=CC.f holds CD.(CP.[g,f]) = CD.f & CC.(CP.[g,f]) = CC.g proof let f,g be Morphism of C; CP.[g,f] = m by A1,CAT_1:9; then reconsider gf = CP.[g,f] as Morphism of C by A1,TARSKI:def 1; CD.f = o & CC.g = o & CD.gf = o & CC.gf = o by A1,FUNCT_2:65; hence thesis; end; thus for f,g,h being Morphism of C st CD.h = CC.g & CD.g = CC.f holds CP.[h,CP.[g,f]] = CP.[CP.[h,g],f] proof let f,g,h be Morphism of C; CP.[g,f] = m & CP.[h,g] = m by A1,CAT_1:9; then reconsider gf = CP.[g,f],hg = CP.[h,g] as Morphism of C by A1,TARSKI:def 1; CP.[h,gf] = m & CP.[hg,f] = m by A1,CAT_1:9; hence thesis; end; let b be Object of C; b = o by A1,TARSKI:def 1; hence CD.(CI.b) = b & CC.(CI.b) = b by A1,FUNCT_2:65; thus for f being Morphism of C st CC.f = b holds CP.[CI.b,f] = f proof let f be Morphism of C; f = m by A1,TARSKI:def 1; hence thesis by A1,CAT_1:9; end; let g be Morphism of C; assume CD.g = b; g = m by A1,TARSKI:def 1; hence CP.[g,CI.b] = g by A1,CAT_1:9; end; definition cluster strict Category-like CoprodCatStr; existence proof c1Cat*(0,1) is Category-like by Lm2; hence thesis; end; end; definition let o,m be set; cluster c1Cat*(o,m) -> Category-like; coherence by Lm2; end; theorem Th48: for a being Object of c1Cat*(o,m) holds a = o proof let a be Object of c1Cat*(o,m); c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26; hence thesis by TARSKI:def 1; end; theorem Th49: for a,b being Object of c1Cat*(o,m) holds a = b proof let a,b be Object of c1Cat*(o,m); a = o & b = o by Th48; hence thesis; end; theorem Th50: for f being Morphism of c1Cat*(o,m) holds f = m proof let f be Morphism of c1Cat*(o,m); c1Cat*(o,m) = CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #) by Def26; hence thesis by TARSKI:def 1; end; theorem Th51: for f,g being Morphism of c1Cat*(o,m) holds f = g proof let f,g be Morphism of c1Cat*(o,m); f = m & g = m by Th50; hence thesis; end; theorem Th52: for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m) holds f in Hom(a,b) proof let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m); dom f = o & cod f = o by Th48; then dom f = a & cod f = b by Th48; hence f in Hom(a,b) by CAT_1:18; end; theorem for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m) holds f is Morphism of a,b proof let a,b be Object of c1Cat*(o,m), f be Morphism of c1Cat*(o,m); f in Hom(a,b) by Th52; hence thesis by CAT_1:def 7; end; theorem for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {} by Th52; theorem Th55: for a being Object of c1Cat*(o,m) holds a is initial proof let a be Object of c1Cat*(o,m); let b be Object of c1Cat*(o,m); thus Hom(a,b)<>{} by Th52; consider f being Morphism of a,b; take f; thus thesis by Th51; end; theorem Th56: for c being Object of c1Cat*(o,m), i1,i2 being Morphism of c1Cat*(o,m) holds c is_a_coproduct_wrt i1,i2 proof let c be Object of c1Cat*(o,m), i1,i2 be Morphism of c1Cat*(o,m); thus cod i1 = c & cod i2 = c by Th49; let d be Object of c1Cat*(o,m), f,g be Morphism of c1Cat*(o,m) such that f in Hom(dom i1,d) & g in Hom(dom i2,d); take h = i1; thus h in Hom(c,d) by Th52; thus thesis by Th51; end; definition let IT be Category-like CoprodCatStr; attr IT is Cocartesian means :Def27: the Initial of IT is initial & for a,b being Object of IT holds dom((the Incl1 of IT).[a,b]) = a & dom((the Incl2 of IT).[a,b]) = b & (the Coproduct of IT).[a,b] is_a_coproduct_wrt (the Incl1 of IT).[a,b],(the Incl2 of IT).[a,b]; end; theorem Th57: for o,m being set holds c1Cat*(o,m) is Cocartesian proof let o,m be set; set 1PCat = c1Cat*(o,m); thus the Initial of 1PCat is initial by Th55; let a,b be Object of 1PCat; thus dom((the Incl1 of 1PCat).[a,b]) = a by Th49; thus dom((the Incl2 of 1PCat).[a,b]) = b by Th49; thus (the Coproduct of 1PCat).[a,b] is_a_coproduct_wrt (the Incl1 of 1PCat).[a,b],(the Incl2 of 1PCat).[a,b] by Th56; end; definition cluster strict Cocartesian (Category-like CoprodCatStr); existence proof c1Cat*(0,1) is Cocartesian by Th57; hence thesis; end; end; definition mode Cocartesian_category is Cocartesian (Category-like CoprodCatStr); end; reserve C for Cocartesian_category; reserve a,b,c,d,e,s for Object of C; theorem Th58: [0]C is initial proof [0]C = the Initial of C by Def22; hence thesis by Def27; end; theorem Th59: for f1,f2 being Morphism of [0]C,a holds f1 = f2 proof let f1,f2 be Morphism of [0]C,a; [0]C is initial by Th58; then consider f being Morphism of [0]C,a such that A1: for g being Morphism of [0]C, a holds f = g by CAT_1:def 16; thus f1 = f by A1 .= f2 by A1; end; definition let C,a; func init a -> Morphism of [0]C, a means not contradiction; existence; uniqueness by Th59; end; theorem Th60: Hom([0]C,a) <> {} proof [0]C is initial by Th58; hence thesis by CAT_1:def 16; end; theorem Th61: init a = init([0]C,a) proof [0]C is initial by Th58; hence thesis by CAT_3:44; end; theorem dom(init a) = [0]C & cod(init a) = a proof [0]C is initial & init a = init([0]C,a) by Th58,Th61; hence thesis by CAT_3:42; end; theorem Hom([0]C,a) = {init a} proof A1: Hom([0]C,a) <> {} by Th60; for f2 being Morphism of [0]C,a holds init a = f2 by Th59; hence thesis by A1,CAT_1:26; end; theorem Th64: dom in1(a,b) = a & cod in1(a,b) = a+b proof set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b]; (the Coproduct of C).[a,b] is_a_coproduct_wrt i1,i2 by Def27; then a+b is_a_coproduct_wrt i1,i2 by Def23; then cod i1 = a+b & dom i1 = a by Def27,CAT_3:def 19; hence thesis by Def24; end; theorem Th65: dom in2(a,b) = b & cod in2(a,b) = a+b proof set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b]; (the Coproduct of C).[a,b] is_a_coproduct_wrt i1,i2 by Def27; then a+b is_a_coproduct_wrt i1,i2 by Def23; then cod i2 = a+b & dom i2 = b by Def27,CAT_3:def 19; hence thesis by Def25; end; theorem Th66: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} proof set c = (the Coproduct of C).[a,b]; set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b]; c is_a_coproduct_wrt i1,i2 by Def27; then cod i1 = c & cod i2 = c & dom(i1) = a & dom(i2) = b by Def27,CAT_3:def 19; then Hom(a,c) <> {} & Hom(b,c) <> {} by CAT_1:18; hence thesis by Def23; end; theorem Th67: a+b is_a_coproduct_wrt in1(a,b),in2(a,b) proof set i1 = (the Incl1 of C).[a,b], i2 = (the Incl2 of C).[a,b]; (the Coproduct of C).[a,b] = a+b & i1 = in1(a,b) & i2 = in2(a,b) by Def23,Def24,Def25; hence thesis by Def27; end; theorem C has_finite_coproduct proof A1: [0]C is initial by Th58; for a,b ex c being Object of C, i1,i2 being Morphism of C st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 proof let a,b; take a+b, in1(a,b), in2(a,b); thus thesis by Th64,Th65,Th67; end; hence thesis by A1,Th46; end; theorem Hom(a,b) <> {} & Hom(b,a) <> {} implies in1(a,b) is coretraction & in2(a,b) is coretraction proof a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & dom in1(a,b) = a & dom in2(a,b) = b by Th64,Th65,Th67; hence thesis by CAT_3:88; end; definition let C,a,b; redefine func in1(a,b) -> Morphism of a,a+b; coherence proof cod in1(a,b) = a+b & dom in1(a,b) = a by Th64; hence thesis by CAT_1:22; end; func in2(a,b) -> Morphism of b,a+b; coherence proof cod in2(a,b) = a+b & dom in2(a,b) = b by Th65; hence thesis by CAT_1:22; end; end; definition let C,a,b,c; let f be Morphism of a,c, g be Morphism of b,c; assume A1: Hom(a,c) <> {} & Hom(b,c) <> {}; func [$f,g$] -> Morphism of a+b,c means :Def29: it*in1(a,b) = f & it*in2(a,b) = g; existence proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} & a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Th66,Th67; then consider h being Morphism of a+b,c such that A2: for k being Morphism of a+b,c holds k*in1(a,b) = f & k*in2(a,b) = g iff h = k by A1,CAT_3:87; take h; thus thesis by A2; end; uniqueness proof let h1,h2 be Morphism of a+b,c such that A3: h1*in1(a,b) = f & h1*in2(a,b) = g and A4: h2*in1(a,b) = f & h2*in2(a,b) = g; a+b is_a_coproduct_wrt in1(a,b),in2(a,b) & Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66,Th67; then consider h being Morphism of a+b,c such that A5: for k being Morphism of a+b,c holds k*in1(a,b) = f & k*in2(a,b) = g iff h = k by A1,CAT_3:87; h1 = h & h2 = h by A3,A4,A5; hence thesis; end; end; theorem Th70: Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {} proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} & a+b is_a_coproduct_wrt in1(a,b),in2(a,b) by Th66,Th67; hence thesis by CAT_3:87; end; theorem Th71: [$in1(a,b),in2(a,b)$] = id(a+b) proof A1: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66; then (id(a+b))*in1(a,b) = in1(a,b) & (id(a+b))*in2(a,b) = in2(a,b) by CAT_1:57; hence thesis by A1,Def29; end; theorem Th72: for f being Morphism of a,c, g being Morphism of b,c, h being Morphism of c,d st Hom(a,c)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} holds [$h*f,h*g$] = h*[$f,g$] proof let f be Morphism of a,c, g be Morphism of b,c, h be Morphism of c,d; assume that A1: Hom(a,c)<>{} and A2: Hom(b,c)<>{} and A3: Hom(c,d)<>{}; Hom(a,a+b) <> {} & Hom(b,a+b) <> {} & Hom(a+b,c) <> {} & h*([$f,g$]*in1(a,b)) = h*f & h*([$f,g$]*in2(a,b)) = h*g by A1,A2,Def29,Th66,Th70; then h*[$f,g$]*in1(a,b) = h*f & h*[$f,g$]*in2(a,b) = h*g & Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A3,CAT_1:52,54; hence thesis by Def29; end; theorem Th73: for f,k being Morphism of a,c, g,h being Morphism of b,c st Hom(a,c) <> {} & Hom(b,c) <> {} & [$f,g$] = [$k,h$] holds f = k & g = h proof let f,k be Morphism of a,c, g,h be Morphism of b,c; assume Hom(a,c) <> {} & Hom(b,c) <> {}; then [$f,g$]*in1(a,b) = f & [$k,h$]*in1(a,b) = k & [$f,g$]*in2(a,b) = g & [$k,h$]*in2(a,b) = h by Def29; hence thesis; end; theorem for f being Morphism of a,c, g being Morphism of b,c st Hom(a,c) <> {} & Hom(b,c) <> {} & (f is epi or g is epi) holds [$f,g$] is epi proof let f be Morphism of a,c, g be Morphism of b,c; assume that A1: Hom(a,c) <> {} and A2: Hom(b,c) <> {} and A3: f is epi or g is epi; A4: now assume A5: f is epi; let d; let f1,f2 be Morphism of c,d such that A6: Hom(c,d)<>{} and A7: f1*[$f,g$] = f2*[$f,g$]; [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] & Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A6,Th72,CAT_1:52; then f1*f = f2*f by A7,Th73; hence f1 = f2 by A1,A5,A6,CAT_1:65; end; A8: Hom(a+b,c) <> {} by A1,A2,Th70; now assume A9: g is epi; let d be Object of C, f1,f2 be Morphism of c,d such that A10: Hom(c,d)<>{} and A11: f1*[$f,g$] = f2*[$f,g$]; [$f1*f,f1*g$] = f1*[$f,g$] & [$f2*f,f2*g$] = f2*[$f,g$] & Hom(a,d) <> {} & Hom(b,d) <> {} by A1,A2,A10,Th72,CAT_1:52; then f1*g = f2*g by A11,Th73; hence f1 = f2 by A2,A9,A10,CAT_1:65; end; hence thesis by A3,A4,A8,CAT_1:65; end; theorem a, a+[0]C are_isomorphic & a,[0]C+a are_isomorphic proof A1: Hom([0]C,a) <> {} & Hom(a,a) <> {} by Th60,CAT_1:56; thus a,a+[0]C are_isomorphic proof thus A2: Hom(a,a+[0]C) <> {} by Th66; thus Hom(a+[0]C,a) <> {} by A1,Th70; take g = in1(a,[0]C), f = [$id a,init a$]; in1(a,[0]C)*id(a) = in1(a,[0]C) & in1(a,[0]C)*init a = in2(a,[0]C) & Hom([0]C,a+[0]C)<>{} by A2,Th59,Th66,CAT_1:58; then g*f = [$in1(a,[0]C),in2(a,[0]C)$] by A1,A2,Th72; hence thesis by A1,Def29,Th71; end; thus A3: Hom(a,[0]C+a) <> {} by Th66; thus Hom([0]C+a,a) <> {} by A1,Th70; take g = in2([0]C,a), f = [$init a,id a$]; in2([0]C,a)*id(a) = in2([0]C,a) & in2([0]C,a)*init a = in1([0]C,a) & Hom([0]C,[0]C+a)<>{} by A3,Th59,Th66,CAT_1:58; then g*f = [$in1([0]C,a),in2([0]C,a)$] by A1,A3,Th72; hence thesis by A1,Def29,Th71; end; theorem a+b,b+a are_isomorphic proof A1: Hom(a,b+a) <> {} & Hom(b,b+a) <> {} by Th66; hence A2: Hom(a+b,b+a)<>{} by Th70; A3: Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66; hence A4: Hom(b+a,a+b)<>{} by Th70; take f' = [$in2(b,a),in1(b,a)$], f = [$in2(a,b),in1(a,b)$]; thus f'*f = [$f'*in2(a,b),f'*in1(a,b)$] by A2,A3,Th72 .= [$in1(b,a),f'*in1(a,b)$] by A1,Def29 .= [$in1(b,a),in2(b,a)$] by A1,Def29 .= id(b+a) by Th71; thus f*f' = [$f*in2(b,a),f*in1(b,a)$] by A1,A4,Th72 .= [$in1(a,b),f*in1(b,a)$] by A3,Def29 .= [$in1(a,b),in2(a,b)$] by A3,Def29 .= id(a+b) by Th71; end; theorem (a+b)+c,a+(b+c) are_isomorphic proof A1: Hom(b,b+c) <> {} by Th66; A2: Hom(b+c,a+(b+c)) <> {} by Th66; then A3: Hom(b,a+(b+c)) <> {} by A1,CAT_1:52; A4: Hom(c,b+c) <> {} by Th66; then A5: Hom(c,a+(b+c)) <> {} by A2,CAT_1:52; A6: Hom(a,a+(b+c)) <> {} by Th66; then A7: Hom(a+b,a+(b+c)) <> {} by A3,Th70; hence A8: Hom((a+b)+c,a+(b+c)) <> {} by A5,Th70; A9: Hom(a,a+b) <> {} by Th66; A10: Hom(a+b,(a+b)+c) <> {} by Th66; then A11: Hom(a,(a+b)+c) <> {} by A9,CAT_1:52; A12: Hom(b,a+b) <> {} by Th66; then A13: Hom(b,(a+b)+c) <> {} by A10,CAT_1:52; A14: Hom(c,(a+b)+c) <> {} by Th66; then A15: Hom(b+c,(a+b)+c) <> {} by A13,Th70; hence A16: Hom(a+(b+c),(a+b)+c) <> {} by A11,Th70; set k = [$in1(a+b,c)*in2(a,b),in2(a+b,c)$]; set l = [$in1(a,b+c),in2(a,b+c)*in1(b,c)$]; take g = [$l,in2(a,b+c)*in2(b,c)$]; take f = [$in1(a+b,c)*in1(a,b),k$]; now thus g*(in1(a+b,c)*in1(a,b)) = g*in1(a+b,c)*in1(a,b) by A8,A9,A10,CAT_1:54 .= l*in1(a,b) by A5,A7,Def29 .= in1(a,b+c) by A3,A6,Def29; g*(in1(a+b,c)*in2(a,b)) = (g*in1(a+b,c))*in2(a,b) by A8,A10,A12,CAT_1:54 .= l*in2(a,b) by A5,A7,Def29 .= in2(a,b+c)*in1(b,c) by A3,A6,Def29; hence g*k = [$in2(a,b+c)*in1(b,c),g*in2(a+b,c)$] by A8,A13,A14,Th72 .= [$in2(a,b+c)*in1(b,c),in2(a,b+c)*in2(b,c)$] by A5,A7,Def29 .= in2(a,b+c)*[$in1(b,c),in2(b,c)$] by A1,A2,A4,Th72 .= in2(a,b+c)*id(b+c) by Th71 .= in2(a,b+c) by A2,CAT_1:58; end; hence g*f = [$in1(a,b+c),in2(a,b+c)$] by A8,A11,A15,Th72 .= id(a+(b+c)) by Th71; now f*(in2(a,b+c)*in1(b,c)) = (f*in2(a,b+c))*in1(b,c) by A1,A2,A16,CAT_1:54 .= k*in1(b,c) by A11,A15,Def29 .= in1(a+b,c)*in2(a,b) by A13,A14,Def29; hence f*l = [$f*in1(a,b+c),in1(a+b,c)*in2(a,b)$] by A3,A6,A16,Th72 .= [$in1(a+b,c)*in1(a,b),in1(a+b,c)*in2(a,b)$] by A11,A15,Def29 .= in1(a+b,c)*[$in1(a,b),in2(a,b)$] by A9,A10,A12,Th72 .= in1(a+b,c)*id(a+b) by Th71 .= in1(a+b,c) by A10,CAT_1:58; thus f*(in2(a,b+c)*in2(b,c)) = (f*in2(a,b+c))*in2(b,c) by A2,A4,A16,CAT_1:54 .= k*in2(b,c) by A11,A15,Def29 .= in2(a+b,c) by A13,A14,Def29; end; hence f*g = [$in1(a+b,c),in2(a+b,c)$] by A5,A7,A16,Th72 .= id((a+b)+c) by Th71; end; definition let C,a; func nabla a -> Morphism of a+a,a equals :Def30: [$id a,id a$]; correctness; end; definition let C,a,b,c,d; let f be Morphism of a,c, g be Morphism of b,d; func f+g -> Morphism of a+b,c+d equals :Def31: [$in1(c,d)*f,in2(c,d)*g$]; correctness; end; theorem Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a+b,c+d) <> {} proof assume A1: Hom(a,c) <> {} & Hom(b,d) <> {}; Hom(c,c+d) <> {} & Hom(d,c+d) <> {} by Th66; then Hom(a,c+d) <> {} & Hom(b,c+d) <> {} by A1,CAT_1:52; hence thesis by Th70; end; theorem (id a)+(id b) = id(a+b) proof Hom(a,a+b) <> {} & Hom(b,a+b) <> {} by Th66; then in1(a,b)*(id a) = in1(a,b) & in2(a,b)*(id b) = in2(a,b) by CAT_1:58; then (id a)+(id b) = [$in1(a,b),in2(a,b)$] by Def31; hence thesis by Th71; end; theorem Th80: for f being Morphism of a,c, h being Morphism of b,d, g being Morphism of c,e, k being Morphism of d,e st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,e) <> {} holds [$g,k$]*(f+h) = [$g*f,k*h$] proof let f be Morphism of a,c, h be Morphism of b,d; let g be Morphism of c,e, k be Morphism of d,e; assume that A1: Hom(a,c) <> {} and A2: Hom(b,d) <> {} and A3: Hom(c,e) <> {} and A4: Hom(d,e) <> {}; A5: Hom(c+d,e) <> {} by A3,A4,Th70; Hom(c,c+d) <> {} & Hom(d,c+d) <> {} & [$g,k$]*in1(c,d) = g & [$g,k$]*in2(c,d) = k by A3,A4,Def29,Th66; then Hom(a,c+d) <> {} & Hom(b,c+d) <> {} & g*f = [$g,k$]*(in1(c,d)*f) & k*h = [$g,k$]*(in2(c,d)*h) by A1,A2,A5,CAT_1:52,54; then [$g*f,k*h$] = [$g,k$]*[$in1(c,d)*f,in2(c,d)*h$] by A5,Th72; hence thesis by Def31; end; theorem for f being Morphism of a,c, g being Morphism of b,c st Hom(a,c) <> {} & Hom(b,c) <> {} holds nabla(c)*(f+g) = [$f,g$] proof let f be Morphism of a,c, g be Morphism of b,c such that A1: Hom(a,c) <> {} and A2: Hom(b,c) <> {}; A3: Hom(c,c) <> {} by CAT_1:56; thus nabla(c)*(f+g) = [$id c,id c$]*(f+g) by Def30 .= [$(id c)*f,(id c)*g$] by A1,A2,A3,Th80 .= [$f,(id c)*g$] by A1,CAT_1:57 .= [$f,g$] by A2,CAT_1:57; end; theorem for f being Morphism of a,c, h being Morphism of b,d, g being Morphism of c,e, k being Morphism of d,s st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,s) <> {} holds (g+k)*(f+h) = (g*f)+(k*h) proof let f be Morphism of a,c, h be Morphism of b,d; let g be Morphism of c,e, k be Morphism of d,s; assume that A1: Hom(a,c) <> {} and A2: Hom(b,d) <> {} and A3: Hom(c,e) <> {} and A4: Hom(d,s) <> {}; A5: Hom(e,e+s) <> {} & Hom(s,e+s) <> {} by Th66; then in1(e,s)*g*f = in1(e,s)*(g*f) & in2(e,s)*k*h = in2(e,s)*(k*h) by A1,A2,A3,A4,CAT_1:54; then Hom(c,e+s) <> {} & Hom(d,e+s) <> {} & (g*f)+(k*h) = [$in1(e,s)*g*f,in2(e,s)*k*h$] & g+k = [$in1(e,s)*g,in2(e,s)*k$] by A3,A4,A5,Def31,CAT_1:52; hence thesis by A1,A2,Th80; end;