Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Examples of Category Structures

**by****Andrzej Trybulec**- Received January 22, 1996
- MML identifier: ALTCAT_2

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCOP_1, RELAT_1, FUNCT_1, CAT_4, PRALG_1, BOOLE, PBOOLE, NATTRA_1, MSUALG_3, CAT_1, MCART_1, ALTCAT_1, BINOP_1, RELAT_2, ALTCAT_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MCART_1, FUNCT_1, STRUCT_0, FUNCT_2, BINOP_1, MULTOP_1, FUNCT_3, FUNCT_4, CQC_LANG, CAT_4, CAT_1, PBOOLE, PRALG_1, ALTCAT_1, MSUALG_1, AUTALG_1, MSUALG_3; constructors ALTCAT_1, CAT_4, CQC_LANG, MSUALG_3, AUTALG_1; clusters STRUCT_0, ALTCAT_1, MSUALG_1, FUNCT_1, RELAT_1, PRALG_1, RELSET_1, CQC_LANG, SUBSET_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]; definition let I be set; cluster [0]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:]; definition 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; definition let I be set; let A be ManySortedSet of [:I,I:]; redefine func ~A -> ManySortedSet of [:I,I:]; 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); definition let I1 be set, f,g be ManySortedFunction of I1; redefine func g**f -> ManySortedFunction of I1; 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; canceled; theorem :: ALTCAT_2:8 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:9 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:10 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 OnSingletons{X()-> non empty set, F(set)-> set, P[set]}: { [o,F(o)] where o is Element of X(): P[o] } is Function; scheme 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 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:11 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:12 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 CatStr; func the_hom_sets_of C -> ManySortedSet of [:the Objects of C, the Objects 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:13 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):]; end; theorem :: ALTCAT_2:14 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:15 for C being Category holds the_comps_of C is associative; theorem :: ALTCAT_2:16 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 Objects of C,the_hom_sets_of C, the_comps_of C#); end; theorem :: ALTCAT_2:17 for C being Category holds Alter C is associative; theorem :: ALTCAT_2:18 for C being Category holds Alter C is with_units; theorem :: ALTCAT_2:19 for C being Category holds Alter C is transitive; definition let C be Category; cluster Alter C -> transitive associative with_units; end; begin :: More on new categories definition cluster non empty strict 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 o' being object of C, m' being Morphism of o',o, m'' being Morphism of o,o' holds (<^o',o^> <> {} implies i*m' = m') & (<^o,o'^> <> {} implies m''*i = m''); end; definition cluster with_units -> reflexive (non empty AltCatStr); end; definition cluster non empty reflexive AltGraph; end; definition cluster non empty reflexive AltCatStr; end; begin definition func the_empty_category -> strict AltCatStr means :: ALTCAT_2:def 10 the carrier of it is empty; end; definition cluster the_empty_category -> empty; end; definition cluster empty strict AltCatStr; end; theorem :: ALTCAT_2:20 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:21 C is SubCatStr of C; theorem :: ALTCAT_2:22 C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3; theorem :: ALTCAT_2:23 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; definition let C be AltCatStr; cluster strict 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:24 for o' being object of ObCat o holds o' = o; definition let C be non empty AltCatStr, o be object of C; cluster ObCat o -> transitive non empty; end; definition let C be non empty AltCatStr; cluster transitive non empty strict SubCatStr of C; end; theorem :: ALTCAT_2:25 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, 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, o' being object of C st o = o' holds idm o' in <^o,o^> if D is non empty otherwise not contradiction; end; definition let C be AltCatStr; cluster full strict SubCatStr of C; end; definition let C be non empty AltCatStr; cluster full non empty strict SubCatStr of C; end; definition let C be category, o be object of C; cluster ObCat o -> full id-inheriting; end; definition let C be category; cluster full id-inheriting non empty strict SubCatStr of C; end; reserve C for non empty transitive AltCatStr; theorem :: ALTCAT_2:26 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:27 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:28 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:29 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:30 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; definition let C be transitive non empty AltCatStr; cluster full non empty -> transitive SubCatStr of C; end; theorem :: ALTCAT_2:31 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:32 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:33 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; definition let C be associative transitive (non empty AltCatStr); cluster transitive -> associative (non empty SubCatStr of C); end; theorem :: ALTCAT_2:34 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; definition let C be transitive with_units (non empty AltCatStr); cluster id-inheriting transitive -> with_units (non empty SubCatStr of C); end; definition let C be category; cluster id-inheriting transitive (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:35 for C being category, D being non empty subcategory of C for o being object of D, o' being object of C st o = o' holds idm o = idm o';

Back to top