:: Subcategories and Products of Categories :: by Czes{\l}aw Byli\'nski :: :: Received May 31, 1990 :: Copyright (c) 1990-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, SUBSET_1, FUNCT_2, FUNCT_1, ZFMISC_1, FUNCT_5, RELAT_1, TARSKI, CAT_1, FUNCOP_1, STRUCT_0, GRAPH_1, FUNCT_3, REALSET1, PARTFUN1, FUNCT_4, MCART_1, CAT_2, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, FUNCOP_1, STRUCT_0, GRAPH_1, CAT_1; constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, CAT_1, FUNCOP_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, STRUCT_0, RELAT_1, XTUPLE_0; requirements SUBSET, BOOLE; begin ::$CT 4 reserve B,C,D,C9,D9 for Category; :: Auxiliary theorems on Functors definition let B,C; let c be Object of C; func B --> c -> Functor of B,C equals :: CAT_2:def 1 (the carrier' of B) --> (id c); end; theorem :: CAT_2:5 for c being Object of C, b being Object of B holds (Obj (B --> c)).b = c; definition let C,D; func Funct(C,D) -> set means :: CAT_2:def 2 for x being set holds x in it iff x is Functor of C,D; end; registration let C,D; cluster Funct(C,D) -> non empty; end; definition let C,D; mode FUNCTOR-DOMAIN of C,D -> non empty set means :: CAT_2:def 3 for x being Element of it holds x is Functor of C,D; end; definition let C,D; let F be FUNCTOR-DOMAIN of C,D; redefine mode Element of F -> Functor of C,D; end; definition let A be non empty set; let C,D; let F be FUNCTOR-DOMAIN of C,D, T be Function of A,F, x be Element of A; redefine func T.x -> Element of F; end; definition let C,D; redefine func Funct(C,D) -> FUNCTOR-DOMAIN of C,D; end; :: Subcategory definition let C; mode Subcategory of C -> Category means :: CAT_2:def 4 the carrier of it c= the carrier of C & (for a,b being Object of it, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) c= Hom(a9,b9)) & the Comp of it c= the Comp of C & for a being Object of it, a9 being Object of C st a = a9 holds id a = id a9; end; registration let C; cluster strict for Subcategory of C; end; reserve E for Subcategory of C; theorem :: CAT_2:6 for e being Object of E holds e is Object of C; theorem :: CAT_2:7 the carrier' of E c= the carrier' of C; theorem :: CAT_2:8 for f being Morphism of E holds f is Morphism of C; theorem :: CAT_2:9 for f being (Morphism of E), f9 being Morphism of C st f = f9 holds dom f = dom f9 & cod f = cod f9; theorem :: CAT_2:10 for a,b being Object of E, a9,b9 being Object of C,f being Morphism of a, b st a = a9 & b = b9 & Hom(a,b)<>{} holds f is Morphism of a9,b9; theorem :: CAT_2:11 for f,g being (Morphism of E), f9,g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds g(*)f = g9(*)f9; theorem :: CAT_2:12 C is Subcategory of C; theorem :: CAT_2:13 id E is Functor of E,C; definition let C,E; func incl(E) -> Functor of E,C equals :: CAT_2:def 5 id E; end; theorem :: CAT_2:14 for a being Object of E holds (Obj incl E).a = a; theorem :: CAT_2:15 for a being Object of E holds (incl E).a = a; theorem :: CAT_2:16 incl E is faithful; theorem :: CAT_2:17 incl E is full iff for a,b being Object of E, a9,b9 being Object of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9); definition let D; let C be Subcategory of D; attr C is full means :: CAT_2:def 6 for c1,c2 being Object of C, d1,d2 being Object of D st c1 = d1 & c2 = d2 holds Hom(c1,c2) = Hom(d1,d2); end; registration let D; cluster full for Subcategory of D; end; theorem :: CAT_2:18 E is full iff incl(E) is full; theorem :: CAT_2:19 for O being non empty Subset of the carrier of C holds union{Hom (a,b) where a is Object of C,b is Object of C: a in O & b in O} is non empty Subset of the carrier' of C; theorem :: CAT_2:20 for O being non empty Subset of the carrier of C, M being non empty set st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} holds (the Source of C)|M is Function of M,O & (the Target of C)|M is Function of M,O & (the Comp of C)||M is PartFunc of [:M,M:],M; registration let O, M be non empty set, d,c being Function of M,O, p being PartFunc of [: M,M:],M; cluster CatStr(#O,M,d,c,p#) -> non void non empty; end; theorem :: CAT_2:21 for O being non empty Subset of the carrier of C, M being non empty set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M holds CatStr(#O,M,d,c,p#) is full Subcategory of C; theorem :: CAT_2:22 for O being non empty Subset of the carrier of C, M being non empty set , d,c being Function of M,O, p being PartFunc of [:M,M:],M st CatStr(#O,M,d,c,p#) is full Subcategory of C holds M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M; :: Product of Categories definition let C,D; func [:C,D:] -> Category equals :: CAT_2:def 7 CatStr (# [:the carrier of C,the carrier of D:], [:the carrier' of C,the carrier' of D:], [:the Source of C,the Source of D:], [:the Target of C,the Target of D:], |:the Comp of C, the Comp of D:| #); end; theorem :: CAT_2:23 the carrier of [:C,D:] = [:the carrier of C,the carrier of D:] & the carrier' of [:C,D:] = [:the carrier' of C,the carrier' of D:] & the Source of [:C,D:] = [:the Source of C,the Source of D:] & the Target of [:C,D:] = [:the Target of C,the Target of D:] & the Comp of [:C,D:] = |:the Comp of C, the Comp of D:|; definition let C,D; let c be Object of C; let d be Object of D; redefine func [c,d] -> Object of [:C,D:]; end; ::$CT theorem :: CAT_2:25 for cd being Object of [:C,D:] ex c being Object of C, d being Object of D st cd = [c,d]; definition let C,D; let f be Morphism of C; let g be Morphism of D; redefine func [f,g] -> Morphism of [:C,D:]; end; ::$CT theorem :: CAT_2:27 for fg being Morphism of [:C,D:] ex f being (Morphism of C), g being Morphism of D st fg = [f,g]; theorem :: CAT_2:28 for f being Morphism of C for g being Morphism of D holds dom [f,g] = [dom f,dom g] & cod [f,g] = [cod f,cod g]; theorem :: CAT_2:29 for f,f9 being Morphism of C for g,g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g]; theorem :: CAT_2:30 for f,f9 being Morphism of C for g,g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g]; theorem :: CAT_2:31 for c being Object of C, d being Object of D holds id [c,d] = [id c,id d]; theorem :: CAT_2:32 for c,c9 being Object of C, d,d9 being Object of D holds Hom([c,d],[c9,d9]) = [:Hom(c,c9),Hom(d,d9):]; theorem :: CAT_2:33 for c,c9 being Object of C, f being Morphism of c,c9, d,d9 being Object of D, g being Morphism of d,d9 st Hom(c,c9) <> {} & Hom(d,d9) <> {} holds [f,g] is Morphism of [c,d],[c9,d9]; :: Bifunctors definition let C,C9,D; let S being Functor of [:C,C9:],D; let m be Morphism of C; let m9 be Morphism of C9; redefine func S.(m,m9) -> Morphism of D; end; theorem :: CAT_2:34 for S being Functor of [:C,C9:],D, c being Object of C holds ( curry S).(id c) is Functor of C9,D; theorem :: CAT_2:35 for S being Functor of [:C,C9:],D, c9 being Object of C9 holds ( curry' S).(id c9) is Functor of C,D; :: Partial Functors definition let C,C9,D; let S be Functor of [:C,C9:],D, c be Object of C; func S?-c -> Functor of C9,D equals :: CAT_2:def 8 (curry S).(id c); end; theorem :: CAT_2:36 for S being Functor of [:C,C9:],D, c being Object of C, f being Morphism of C9 holds (S?-c).f = S.(id c,f); theorem :: CAT_2:37 for S being Functor of [:C,C9:],D, c being Object of C, c9 being Object of C9 holds (Obj S?-c).c9 = (Obj S).(c,c9); definition let C,C9,D; let S be Functor of [:C,C9:],D, c9 be Object of C9; func S-?c9 -> Functor of C,D equals :: CAT_2:def 9 (curry' S).(id c9); end; theorem :: CAT_2:38 for S being Functor of [:C,C9:],D, c9 being Object of C9, f being Morphism of C holds (S-?c9).f = S.(f,id c9); theorem :: CAT_2:39 for S being Functor of [:C,C9:],D, c being Object of C, c9 being Object of C9 holds (Obj S-?c9).c = (Obj S).(c,c9); theorem :: CAT_2:40 for L being Function of the carrier of C,Funct(B,D), M being Function of the carrier of B,Funct(C,D) st ( for c being Object of C,b being Object of B holds (M.b).(id c) = (L.c).(id b) ) & ( for f being Morphism of B for g being Morphism of C holds ((M.(cod f)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom f)).g) ) ex S being Functor of [:B,C:],D st for f being Morphism of B for g being Morphism of C holds S.(f,g) = ((L.(cod g)).f)(*)((M.(dom f)).g); theorem :: CAT_2:41 for L being Function of the carrier of C,Funct(B,D), M being Function of the carrier of B,Funct(C,D) st ex S being Functor of [:B,C:],D st for c being Object of C,b being Object of B holds S-?c = L.c & S?-b = M.b for f being Morphism of B for g being Morphism of C holds ((M.(cod f)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom f)).g); definition let C,D; func pr1(C,D) -> Functor of [:C,D:],C equals :: CAT_2:def 10 pr1(the carrier' of C,the carrier' of D); func pr2(C,D) -> Functor of [:C,D:],D equals :: CAT_2:def 11 pr2(the carrier' of C,the carrier' of D); end; ::$CT 2 theorem :: CAT_2:44 for c being Object of C, d being Object of D holds (Obj pr1(C,D)).(c,d ) = c; theorem :: CAT_2:45 for c being Object of C, d being Object of D holds (Obj pr2(C,D)).(c,d ) = d; definition let C,D,D9; let T be Functor of C,D, T9 be Functor of C,D9; redefine func <:T,T9:> -> Functor of C,[:D,D9:]; end; ::$CT theorem :: CAT_2:47 for T being Functor of C,D, T9 being Functor of C,D9, c being Object of C holds (Obj <:T,T9:>).c = [(Obj T).c,(Obj T9).c]; theorem :: CAT_2:48 for T being Functor of C,D, T9 being Functor of C9,D9 holds [:T, T9:] = <:T*pr1(C,C9),T9*pr2(C,C9):>; definition let C,C9,D,D9; let T be Functor of C,D, T9 be Functor of C9,D9; redefine func [:T,T9:] -> Functor of [:C,C9:],[:D,D9:]; end; ::$CT theorem :: CAT_2:50 for T being Functor of C,D, T9 being Functor of C9,D9, c being Object of C, c9 being Object of C9 holds (Obj [:T,T9:]).(c,c9) = [(Obj T).c,(Obj T9). c9];