### The Mizar article:

### Examples of Category Structures

**by****Andrzej Trybulec**

- Received January 22, 1996
Copyright (c) 1996 Association of Mizar Users

- MML identifier: ALTCAT_2
- [ 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; definitions STRUCT_0, PBOOLE, MSUALG_1, ALTCAT_1, PRALG_1, FUNCT_1, RELAT_1, TARSKI; theorems MCART_1, ALTCAT_1, PBOOLE, TARSKI, GRFUNC_1, ZFMISC_1, MULTOP_1, BINOP_1, RELAT_1, FUNCT_2, CQC_LANG, STRUCT_0, FUNCOP_1, FUNCT_4, MSUALG_1, FUNCT_1, FUNCT_3, MSUALG_3, DOMAIN_1, MSSUBFAM, AUTALG_1, FUNCT_7, PRALG_1, CAT_1, RELSET_1, XBOOLE_0, XBOOLE_1; schemes ALTCAT_1, FUNCT_1; begin :: Preliminaries reserve e for set; theorem for X1,X2 being set, a1,a2 being set holds [:X1 -->a1,X2-->a2:] = [:X1,X2:] --> [a1,a2] proof let X1,X2 be set, a1,a2 be set; A1: dom(X1 -->a1) = X1 & dom(X2-->a2) = X2 by FUNCOP_1:19; then A2: dom([:X1,X2:] --> [a1,a2]) = [:dom(X1 -->a1), dom(X2-->a2):] by FUNCOP_1:19; now let x,y be set; assume A3: x in dom(X1-->a1) & y in dom(X2-->a2); then A4: (X1-->a1).x = a1 & (X2-->a2).y = a2 by A1,FUNCOP_1:13; [x,y] in dom([:X1,X2:] --> [a1,a2]) by A2,A3,ZFMISC_1:106; then [x,y] in [:X1,X2:] by FUNCOP_1:19; hence ([:X1,X2:] --> [a1,a2]).[x,y] = [(X1-->a1).x,(X2-->a2).y] by A4,FUNCOP_1:13; end; hence [:X1 -->a1,X2-->a2:] = [:X1,X2:] --> [a1,a2] by A2,FUNCT_3:def 9; end; definition let I be set; cluster [0]I -> Function-yielding; coherence proof let x be set; assume x in dom[0]I; then x in I by PBOOLE:def 3; hence [0]I.x is Function by PBOOLE:5; end; end; theorem for f,g being Function holds ~(g*f) = g*~f proof let f,g be Function; A1: now let x be set; hereby assume A2: x in dom(g*~f); then x in dom~f by FUNCT_1:21; then consider y1,z1 being set such that A3: x = [z1,y1] and A4: [y1,z1] in dom f by FUNCT_4:def 2; take y1,z1; thus x = [z1,y1] by A3; ~f.x in dom g by A2,FUNCT_1:21; then f.[y1,z1] in dom g by A3,A4,FUNCT_4:def 2; hence [y1,z1] in dom(g*f) by A4,FUNCT_1:21; end; given y,z being set such that A5: x = [z,y] and A6: [y,z] in dom(g*f); A7: [y,z] in dom f by A6,FUNCT_1:21; f.[y,z] in dom g by A6,FUNCT_1:21; then A8: ~f.x in dom g by A5,A7,FUNCT_4:def 2; x in dom ~f by A5,A7,FUNCT_4:def 2; hence x in dom(g*~f) by A8,FUNCT_1:21; end; now let y,z be set; assume A9: [y,z] in dom(g*f); then [y,z] in dom f by FUNCT_1:21; then A10: [z,y] in dom ~f by FUNCT_4:43; hence (g*~f).[z,y] = g.(~f.[z,y]) by FUNCT_1:23 .= g.(f.[y,z]) by A10,FUNCT_4:44 .= (g*f).[y,z] by A9,FUNCT_1:22; end; hence ~(g*f) = g*~f by A1,FUNCT_4:def 2; end; theorem for f,g,h being Function holds ~(f*[:g,h:]) = ~f*[:h,g:] proof let f,g,h be Function; A1: now let x be set; hereby assume A2: x in dom(~f*[:h,g:]); then x in dom[:h,g:] by FUNCT_1:21; then x in [:dom h, dom g:] by FUNCT_3:def 9; then consider y1,z1 being set such that A3: y1 in dom h and A4: z1 in dom g and A5: x = [y1,z1] by ZFMISC_1:103; take z1,y1; thus x = [y1,z1] by A5; dom[:g,h:] = [:dom g,dom h:] by FUNCT_3:def 9; then A6: [z1,y1] in dom[:g,h:] by A3,A4,ZFMISC_1:106; A7: [:h,g:].x = [h.y1,g.z1] by A3,A4,A5,FUNCT_3:def 9; A8: [:g,h:].[z1,y1] = [g.z1,h.y1] by A3,A4,FUNCT_3:def 9; [:h,g:].x in dom~f by A2,FUNCT_1:21; then [:g,h:].[z1,y1] in dom f by A7,A8,FUNCT_4:43; hence [z1,y1] in dom(f*[:g,h:]) by A6,FUNCT_1:21; end; given y,z being set such that A9: x = [z,y] and A10: [y,z] in dom(f*[:g,h:]); A11: [y,z] in dom [:g,h:] by A10,FUNCT_1:21; dom [:g,h:] = [:dom g, dom h:] by FUNCT_3:def 9; then A12: y in dom g & z in dom h by A11,ZFMISC_1:106; dom[:h,g:] = [:dom h, dom g:] by FUNCT_3:def 9; then A13: x in dom[:h,g:] by A9,A12,ZFMISC_1:106; A14: [:g,h:].[y,z] = [g.y,h.z] by A12,FUNCT_3:def 9; A15: [:h,g:].x = [h.z,g.y] by A9,A12,FUNCT_3:def 9; [:g,h:].[y,z] in dom f by A10,FUNCT_1:21; then [:h,g:].x in dom~f by A14,A15,FUNCT_4:43; hence x in dom(~f*[:h,g:]) by A13,FUNCT_1:21; end; now let y,z be set; assume A16: [y,z] in dom(f*[:g,h:]); then [y,z] in dom[:g,h:] by FUNCT_1:21; then [y,z] in [:dom g, dom h:] by FUNCT_3:def 9; then A17: y in dom g & z in dom h by ZFMISC_1:106; [:g,h:].[y,z] in dom f by A16,FUNCT_1:21; then A18: [g.y,h.z] in dom f by A17,FUNCT_3:def 9; [z,y] in [:dom h, dom g:] by A17,ZFMISC_1:106; then [z,y] in dom[:h,g:] by FUNCT_3:def 9; hence (~f*[:h,g:]).[z,y] = ~f.([:h,g:].[z,y]) by FUNCT_1:23 .= ~f.[h.z,g.y] by A17,FUNCT_3:def 9 .= f.[g.y,h.z] by A18,FUNCT_4:def 2 .= f.([:g,h:].[y,z]) by A17,FUNCT_3:def 9 .= (f*[:g,h:]).[y,z] by A16,FUNCT_1:22; end; hence ~(f*[:g,h:]) = ~f*[:h,g:] by A1,FUNCT_4:def 2; end; definition let f be Function-yielding Function; cluster ~f -> Function-yielding; coherence proof let x be set; assume x in dom~f; then consider z,y being set such that A1: x = [y,z] and A2: [z,y] in dom f by FUNCT_4:def 2; f.[z,y] = (~f).x by A1,A2,FUNCT_4:def 2; hence (~f).x is Function; end; end; theorem 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 proof let I be set, A,B,C be ManySortedSet of I such that A1: A is_transformable_to B; let F be ManySortedFunction of A,B, G be ManySortedFunction of B,C; reconsider GF = G**F as ManySortedFunction of I by MSSUBFAM:15; GF is ManySortedFunction of A,C proof let i be set; assume A2: i in I; then A3: B.i = {} implies A.i = {} by A1,AUTALG_1:def 4; reconsider Gi = G.i as Function of B.i,C.i by A2,MSUALG_1:def 2; reconsider Fi = F.i as Function of A.i,B.i by A2,MSUALG_1:def 2; i in dom GF by A2,PBOOLE:def 3; then (G**F).i = (Gi)*(Fi) by MSUALG_3:def 4; hence GF.i is Function of A.i,C.i by A3,FUNCT_2:19; end; hence thesis; end; definition let I be set; let A be ManySortedSet of [:I,I:]; redefine func ~A -> ManySortedSet of [:I,I:]; coherence proof thus dom~A = [:I,I:] by PBOOLE:def 3; end; end; theorem 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 proof let I1 be set, I2 be non empty set, f be Function of I1,I2, B,C be ManySortedSet of I2, G be ManySortedFunction of B,C; let i be set; assume A1: i in I1; then A2: i in dom f by FUNCT_2:def 1; then A3: B.(f.i) = (B*f).i & C.(f.i) = (C*f).i by FUNCT_1:23; f.i in I2 by A1,FUNCT_2:7; then G.(f.i) is Function of B.(f.i),C.(f.i) by MSUALG_1:def 2; hence (G*f).i is Function of (B*f).i, (C*f).i by A2,A3,FUNCT_1:23; end; 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; coherence proof reconsider G = ~F as ManySortedSet of [:I,I:]; :: dlaczego ten "reconsider" jest potrzebny ??? G is ManySortedFunction of ~A,~B proof let ii be set; assume ii in [:I,I:]; then consider i1,i2 being set such that A1: i1 in I & i2 in I and A2: ii = [i1,i2] by ZFMISC_1:103; A3: [i2,i1] in [:I,I:] by A1,ZFMISC_1:106; dom F = [:I,I:] by PBOOLE:def 3; then A4: F.[i2,i1] = G.ii by A2,A3,FUNCT_4:def 2; dom A = [:I,I:] by PBOOLE:def 3; then A5: A.[i2,i1] = ~A.ii by A2,A3,FUNCT_4:def 2; dom B = [:I,I:] by PBOOLE:def 3; then B.[i2,i1] = ~B.ii by A2,A3,FUNCT_4:def 2; hence G.ii is Function of ~A.ii, ~B.ii by A3,A4,A5,MSUALG_1:def 2; end; hence thesis; end; end; theorem 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) proof let I1,I2 be non empty set, M be ManySortedSet of [:I1,I2:], o1 be Element of I1, o2 be Element of I2; [o1,o2] in [:I1,I2:] by ZFMISC_1:106; then A1: [o1,o2] in dom M by PBOOLE:def 3; thus (~M).(o2,o1) = (~M).[o2,o1] by BINOP_1:def 1 .= M.[o1,o2] by A1,FUNCT_4:def 2 .= M.(o1,o2) by BINOP_1:def 1; end; definition let I1 be set, f,g be ManySortedFunction of I1; redefine func g**f -> ManySortedFunction of I1; coherence proof A1: dom f = I1 & dom g = I1 by PBOOLE:def 3; dom(g**f) = dom g /\ dom f by MSUALG_3:def 4 .= I1 by A1; hence thesis by PBOOLE:def 3; end; end; begin :: An auxiliary notion definition let f,g be Function; pred f cc= g means :Def1: 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 :Def2: I c= J & for i being set st i in I holds A.i c= B.i; compatibility proof A1: dom A = I & dom B = J by PBOOLE:def 3; hence A cc= B implies I c= J & for i being set st i in I holds A.i c= B.i by Def1; assume that A2: I c= J and A3: for i being set st i in I holds A.i c= B.i; thus dom A c= dom B by A1,A2; let i be set; assume i in dom A; hence A.i c= B.i by A1,A3; end; end; canceled; theorem Th8: 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 proof let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J; assume that A1: A cc= B and A2: B cc= A; A3: I c= J & J c= I by A1,A2,Def2; then reconsider B' = B as ManySortedSet of I by XBOOLE_0:def 10; now let i be set; assume i in I; then A.i c= B.i & B.i c= A.i by A1,A2,A3,Def2; hence A.i = B'.i by XBOOLE_0:def 10; end; hence thesis by PBOOLE:3; end; theorem Th9: 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 proof let I,J,K be set, A be ManySortedSet of I, B be ManySortedSet of J, C be ManySortedSet of K; assume that A1: A cc= B and A2: B cc= C; A3: I c= J by A1,Def2; J c= K by A2,Def2; hence I c= K by A3,XBOOLE_1:1; let i be set; assume i in I; then A.i c= B.i & B.i c= C.i by A1,A2,A3,Def2; hence thesis by XBOOLE_1:1; end; theorem for I being set, A being ManySortedSet of I, B being ManySortedSet of I holds A cc= B iff A c= B proof let I be set, A be ManySortedSet of I, B be ManySortedSet of I; thus A cc= B implies A c= B proof assume A1: A cc= B; let i be set; thus thesis by A1,Def2; end; assume A2: A c= B; thus I c= I; thus thesis by A2,PBOOLE:def 5; end; 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 proof set f = { [o,F(o)] where o is Element of X(): P[o] }; A1: f is Relation-like proof let x be set; assume x in f; then consider o being Element of X() such that A2: x = [o,F(o)] and P[o]; take o,F(o); thus x = [o,F(o)] by A2; end; f is Function-like proof let x,y1,y2 be set; assume [x,y1] in f; then consider o1 being Element of X() such that A3: [x,y1] = [o1,F(o1)] and P[o1]; assume [x,y2] in f; then consider o2 being Element of X() such that A4: [x,y2] = [o2,F(o2)] and P[o2]; o1 = x & o2 = x by A3,A4,ZFMISC_1:33; hence y1 = y2 by A3,A4,ZFMISC_1:33; end; hence f is Function by A1; end; 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 A1: f() = { [o,F(o)] where o is Element of X(): P[o] } proof set A = { o where o is Element of X(): P[o]}; now let x be set; hereby assume x in A; then consider o being Element of X() such that A2: x = o and A3: P[o]; take y = F(o); thus [x,y] in f() by A1,A2,A3; end; given y being set such that A4: [x,y] in f(); consider o being Element of X() such that A5: [x,y] = [o,F(o)] and A6: P[o] by A1,A4; x = o by A5,ZFMISC_1:33; hence x in A by A6; end; hence dom f() = A by RELAT_1:def 4; end; scheme ValOnSingletons {X()-> non empty set,f()-> Function, x()-> Element of X(), F(set)-> set, P[set]}: f().x() = F(x()) provided A1: f() = { [o,F(o)] where o is Element of X(): P[o] } and A2: P[x()] proof deffunc _F(set) = F($1); defpred _P[set] means P[($1)]; A3: f() = { [o,_F(o)] where o is Element of X(): _P[o] } by A1; dom f() = { o where o is Element of X(): _P[o] } from DomOnSingletons(A3); then A4: x() in dom f() by A2; [x(),F(x())] in { [o,F(o)] where o is Element of X(): P[o] } by A2; hence thesis by A1,A4,FUNCT_1:def 4; end; begin :: More on old categories theorem Th11: for C being Category, i,j,k being Object of C holds [:Hom(j,k),Hom(i,j):] c= dom the Comp of C proof let C be Category, i,j,k be Object of C; let e be set; assume A1: e in [:Hom(j,k),Hom(i,j):]; then A2: e`1 in Hom(j,k) & e`2 in Hom(i,j) by MCART_1:10; reconsider y = e`1, x = e`2 as Morphism of C by A1,MCART_1:10; A3: e = [y,x] by A1,MCART_1:23; dom y = j by A2,CAT_1:18 .= cod x by A2,CAT_1:18; hence e in dom the Comp of C by A3,CAT_1:40; end; theorem Th12: 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) proof let C be Category, i,j,k be Object of C; let e be set; assume e in (the Comp of C).:[:Hom(j,k),Hom(i,j):]; then consider x being set such that A1: x in dom the Comp of C and A2: x in [:Hom(j,k),Hom(i,j):] and A3: e = (the Comp of C).x by FUNCT_1:def 12; A4: x`1 in Hom(j,k) & x`2 in Hom(i,j) by A2,MCART_1:10; reconsider y = x`1, z = x`2 as Morphism of C by A2,MCART_1:10; A5: x = [y,z] by A2,MCART_1:23; y is Morphism of j,k & z is Morphism of i,j by A4,CAT_1:def 7; then y*z in Hom(i,k) by A4,CAT_1:51; hence e in Hom(i,k) by A1,A3,A5,CAT_1:def 4; end; definition let C be CatStr; func the_hom_sets_of C -> ManySortedSet of [:the Objects of C, the Objects of C:] means :Def3: for i,j being Object of C holds it.(i,j) = Hom(i,j); existence proof deffunc _H(Object of C, Object of C) = Hom($1,$2); thus ex M being ManySortedSet of [:the Objects of C, the Objects of C:] st for i,j being Object of C holds M.(i,j) = _H(i,j) from MSSLambda2D; end; uniqueness proof let M1,M2 be ManySortedSet of [:the Objects of C, the Objects of C:] such that A1: for i,j being Object of C holds M1.(i,j) = Hom(i,j) and A2: for i,j being Object of C holds M2.(i,j) = Hom(i,j); now let i,j be Object of C; thus M1.(i,j) = Hom(i,j) by A1 .= M2.(i,j) by A2; end; hence thesis by ALTCAT_1:9; end; end; theorem Th13: for C be Category, i be Object of C holds id i in (the_hom_sets_of C).(i,i) proof let C be Category, i be Object of C; id i in Hom(i,i) by CAT_1:55; hence id i in (the_hom_sets_of C).(i,i) by Def3; end; definition let C be Category; func the_comps_of C -> BinComp of the_hom_sets_of C means :Def4: 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):]; existence proof set Ob3 = [:the Objects of C,the Objects of C,the Objects of C:], G = the_hom_sets_of C; deffunc _F(set) = (the Comp of C)| [:(the_hom_sets_of C).($1`1`2,$1`2), (the_hom_sets_of C).($1`1`1,$1`1`2):]; consider o being Function such that A1: dom o = Ob3 and A2: for e st e in Ob3 holds o.e = _F(e) from Lambda; reconsider o as ManySortedSet of Ob3 by A1,PBOOLE:def 3; now let e; assume e in dom o; then o.e = (the Comp of C)| [:(the_hom_sets_of C).(e`1`2,e`2),(the_hom_sets_of C).(e`1`1,e`1`2):] by A1,A2; hence o.e is Function; end; then reconsider o as ManySortedFunction of Ob3 by PRALG_1:def 15; now let e; assume A3: e in Ob3; reconsider f = o.e as Function; consider i,j,k being Object of C such that A4: e = [i,j,k] by A3,DOMAIN_1:15; reconsider e' = e as Element of Ob3 by A3; A5: [i,j,k] qua set `1`1 = e'`1 by A4,MCART_1:50 .= i by A4,MCART_1:47; A6: [i,j,k] qua set `1`2 = e'`2 by A4,MCART_1:50 .= j by A4,MCART_1:47; A7: [i,j,k] qua set `2 = e'`3 by A4,MCART_1:50 .= k by A4,MCART_1:47; A8: G.(i,j) = Hom(i,j) & G.(j,k) = Hom(j,k) by Def3; A9: f = (the Comp of C)|[:G.(j,k),G.(i,j):] by A2,A3,A4,A5,A6,A7; A10: {|G|}.e = {|G|}.(i,j,k) by A4,MULTOP_1:def 1 .= G.(i,k) by ALTCAT_1:def 5 .= Hom(i,k) by Def3; A11: {|G,G|}.e = {|G,G|}.(i,j,k) by A4,MULTOP_1:def 1 .= [:Hom(j,k),Hom(i,j):] by A8,ALTCAT_1:def 6; A12: now assume {|G|}.e = {}; then Hom(i,j) = {} or Hom(j,k) = {} by A10,CAT_1:52; hence {|G,G|}.e = {} by A11,ZFMISC_1:113; end; [:Hom(j,k),Hom(i,j):] c= dom the Comp of C by Th11; then A13: dom f = {|G,G|}.e by A8,A9,A11,RELAT_1:91; (the Comp of C).:[:Hom(j,k),Hom(i,j):] c= Hom(i,k) by Th12; then rng f c= {|G|}.e by A8,A9,A10,RELAT_1:148; hence o.e is Function of {|G,G|}.e,{|G|}.e by A12,A13,FUNCT_2:def 1, RELSET_1:11; end; then reconsider o as BinComp of G by MSUALG_1:def 2; take o; let i,j,k be Object of C; A14: [i,j,k] in Ob3 by DOMAIN_1:15; reconsider e = [i,j,k] as Element of Ob3 by DOMAIN_1:15; A15: [i,j,k] qua set `1`1 = e`1 by MCART_1:50 .= i by MCART_1:47; A16: [i,j,k] qua set `1`2 = e`2 by MCART_1:50 .= j by MCART_1:47; A17: [i,j,k] qua set `2 = e`3 by MCART_1:50 .= k by MCART_1:47; thus o.(i,j,k) = o.[i,j,k] by MULTOP_1:def 1 .= (the Comp of C)| [:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):] by A2,A14,A15,A16,A17; end; uniqueness proof let o1,o2 be BinComp of the_hom_sets_of C such that A18: for i,j,k being Object of C holds o1.(i,j,k) = (the Comp of C)|[:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):] and A19: for i,j,k being Object of C holds o2.(i,j,k) = (the Comp of C)|[:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):]; now let a be set; assume a in [:the Objects of C,the Objects of C,the Objects of C:]; then consider i,j,k being Object of C such that A20: a = [i,j,k] by DOMAIN_1:15; thus o1.a = o1.(i,j,k) by A20,MULTOP_1:def 1 .= (the Comp of C)| [:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):] by A18 .= o2.(i,j,k) by A19 .= o2.a by A20,MULTOP_1:def 1; end; hence o1 = o2 by PBOOLE:3; end; end; theorem Th14: 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 proof let C be Category, i,j,k be Object of C such that A1: Hom(i,j) <> {} and A2: Hom(j,k) <> {}; let f be Morphism of i,j, g be Morphism of j,k; A3: f in Hom(i,j) by A1,CAT_1:def 7; A4: g in Hom(j,k) by A2,CAT_1:def 7; then A5: dom g = j by CAT_1:18 .= cod f by A3,CAT_1:18; A6: f in (the_hom_sets_of C).(i,j) by A3,Def3; g in (the_hom_sets_of C).(j,k) by A4,Def3; then A7: [g,f] in [:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):] by A6,ZFMISC_1:106; thus (the_comps_of C).(i,j,k).(g,f) = ((the Comp of C)|[:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):]) .(g,f) by Def4 .= ((the Comp of C)|[:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):]) .[g,f] by BINOP_1:def 1 .= (the Comp of C).[g,f] by A7,FUNCT_1:72 .= g*(f qua Morphism of C) by A5,CAT_1:41 .= g*f by A1,A2,CAT_1:def 13; end; theorem Th15: for C being Category holds the_comps_of C is associative proof let C be Category; let i,j,k,l be Object of C; let f,g,h be set; assume f in (the_hom_sets_of C).(i,j); then A1: f in Hom(i,j) by Def3; then reconsider f' = f as Morphism of i,j by CAT_1:def 7; assume g in (the_hom_sets_of C).(j,k); then A2: g in Hom(j,k) by Def3; then reconsider g' = g as Morphism of j,k by CAT_1:def 7; assume h in (the_hom_sets_of C).(k,l); then A3: h in Hom(k,l) by Def3; then reconsider h' = h as Morphism of k,l by CAT_1:def 7; A4: Hom(i,k) <> {} by A1,A2,CAT_1:52; A5: Hom(j,l) <> {} by A2,A3,CAT_1:52; A6: (the_comps_of C).(i,j,k).(g,f) = g'*f' by A1,A2,Th14; A7: (the_comps_of C).(j,k,l).(h,g) = h'*g' by A2,A3,Th14; thus (the_comps_of C).(i,k,l).(h,(the_comps_of C).(i,j,k).(g,f)) = h'*(g'*f') by A3,A4,A6,Th14 .= h'*g'*f' by A1,A2,A3,CAT_1:54 .= (the_comps_of C).(i,j,l).((the_comps_of C).(j,k,l).(h,g),f) by A1,A5,A7,Th14; end; theorem Th16: for C being Category holds the_comps_of C is with_left_units with_right_units proof let C be Category; thus the_comps_of C is with_left_units proof let i be Object of C; take id i; thus id i in (the_hom_sets_of C).(i,i) by Th13; A1: Hom(i,i) <> {} by CAT_1:56; let j be Object of C, f be set; assume f in (the_hom_sets_of C).(j,i); then A2: f in Hom(j,i) by Def3; then reconsider m = f as Morphism of j,i by CAT_1:def 7; thus (the_comps_of C).(j,i,i).(id i,f) = (id i)*m by A1,A2,Th14 .= f by A2,CAT_1:57; end; let j be Object of C; take id j; thus id j in (the_hom_sets_of C).(j,j) by Th13; A3: Hom(j,j) <> {} by CAT_1:56; let i be Object of C, f be set; assume f in (the_hom_sets_of C).(j,i); then A4: f in Hom(j,i) by Def3; then reconsider m = f as Morphism of j,i by CAT_1:def 7; thus (the_comps_of C).(j,j,i).(f,id j) = m*(id j) by A3,A4,Th14 .= f by A4,CAT_1:58; end; begin :: Transforming an old category into new one definition let C be Category; func Alter C -> strict non empty AltCatStr equals :Def5: AltCatStr(#the Objects of C,the_hom_sets_of C, the_comps_of C#); correctness; end; theorem Th17: for C being Category holds Alter C is associative proof let C be Category; Alter C = AltCatStr(#the Objects of C,the_hom_sets_of C, the_comps_of C#) by Def5; hence the Comp of Alter C is associative by Th15; end; theorem Th18: for C being Category holds Alter C is with_units proof let C be Category; Alter C = AltCatStr(#the Objects of C,the_hom_sets_of C, the_comps_of C#) by Def5; hence the Comp of Alter C is with_left_units with_right_units by Th16; end; theorem Th19: for C being Category holds Alter C is transitive proof let C be Category; A1: Alter C = AltCatStr(#the Objects of C,the_hom_sets_of C, the_comps_of C#) by Def5; let o1,o2,o3 be object of Alter C such that A2: <^o1,o2^> <> {} & <^o2,o3^> <> {}; reconsider x1 = o1, x2 = o2, x3 = o3 as Object of C by A1; A3: <^o1,o2^> = (the_hom_sets_of C).(x1,x2) by A1,ALTCAT_1:def 2 .= Hom(x1,x2) by Def3; A4: <^o2,o3^> = (the_hom_sets_of C).(x2,x3) by A1,ALTCAT_1:def 2 .= Hom(x2,x3) by Def3; <^o1,o3^> = (the_hom_sets_of C).(x1,x3) by A1,ALTCAT_1:def 2 .= Hom(x1,x3) by Def3; hence <^o1,o3^> <> {} by A2,A3,A4,CAT_1:52; end; definition let C be Category; cluster Alter C -> transitive associative with_units; coherence by Th17,Th18,Th19; end; begin :: More on new categories definition cluster non empty strict AltGraph; existence proof consider M being ManySortedSet of [:1,1:]; take A = AltGraph(#1,M#); thus the carrier of A is non empty; thus thesis; end; end; definition let C be AltGraph; attr C is reflexive means :Def6: 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 for o being object of C holds <^o,o^> <> {}; compatibility proof hereby assume A1: C is reflexive; let o be object of C; <^o,o^> = (the Arrows of C).(o,o) by ALTCAT_1:def 2; hence <^o,o^> <> {} by A1,Def6; end; assume A2: for o being object of C holds <^o,o^> <> {}; let x be set; assume x in the carrier of C; then reconsider o=x as object of C; (the Arrows of C).(x,x) = <^o,o^> by ALTCAT_1:def 2; hence (the Arrows of C).(x,x) <> {} by A2; thus thesis; end; end; definition let C be non empty transitive AltCatStr; redefine attr C is associative means :Def8: 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); compatibility proof thus C is associative implies 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) by ALTCAT_1:25; assume A1: 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); let i,j,k,l be Element of C; reconsider o1=i, o2=j, o3=k, o4=l as object of C; let f,g,h be set; assume f in (the Arrows of C).(i,j); then A2: f in <^o1,o2^> by ALTCAT_1:def 2; then reconsider ff = f as Morphism of o1,o2 ; assume g in (the Arrows of C).(j,k); then A3: g in <^o2,o3^> by ALTCAT_1:def 2; then reconsider gg = g as Morphism of o2,o3 ; assume h in (the Arrows of C).(k,l); then A4: h in <^o3,o4^> by ALTCAT_1:def 2; then reconsider hh = h as Morphism of o3,o4 ; A5: <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 4; A6: <^o2,o4^> <> {} by A3,A4,ALTCAT_1:def 4; A7:(the Comp of C).(j,k,l).(h,g) = hh*gg by A3,A4,ALTCAT_1:def 10; (the Comp of C).(i,j,k).(g,f) = gg*ff by A2,A3,ALTCAT_1:def 10; hence (the Comp of C).(i,k,l).(h,(the Comp of C).(i,j,k).(g,f)) = hh*(gg*ff) by A4,A5,ALTCAT_1:def 10 .= hh*gg*ff by A1,A2,A3,A4 .= (the Comp of C).(i,j,l).((the Comp of C).(j,k,l).(h,g),f) by A2,A6,A7,ALTCAT_1:def 10; end; end; definition let C be non empty AltCatStr; redefine attr C is with_units means 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''); compatibility proof hereby assume A1: C is with_units; then reconsider C' = C as with_units (non empty AltCatStr); let o be object of C; thus <^o,o^> <> {} by A1,ALTCAT_1:21; reconsider p = o as object of C'; reconsider i = idm p as Morphism of o,o; take i; let o' be object of C, m' be Morphism of o',o, m'' be Morphism of o,o'; thus <^o',o^> <> {} implies i*m' = m' by ALTCAT_1:24; thus <^o,o'^> <> {} implies m''*i = m'' by ALTCAT_1:def 19; end; assume A2: 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''); hereby let j be Element of C; reconsider o = j as object of C; consider m being Morphism of o,o such that A3: for o' being object of C, m' being Morphism of o',o, m'' being Morphism of o,o' holds (<^o',o^> <> {} implies m*m' = m') & (<^o,o'^> <> {} implies m''*m = m'') by A2; reconsider e = m as set; take e; A4: <^o,o^> <> {} by A2; then m in <^o,o^>; hence e in (the Arrows of C).(j,j) by ALTCAT_1:def 2; let i be Element of C, f be set such that A5: f in (the Arrows of C).(i,j); reconsider o' = i as object of C; A6: f in <^o',o^> by A5,ALTCAT_1:def 2; then reconsider m' = f as Morphism of o',o ; thus (the Comp of C).(i,j,j).(e,f) = m*m' by A4,A6,ALTCAT_1:def 10 .= f by A3,A6; end; let i be Element of C; reconsider o = i as object of C; consider m being Morphism of o,o such that A7: for o' being object of C, m' being Morphism of o',o, m'' being Morphism of o,o' holds (<^o',o^> <> {} implies m*m' = m') & (<^o,o'^> <> {} implies m''*m = m'') by A2; take e = m; A8: <^o,o^> <> {} by A2; then m in <^o,o^>; hence e in (the Arrows of C).(i,i) by ALTCAT_1:def 2; let j be Element of C, f be set such that A9: f in (the Arrows of C).(i,j); reconsider o' = j as object of C; A10: f in <^o,o'^> by A9,ALTCAT_1:def 2; then reconsider m' = f as Morphism of o,o' ; thus (the Comp of C).(i,i,j).(f,e) = m'*m by A8,A10,ALTCAT_1:def 10 .= f by A7,A10; end; end; definition cluster with_units -> reflexive (non empty AltCatStr); coherence proof let C be non empty AltCatStr; assume A1: C is with_units; let o be object of C; thus <^o,o^> <> {} by A1,ALTCAT_1:21; end; end; definition cluster non empty reflexive AltGraph; existence proof consider C being with_units (non empty AltCatStr); take C; thus thesis; end; end; definition cluster non empty reflexive AltCatStr; existence proof consider C being category; take C; thus thesis; end; end; begin :: The empty category Lm1: for E1,E2 being strict AltCatStr st the carrier of E1 is empty & the carrier of E2 is empty holds E1 = E2 proof let E1,E2 be strict AltCatStr; set C1 = the carrier of E1, C2 = the carrier of E2; assume A1: C1 is empty & C2 is empty; then A2: [:C2,C2:] = {} by ZFMISC_1:113; [:C1,C1:] = {} by A1,ZFMISC_1:113; then A3: the Arrows of E1 = {} by PBOOLE:134 .= the Arrows of E2 by A2,PBOOLE:134; A4: [:C2,C2,C2:] = {} by A1,MCART_1:35; [:C1,C1,C1:] = {} by A1,MCART_1:35; then the Comp of E1 = {} by PBOOLE:134 .= the Comp of E2 by A4,PBOOLE:134; hence E1 = E2 by A1,A3; end; definition func the_empty_category -> strict AltCatStr means :Def10: the carrier of it is empty; existence proof reconsider a = {} as set; consider m being ManySortedSet of [:a,a:]; consider c being BinComp of m; take AltCatStr(#a,m,c#); thus thesis; end; uniqueness by Lm1; end; definition cluster the_empty_category -> empty; coherence proof the carrier of the_empty_category is empty by Def10; hence the_empty_category is empty by STRUCT_0:def 1; end; end; definition cluster empty strict AltCatStr; existence proof take the_empty_category; thus thesis; end; end; theorem for E being empty strict AltCatStr holds E = the_empty_category proof let E be empty strict AltCatStr; the carrier of E is empty & the carrier of the_empty_category is empty by STRUCT_0:def 1; hence E = the_empty_category by Lm1; end; begin :: Subcategories :: Semadeni Wiweger 1.6.1 str. 24 definition let C be AltCatStr; mode SubCatStr of C -> AltCatStr means :Def11: 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; existence; end; reserve C,C1,C2,C3 for AltCatStr; theorem Th21: C is SubCatStr of C proof thus the carrier of C c= the carrier of C; thus the Arrows of C cc= the Arrows of C & the Comp of C cc= the Comp of C; end; theorem C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3 proof assume the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 & the Comp of C1 cc= the Comp of C2 & the carrier of C2 c= the carrier of C3 & the Arrows of C2 cc= the Arrows of C3 & the Comp of C2 cc= the Comp of C3; hence the carrier of C1 c= the carrier of C3 & the Arrows of C1 cc= the Arrows of C3 & the Comp of C1 cc= the Comp of C3 by Th9,XBOOLE_1:1; end; theorem Th23: 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 proof let C1,C2 be AltCatStr; assume the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the Arrows of C2 & the Comp of C1 cc= the Comp of C2 & the carrier of C2 c= the carrier of C1 & the Arrows of C2 cc= the Arrows of C1 & the Comp of C2 cc= the Comp of C1; then the carrier of C1 = the carrier of C2 & the Arrows of C1 = the Arrows of C2 & the Comp of C1 = the Comp of C2 by Th8,XBOOLE_0:def 10; hence thesis; end; definition let C be AltCatStr; cluster strict SubCatStr of C; existence proof set D = the AltCatStr of C; reconsider D as SubCatStr of C by Def11; take D; thus thesis; end; end; definition let C be non empty AltCatStr, o be object of C; func ObCat o -> strict SubCatStr of C means :Def12: 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); existence proof set a = (o,o):-> <^o,o^>; dom a = [:{o},{o}:] by FUNCT_2:def 1; then reconsider a as ManySortedSet of [:{o},{o}:] by PBOOLE:def 3; set m = [o,o,o] .--> (the Comp of C).(o,o,o); dom m = {[o,o,o]} by CQC_LANG:5 .= [:{o},{o},{o}:] by MCART_1:39; then reconsider m as ManySortedSet of [:{o},{o},{o}:] by PBOOLE:def 3; A1: a.(o,o) = <^o,o^> by ALTCAT_1:12 .= (the Arrows of C).(o,o) by ALTCAT_1:def 2; m is ManySortedFunction of {|a,a|},{|a|} proof let i be set; assume i in [:{o},{o},{o}:]; then i in {[o,o,o]} by MCART_1:39; then A2: i = [o,o,o] by TARSKI:def 1; A3: o in {o} by TARSKI:def 1; A4: {|a,a|}.i = {|a,a|}.(o,o,o) by A2,MULTOP_1:def 1 .= [:(the Arrows of C).(o,o),(the Arrows of C).(o,o):] by A1,A3,ALTCAT_1:def 6; {|a|}.i = {|a|}.(o,o,o) by A2,MULTOP_1:def 1 .= (the Arrows of C).(o,o) by A1,A3,ALTCAT_1:def 5; hence m.i is Function of {|a,a|}.i, {|a|}.i by A2,A4,CQC_LANG:6; end; then reconsider m as BinComp of a; set D = AltCatStr(#{o},a,m#); D is SubCatStr of C proof thus the carrier of D c= the carrier of C; thus the Arrows of D cc= the Arrows of C proof thus [:the carrier of D,the carrier of D:] c= [:the carrier of C,the carrier of C:]; let i be set; assume i in [:the carrier of D,the carrier of D:]; then i in {[o,o]} by ZFMISC_1:35; then A5: i = [o,o] by TARSKI:def 1; then (the Arrows of D).i = a.(o,o) by BINOP_1:def 1; hence (the Arrows of D).i c= (the Arrows of C).i by A1,A5,BINOP_1:def 1 ; end; thus [:the carrier of D,the carrier of D,the carrier of D:] c= [:the carrier of C,the carrier of C,the carrier of C:]; let i be set; assume i in [:the carrier of D,the carrier of D,the carrier of D:]; then i in {[o,o,o]} by MCART_1:39; then A6: i = [o,o,o] by TARSKI:def 1; then (the Comp of D).i = (the Comp of C).(o,o,o) by CQC_LANG:6 .= (the Comp of C).i by A6,MULTOP_1:def 1; hence (the Comp of D).i c= (the Comp of C).i; end; then reconsider D as strict SubCatStr of C; take D; thus thesis; end; uniqueness; end; reserve C for non empty AltCatStr, o for object of C; theorem Th24: for o' being object of ObCat o holds o' = o proof let o' be object of ObCat o; the carrier of ObCat o = {o} by Def12; hence o' = o by TARSKI:def 1; end; definition let C be non empty AltCatStr, o be object of C; cluster ObCat o -> transitive non empty; coherence proof thus ObCat o is transitive proof let o1,o2,o3 be object of ObCat o; assume A1: <^o1,o2^> <> {} & <^o2,o3^> <> {}; o1 = o & o2 = o by Th24; hence <^o1,o3^> <> {} by A1; end; the carrier of ObCat o = {o} by Def12; hence the carrier of ObCat o is non empty; end; end; definition let C be non empty AltCatStr; cluster transitive non empty strict SubCatStr of C; existence proof consider o being object of C; take ObCat o; thus thesis; end; end; theorem Th25: 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 proof let C be transitive non empty AltCatStr, D1,D2 be transitive non empty SubCatStr of C such that A1: the carrier of D1 c= the carrier of D2 and A2: the Arrows of D1 cc= the Arrows of D2; thus the carrier of D1 c= the carrier of D2 by A1; thus the Arrows of D1 cc= the Arrows of D2 by A2; thus [: the carrier of D1, the carrier of D1, the carrier of D1:] c= [: the carrier of D2, the carrier of D2, the carrier of D2:] by A1,MCART_1:77; let x be set; assume A3: x in [:the carrier of D1,the carrier of D1,the carrier of D1:]; then consider i1,i2,i3 being set such that A4: i1 in the carrier of D1 & i2 in the carrier of D1 & i3 in the carrier of D1 and A5: x = [i1,i2,i3] by MCART_1:72; reconsider i1,i2,i3 as object of D1 by A4; <^i1,i3^> = {} implies <^i2,i3^> = {} or <^i1,i2^> = {} by ALTCAT_1:def 4; then A6: <^i1,i3^> = {} implies [:<^i2,i3^>,<^i1,i2^>:] = {} by ZFMISC_1: 113; reconsider c1 = (the Comp of D1).(i1,i2,i3) as Function of [:<^i2,i3^>,<^i1,i2^>:],<^i1,i3^> by ALTCAT_1:17; A7: dom c1 = [:<^i2,i3^>,<^i1,i2^>:] by A6,FUNCT_2:def 1; reconsider j1=i1, j2=i2, j3=i3 as object of D2 by A1,A4; <^j1,j3^> = {} implies <^j2,j3^> = {} or <^j1,j2^> = {} by ALTCAT_1:def 4; then A8: <^j1,j3^> = {} implies [:<^j2,j3^>,<^j1,j2^>:] = {} by ZFMISC_1: 113; reconsider c2 = (the Comp of D2).(j1,j2,j3) as Function of [:<^j2,j3^>,<^j1,j2^>:],<^j1,j3^> by ALTCAT_1:17; A9: (the Arrows of D1).[i1,i2] = (the Arrows of D1).(i1,i2) by BINOP_1:def 1 .= <^i1,i2^> by ALTCAT_1:def 2; A10: (the Arrows of D1).[i2,i3] = (the Arrows of D1).(i2,i3) by BINOP_1:def 1 .= <^i2,i3^> by ALTCAT_1:def 2; A11: (the Arrows of D2).[j1,j2] = (the Arrows of D2).(j1,j2) by BINOP_1:def 1 .= <^j1,j2^> by ALTCAT_1:def 2; A12: (the Arrows of D2).[j2,j3] = (the Arrows of D2).(j2,j3) by BINOP_1:def 1 .= <^j2,j3^> by ALTCAT_1:def 2; [i1,i2] in [:the carrier of D1,the carrier of D1:] & [i2,i3] in [:the carrier of D1,the carrier of D1:] by ZFMISC_1:106; then A13: <^i1,i2^> c= <^j1,j2^> & <^i2,i3^> c= <^j2,j3^> by A2,A9,A10,A11, A12,Def2 ; dom c2 = [:<^j2,j3^>,<^j1,j2^>:] by A8,FUNCT_2:def 1; then A14: dom c1 c= dom c2 by A7,A13,ZFMISC_1:119; A15: now let y be set; the carrier of D1 c= the carrier of C by Def11; then reconsider o1=i1, o2=i2, o3=i3 as object of C by A4; reconsider c = (the Comp of C).(o1,o2,o3) as Function of [:<^o2,o3^>,<^o1,o2^>:],<^o1,o3^> by ALTCAT_1:17; A16: c = (the Comp of C).[o1,o2,o3] by MULTOP_1:def 1; A17: [o1,o2,o3] in [:the carrier of D2,the carrier of D2,the carrier of D2:] by A1,A4,MCART_1:73; assume A18: y in dom c1; A19: the Comp of D2 cc= the Comp of C by Def11; c2 = (the Comp of D2).[o1,o2,o3] by MULTOP_1:def 1; then A20: c2 c= c by A16,A17,A19,Def2; A21: the Comp of D1 cc= the Comp of C by Def11; c1 = (the Comp of D1).[o1,o2,o3] by MULTOP_1:def 1; then c1 c= c by A3,A5,A16,A21,Def2; hence c1.y = c.y by A18,GRFUNC_1:8 .= c2.y by A14,A18,A20,GRFUNC_1:8; end; c1 = (the Comp of D1).x & c2 = (the Comp of D2).x by A5,MULTOP_1:def 1; hence (the Comp of D1).x c= (the Comp of D2).x by A14,A15,GRFUNC_1:8; end; definition let C be AltCatStr, D be SubCatStr of C; attr D is full means :Def13: 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 :Def14: 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; consistency; end; definition let C be AltCatStr; cluster full strict SubCatStr of C; existence proof set D = the AltCatStr of C; D is SubCatStr of C proof thus the carrier of D c= the carrier of C & the Arrows of D cc= the Arrows of C & the Comp of D cc= the Comp of C; end; then reconsider D as SubCatStr of C; take D; dom(the Arrows of C) =[:the carrier of D, the carrier of D:] by PBOOLE:def 3; hence the Arrows of D = (the Arrows of C)|[:the carrier of D, the carrier of D:] by RELAT_1:98; thus thesis; end; end; definition let C be non empty AltCatStr; cluster full non empty strict SubCatStr of C; existence proof set D = the AltCatStr of C; D is SubCatStr of C proof thus the carrier of D c= the carrier of C & the Arrows of D cc= the Arrows of C & the Comp of D cc= the Comp of C; end; then reconsider D as SubCatStr of C; take D; dom(the Arrows of C) =[:the carrier of D, the carrier of D:] by PBOOLE:def 3; hence the Arrows of D = (the Arrows of C)|[:the carrier of D, the carrier of D:] by RELAT_1:98; thus the carrier of D is non empty; thus thesis; end; end; definition let C be category, o be object of C; cluster ObCat o -> full id-inheriting; coherence proof A1: the carrier of ObCat o = {o} by Def12; thus ObCat o is full proof thus the Arrows of ObCat o = (o,o):-> <^o,o^> by Def12 .= (o,o):-> ((the Arrows of C).(o,o)) by ALTCAT_1:def 2 .= (the Arrows of C)|[:the carrier of ObCat o, the carrier of ObCat o:] by A1,FUNCT_7:8; end; now let o1 be object of ObCat o, o2 be object of C; A2: o1 = o by Th24; assume A3: o1 = o2; <^o1,o1^> = (the Arrows of ObCat o).(o,o) by A2,ALTCAT_1:def 2 .= ((o,o):-> <^o,o^>).(o,o) by Def12 .= <^o2,o2^> by A2,A3,ALTCAT_1:12; hence idm o2 in <^o1,o1^> by ALTCAT_1:23; end; hence thesis by Def14; end; end; definition let C be category; cluster full id-inheriting non empty strict SubCatStr of C; existence proof consider o being object of C; take ObCat o; thus thesis; end; end; reserve C for non empty transitive AltCatStr; theorem Th26: 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 proof let D be SubCatStr of C such that A1: the carrier of D = the carrier of C and A2: the Arrows of D = the Arrows of C; A3: D is non empty by A1,STRUCT_0:def 1; A4: D is transitive proof let o1,o2,o3 be object of D; reconsider p1 = o1, p2 = o2, p3 = o3 as object of C by A1; A5: <^o1,o2^> = (the Arrows of D).(o1,o2) by ALTCAT_1:def 2 .= <^p1,p2^> by A2,ALTCAT_1:def 2; A6: <^o2,o3^> = (the Arrows of D).(o2,o3) by ALTCAT_1:def 2 .= <^p2,p3^> by A2,ALTCAT_1:def 2; A7: <^o1,o3^> = (the Arrows of D).(o1,o3) by ALTCAT_1:def 2 .= <^p1,p3^> by A2,ALTCAT_1:def 2; assume <^o1,o2^> <> {} & <^o2,o3^> <> {}; hence <^o1,o3^> <> {} by A5,A6,A7,ALTCAT_1:def 4; end; C is SubCatStr of C by Th21; then C is SubCatStr of D by A1,A2,A3,A4,Th25; hence the AltCatStr of D = the AltCatStr of C by Th23; end; theorem Th27: 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 proof let D1,D2 be non empty transitive SubCatStr of C such that A1: the carrier of D1 = the carrier of D2 and A2: the Arrows of D1 = the Arrows of D2; A3: D1 is SubCatStr of D2 by A1,A2,Th25; D2 is SubCatStr of D1 by A1,A2,Th25; hence the AltCatStr of D1 = the AltCatStr of D2 by A3,Th23; end; theorem 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 proof let D be full SubCatStr of C such that A1: the carrier of D = the carrier of C; A2: dom the Arrows of C = [:the carrier of C, the carrier of C:] by PBOOLE:def 3; the Arrows of D = (the Arrows of C)|[:the carrier of D, the carrier of D:] by Def13 .= the Arrows of C by A1,A2,RELAT_1:98; hence the AltCatStr of D = the AltCatStr of C by A1,Th26; end; theorem Th29: 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^> proof let C be non empty AltCatStr, D be full non empty SubCatStr of C, o1,o2 be object of C, p1,p2 be object of D such that A1: o1 = p1 & o2 = p2; A2: [p1,p2] in [:the carrier of D, the carrier of D:] by ZFMISC_1:106; thus <^o1,o2^> = (the Arrows of C).(o1,o2) by ALTCAT_1:def 2 .= (the Arrows of C).[o1,o2] by BINOP_1:def 1 .= ((the Arrows of C)|[:the carrier of D, the carrier of D:]).[p1,p2] by A1,A2,FUNCT_1:72 .= ((the Arrows of C)|[:the carrier of D, the carrier of D:]).(p1,p2) by BINOP_1:def 1 .= (the Arrows of D).(p1,p2) by Def13 .= <^p1,p2^> by ALTCAT_1:def 2; end; theorem Th30: 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 proof let C be non empty AltCatStr, D be non empty SubCatStr of C; let o be object of D; A1: o in the carrier of D; the carrier of D c= the carrier of C by Def11; hence o is object of C by A1; end; definition let C be transitive non empty AltCatStr; cluster full non empty -> transitive SubCatStr of C; coherence proof let D be SubCatStr of C; assume A1: D is full non empty; let o1,o2,o3 be object of D such that A2: <^o1,o2^> <> {} & <^o2,o3^> <> {}; reconsider p1 = o1, p2 = o2, p3 = o3 as object of C by A1,Th30; <^p1,p2^> <> {} & <^p2,p3^> <> {} by A1,A2,Th29; then <^p1,p3^> <> {} by ALTCAT_1:def 4; hence <^o1,o3^> <> {} by A1,Th29; end; end; theorem 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 proof let D1,D2 be full non empty SubCatStr of C; assume A1: the carrier of D1 = the carrier of D2; then the Arrows of D1 =(the Arrows of C)|[:the carrier of D2, the carrier of D2:] by Def13 .= the Arrows of D2 by Def13; hence the AltCatStr of D1 = the AltCatStr of D2 by A1,Th27; end; theorem Th32: 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^> proof let C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be object of C, p1,p2 be object of D such that A1: o1 = p1 & o2 = p2; A2: [p1,p2] in [:the carrier of D, the carrier of D:] by ZFMISC_1:106; A3: <^o1,o2^> = (the Arrows of C).(o1,o2) by ALTCAT_1:def 2 .= (the Arrows of C).[o1,o2] by BINOP_1:def 1; A4: <^p1,p2^> = (the Arrows of D).(p1,p2) by ALTCAT_1:def 2 .= (the Arrows of D).[p1,p2] by BINOP_1:def 1; the Arrows of D cc= the Arrows of C by Def11; hence thesis by A1,A2,A3,A4,Def2; end; theorem Th33: 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 proof let C be non empty transitive AltCatStr, D be non empty transitive SubCatStr of C; let p1,p2,p3 be object of D such that A1: <^p1,p2^> <> {} & <^p2,p3^> <> {}; let o1,o2,o3 be object of C such that A2: o1 = p1 & o2 = p2 & o3 = p3; let f be Morphism of o1,o2, g be Morphism of o2,o3, ff be Morphism of p1,p2, gg be Morphism of p2,p3 such that A3: f = ff & g = gg; A4: (the Arrows of D).(p2,p3) = <^p2,p3^> & (the Arrows of D).(p1,p2) = <^p1,p2^> by ALTCAT_1:def 2; <^p1,p3^> <> {} by A1,ALTCAT_1:def 4; then (the Arrows of D).(p1,p3) <> {} by ALTCAT_1:def 2; then dom((the Comp of D).(p1,p2,p3)) = [:<^p2,p3^>,<^p1,p2^>:] by A4,FUNCT_2:def 1; then A5: [gg,ff] in dom((the Comp of D).(p1,p2,p3)) by A1,ZFMISC_1:106; A6: [p1,p2,p3] in [:the carrier of D,the carrier of D,the carrier of D:] by MCART_1:73; A7: (the Comp of D).(p1,p2,p3) = (the Comp of D).[p1,p2,p3] & (the Comp of C).(o1,o2,o3) = (the Comp of C).[o1,o2,o3] by MULTOP_1:def 1; the Comp of D cc= the Comp of C by Def11; then A8: (the Comp of D).(p1,p2,p3) c= (the Comp of C).(o1,o2,o3) by A2,A6, A7,Def2; <^p1,p2^> c= <^o1,o2^> & <^p2,p3^> c= <^o2,o3^> by A2,Th32; then <^o1,o2^> <> {} & <^o2,o3^> <> {} by A1,XBOOLE_1:3; hence g*f = (the Comp of C).(o1,o2,o3).(g,f) by ALTCAT_1:def 10 .= (the Comp of C).(o1,o2,o3).[g,f] by BINOP_1:def 1 .= (the Comp of D).(p1,p2,p3).[gg,ff] by A3,A5,A8,GRFUNC_1:8 .= (the Comp of D).(p1,p2,p3).(gg,ff) by BINOP_1:def 1 .= gg*ff by A1,ALTCAT_1:def 10; end; definition let C be associative transitive (non empty AltCatStr); cluster transitive -> associative (non empty SubCatStr of C); coherence proof let D be non empty SubCatStr of C; assume D is transitive; then reconsider D as transitive non empty SubCatStr of C; D is associative proof let o1,o2,o3,o4 be object of D; A1: o1 in the carrier of D & o2 in the carrier of D & o3 in the carrier of D & o4 in the carrier of D; the carrier of D c= the carrier of C by Def11; then reconsider p1=o1, p2=o2, p3=o3, p4=o4 as object of C by A1; let f be Morphism of o1,o2, g be Morphism of o2,o3, h be Morphism of o3,o4 such that A2: <^o1,o2^> <> {} and A3: <^o2,o3^> <> {} and A4: <^o3,o4^> <> {}; A5: <^o1,o2^> c= <^p1,p2^> by Th32; then A6: <^p1,p2^> <> {} by A2,XBOOLE_1:3; A7: <^o2,o3^> c= <^p2,p3^> by Th32; then A8: <^p2,p3^> <> {} by A3,XBOOLE_1:3; A9: <^o3,o4^> c= <^p3,p4^> by Th32; then A10: <^p3,p4^> <> {} by A4,XBOOLE_1:3; A11: <^o1,o3^> <> {} by A2,A3,ALTCAT_1:def 4; A12: <^o2,o4^> <> {} by A3,A4,ALTCAT_1:def 4; f in <^o1,o2^> by A2; then reconsider ff = f as Morphism of p1,p2 by A5; g in <^o2,o3^> by A3; then reconsider gg = g as Morphism of p2,p3 by A7; h in <^o3,o4^> by A4; then reconsider hh = h as Morphism of p3,p4 by A9; A13: g*f = gg*ff by A2,A3,Th33; h*g = hh* gg by A3,A4,Th33; hence h*g*f =hh*gg*ff by A2,A12,Th33 .= hh*(gg*ff) by A6,A8,A10,Def8 .= h*(g*f) by A4,A11,A13,Th33; end; hence thesis; end; end; theorem Th34: 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 proof let C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be object of C, p1,p2 be object of D such that A1: o1 = p1 & o2 = p2 and A2: <^p1,p2^> <> {}; let n be Morphism of p1,p2; A3: n in <^p1,p2^> by A2; <^p1,p2^> c= <^o1,o2^> by A1,Th32; hence n is Morphism of o1,o2 by A3; end; definition let C be transitive with_units (non empty AltCatStr); cluster id-inheriting transitive -> with_units (non empty SubCatStr of C); coherence proof let D be non empty SubCatStr of C such that A1: D is id-inheriting and A2: D is transitive; let o be object of D; reconsider p = o as object of C by Th30; A3: idm p in <^o,o^> by A1,Def14; hence <^o,o^> <> {}; reconsider i = idm p as Morphism of o,o by A3; take i; let o' be object of D, m' be Morphism of o',o, m'' be Morphism of o,o'; hereby assume A4: <^o',o^> <> {}; reconsider p' = o' as object of C by Th30; <^o',o^> c= <^p',p^> by Th32; then A5: <^p',p^> <> {} by A4,XBOOLE_1:3; reconsider n' = m' as Morphism of p',p by A4,Th34; thus i*m' = (idm p)*n' by A2,A3,A4,Th33 .= m' by A5,ALTCAT_1:24; end; assume A6: <^o,o'^> <> {}; reconsider p' = o' as object of C by Th30; <^o,o'^> c= <^p,p'^> by Th32; then A7: <^p,p'^> <> {} by A6,XBOOLE_1:3; reconsider n'' = m'' as Morphism of p,p' by A6,Th34; thus m''*i = n'' * idm p by A2,A3,A6,Th33 .= m'' by A7,ALTCAT_1:def 19; end; end; definition let C be category; cluster id-inheriting transitive (non empty SubCatStr of C); existence proof consider o being object of C; take D = ObCat o; thus D is id-inheriting transitive; end; end; definition let C be category; mode subcategory of C is id-inheriting transitive SubCatStr of C; end; theorem 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' proof let C be category, D be non empty subcategory of C; let o be object of D, o' be object of C; assume A1: o = o'; then A2: idm o' in <^o,o^> by Def14; then reconsider m = idm o' as Morphism of o,o ; now let p be object of D such that A3: <^o,p^> <> {}; let a be Morphism of o,p; reconsider p' = p as object of C by Th30; <^o,p^> c= <^o',p'^> by A1,Th32; then A4: <^o',p'^> <> {} by A3,XBOOLE_1:3; reconsider n = a as Morphism of o',p' by A1,A3,Th34; thus a*m = n*(idm o') by A1,A2,A3,Th33 .= a by A4,ALTCAT_1:def 19; end; hence idm o = idm o' by ALTCAT_1:def 19; end;

Back to top