:: Examples of Category Structures. Subcategories :: by Andrzej Trybulec :: :: Received January 22, 1996 :: Copyright (c) 1996-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 ZFMISC_1, FUNCOP_1, RELAT_1, FUNCT_1, PBOOLE, PZFMISC1, MEMBER_1, XBOOLE_0, PARTFUN1, SUBSET_1, TARSKI, CAT_1, MCART_1, GRAPH_1, STRUCT_0, ALTCAT_1, BINOP_1, RELAT_2, REALSET1, ALTCAT_2, MONOID_0, RECDEF_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, XTUPLE_0, MCART_1, FUNCT_1, PZFMISC1, REALSET1, DOMAIN_1, STRUCT_0, PARTFUN1, FUNCT_2, BINOP_1, MULTOP_1, FUNCT_3, FUNCT_4, GRAPH_1, CAT_1, PBOOLE, FUNCOP_1, ALTCAT_1; constructors FUNCT_3, REALSET1, PZFMISC1, CAT_1, ALTCAT_1, RELSET_1, FUNCT_4, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, PBOOLE, FUNCOP_1, REALSET1, STRUCT_0, ALTCAT_1, CAT_1, PRALG_1, RELSET_1; requirements SUBSET, BOOLE; begin :: Preliminaries reserve e for set; theorem :: ALTCAT_2:1 for X1,X2 being set, a1,a2 being set holds [:X1 -->a1,X2-->a2:] = [:X1 ,X2:] --> [a1,a2]; registration let I be set; cluster EmptyMS I -> Function-yielding; end; theorem :: ALTCAT_2:2 for f,g being Function holds ~(g*f) = g*~f; theorem :: ALTCAT_2:3 for f,g,h being Function holds ~(f*[:g,h:]) = ~f*[:h,g:]; registration let f be Function-yielding Function; cluster ~f -> Function-yielding; end; theorem :: ALTCAT_2:4 for I being set, A,B,C being ManySortedSet of I st A is_transformable_to B for F being ManySortedFunction of A,B, G being ManySortedFunction of B,C holds G**F is ManySortedFunction of A,C; registration let I be set; let A be ManySortedSet of [:I,I:]; cluster ~A -> [:I,I:]-defined; end; registration let I be set; let A be ManySortedSet of [:I,I:]; cluster ~A -> total for [:I,I:]-defined Function; end; theorem :: ALTCAT_2:5 for I1 being set, I2 being non empty set, f being Function of I1,I2, B ,C being ManySortedSet of I2, G being ManySortedFunction of B,C holds G*f is ManySortedFunction of B*f, C*f; definition let I be set, A,B be ManySortedSet of [:I,I:], F be ManySortedFunction of A, B; redefine func ~F -> ManySortedFunction of ~A,~B; end; theorem :: ALTCAT_2:6 for I1,I2 being non empty set, M being ManySortedSet of [:I1,I2:], o1 being Element of I1, o2 being Element of I2 holds (~M).(o2,o1) = M.(o1,o2); registration let I1 be set, f,g be ManySortedFunction of I1; cluster g**f -> I1-defined; end; registration let I1 be set, f,g be ManySortedFunction of I1; cluster g**f -> total; end; begin :: An auxiliary notion definition let f,g be Function; pred f cc= g means :: ALTCAT_2:def 1 dom f c= dom g & for i being set st i in dom f holds f.i c= g.i; reflexivity; end; definition let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J; redefine pred A cc= B means :: ALTCAT_2:def 2 I c= J & for i being set st i in I holds A.i c= B.i; end; theorem :: ALTCAT_2:7 for I,J being set, A being ManySortedSet of I, B being ManySortedSet of J holds A cc= B & B cc= A implies A = B; theorem :: ALTCAT_2:8 for I,J,K being set, A being ManySortedSet of I, B being ManySortedSet of J, C being ManySortedSet of K holds A cc= B & B cc= C implies A cc= C; theorem :: ALTCAT_2:9 for I being set, A being ManySortedSet of I, B being ManySortedSet of I holds A cc= B iff A c= B; begin :: A bit of lambda calculus scheme :: ALTCAT_2:sch 1 OnSingletons{X()-> non empty set, F(set)-> set, P[set]}: { [o,F(o)] where o is Element of X(): P[o] } is Function; scheme :: ALTCAT_2:sch 2 DomOnSingletons {X()-> non empty set,f()-> Function, F(set)-> set, P[set]}: dom f() = { o where o is Element of X(): P[o]} provided f() = { [o,F(o)] where o is Element of X(): P[o] }; scheme :: ALTCAT_2:sch 3 ValOnSingletons {X()-> non empty set,f()-> Function, x()-> Element of X(), F (set)-> set, P[set]}: f().x() = F(x()) provided f() = { [o,F(o)] where o is Element of X(): P[o] } and P[x()]; begin :: More on old categories theorem :: ALTCAT_2:10 for C being Category, i,j,k being Object of C holds [:Hom(j,k), Hom(i,j):] c= dom the Comp of C; theorem :: ALTCAT_2:11 for C being Category, i,j,k being Object of C holds (the Comp of C).:[:Hom(j,k),Hom(i,j):] c= Hom(i,k); definition let C be non void non empty CatStr; func the_hom_sets_of C -> ManySortedSet of [:the carrier of C, the carrier of C:] means :: ALTCAT_2:def 3 for i,j being Object of C holds it.(i,j) = Hom(i,j); end; theorem :: ALTCAT_2:12 for C be Category, i be Object of C holds id i in ( the_hom_sets_of C).(i,i); definition let C be Category; func the_comps_of C -> BinComp of the_hom_sets_of C means :: ALTCAT_2:def 4 for i,j,k being Object of C holds it.(i,j,k) = (the Comp of C)| ([:(the_hom_sets_of C).(j ,k),(the_hom_sets_of C).(i,j):] qua set); end; theorem :: ALTCAT_2:13 for C being Category, i,j,k being Object of C st Hom(i,j) <> {} & Hom(j,k) <> {} for f being Morphism of i,j, g being Morphism of j,k holds ( the_comps_of C).(i,j,k).(g,f) = g*f; theorem :: ALTCAT_2:14 for C being Category holds the_comps_of C is associative; theorem :: ALTCAT_2:15 for C being Category holds the_comps_of C is with_left_units with_right_units ; begin :: Transforming an old category into new one definition let C be Category; func Alter C -> strict non empty AltCatStr equals :: ALTCAT_2:def 5 AltCatStr(#the carrier of C,the_hom_sets_of C, the_comps_of C#); end; theorem :: ALTCAT_2:16 for C being Category holds Alter C is associative; theorem :: ALTCAT_2:17 for C being Category holds Alter C is with_units; theorem :: ALTCAT_2:18 for C being Category holds Alter C is transitive; registration let C be Category; cluster Alter C -> transitive associative with_units; end; begin :: More on new categories registration cluster non empty strict for AltGraph; end; definition let C be AltGraph; attr C is reflexive means :: ALTCAT_2:def 6 for x being set st x in the carrier of C holds (the Arrows of C).(x,x) <> {}; end; definition let C be non empty AltGraph; redefine attr C is reflexive means :: ALTCAT_2:def 7 for o being Object of C holds <^o,o^> <> {}; end; definition let C be non empty transitive AltCatStr; redefine attr C is associative means :: ALTCAT_2:def 8 for o1,o2,o3,o4 being Object of C for f being Morphism of o1,o2, g being Morphism of o2,o3, h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds h*g*f = h*(g *f); end; definition let C be non empty AltCatStr; redefine attr C is with_units means :: ALTCAT_2:def 9 for o being Object of C holds <^o,o^> <> {} & ex i being Morphism of o,o st for o9 being Object of C, m9 being Morphism of o9,o, m99 being Morphism of o,o9 holds (<^o9,o^> <> {} implies i*m9 = m9) & (<^o,o9^> <> {} implies m99*i = m99); end; registration cluster with_units -> reflexive for non empty AltCatStr; end; registration cluster non empty reflexive for AltGraph; end; registration cluster non empty reflexive for AltCatStr; end; begin definition func the_empty_category -> strict AltCatStr means :: ALTCAT_2:def 10 the carrier of it is empty; end; registration cluster the_empty_category -> empty; end; registration cluster empty strict for AltCatStr; end; theorem :: ALTCAT_2:19 for E being empty strict AltCatStr holds E = the_empty_category; begin :: Subcategories :: Semadeni Wiweger 1.6.1 str. 24 definition let C be AltCatStr; mode SubCatStr of C -> AltCatStr means :: ALTCAT_2:def 11 the carrier of it c= the carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the Comp of C; end; reserve C,C1,C2,C3 for AltCatStr; theorem :: ALTCAT_2:20 C is SubCatStr of C; theorem :: ALTCAT_2:21 C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3; theorem :: ALTCAT_2:22 for C1,C2 being AltCatStr st C1 is SubCatStr of C2 & C2 is SubCatStr of C1 holds the AltCatStr of C1 = the AltCatStr of C2; registration let C be AltCatStr; cluster strict for SubCatStr of C; end; definition let C be non empty AltCatStr, o be Object of C; func ObCat o -> strict SubCatStr of C means :: ALTCAT_2:def 12 the carrier of it = { o } & the Arrows of it = (o,o):-> <^o,o^> & the Comp of it = [o,o,o] .--> (the Comp of C).(o,o,o); end; reserve C for non empty AltCatStr, o for Object of C; theorem :: ALTCAT_2:23 for o9 being Object of ObCat o holds o9 = o; registration let C be non empty AltCatStr, o be Object of C; cluster ObCat o -> transitive non empty; end; registration let C be non empty AltCatStr; cluster transitive non empty strict for SubCatStr of C; end; theorem :: ALTCAT_2:24 for C being transitive non empty AltCatStr, D1,D2 being transitive non empty SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds D1 is SubCatStr of D2; definition let C be AltCatStr, D be SubCatStr of C; attr D is full means :: ALTCAT_2:def 13 the Arrows of D = (the Arrows of C)||the carrier of D; end; definition let C be with_units non empty AltCatStr, D be SubCatStr of C; attr D is id-inheriting means :: ALTCAT_2:def 14 for o being Object of D, o9 being Object of C st o = o9 holds idm o9 in <^o,o^> if D is non empty otherwise not contradiction; end; registration let C be AltCatStr; cluster full strict for SubCatStr of C; end; registration let C be non empty AltCatStr; cluster full non empty strict for SubCatStr of C; end; registration let C be category, o be Object of C; cluster ObCat o -> full id-inheriting; end; registration let C be category; cluster full id-inheriting non empty strict for SubCatStr of C; end; reserve C for non empty transitive AltCatStr; theorem :: ALTCAT_2:25 for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds the AltCatStr of D = the AltCatStr of C; theorem :: ALTCAT_2:26 for D1,D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds the AltCatStr of D1 = the AltCatStr of D2; theorem :: ALTCAT_2:27 for D being full SubCatStr of C st the carrier of D = the carrier of C holds the AltCatStr of D = the AltCatStr of C; theorem :: ALTCAT_2:28 for C being non empty AltCatStr, D being full non empty SubCatStr of C, o1,o2 being Object of C, p1,p2 being Object of D st o1 = p1 & o2 = p2 holds <^o1,o2^> = <^p1,p2^>; theorem :: ALTCAT_2:29 for C being non empty AltCatStr, D being non empty SubCatStr of C for o being Object of D holds o is Object of C; registration let C be transitive non empty AltCatStr; cluster full non empty -> transitive for SubCatStr of C; end; theorem :: ALTCAT_2:30 for D1,D2 being full non empty SubCatStr of C st the carrier of D1 = the carrier of D2 holds the AltCatStr of D1 = the AltCatStr of D2; theorem :: ALTCAT_2:31 for C being non empty AltCatStr, D being non empty SubCatStr of C, o1,o2 being Object of C, p1,p2 being Object of D st o1 = p1 & o2 = p2 holds <^p1,p2^> c= <^o1,o2^>; theorem :: ALTCAT_2:32 for C being non empty transitive AltCatStr, D being non empty transitive SubCatStr of C, p1,p2,p3 being Object of D st <^p1,p2^> <> {} & <^p2 ,p3^> <> {} for o1,o2,o3 being Object of C st o1 = p1 & o2 = p2 & o3 = p3 for f being Morphism of o1,o2, g being Morphism of o2,o3, ff being Morphism of p1,p2, gg being Morphism of p2,p3 st f = ff & g = gg holds g*f = gg*ff; registration let C be associative transitive non empty AltCatStr; cluster transitive -> associative for non empty SubCatStr of C; end; theorem :: ALTCAT_2:33 for C being non empty AltCatStr, D being non empty SubCatStr of C, o1,o2 being Object of C, p1,p2 being Object of D st o1 = p1 & o2 = p2 & <^p1 ,p2^> <> {} for n being Morphism of p1,p2 holds n is Morphism of o1,o2; registration let C be transitive with_units non empty AltCatStr; cluster id-inheriting transitive -> with_units for non empty SubCatStr of C; end; registration let C be category; cluster id-inheriting transitive for non empty SubCatStr of C; end; definition let C be category; mode subcategory of C is id-inheriting transitive SubCatStr of C; end; theorem :: ALTCAT_2:34 for C being category, D being non empty subcategory of C for o being Object of D, o9 being Object of C st o = o9 holds idm o = idm o9;