:: Cartesian Categories :: by Czes{\l}aw Byli\'nski :: :: Received October 27, 1992 :: Copyright (c) 1992-2016 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, WELLORD1, XBOOLE_0, RELAT_1, FINSET_1, FUNCT_1, STRUCT_0, CAT_3, GRAPH_1, CARD_1, FUNCOP_1, PARTFUN1, NAT_1, ARYTM_3, SUBSET_1, TARSKI, ARYTM_1, FUNCT_4, FUNCT_6, ZFMISC_1, ALGSTR_1, MCART_1, DIRAF, PBOOLE, EQREL_1, CAT_4, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, ALGSTR_1, XCMPLX_0, ORDINAL1, CARD_1, FUNCT_4, STRUCT_0, GRAPH_1, CAT_1, CAT_3; constructors BINOP_1, REAL_1, NAT_1, ALGSTR_1, CAT_3, RELSET_1, XREAL_0, FUNCT_4; registrations XBOOLE_0, FUNCT_1, FINSET_1, XREAL_0, NAT_1, ORDINAL1, CARD_1, STRUCT_0, PARTFUN1, FUNCT_2, RELSET_1, CAT_1; requirements NUMERALS, SUBSET, BOOLE; begin reserve o,m for set; definition let C be Category, a,b be Object of C; redefine pred a,b are_isomorphic means :: CAT_4:def 1 Hom(a,b)<>{} & Hom(b,a)<>{} & ex f being Morphism of a,b, f9 being Morphism of b,a st f*f9 = id b & f9*f = id a; end; begin :: Cartesian Categories definition let C be Category; attr C is with_finite_product means :: CAT_4:def 2 for I being finite set, F being Function of I,the carrier of C ex a being Object of C, F9 being Projections_family of a, I st cods F9 = F & a is_a_product_wrt F9; end; theorem :: CAT_4:1 for C being Category holds C is with_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; definition struct (CatStr)ProdCatStr (# carrier,carrier' -> set, Source,Target -> Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the carrier' :],the carrier', TerminalObj -> Element of the carrier, CatProd -> Function of [:the carrier,the carrier:],the carrier, Proj1,Proj2 -> Function of [:the carrier,the carrier:], the carrier' #); end; registration cluster non void non empty for ProdCatStr; end; definition let C be non void non empty ProdCatStr; func [1]C -> Object of C equals :: CAT_4:def 3 the TerminalObj of C; let a,b be Object of C; func a[x]b -> Object of C equals :: CAT_4:def 4 (the CatProd of C).(a,b); func pr1(a,b) -> Morphism of C equals :: CAT_4:def 5 (the Proj1 of C).(a,b); func pr2(a,b) -> Morphism of C equals :: CAT_4:def 6 (the Proj2 of C).(a,b); end; definition let o,m; func c1Cat(o,m) -> strict ProdCatStr equals :: CAT_4:def 7 ProdCatStr(# {o},{m},m:->o,m:->o,(m,m):->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #); end; registration let o,m be set; cluster c1Cat(o,m) -> non empty trivial non void trivial'; end; theorem :: CAT_4:2 the CatStr of c1Cat(o,m) = 1Cat(o,m); registration cluster strict Category-like reflexive transitive associative with_identities non void non empty for non void non empty ProdCatStr; end; registration let o,m be set; cluster c1Cat(o,m) -> Category-like reflexive transitive associative with_identities non empty non void; end; theorem :: CAT_4:3 for a,b being Object of c1Cat(o,m) holds a = b; theorem :: CAT_4:4 for f,g being Morphism of c1Cat(o,m) holds f = g; theorem :: CAT_4:5 for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m ) holds f in Hom(a,b); theorem :: CAT_4:6 for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m) holds f is Morphism of a,b; theorem :: CAT_4:7 for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {}; theorem :: CAT_4:8 for a being Object of c1Cat(o,m) holds a is terminal; theorem :: CAT_4:9 for c being Object of c1Cat(o,m), p1,p2 being Morphism of c1Cat( o,m) holds c is_a_product_wrt p1,p2; definition let IT be Category-like reflexive transitive associative with_identities non void non empty ProdCatStr; attr IT is Cartesian means :: CAT_4:def 8 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 :: CAT_4:10 for o,m being set holds c1Cat(o,m) is Cartesian; registration cluster strict Cartesian for Category-like reflexive transitive associative with_identities non void non empty ProdCatStr; end; definition mode Cartesian_category is Cartesian Category-like non void non empty reflexive transitive associative with_identities non void non empty ProdCatStr; end; reserve C for Cartesian_category; reserve a,b,c,d,e,s for Object of C; theorem :: CAT_4:11 [1]C is terminal; theorem :: CAT_4:12 for f1,f2 being Morphism of a,[1]C holds f1 = f2; theorem :: CAT_4:13 Hom(a,[1]C) <> {}; definition let C,a; func term(a) -> Morphism of a,[1]C means :: CAT_4:def 9 not contradiction; end; theorem :: CAT_4:14 term a = term(a,[1]C); theorem :: CAT_4:15 dom(term a) = a & cod(term a) = [1]C; theorem :: CAT_4:16 Hom(a,[1]C) = {term a}; theorem :: CAT_4:17 dom pr1(a,b) = a[x]b & cod pr1(a,b) = a; theorem :: CAT_4:18 dom pr2(a,b) = a[x]b & cod pr2(a,b) = b; definition let C,a,b; redefine func pr1(a,b) -> Morphism of a[x]b,a; redefine func pr2(a,b) -> Morphism of a[x]b,b; end; theorem :: CAT_4:19 Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {}; theorem :: CAT_4:20 a[x]b is_a_product_wrt pr1(a,b),pr2(a,b); theorem :: CAT_4:21 C is with_finite_product; theorem :: CAT_4:22 Hom(a,b) <> {} & Hom(b,a) <> {} implies pr1(a,b) is retraction & pr2(a,b) is retraction; definition let C,a,b,c; let f be Morphism of c,a, g be Morphism of c,b; assume Hom(c,a) <> {} & Hom(c,b) <> {}; func <:f,g:> -> Morphism of c,a[x]b means :: CAT_4:def 10 pr1(a,b)*it = f & pr2(a,b) *it = g; end; theorem :: CAT_4:23 Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {}; theorem :: CAT_4:24 <:pr1(a,b),pr2(a,b):> = id(a[x]b); theorem :: CAT_4:25 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; theorem :: CAT_4:26 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; theorem :: CAT_4:27 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; theorem :: CAT_4:28 Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {}; definition let C,a; func lambda(a) -> Morphism of [1]C[x]a,a equals :: CAT_4:def 11 pr2([1]C,a); func lambda'(a) -> Morphism of a,[1]C[x]a equals :: CAT_4:def 12 <:term a,id a:>; func rho(a) -> Morphism of a[x][1]C,a equals :: CAT_4:def 13 pr1(a,[1]C); func rho'(a) -> Morphism of a,a[x][1]C equals :: CAT_4:def 14 <:id a,term a:>; end; theorem :: CAT_4:29 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); theorem :: CAT_4:30 a, a[x][1]C are_isomorphic & a,[1]C[x]a are_isomorphic; definition let C,a,b; func Switch(a,b) -> Morphism of a[x]b,b[x]a equals :: CAT_4:def 15 <:pr2(a,b),pr1(a,b):>; end; theorem :: CAT_4:31 Hom(a[x]b,b[x]a)<>{}; theorem :: CAT_4:32 Switch(a,b)*Switch(b,a) = id(b[x]a); theorem :: CAT_4:33 a[x]b,b[x]a are_isomorphic; definition let C,a; func Delta a -> Morphism of a,a[x]a equals :: CAT_4:def 16 <:id a,id a:>; end; theorem :: CAT_4:34 Hom(a,a[x]a) <> {}; theorem :: CAT_4:35 for f being Morphism of a,b st Hom(a,b) <> {} holds <:f,f:> = Delta(b) *f; definition let C,a,b,c; func Alpha(a,b,c) -> Morphism of (a[x]b)[x]c,a[x](b[x]c) equals :: CAT_4:def 17 <:pr1(a,b)* pr1(a[x]b,c),<:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>:>; func Alpha'(a,b,c) -> Morphism of a[x](b[x]c),(a[x]b)[x]c equals :: CAT_4:def 18 <:<:pr1(a,b [x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>; end; theorem :: CAT_4:36 Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c ) <> {}; theorem :: CAT_4:37 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); theorem :: CAT_4:38 (a[x]b)[x]c,a[x](b[x]c) are_isomorphic; 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 :: CAT_4:def 19 <:f*pr1(a,c),g*pr2(a,c):>; end; theorem :: CAT_4:39 Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a[x]b,c[x]d) <> {}; theorem :: CAT_4:40 (id a)[x](id b) = id(a[x]b); theorem :: CAT_4:41 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:>; theorem :: CAT_4:42 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); theorem :: CAT_4:43 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); begin :: Categories with Finite Coproducts definition let C be Category; attr C is with_finite_coproduct means :: CAT_4:def 20 for I being finite set, F being Function of I,the carrier of C ex a being Object of C, F9 being Injections_family of a,I st doms F9 = F & a is_a_coproduct_wrt F9; end; theorem :: CAT_4:44 for C being Category holds C is with_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; definition struct (CatStr)CoprodCatStr (# carrier,carrier' -> set, Source,Target -> Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the carrier' :],the carrier', Initial -> Element of the carrier, Coproduct -> Function of [:the carrier,the carrier:] ,the carrier, Incl1,Incl2 -> Function of [:the carrier,the carrier:],the carrier' #); end; registration cluster non void non empty for CoprodCatStr; end; definition let C be non void non empty CoprodCatStr; func EmptyMS C -> Object of C equals :: CAT_4:def 21 the Initial of C; let a,b be Object of C; func a+b -> Object of C equals :: CAT_4:def 22 (the Coproduct of C).(a,b); func in1(a,b) -> Morphism of C equals :: CAT_4:def 23 (the Incl1 of C).(a,b); func in2(a,b) -> Morphism of C equals :: CAT_4:def 24 (the Incl2 of C).(a,b); end; definition let o,m; func c1Cat*(o,m) -> strict CoprodCatStr equals :: CAT_4:def 25 CoprodCatStr(# {o},{m},m:->o,m:->o,(m,m):->m, Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #); end; ::\$CT registration let o,m; cluster c1Cat*(o,m) -> non void non empty trivial trivial'; end; registration cluster strict Category-like reflexive transitive associative with_identities for non void non empty CoprodCatStr; end; registration let o,m be set; cluster c1Cat*(o,m) -> Category-like reflexive transitive associative with_identities non void non empty; end; theorem :: CAT_4:46 for a,b being Object of c1Cat*(o,m) holds a = b; theorem :: CAT_4:47 for f,g being Morphism of c1Cat*(o,m) holds f = g; theorem :: CAT_4:48 for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*( o,m) holds f in Hom(a,b); theorem :: CAT_4:49 for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m) holds f is Morphism of a,b; theorem :: CAT_4:50 for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {}; theorem :: CAT_4:51 for a being Object of c1Cat*(o,m) holds a is initial; theorem :: CAT_4:52 for c being Object of c1Cat*(o,m), i1,i2 being Morphism of c1Cat*(o,m) holds c is_a_coproduct_wrt i1,i2; definition let IT be Category-like reflexive transitive associative with_identities non void non empty CoprodCatStr; attr IT is Cocartesian means :: CAT_4:def 26 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 :: CAT_4:53 for o,m being set holds c1Cat*(o,m) is Cocartesian; registration cluster strict Cocartesian for reflexive transitive associative with_identities Category-like non void non empty CoprodCatStr; end; definition mode Cocartesian_category is Cocartesian reflexive transitive associative with_identities Category-like non void non empty CoprodCatStr; end; reserve C for Cocartesian_category; reserve a,b,c,d,e,s for Object of C; theorem :: CAT_4:54 EmptyMS C is initial; theorem :: CAT_4:55 for f1,f2 being Morphism of EmptyMS C,a holds f1 = f2; definition let C,a; func init a -> Morphism of EmptyMS C, a means :: CAT_4:def 27 not contradiction; end; theorem :: CAT_4:56 Hom(EmptyMS C,a) <> {}; theorem :: CAT_4:57 init a = init(EmptyMS C,a); theorem :: CAT_4:58 dom(init a) = EmptyMS C & cod(init a) = a; theorem :: CAT_4:59 Hom(EmptyMS C,a) = {init a}; theorem :: CAT_4:60 dom in1(a,b) = a & cod in1(a,b) = a+b; theorem :: CAT_4:61 dom in2(a,b) = b & cod in2(a,b) = a+b; theorem :: CAT_4:62 Hom(a,a+b) <> {} & Hom(b,a+b) <> {}; theorem :: CAT_4:63 a+b is_a_coproduct_wrt in1(a,b),in2(a,b); theorem :: CAT_4:64 C is with_finite_coproduct; definition let C,a,b; redefine func in1(a,b) -> Morphism of a,a+b; redefine func in2(a,b) -> Morphism of b,a+b; end; theorem :: CAT_4:65 Hom(a,b) <> {} & Hom(b,a) <> {} implies in1(a,b) is coretraction & in2 (a,b) is coretraction; definition let C,a,b; redefine func in1(a,b) -> Morphism of a,a+b; redefine func in2(a,b) -> Morphism of b,a+b; end; definition let C,a,b,c; let f be Morphism of a,c, g be Morphism of b,c; assume Hom(a,c) <> {} & Hom(b,c) <> {}; func [\$f,g\$] -> Morphism of a+b,c means :: CAT_4:def 28 it*in1(a,b) = f & it*in2(a,b ) = g; end; theorem :: CAT_4:66 Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {}; theorem :: CAT_4:67 [\$in1(a,b),in2(a,b)\$] = id(a+b); theorem :: CAT_4:68 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\$]; theorem :: CAT_4:69 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; theorem :: CAT_4:70 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; theorem :: CAT_4:71 a, a+EmptyMS C are_isomorphic & a,EmptyMS C+a are_isomorphic; theorem :: CAT_4:72 a+b,b+a are_isomorphic; theorem :: CAT_4:73 (a+b)+c,a+(b+c) are_isomorphic; definition let C,a; func nabla a -> Morphism of a+a,a equals :: CAT_4:def 29 [\$id a,id a\$]; 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 :: CAT_4:def 30 [\$in1(c,d)*f,in2(c,d)*g\$]; end; theorem :: CAT_4:74 Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a+b,c+d) <> {}; theorem :: CAT_4:75 (id a)+(id b) = id(a+b); theorem :: CAT_4:76 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\$]; theorem :: CAT_4:77 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\$]; theorem :: CAT_4:78 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);