Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### Categories without Uniqueness of \rm cod and \rm dom

**by****Andrzej Trybulec**- Received February 28, 1995
- MML identifier: ALTCAT_1

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, FRAENKEL, FUNCT_1, PRALG_1, RELAT_1, FUNCT_2, PBOOLE, MCART_1, CAT_4, CAT_1, RELAT_2, BINOP_1, REALSET1, CQC_LANG, ALTCAT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, RELAT_1, STRUCT_0, REALSET1, FUNCT_1, FUNCT_2, BINOP_1, MULTOP_1, CQC_LANG, CAT_4, FRAENKEL, PBOOLE, PRALG_1, MSUALG_1; constructors DOMAIN_1, BINOP_1, MULTOP_1, CQC_LANG, CAT_4, FRAENKEL, PRALG_1, MSUALG_1, STRUCT_0, XBOOLE_0; clusters FUNCT_1, FRAENKEL, TEX_2, PRALG_1, STRUCT_0, SUBSET_1, RELAT_1, CQC_LANG, RELSET_1, FUNCT_2, ZFMISC_1, XBOOLE_0; requirements BOOLE, SUBSET; begin :: Preliminaries theorem :: ALTCAT_1:1 for A being non empty set, B,C,D being set st [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] holds B c= D; reserve i,j,k,x for set; definition let A be functional set; cluster -> functional Subset of A; end; definition let f be Function-yielding Function, C be set; cluster f|C -> Function-yielding; end; definition let f be Function; cluster {f} -> functional; end; theorem :: ALTCAT_1:2 for A being set holds id A in Funcs(A,A); theorem :: ALTCAT_1:3 Funcs({},{}) = { id {} }; theorem :: ALTCAT_1:4 for A,B,C being set, f,g being Function st f in Funcs(A,B) & g in Funcs(B,C) holds g*f in Funcs(A,C); theorem :: ALTCAT_1:5 for A,B,C being set st Funcs(A,B) <> {} & Funcs(B,C) <> {} holds Funcs(A,C) <> {}; theorem :: ALTCAT_1:6 for A,B being set for f being Function st f in Funcs(A,B) holds dom f = A & rng f c= B; theorem :: ALTCAT_1:7 for A,B being set, F being ManySortedSet of [:B,A:], C being Subset of A, D being Subset of B, x,y being set st x in C & y in D holds F.(y,x) = (F|([:D,C:] qua set)).(y,x); scheme MSSLambda2{ A,B() -> set, F(set,set) -> set }: ex M being ManySortedSet of [:A(),B():] st for i,j st i in A() & j in B() holds M.(i,j) = F(i,j); scheme MSSLambda2D{ A,B() -> non empty set, F(set,set) -> set }: ex M being ManySortedSet of [:A(),B():] st for i being Element of A(), j being Element of B() holds M.(i,j) = F(i,j); scheme MSSLambda3{ A,B,C() -> set, F(set,set,set) -> set }: ex M being ManySortedSet of [:A(),B(),C():] st for i,j,k st i in A() & j in B() & k in C() holds M.(i,j,k) = F(i,j,k); scheme MSSLambda3D{ A,B,C() -> non empty set, F(set,set,set) -> set }: ex M being ManySortedSet of [:A(),B(),C():] st for i being Element of A(), j being Element of B(), k being Element of C() holds M.(i,j,k) = F(i,j,k); theorem :: ALTCAT_1:8 for A,B being set, N,M being ManySortedSet of [:A,B:] st for i,j st i in A & j in B holds N.(i,j) = M.(i,j) holds M = N; theorem :: ALTCAT_1:9 for A,B being non empty set, N,M being ManySortedSet of [:A,B:] st for i being Element of A, j being Element of B holds N.(i,j) = M.(i,j) holds M = N; theorem :: ALTCAT_1:10 for A being set, N,M being ManySortedSet of [:A,A,A:] st for i,j,k st i in A & j in A & k in A holds N.(i,j,k) = M.(i,j,k) holds M = N; theorem :: ALTCAT_1:11 (i,j):->k = [i,j].-->k; theorem :: ALTCAT_1:12 ((i,j):->k).(i,j) = k; begin :: Alternative Graphs definition struct(1-sorted) AltGraph (# carrier -> set, Arrows -> ManySortedSet of [:the carrier, the carrier:] #); end; definition let G be AltGraph; mode object of G is Element of G; end; definition let G be AltGraph; let o1,o2 be object of G; canceled; func <^o1,o2^> equals :: ALTCAT_1:def 2 (the Arrows of G).(o1,o2); end; definition let G be AltGraph; let o1,o2 be object of G; mode Morphism of o1,o2 is Element of <^o1,o2^>; canceled; end; definition let G be AltGraph; attr G is transitive means :: ALTCAT_1:def 4 for o1,o2,o3 being object of G st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds <^o1,o3^> <> {}; end; begin :: Binary Compositions definition let I be set; let G be ManySortedSet of [:I,I:]; func {|G|} -> ManySortedSet of [:I,I,I:] means :: ALTCAT_1:def 5 for i,j,k st i in I & j in I & k in I holds it.(i,j,k) = G.(i,k); let H be ManySortedSet of [:I,I:]; func {|G,H|} -> ManySortedSet of [:I,I,I:] means :: ALTCAT_1:def 6 for i,j,k st i in I & j in I & k in I holds it.(i,j,k) = [:H.(j,k),G.(i,j):]; end; definition let I be set; let G be ManySortedSet of [:I,I:]; mode BinComp of G is ManySortedFunction of {|G,G|},{|G|}; end; definition let I be non empty set; let G be ManySortedSet of [:I,I:]; let o be BinComp of G; let i,j,k be Element of I; redefine func o.(i,j,k) -> Function of [:G.(j,k),G.(i,j):], G.(i,k); end; definition let I be non empty set; let G be ManySortedSet of [:I,I:]; let IT be BinComp of G; attr IT is associative means :: ALTCAT_1:def 7 for i,j,k,l being Element of I for f,g,h being set st f in G.(i,j) & g in G.(j,k) & h in G.(k,l) holds IT.(i,k,l).(h,IT.(i,j,k).(g,f)) = IT.(i,j,l).(IT.(j,k,l).(h,g),f); attr IT is with_right_units means :: ALTCAT_1:def 8 for i being Element of I ex e being set st e in G.(i,i) & for j being Element of I, f be set st f in G.(i,j) holds IT.(i,i,j).(f,e) = f; attr IT is with_left_units means :: ALTCAT_1:def 9 for j being Element of I ex e being set st e in G.(j,j) & for i being Element of I, f be set st f in G.(i,j) holds IT.(i,j,j).(e,f) = f; end; begin :: Alternative categories definition struct(AltGraph) AltCatStr (# carrier -> set, Arrows -> ManySortedSet of [:the carrier, the carrier:], Comp -> BinComp of the Arrows #); end; definition cluster strict non empty AltCatStr; end; definition let C be non empty AltCatStr; let o1,o2,o3 be object of C such that <^o1,o2^> <> {} & <^o2,o3^> <> {}; let f be Morphism of o1,o2, g be Morphism of o2,o3; func g*f -> Morphism of o1,o3 equals :: ALTCAT_1:def 10 (the Comp of C).(o1,o2,o3).(g,f); end; definition let IT be Function; attr IT is compositional means :: ALTCAT_1:def 11 x in dom IT implies ex f,g being Function st x = [g,f] & IT.x = g*f; end; definition let A,B be functional set; cluster compositional ManySortedFunction of [:A,B:]; end; theorem :: ALTCAT_1:13 for A,B being functional set for F being compositional ManySortedSet of [:A,B:], g,f being Function st g in A & f in B holds F.(g,f) = g*f; definition let A,B be functional set; func FuncComp(A,B) -> compositional ManySortedFunction of [:B,A:] means :: ALTCAT_1:def 12 not contradiction; end; theorem :: ALTCAT_1:14 for A,B,C being set holds rng FuncComp(Funcs(A,B),Funcs(B,C)) c= Funcs(A,C); theorem :: ALTCAT_1:15 for o be set holds FuncComp({id o},{id o}) = (id o,id o) :-> id o; theorem :: ALTCAT_1:16 for A,B being functional set, A1 being Subset of A, B1 being Subset of B holds FuncComp(A1,B1) = FuncComp(A,B)|([:B1,A1:] qua set); :: Kategorie przeksztalcen, Semadeni Wiweger, 1.2.2, str.15 definition let C be non empty AltCatStr; attr C is quasi-functional means :: ALTCAT_1:def 13 for a1,a2 being object of C holds <^a1,a2^> c= Funcs(a1,a2); attr C is semi-functional means :: ALTCAT_1:def 14 for a1,a2,a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} for f being Morphism of a1,a2, g being Morphism of a2,a3, f',g' being Function st f = f' & g = g' holds g*f =g'*f'; attr C is pseudo-functional means :: ALTCAT_1:def 15 for o1,o2,o3 being object of C holds (the Comp of C).(o1,o2,o3) = FuncComp(Funcs(o1,o2),Funcs(o2,o3))|[:<^o2,o3^>,<^o1,o2^>:]; end; definition let X be non empty set, A be ManySortedSet of [:X,X:], C be BinComp of A; cluster AltCatStr(#X,A,C#) -> non empty; end; definition cluster strict pseudo-functional (non empty AltCatStr); end; theorem :: ALTCAT_1:17 for C being non empty AltCatStr, a1,a2,a3 being object of C holds (the Comp of C).(a1,a2,a3) is Function of [:<^a2,a3^>,<^a1,a2^>:],<^a1,a3^>; theorem :: ALTCAT_1:18 for C being pseudo-functional (non empty AltCatStr) for a1,a2,a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} for f being Morphism of a1,a2, g being Morphism of a2,a3, f',g' being Function st f = f' & g = g' holds g*f =g'*f'; :: Kategorie EnsCat(A), Semadeni Wiweger 1.2.3, str. 15 :: ale bez parametryzacji definition let A be non empty set; func EnsCat A -> strict pseudo-functional (non empty AltCatStr) means :: ALTCAT_1:def 16 the carrier of it = A & for a1,a2 being object of it holds <^a1,a2^> = Funcs(a1,a2); end; definition let C be non empty AltCatStr; attr C is associative means :: ALTCAT_1:def 17 the Comp of C is associative; attr C is with_units means :: ALTCAT_1:def 18 the Comp of C is with_left_units with_right_units; end; definition cluster transitive associative with_units strict (non empty AltCatStr); end; canceled; theorem :: ALTCAT_1:20 for C being transitive non empty AltCatStr, a1,a2,a3 being object of C holds dom((the Comp of C).(a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng((the Comp of C).(a1,a2,a3)) c= <^a1,a3^>; theorem :: ALTCAT_1:21 for C being with_units (non empty AltCatStr) for o being object of C holds <^o,o^> <> {}; definition let A be non empty set; cluster EnsCat A -> transitive associative with_units; end; definition cluster quasi-functional semi-functional transitive -> pseudo-functional (non empty AltCatStr); cluster with_units pseudo-functional transitive -> quasi-functional semi-functional (non empty AltCatStr); end; :: Definicja kategorii, Semadeni Wiweger 1.3.1, str. 16-17 definition mode category is transitive associative with_units (non empty AltCatStr); end; begin definition let C be with_units (non empty AltCatStr); let o be object of C; func idm o -> Morphism of o,o means :: ALTCAT_1:def 19 for o' being object of C st <^o,o'^> <> {} for a being Morphism of o,o' holds a*it = a; end; canceled; theorem :: ALTCAT_1:23 for C being with_units (non empty AltCatStr) for o being object of C holds idm o in <^o,o^>; theorem :: ALTCAT_1:24 for C being with_units (non empty AltCatStr) for o1,o2 being object of C st <^o1,o2^> <> {} for a being Morphism of o1,o2 holds (idm o2)*a = a; theorem :: ALTCAT_1:25 for C being associative transitive (non empty AltCatStr) for o1,o2,o3,o4 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} for a being Morphism of o1,o2, b being Morphism of o2,o3, c being Morphism of o3,o4 holds c*(b*a) = (c*b)*a; begin :: kategoria dyskretna, Semadeni Wiweger, 1.3.1, str.18 definition let C be AltCatStr; attr C is quasi-discrete means :: ALTCAT_1:def 20 for i,j being object of C st <^i,j^> <> {} holds i = j; :: to sa po prostu zbiory monoidow attr C is pseudo-discrete means :: ALTCAT_1:def 21 for i being object of C holds <^i,i^> is trivial; end; theorem :: ALTCAT_1:26 for C being with_units (non empty AltCatStr) holds C is pseudo-discrete iff for o being object of C holds <^o,o^> = { idm o }; definition cluster trivial non empty -> quasi-discrete AltCatStr; end; theorem :: ALTCAT_1:27 EnsCat 1 is pseudo-discrete trivial; definition cluster pseudo-discrete trivial strict category; end; definition cluster quasi-discrete pseudo-discrete trivial strict category; end; definition mode discrete_category is quasi-discrete pseudo-discrete category; end; definition let A be non empty set; func DiscrCat A -> quasi-discrete strict non empty AltCatStr means :: ALTCAT_1:def 22 the carrier of it = A & for i being object of it holds <^i,i^> = { id i }; end; definition cluster quasi-discrete -> transitive AltCatStr; end; theorem :: ALTCAT_1:28 for A being non empty set, o1,o2,o3 being object of DiscrCat A st o1 <> o2 or o2 <> o3 holds (the Comp of DiscrCat A).(o1,o2,o3) = {}; theorem :: ALTCAT_1:29 for A being non empty set, o being object of DiscrCat A holds (the Comp of DiscrCat A).(o,o,o) = (id o,id o) :-> id o; definition let A be non empty set; cluster DiscrCat A -> pseudo-functional pseudo-discrete with_units associative; end;

Back to top