:: CAT_5 semantic presentation begin theorem Th1: :: CAT_5:1 for C being Category for D being non empty non void CatStr st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) holds ( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities ) proof let C be Category; ::_thesis: for D being non empty non void CatStr st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) holds ( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities ) let D be non empty non void CatStr ; ::_thesis: ( CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) implies ( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities ) ) assume A1: CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) ; ::_thesis: ( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities ) thus A2: for f, g being Morphism of D holds ( [g,f] in dom the Comp of D iff dom g = cod f ) :: according to CAT_1:def_6 ::_thesis: ( D is transitive & D is associative & D is reflexive & D is with_identities ) proof let f, g be Morphism of D; ::_thesis: ( [g,f] in dom the Comp of D iff dom g = cod f ) reconsider ff = f, gg = g as Morphism of C by A1; A3: ( [gg,ff] in dom the Comp of D iff dom gg = cod ff ) by A1, CAT_1:def_6; thus ( [g,f] in dom the Comp of D implies dom g = cod f ) ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of D ) proof assume A4: [g,f] in dom the Comp of D ; ::_thesis: dom g = cod f thus dom g = dom gg by A1 .= cod ff by A4, A1, CAT_1:def_6 .= cod f by A1 ; ::_thesis: verum end; thus ( dom g = cod f implies [g,f] in dom the Comp of D ) by A1, A3; ::_thesis: verum end; thus A5: for f, g being Morphism of D st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def_7 ::_thesis: ( D is associative & D is reflexive & D is with_identities ) proof let f, g be Morphism of D; ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) reconsider ff = f, gg = g as Morphism of C by A1; assume A6: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) A7: dom gg = cod ff by A1, A6; then [gg,ff] in dom the Comp of C by CAT_1:def_6; then A8: the Comp of C . (gg,ff) = gg (*) ff by CAT_1:def_1; ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) by A7, CAT_1:def_7; hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A1, A8, A6, A2, CAT_1:def_1; ::_thesis: verum end; A9: for f, g being Morphism of D st cod g = dom f holds for ff, gg being Morphism of C st ff = f & gg = g holds f (*) g = ff (*) gg proof let f, g be Morphism of D; ::_thesis: ( cod g = dom f implies for ff, gg being Morphism of C st ff = f & gg = g holds f (*) g = ff (*) gg ) assume A10: cod g = dom f ; ::_thesis: for ff, gg being Morphism of C st ff = f & gg = g holds f (*) g = ff (*) gg let ff, gg be Morphism of C; ::_thesis: ( ff = f & gg = g implies f (*) g = ff (*) gg ) assume A11: ( ff = f & gg = g ) ; ::_thesis: f (*) g = ff (*) gg A12: cod gg = dom ff by A10, A11, A1; thus f (*) g = the Comp of D . (f,g) by CAT_1:def_1, A10, A2 .= the Comp of C . (ff,gg) by A1, A11 .= ff (*) gg by A12, CAT_1:16 ; ::_thesis: verum end; thus for f, g, h being Morphism of D st dom h = cod g & dom g = cod f holds h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def_8 ::_thesis: ( D is reflexive & D is with_identities ) proof let f, g, h be Morphism of D; ::_thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f ) reconsider ff = f, gg = g, hh = h as Morphism of C by A1; assume that A13: dom h = cod g and A14: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f A15: ( dom hh = cod gg & dom gg = cod ff ) by A13, A14, A1; A16: g (*) f = gg (*) ff by A14, A9; A17: h (*) g = hh (*) gg by A13, A9; A18: dom (h (*) g) = dom g by A13, A5; cod (g (*) f) = cod g by A14, A5; hence h (*) (g (*) f) = hh (*) (gg (*) ff) by A9, A16, A13 .= (hh (*) gg) (*) ff by A15, CAT_1:def_8 .= (h (*) g) (*) f by A14, A9, A17, A18 ; ::_thesis: verum end; thus D is reflexive ::_thesis: D is with_identities proof let b be Element of D; :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {} reconsider bb = b as Element of C by A1; reconsider ii = id bb as Morphism of D by A1; A19: cod ii = cod (id bb) by A1 .= b ; dom ii = dom (id bb) by A1 .= b ; then id bb in Hom (b,b) by A19; hence Hom (b,b) <> {} ; ::_thesis: verum end; let a be Element of D; :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of D holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider aa = a as Element of C by A1; reconsider ii = id aa as Morphism of D by A1; A20: cod ii = cod (id aa) by A1 .= a ; dom ii = dom (id aa) by A1 .= a ; then reconsider ii = ii as Morphism of a,a by A20, CAT_1:4; take ii ; ::_thesis: for b1 being Element of the carrier of D holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) let b be Element of D; ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) ) reconsider bb = b as Element of C by A1; thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) proof assume A21: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g let g be Morphism of a,b; ::_thesis: g (*) ii = g reconsider gg = g as Morphism of C by A1; A22: cod gg = cod g by A1 .= bb by A21, CAT_1:5 ; A23: cod (id aa) = aa ; A24: dom gg = dom g by A1 .= aa by A21, CAT_1:5 ; then gg in Hom (aa,bb) by A22; then reconsider gg = gg as Morphism of aa,bb by CAT_1:def_5; A25: dom g = dom gg by A1 .= a by A24 ; cod ii = cod (id aa) by A1 .= a ; hence g (*) ii = the Comp of D . (g,ii) by CAT_1:def_1, A25, A2 .= the Comp of C . (gg,(id aa)) by A1 .= gg (*) (id aa) by A23, A24, CAT_1:16 .= g by A24, CAT_1:22 ; ::_thesis: verum end; assume A26: Hom (b,a) <> {} ; ::_thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1 let g be Morphism of b,a; ::_thesis: ii (*) g = g reconsider gg = g as Morphism of C by A1; A27: dom gg = dom g by A1 .= bb by A26, CAT_1:5 ; A28: dom (id aa) = aa ; A29: cod gg = cod g by A1 .= aa by A26, CAT_1:5 ; then gg in Hom (bb,aa) by A27; then reconsider gg = gg as Morphism of bb,aa by CAT_1:def_5; A30: cod g = cod gg by A1 .= a by A29 ; dom ii = dom (id aa) by A1 .= a ; hence ii (*) g = the Comp of D . (ii,g) by CAT_1:def_1, A30, A2 .= the Comp of C . ((id aa),gg) by A1 .= (id aa) (*) gg by A28, A29, CAT_1:16 .= g by A29, CAT_1:21 ; ::_thesis: verum end; Lm1: for C, D being Category st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) holds for c being Element of C for d being Element of D st c = d holds id c = id d proof let C, D be Category; ::_thesis: ( CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) implies for c being Element of C for d being Element of D st c = d holds id c = id d ) assume A1: CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) ; ::_thesis: for c being Element of C for d being Element of D st c = d holds id c = id d let c be Element of C; ::_thesis: for d being Element of D st c = d holds id c = id d let d be Element of D; ::_thesis: ( c = d implies id c = id d ) assume A2: c = d ; ::_thesis: id c = id d reconsider ii = id c as Morphism of D by A1; A3: cod ii = cod (id c) by A1 .= d by A2 ; A4: dom ii = dom (id c) by A1 .= d by A2 ; then reconsider ii = ii as Morphism of d,d by A3, CAT_1:4; for b being Object of D holds ( ( Hom (d,b) <> {} implies for f being Morphism of d,b holds f (*) ii = f ) & ( Hom (b,d) <> {} implies for f being Morphism of b,d holds ii (*) f = f ) ) proof let b be Object of D; ::_thesis: ( ( Hom (d,b) <> {} implies for f being Morphism of d,b holds f (*) ii = f ) & ( Hom (b,d) <> {} implies for f being Morphism of b,d holds ii (*) f = f ) ) reconsider bb = b as Element of C by A1; thus ( Hom (d,b) <> {} implies for f being Morphism of d,b holds f (*) ii = f ) ::_thesis: ( Hom (b,d) <> {} implies for f being Morphism of b,d holds ii (*) f = f ) proof assume A5: Hom (d,b) <> {} ; ::_thesis: for f being Morphism of d,b holds f (*) ii = f let f be Morphism of d,b; ::_thesis: f (*) ii = f reconsider ff = f as Morphism of C by A1; A6: dom ff = dom f by A1 .= c by A2, A5, CAT_1:5 ; A7: cod (id c) = c .= dom ff by A6 ; cod ii = d by A3 .= dom f by A5, CAT_1:5 ; hence f (*) ii = the Comp of D . (f,ii) by CAT_1:16 .= the Comp of C . (ff,(id c)) by A1 .= ff (*) (id c) by A7, CAT_1:16 .= f by A6, CAT_1:22 ; ::_thesis: verum end; assume A8: Hom (b,d) <> {} ; ::_thesis: for f being Morphism of b,d holds ii (*) f = f let f be Morphism of b,d; ::_thesis: ii (*) f = f reconsider ff = f as Morphism of C by A1; A9: cod ff = cod f by A1 .= c by A2, A8, CAT_1:5 ; A10: dom (id c) = c .= cod ff by A9 ; dom ii = d by A4 .= cod f by A8, CAT_1:5 ; hence ii (*) f = the Comp of D . (ii,f) by CAT_1:16 .= the Comp of C . ((id c),ff) by A1 .= (id c) (*) ff by A10, CAT_1:16 .= f by A9, CAT_1:21 ; ::_thesis: verum end; hence id c = id d by CAT_1:def_12; ::_thesis: verum end; definition let IT be non empty non void CatStr ; attrIT is with_triple-like_morphisms means :Def1: :: CAT_5:def 1 for f being Morphism of IT ex x being set st f = [[(dom f),(cod f)],x]; end; :: deftheorem Def1 defines with_triple-like_morphisms CAT_5:def_1_:_ for IT being non empty non void CatStr holds ( IT is with_triple-like_morphisms iff for f being Morphism of IT ex x being set st f = [[(dom f),(cod f)],x] ); registration cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities with_triple-like_morphisms for CatStr ; existence ex b1 being strict Category st b1 is with_triple-like_morphisms proof take C = 1Cat (0,[[0,0],1]); ::_thesis: C is with_triple-like_morphisms let f be Morphism of C; :: according to CAT_5:def_1 ::_thesis: ex x being set st f = [[(dom f),(cod f)],x] take 1 ; ::_thesis: f = [[(dom f),(cod f)],1] dom f = 0 by TARSKI:def_1; hence f = [[(dom f),(cod f)],1] by TARSKI:def_1; ::_thesis: verum end; end; theorem Th2: :: CAT_5:2 for C being non empty non void with_triple-like_morphisms CatStr for f being Morphism of C holds ( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] ) proof let C be non empty non void with_triple-like_morphisms CatStr ; ::_thesis: for f being Morphism of C holds ( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] ) let f be Morphism of C; ::_thesis: ( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] ) ex x being set st f = [[(dom f),(cod f)],x] by Def1; hence ( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] ) by MCART_1:7, MCART_1:85; ::_thesis: verum end; definition let C be non empty non void with_triple-like_morphisms CatStr ; let f be Morphism of C; :: original: `11 redefine funcf `11 -> Object of C; coherence f `11 is Object of C proof f `11 = dom f by Th2; hence f `11 is Object of C ; ::_thesis: verum end; :: original: `12 redefine funcf `12 -> Object of C; coherence f `12 is Object of C proof f `12 = cod f by Th2; hence f `12 is Object of C ; ::_thesis: verum end; end; scheme :: CAT_5:sch 1 CatEx{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ], F3( set , set ) -> set } : ex C being strict with_triple-like_morphisms Category st ( the carrier of C = F1() & ( for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) ) provided A1: for a, b, c being Element of F1() for f, g being Element of F2() st P1[a,b,f] & P1[b,c,g] holds ( F3(g,f) in F2() & P1[a,c,F3(g,f)] ) and A2: for a being Element of F1() ex f being Element of F2() st ( P1[a,a,f] & ( for b being Element of F1() for g being Element of F2() holds ( ( P1[a,b,g] implies F3(g,f) = g ) & ( P1[b,a,g] implies F3(f,g) = g ) ) ) ) and A3: for a, b, c, d being Element of F1() for f, g, h being Element of F2() st P1[a,b,f] & P1[b,c,g] & P1[c,d,h] holds F3(h,F3(g,f)) = F3(F3(h,g),f) proof set M = { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } ; set a0 = the Element of F1(); consider f0 being Element of F2() such that A4: P1[ the Element of F1(), the Element of F1(),f0] and for b being Element of F1() for g being Element of F2() holds ( ( P1[ the Element of F1(),b,g] implies F3(g,f0) = g ) & ( P1[b, the Element of F1(),g] implies F3(f0,g) = g ) ) by A2; A5: [[ the Element of F1(), the Element of F1()],f0] in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } by A4; { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } c= [:[:F1(),F1():],F2():] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } or x in [:[:F1(),F1():],F2():] ) assume x in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } ; ::_thesis: x in [:[:F1(),F1():],F2():] then ex a, b being Element of F1() ex f being Element of F2() st ( x = [[a,b],f] & P1[a,b,f] ) ; hence x in [:[:F1(),F1():],F2():] ; ::_thesis: verum end; then reconsider M = { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } as non empty Subset of [:[:F1(),F1():],F2():] by A5; A6: now__::_thesis:_for_m_being_Element_of_M_holds_ (_m_=_[[(m_`11),(m_`12)],(m_`2)]_&_P1[m_`11_,m_`12_,m_`2_]_) let m be Element of M; ::_thesis: ( m = [[(m `11),(m `12)],(m `2)] & P1[m `11 ,m `12 ,m `2 ] ) m in M ; then consider a, b being Element of F1(), f being Element of F2() such that A7: m = [[a,b],f] and A8: P1[a,b,f] ; A9: m `11 = a by A7, MCART_1:85; m `12 = b by A7, MCART_1:85; hence ( m = [[(m `11),(m `12)],(m `2)] & P1[m `11 ,m `12 ,m `2 ] ) by A7, A8, A9, MCART_1:7; ::_thesis: verum end; deffunc H1( Element of M) -> Element of F1() = \$1 `11 ; consider DM being Function of M,F1() such that A10: for m being Element of M holds DM . m = H1(m) from FUNCT_2:sch_4(); deffunc H2( Element of M) -> Element of F1() = \$1 `12 ; consider CM being Function of M,F1() such that A11: for m being Element of M holds CM . m = H2(m) from FUNCT_2:sch_4(); deffunc H3( set , set ) -> set = [[(\$2 `11),(\$1 `12)],F3((\$1 `2),(\$2 `2))]; defpred S1[ set , set ] means ( \$1 `11 = \$2 `12 & \$1 in M & \$2 in M ); A12: now__::_thesis:_for_x,_y_being_set_st_S1[x,y]_holds_ H3(x,y)_in_M let x, y be set ; ::_thesis: ( S1[x,y] implies H3(x,y) in M ) assume A13: S1[x,y] ; ::_thesis: H3(x,y) in M then consider ax, bx being Element of F1(), fx being Element of F2() such that A14: x = [[ax,bx],fx] and A15: P1[ax,bx,fx] ; consider ay, b2 being Element of F1(), fy being Element of F2() such that A16: y = [[ay,b2],fy] and A17: P1[ay,b2,fy] by A13; A18: x `11 = ax by A14, MCART_1:85; A19: x `12 = bx by A14, MCART_1:85; A20: y `11 = ay by A16, MCART_1:85; A21: y `12 = b2 by A16, MCART_1:85; A22: x `2 = fx by A14, MCART_1:7; A23: y `2 = fy by A16, MCART_1:7; A24: F3(fx,fy) in F2() by A1, A13, A15, A17, A18, A21; P1[ay,bx,F3(fx,fy)] by A1, A13, A15, A17, A18, A21; hence H3(x,y) in M by A19, A20, A22, A23, A24; ::_thesis: verum end; consider CC being PartFunc of [:M,M:],M such that A25: for x, y being set holds ( [x,y] in dom CC iff ( x in M & y in M & S1[x,y] ) ) and A26: for x, y being set st [x,y] in dom CC holds CC . (x,y) = H3(x,y) from BINOP_1:sch_6(A12); defpred S2[ Element of F1(), set ] means ex f being Element of F2() st ( \$2 = [[\$1,\$1],f] & P1[\$1,\$1,f] & ( for b being Element of F1() for g being Element of F2() holds ( ( P1[\$1,b,g] implies F3(g,f) = g ) & ( P1[b,\$1,g] implies F3(f,g) = g ) ) ) ); A27: now__::_thesis:_for_a_being_Element_of_F1()_ex_y_being_Element_of_M_st_S2[a,y] let a be Element of F1(); ::_thesis: ex y being Element of M st S2[a,y] consider f being Element of F2() such that A28: P1[a,a,f] and A29: for b being Element of F1() for g being Element of F2() holds ( ( P1[a,b,g] implies F3(g,f) = g ) & ( P1[b,a,g] implies F3(f,g) = g ) ) by A2; [[a,a],f] in M by A28; then reconsider y = [[a,a],f] as Element of M ; take y = y; ::_thesis: S2[a,y] thus S2[a,y] by A28, A29; ::_thesis: verum end; consider I being Function of F1(),M such that A30: for o being Element of F1() holds S2[o,I . o] from FUNCT_2:sch_3(A27); set C = CatStr(# F1(),M,DM,CM,CC #); A31: CatStr(# F1(),M,DM,CM,CC #) is Category-like proof hereby :: according to CAT_1:def_6 ::_thesis: verum let f, g be Morphism of CatStr(# F1(),M,DM,CM,CC #); ::_thesis: ( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f ) A32: ( [g,f] in dom CC iff ( g in M & f in M & g `11 = f `12 & g in M & f in M ) ) by A25; DM . g = g `11 by A10; hence ( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f ) by A11, A32; ::_thesis: verum end; end; A33: for f, g being Morphism of CatStr(# F1(),M,DM,CM,CC #) holds ( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f ) by A31, CAT_1:def_6; A34: CatStr(# F1(),M,DM,CM,CC #) is transitive proof let f, g be Morphism of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) A35: the Source of CatStr(# F1(),M,DM,CM,CC #) . f = f `11 by A10; A36: the Source of CatStr(# F1(),M,DM,CM,CC #) . g = g `11 by A10; A37: the Target of CatStr(# F1(),M,DM,CM,CC #) . f = f `12 by A11; A38: the Target of CatStr(# F1(),M,DM,CM,CC #) . g = g `12 by A11; assume A39: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) then A40: CC . (g,f) = [[(f `11),(g `12)],F3((g `2),(f `2))] by A26, A25, A36, A37; A41: (CC . [g,f]) `11 = f `11 by A40, MCART_1:85; A42: the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,f) = g (*) f by A39, CAT_1:def_1, A25, A36, A37; (CC . [g,f]) `12 = g `12 by A40, MCART_1:85; hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A10, A11, A35, A38, A41, A42; ::_thesis: verum end; A43: CatStr(# F1(),M,DM,CM,CC #) is associative proof let f, g, h be Morphism of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f ) A44: the Source of CatStr(# F1(),M,DM,CM,CC #) . g = g `11 by A10; A45: the Source of CatStr(# F1(),M,DM,CM,CC #) . h = h `11 by A10; A46: the Target of CatStr(# F1(),M,DM,CM,CC #) . f = f `12 by A11; A47: the Target of CatStr(# F1(),M,DM,CM,CC #) . g = g `12 by A11; assume that A48: dom h = cod g and A49: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f A50: [g,f] in dom CC by A25, A44, A46, A49; A51: [h,g] in dom CC by A25, A45, A47, A48; A52: CC . [g,f] in rng CC by A50, FUNCT_1:def_3; CC . [h,g] in rng CC by A51, FUNCT_1:def_3; then reconsider gf = CC . (g,f), hg = CC . (h,g) as Element of M by A52; A53: gf = [[(f `11),(g `12)],F3((g `2),(f `2))] by A26, A25, A44, A46, A49; A54: hg = [[(g `11),(h `12)],F3((h `2),(g `2))] by A26, A25, A45, A47, A48; A55: DM . gf = gf `11 by A10; A56: DM . hg = hg `11 by A10; A57: CM . gf = gf `12 by A11; A58: CM . hg = hg `12 by A11; A59: DM . gf = f `11 by A53, A55, MCART_1:85; A60: CM . gf = g `12 by A53, A57, MCART_1:85; A61: CM . hg = h `12 by A54, A58, MCART_1:85; A62: [h,gf] in dom CC by A25, A45, A11, A48, A57, A60; A63: [hg,f] in dom CC by A25, A44, A46, A49, A56, A54, MCART_1:85; reconsider f9 = f, g9 = g, h9 = h as Element of M ; A64: P1[f9 `11 ,f9 `12 ,f9 `2 ] by A6; A65: P1[g9 `11 ,g9 `12 ,g9 `2 ] by A6; A66: P1[h9 `11 ,h9 `12 ,h9 `2 ] by A6; A67: the Comp of CatStr(# F1(),M,DM,CM,CC #) . (h,g) = h (*) g by CAT_1:def_1, A33, A48; A68: dom (h (*) g) = dom g by A34, CAT_1:def_7, A48; A69: the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,f) = g (*) f by CAT_1:def_1, A33, A49; cod (g (*) f) = cod g by A34, CAT_1:def_7, A49; hence h (*) (g (*) f) = the Comp of CatStr(# F1(),M,DM,CM,CC #) . (h,( the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,f))) by A69, CAT_1:def_1, A33, A48 .= [[(f `11),(h `12)],F3((h `2),(gf `2))] by A26, A55, A59, A62 .= [[(f `11),(h `12)],F3((h9 `2),F3((g9 `2),(f9 `2)))] by A53, MCART_1:7 .= [[(f `11),(h `12)],F3(F3((h9 `2),(g9 `2)),(f9 `2))] by A3, A44, A45, A46, A47, A48, A49, A64, A65, A66 .= [[(f `11),(h `12)],F3((hg `2),(f `2))] by A54, MCART_1:7 .= the Comp of CatStr(# F1(),M,DM,CM,CC #) . (( the Comp of CatStr(# F1(),M,DM,CM,CC #) . (h,g)),f) by A26, A58, A61, A63 .= (h (*) g) (*) f by A67, A33, A49, CAT_1:def_1, A68 ; ::_thesis: verum end; A70: CatStr(# F1(),M,DM,CM,CC #) is reflexive proof let b be Object of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {} consider f being Element of F2() such that A71: I . b = [[b,b],f] and P1[b,b,f] and for c being Element of F1() for g being Element of F2() holds ( ( P1[b,c,g] implies F3(g,f) = g ) & ( P1[c,b,g] implies F3(f,g) = g ) ) by A30; reconsider bb = b as Element of F1() ; reconsider Ib = I . bb as Element of M ; reconsider ii = I . bb as Morphism of CatStr(# F1(),M,DM,CM,CC #) ; A72: cod ii = (I . b) `12 by A11 .= b by A71, MCART_1:85 ; dom ii = (I . b) `11 by A10 .= b by A71, MCART_1:85 ; then I . b in Hom (b,b) by A72; hence Hom (b,b) <> {} ; ::_thesis: verum end; CatStr(# F1(),M,DM,CM,CC #) is with_identities proof let a be Object of CatStr(# F1(),M,DM,CM,CC #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of CatStr(# F1(),M,DM,CM,CC #) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) consider f being Element of F2() such that A73: I . a = [[a,a],f] and P1[a,a,f] and A74: for c being Element of F1() for g being Element of F2() holds ( ( P1[a,c,g] implies F3(g,f) = g ) & ( P1[c,a,g] implies F3(f,g) = g ) ) by A30; reconsider aa = a as Element of F1() ; reconsider Ia = I . aa as Element of M ; reconsider ii = I . aa as Morphism of CatStr(# F1(),M,DM,CM,CC #) ; A75: cod ii = (I . a) `12 by A11 .= a by A73, MCART_1:85 ; dom ii = (I . a) `11 by A10 .= a by A73, MCART_1:85 ; then reconsider ii = ii as Morphism of a,a by A75, CAT_1:4; take ii ; ::_thesis: for b1 being Element of the carrier of CatStr(# F1(),M,DM,CM,CC #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) let b be Element of CatStr(# F1(),M,DM,CM,CC #); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) proof assume A76: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g let g be Morphism of a,b; ::_thesis: g (*) ii = g reconsider bb = b as Element of F1() ; g in M ; then consider a1, b1 being Element of F1(), f1 being Element of F2() such that A77: g = [[a1,b1],f1] and A78: P1[a1,b1,f1] ; A79: a = dom g by A76, CAT_1:5 .= DM . g .= [[a1,b1],f1] `11 by A77, A10 .= a1 by MCART_1:85 ; then A80: F3(f1,f) = f1 by A74, A78; A81: [[a,a],f] `11 = a1 by A79, MCART_1:85; A82: [[a,a],f] `2 = f ; A83: [[a1,b1],f1] `12 = b1 by MCART_1:85; A84: [[a1,b1],f1] `2 = f1 ; g `11 = [[a1,b1],f1] `11 by A77 .= a by A79, MCART_1:85 .= [[a,a],f] `12 by MCART_1:85 .= ii `12 by A73 ; then A85: [g,ii] in dom CC by A25; hence g (*) ii = the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,ii) by CAT_1:def_1 .= CC . (g,ii) .= [[(ii `11),(g `12)],F3((g `2),(ii `2))] by A26, A85 .= [[a1,b1],f1] by A80, A81, A82, A83, A84, A77, A73 .= g by A77 ; ::_thesis: verum end; thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ::_thesis: verum proof assume A86: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds ii (*) f = f let g be Morphism of b,a; ::_thesis: ii (*) g = g reconsider bb = b as Element of F1() ; g in M ; then consider b1, a1 being Element of F1(), f1 being Element of F2() such that A87: g = [[b1,a1],f1] and A88: P1[b1,a1,f1] ; A89: a = cod g by A86, CAT_1:5 .= CM . g .= [[b1,a1],f1] `12 by A87, A11 .= a1 by MCART_1:85 ; then A90: F3(f,f1) = f1 by A74, A88; A91: [[a,a],f] `12 = a1 by A89, MCART_1:85; A92: [[a,a],f] `2 = f ; A93: [[b1,a1],f1] `11 = b1 by MCART_1:85; A94: [[b1,a1],f1] `2 = f1 ; g `12 = [[b1,a1],f1] `12 by A87 .= a by A89, MCART_1:85 .= [[a,a],f] `11 by MCART_1:85 .= ii `11 by A73 ; then A95: [ii,g] in dom CC by A25; hence ii (*) g = the Comp of CatStr(# F1(),M,DM,CM,CC #) . (ii,g) by CAT_1:def_1 .= CC . (ii,g) .= [[(g `11),(ii `12)],F3((ii `2),(g `2))] by A26, A95 .= [[b1,a1],f1] by A90, A91, A92, A93, A94, A87, A73 .= g by A87 ; ::_thesis: verum end; end; then reconsider C = CatStr(# F1(),M,DM,CM,CC #) as strict Category by A31, A34, A43, A70; C is with_triple-like_morphisms proof let f be Morphism of C; :: according to CAT_5:def_1 ::_thesis: ex x being set st f = [[(dom f),(cod f)],x] f in M ; then consider a, b being Element of F1(), g being Element of F2() such that A96: f = [[a,b],g] and P1[a,b,g] ; take g ; ::_thesis: f = [[(dom f),(cod f)],g] A97: dom f = f `11 by A10 .= a by A96, MCART_1:85 ; cod f = f `12 by A11 .= b by A96, MCART_1:85 ; hence f = [[(dom f),(cod f)],g] by A96, A97; ::_thesis: verum end; then reconsider C = C as strict with_triple-like_morphisms Category ; take C ; ::_thesis: ( the carrier of C = F1() & ( for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) ) thus the carrier of C = F1() ; ::_thesis: ( ( for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) ) hereby ::_thesis: ( ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) ) let a, b be Element of F1(); ::_thesis: for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C let f be Element of F2(); ::_thesis: ( P1[a,b,f] implies [[a,b],f] is Morphism of C ) assume P1[a,b,f] ; ::_thesis: [[a,b],f] is Morphism of C then [[a,b],f] in M ; hence [[a,b],f] is Morphism of C ; ::_thesis: verum end; hereby ::_thesis: for m1, m2 being Morphism of C for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] let m be Morphism of C; ::_thesis: ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) m in M ; hence ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ; ::_thesis: verum end; let m1, m2 be Morphism of C; ::_thesis: for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] let a1, a2, a3 be Element of F1(); ::_thesis: for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] let f1, f2 be Element of F2(); ::_thesis: ( m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] implies m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) assume that A98: m1 = [[a1,a2],f1] and A99: m2 = [[a2,a3],f2] ; ::_thesis: m2 (*) m1 = [[a1,a3],F3(f2,f1)] A100: m1 `11 = a1 by A98, MCART_1:85; A101: m1 `12 = a2 by A98, MCART_1:85; A102: m2 `11 = a2 by A99, MCART_1:85; A103: m2 `12 = a3 by A99, MCART_1:85; thus m2 (*) m1 = CC . (m2,m1) by CAT_1:def_1, A25, A101, A102 .= [[a1,a3],F3((m2 `2),(m1 `2))] by A26, A100, A103, A25, A101, A102 .= [[a1,a3],F3(f2,(m1 `2))] by A99, MCART_1:7 .= [[a1,a3],F3(f2,f1)] by A98, MCART_1:7 ; ::_thesis: verum end; scheme :: CAT_5:sch 2 CatUniq{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ], F3( set , set ) -> set } : for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = F1() & ( for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C1 for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) & the carrier of C2 = F1() & ( for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C2 for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) holds C1 = C2 provided for a being Element of F1() ex f being Element of F2() st ( P1[a,a,f] & ( for b being Element of F1() for g being Element of F2() holds ( ( P1[a,b,g] implies F3(g,f) = g ) & ( P1[b,a,g] implies F3(f,g) = g ) ) ) ) proof let C1, C2 be strict with_triple-like_morphisms Category; ::_thesis: ( the carrier of C1 = F1() & ( for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C1 for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) & the carrier of C2 = F1() & ( for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C2 for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) implies C1 = C2 ) assume that A1: the carrier of C1 = F1() and A2: for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C1 and A3: for m being Morphism of C1 ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) and A4: for m1, m2 being Morphism of C1 for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] and A5: the carrier of C2 = F1() and A6: for a, b being Element of F1() for f being Element of F2() st P1[a,b,f] holds [[a,b],f] is Morphism of C2 and A7: for m being Morphism of C2 ex a, b being Element of F1() ex f being Element of F2() st ( m = [[a,b],f] & P1[a,b,f] ) and A8: for m1, m2 being Morphism of C2 for a1, a2, a3 being Element of F1() for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],F3(f2,f1)] ; ::_thesis: C1 = C2 A9: the carrier' of C1 = the carrier' of C2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier' of C2 c= the carrier' of C1 let x be set ; ::_thesis: ( x in the carrier' of C1 implies x in the carrier' of C2 ) assume x in the carrier' of C1 ; ::_thesis: x in the carrier' of C2 then ex a, b being Element of F1() ex f being Element of F2() st ( x = [[a,b],f] & P1[a,b,f] ) by A3; then x is Morphism of C2 by A6; hence x in the carrier' of C2 ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of C2 or x in the carrier' of C1 ) assume x in the carrier' of C2 ; ::_thesis: x in the carrier' of C1 then ex a, b being Element of F1() ex f being Element of F2() st ( x = [[a,b],f] & P1[a,b,f] ) by A7; then x is Morphism of C1 by A2; hence x in the carrier' of C1 ; ::_thesis: verum end; A10: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def_1; A11: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def_1; A12: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def_1; A13: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def_1; A14: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_C1_holds_ the_Source_of_C1_._x_=_the_Source_of_C2_._x let x be set ; ::_thesis: ( x in the carrier' of C1 implies the Source of C1 . x = the Source of C2 . x ) assume x in the carrier' of C1 ; ::_thesis: the Source of C1 . x = the Source of C2 . x then reconsider m1 = x as Morphism of C1 ; reconsider m2 = m1 as Morphism of C2 by A9; thus the Source of C1 . x = dom m1 .= m1 `11 by Th2 .= dom m2 by Th2 .= the Source of C2 . x ; ::_thesis: verum end; then A15: the Source of C1 = the Source of C2 by A9, A10, A11, FUNCT_1:2; now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_C1_holds_ the_Target_of_C1_._x_=_the_Target_of_C2_._x let x be set ; ::_thesis: ( x in the carrier' of C1 implies the Target of C1 . x = the Target of C2 . x ) assume x in the carrier' of C1 ; ::_thesis: the Target of C1 . x = the Target of C2 . x then reconsider m1 = x as Morphism of C1 ; reconsider m2 = m1 as Morphism of C2 by A9; thus the Target of C1 . x = cod m1 .= m1 `12 by Th2 .= cod m2 by Th2 .= the Target of C2 . x ; ::_thesis: verum end; then A16: the Target of C1 = the Target of C2 by A9, A12, A13, FUNCT_1:2; A17: dom the Comp of C1 = dom the Comp of C2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: dom the Comp of C2 c= dom the Comp of C1 let x be set ; ::_thesis: ( x in dom the Comp of C1 implies x in dom the Comp of C2 ) assume A18: x in dom the Comp of C1 ; ::_thesis: x in dom the Comp of C2 then reconsider xx = x as Element of [: the carrier' of C1, the carrier' of C1:] ; reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A9; A19: y = [(xx `1),(xx `2)] by MCART_1:21; then dom (xx `1) = cod (xx `2) by A18, CAT_1:def_6; then dom (y `1) = cod (y `2) by A14, A16; hence x in dom the Comp of C2 by A19, CAT_1:def_6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom the Comp of C2 or x in dom the Comp of C1 ) assume A20: x in dom the Comp of C2 ; ::_thesis: x in dom the Comp of C1 then reconsider xx = x as Element of [: the carrier' of C1, the carrier' of C1:] by A9; reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A9; A21: xx = [(y `1),(y `2)] by MCART_1:21; then dom (y `1) = cod (y `2) by A20, CAT_1:def_6; then dom (xx `1) = cod (xx `2) by A14, A16; hence x in dom the Comp of C1 by A21, CAT_1:def_6; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_dom_the_Comp_of_C1_holds_ the_Comp_of_C1_._(x,y)_=_the_Comp_of_C2_._(x,y) let x, y be set ; ::_thesis: ( [x,y] in dom the Comp of C1 implies the Comp of C1 . (x,y) = the Comp of C2 . (x,y) ) assume A22: [x,y] in dom the Comp of C1 ; ::_thesis: the Comp of C1 . (x,y) = the Comp of C2 . (x,y) then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87; reconsider g2 = g1, h2 = h1 as Morphism of C2 by A9; consider a1, b1 being Element of F1(), f1 being Element of F2() such that A23: g1 = [[a1,b1],f1] and P1[a1,b1,f1] by A3; consider c1, d1 being Element of F1(), i1 being Element of F2() such that A24: h1 = [[c1,d1],i1] and P1[c1,d1,i1] by A3; A25: a1 = g1 `11 by A23, MCART_1:85 .= dom g1 by Th2 .= cod h1 by A22, CAT_1:15 .= h1 `12 by Th2 .= d1 by A24, MCART_1:85 ; thus the Comp of C1 . (x,y) = g1 (*) h1 by A22, CAT_1:def_1 .= [[c1,b1],F3(f1,i1)] by A4, A23, A24, A25 .= g2 (*) h2 by A8, A23, A24, A25 .= the Comp of C2 . (x,y) by A17, A22, CAT_1:def_1 ; ::_thesis: verum end; hence C1 = C2 by A1, A5, A9, A15, A16, A17, BINOP_1:20; ::_thesis: verum end; scheme :: CAT_5:sch 3 FunctorEx{ F1() -> Category, F2() -> Category, F3( set ) -> Object of F2(), F4( set ) -> set } : ex F being Functor of F1(),F2() st for f being Morphism of F1() holds F . f = F4(f) provided A1: for f being Morphism of F1() holds ( F4(f) is Morphism of F2() & ( for g being Morphism of F2() st g = F4(f) holds ( dom g = F3((dom f)) & cod g = F3((cod f)) ) ) ) and A2: for a being Object of F1() holds F4((id a)) = id F3(a) and A3: for f1, f2 being Morphism of F1() for g1, g2 being Morphism of F2() st g1 = F4(f1) & g2 = F4(f2) & dom f2 = cod f1 holds F4((f2 (*) f1)) = g2 (*) g1 proof consider F being Function such that A4: dom F = the carrier' of F1() and A5: for x being set st x in the carrier' of F1() holds F . x = F4(x) from FUNCT_1:sch_3(); rng F c= the carrier' of F2() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in the carrier' of F2() ) assume x in rng F ; ::_thesis: x in the carrier' of F2() then consider y being set such that A6: y in dom F and A7: x = F . y by FUNCT_1:def_3; x = F4(y) by A4, A5, A6, A7; then x is Morphism of F2() by A1, A4, A6; hence x in the carrier' of F2() ; ::_thesis: verum end; then reconsider F = F as Function of the carrier' of F1(), the carrier' of F2() by A4, FUNCT_2:def_1, RELSET_1:4; A8: now__::_thesis:_for_c_being_Object_of_F1()_ex_d_being_Object_of_F2()_st_F_._(id_c)_=_id_d let c be Object of F1(); ::_thesis: ex d being Object of F2() st F . (id c) = id d take d = F3(c); ::_thesis: F . (id c) = id d thus F . (id c) = F4((id c)) by A5 .= id d by A2 ; ::_thesis: verum end; A9: now__::_thesis:_for_f_being_Morphism_of_F1()_holds_ (_F_._(id_(dom_f))_=_id_(dom_(F_._f))_&_F_._(id_(cod_f))_=_id_(cod_(F_._f))_) let f be Morphism of F1(); ::_thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) reconsider g = F4(f) as Morphism of F2() by A1; thus F . (id (dom f)) = F4((id (dom f))) by A5 .= id F3((dom f)) by A2 .= id (dom g) by A1 .= id (dom (F . f)) by A5 ; ::_thesis: F . (id (cod f)) = id (cod (F . f)) thus F . (id (cod f)) = F4((id (cod f))) by A5 .= id F3((cod f)) by A2 .= id (cod g) by A1 .= id (cod (F . f)) by A5 ; ::_thesis: verum end; now__::_thesis:_for_f,_g_being_Morphism_of_F1()_st_dom_g_=_cod_f_holds_ F_._(g_(*)_f)_=_(F_._g)_(*)_(F_._f) let f, g be Morphism of F1(); ::_thesis: ( dom g = cod f implies F . (g (*) f) = (F . g) (*) (F . f) ) assume A10: dom g = cod f ; ::_thesis: F . (g (*) f) = (F . g) (*) (F . f) A11: F . g = F4(g) by A5; A12: F . f = F4(f) by A5; F . (g (*) f) = F4((g (*) f)) by A5; hence F . (g (*) f) = (F . g) (*) (F . f) by A3, A10, A11, A12; ::_thesis: verum end; then reconsider F = F as Functor of F1(),F2() by A8, A9, CAT_1:61; take F ; ::_thesis: for f being Morphism of F1() holds F . f = F4(f) thus for f being Morphism of F1() holds F . f = F4(f) by A5; ::_thesis: verum end; theorem Th3: :: CAT_5:3 for C1 being Category for C2 being Subcategory of C1 st C1 is Subcategory of C2 holds CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) proof let C1 be Category; ::_thesis: for C2 being Subcategory of C1 st C1 is Subcategory of C2 holds CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) let C2 be Subcategory of C1; ::_thesis: ( C1 is Subcategory of C2 implies CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) ) assume A1: C1 is Subcategory of C2 ; ::_thesis: CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) then A2: the carrier of C1 c= the carrier of C2 by CAT_2:def_4; the carrier of C2 c= the carrier of C1 by CAT_2:def_4; then A3: the carrier of C1 = the carrier of C2 by A2, XBOOLE_0:def_10; A4: the carrier' of C1 c= the carrier' of C2 by A1, CAT_2:7; A5: the carrier' of C2 c= the carrier' of C1 by CAT_2:7; then A6: the carrier' of C1 = the carrier' of C2 by A4, XBOOLE_0:def_10; A7: the Comp of C1 c= the Comp of C2 by A1, CAT_2:def_4; the Comp of C2 c= the Comp of C1 by CAT_2:def_4; then A8: the Comp of C1 = the Comp of C2 by A7, XBOOLE_0:def_10; now__::_thesis:_for_m1_being_Morphism_of_C1_holds_the_Source_of_C1_._m1_=_the_Source_of_C2_._m1 let m1 be Morphism of C1; ::_thesis: the Source of C1 . m1 = the Source of C2 . m1 reconsider m2 = m1 as Morphism of C2 by A4, A5, XBOOLE_0:def_10; thus the Source of C1 . m1 = dom m1 .= dom m2 by CAT_2:9 .= the Source of C2 . m1 ; ::_thesis: verum end; then A9: the Source of C1 = the Source of C2 by A3, A6, FUNCT_2:63; now__::_thesis:_for_m1_being_Morphism_of_C1_holds_the_Target_of_C1_._m1_=_the_Target_of_C2_._m1 let m1 be Morphism of C1; ::_thesis: the Target of C1 . m1 = the Target of C2 . m1 reconsider m2 = m1 as Morphism of C2 by A4, A5, XBOOLE_0:def_10; thus the Target of C1 . m1 = cod m1 .= cod m2 by CAT_2:9 .= the Target of C2 . m1 ; ::_thesis: verum end; then the Target of C1 = the Target of C2 by A3, A6, FUNCT_2:63; hence CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) by A3, A6, A8, A9; ::_thesis: verum end; theorem Th4: :: CAT_5:4 for C being Category for D being Subcategory of C for E being Subcategory of D holds E is Subcategory of C proof let C be Category; ::_thesis: for D being Subcategory of C for E being Subcategory of D holds E is Subcategory of C let D be Subcategory of C; ::_thesis: for E being Subcategory of D holds E is Subcategory of C let E be Subcategory of D; ::_thesis: E is Subcategory of C A1: the carrier of D c= the carrier of C by CAT_2:def_4; A2: the Comp of D c= the Comp of C by CAT_2:def_4; A3: the carrier of E c= the carrier of D by CAT_2:def_4; A4: the Comp of E c= the Comp of D by CAT_2:def_4; thus the carrier of E c= the carrier of C by A1, A3, XBOOLE_1:1; :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of E for b3, b4 being Element of the carrier of C holds ( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of E c= the Comp of C & ( for b1 being Element of the carrier of E for b2 being Element of the carrier of C holds ( not b1 = b2 or id b1 = id b2 ) ) ) hereby ::_thesis: ( the Comp of E c= the Comp of C & ( for b1 being Element of the carrier of E for b2 being Element of the carrier of C holds ( not b1 = b2 or id b1 = id b2 ) ) ) let a, b be Object of E; ::_thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) let a9, b9 be Object of C; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) ) reconsider a1 = a, b1 = b as Object of D by CAT_2:6; assume that A5: a = a9 and A6: b = b9 ; ::_thesis: Hom (a,b) c= Hom (a9,b9) A7: Hom (a,b) c= Hom (a1,b1) by CAT_2:def_4; Hom (a1,b1) c= Hom (a9,b9) by A5, A6, CAT_2:def_4; hence Hom (a,b) c= Hom (a9,b9) by A7, XBOOLE_1:1; ::_thesis: verum end; thus the Comp of E c= the Comp of C by A2, A4, XBOOLE_1:1; ::_thesis: for b1 being Element of the carrier of E for b2 being Element of the carrier of C holds ( not b1 = b2 or id b1 = id b2 ) let a be Object of E; ::_thesis: for b1 being Element of the carrier of C holds ( not a = b1 or id a = id b1 ) let a9 be Object of C; ::_thesis: ( not a = a9 or id a = id a9 ) reconsider a1 = a as Object of D by CAT_2:6; assume A8: a = a9 ; ::_thesis: id a = id a9 id a = id a1 by CAT_2:def_4; hence id a = id a9 by A8, CAT_2:def_4; ::_thesis: verum end; definition let C1, C2 be Category; given C being Category such that A1: C1 is Subcategory of C and A2: C2 is Subcategory of C ; given o1 being Object of C1 such that A3: o1 is Object of C2 ; funcC1 /\ C2 -> strict Category means :Def2: :: CAT_5:def 2 ( the carrier of it = the carrier of C1 /\ the carrier of C2 & the carrier' of it = the carrier' of C1 /\ the carrier' of C2 & the Source of it = the Source of C1 | the carrier' of C2 & the Target of it = the Target of C1 | the carrier' of C2 & the Comp of it = the Comp of C1 || the carrier' of C2 ); existence ex b1 being strict Category st ( the carrier of b1 = the carrier of C1 /\ the carrier of C2 & the carrier' of b1 = the carrier' of C1 /\ the carrier' of C2 & the Source of b1 = the Source of C1 | the carrier' of C2 & the Target of b1 = the Target of C1 | the carrier' of C2 & the Comp of b1 = the Comp of C1 || the carrier' of C2 ) proof set DD = the Source of C1 | the carrier' of C2; set CC = the Target of C1 | the carrier' of C2; set Cm = the Comp of C1 || the carrier' of C2; reconsider O = the carrier of C1 /\ the carrier of C2 as non empty set by A3, XBOOLE_0:def_4; reconsider o2 = o1 as Object of C2 by A3; reconsider o = o1 as Object of C by A1, CAT_2:6; A4: id o1 = id o by A1, CAT_2:def_4; id o2 = id o by A2, CAT_2:def_4; then reconsider M = the carrier' of C1 /\ the carrier' of C2 as non empty set by A4, XBOOLE_0:def_4; A5: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def_1; A6: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def_1; A7: dom ( the Source of C1 | the carrier' of C2) = M by A5, RELAT_1:61; A8: dom ( the Target of C1 | the carrier' of C2) = M by A6, RELAT_1:61; rng ( the Source of C1 | the carrier' of C2) c= O proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the Source of C1 | the carrier' of C2) or x in O ) assume x in rng ( the Source of C1 | the carrier' of C2) ; ::_thesis: x in O then consider m being set such that A9: m in dom ( the Source of C1 | the carrier' of C2) and A10: x = ( the Source of C1 | the carrier' of C2) . m by FUNCT_1:def_3; reconsider m1 = m as Morphism of C1 by A9; reconsider m2 = m as Morphism of C2 by A7, A9, XBOOLE_0:def_4; reconsider m = m1 as Morphism of C by A1, CAT_2:8; A11: x = dom m1 by A9, A10, FUNCT_1:47; A12: dom m1 = dom m by A1, CAT_2:9; dom m = dom m2 by A2, CAT_2:9; hence x in O by A11, A12, XBOOLE_0:def_4; ::_thesis: verum end; then reconsider DD = the Source of C1 | the carrier' of C2 as Function of M,O by A7, FUNCT_2:def_1, RELSET_1:4; rng ( the Target of C1 | the carrier' of C2) c= O proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the Target of C1 | the carrier' of C2) or x in O ) assume x in rng ( the Target of C1 | the carrier' of C2) ; ::_thesis: x in O then consider m being set such that A13: m in dom ( the Target of C1 | the carrier' of C2) and A14: x = ( the Target of C1 | the carrier' of C2) . m by FUNCT_1:def_3; reconsider m1 = m as Morphism of C1 by A13; reconsider m2 = m as Morphism of C2 by A8, A13, XBOOLE_0:def_4; reconsider m = m1 as Morphism of C by A1, CAT_2:8; A15: x = cod m1 by A13, A14, FUNCT_1:47; A16: cod m1 = cod m by A1, CAT_2:9; cod m = cod m2 by A2, CAT_2:9; hence x in O by A15, A16, XBOOLE_0:def_4; ::_thesis: verum end; then reconsider CC = the Target of C1 | the carrier' of C2 as Function of M,O by A8, FUNCT_2:def_1, RELSET_1:4; A17: dom ( the Comp of C1 || the carrier' of C2) = (dom the Comp of C1) /\ [: the carrier' of C2, the carrier' of C2:] by RELAT_1:61; then dom ( the Comp of C1 || the carrier' of C2) c= [: the carrier' of C1, the carrier' of C1:] /\ [: the carrier' of C2, the carrier' of C2:] by XBOOLE_1:26; then A18: dom ( the Comp of C1 || the carrier' of C2) c= [:M,M:] by ZFMISC_1:100; rng ( the Comp of C1 || the carrier' of C2) c= M proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the Comp of C1 || the carrier' of C2) or x in M ) assume x in rng ( the Comp of C1 || the carrier' of C2) ; ::_thesis: x in M then consider m being set such that A19: m in dom ( the Comp of C1 || the carrier' of C2) and A20: x = ( the Comp of C1 || the carrier' of C2) . m by FUNCT_1:def_3; A21: m `1 in M by A18, A19, MCART_1:10; A22: m `2 in M by A18, A19, MCART_1:10; A23: m = [(m `1),(m `2)] by A17, A19, MCART_1:21; reconsider m1 = m `1 , m2 = m `2 as Morphism of C1 by A21, A22, XBOOLE_0:def_4; reconsider n1 = m `1 , n2 = m `2 as Morphism of C2 by A21, A22, XBOOLE_0:def_4; reconsider mm = m1, n = m2 as Morphism of C by A1, CAT_2:8; A24: m in dom the Comp of C1 by A17, A19, XBOOLE_0:def_4; then A25: dom m1 = cod m2 by A23, CAT_1:15; A26: x = the Comp of C1 . (m1,m2) by A19, A20, A23, FUNCT_1:47; A27: dom m1 = dom mm by A1, CAT_2:9; A28: dom n1 = dom mm by A2, CAT_2:9; A29: cod m2 = cod n by A1, CAT_2:9; A30: cod n2 = cod n by A2, CAT_2:9; A31: x = m1 (*) m2 by A23, A24, A26, CAT_1:def_1; A32: m1 (*) m2 = mm (*) n by A1, A25, CAT_2:11; mm (*) n = n1 (*) n2 by A2, A25, A27, A28, A29, A30, CAT_2:11; hence x in M by A31, A32, XBOOLE_0:def_4; ::_thesis: verum end; then reconsider Cm = the Comp of C1 || the carrier' of C2 as PartFunc of [:M,M:],M by A18, RELSET_1:4; set CAT = CatStr(# O,M,DD,CC,Cm #); A33: CatStr(# O,M,DD,CC,Cm #) is Category-like proof let f, g be Morphism of CatStr(# O,M,DD,CC,Cm #); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #) ) ) reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def_4; A34: g in the carrier' of C2 by XBOOLE_0:def_4; A35: f in the carrier' of C2 by XBOOLE_0:def_4; hereby ::_thesis: ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #) ) assume [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) ; ::_thesis: dom g = cod f then A36: [g,f] in dom the Comp of C1 by A17, XBOOLE_0:def_4; thus dom g = dom g9 by A34, FUNCT_1:49 .= cod f9 by A36, CAT_1:def_6 .= cod f by A35, FUNCT_1:49 ; ::_thesis: verum end; assume A37: dom g = cod f ; ::_thesis: [g,f] in proj1 the Comp of CatStr(# O,M,DD,CC,Cm #) A38: dom g = dom g9 by A7, FUNCT_1:47; A39: dom g = cod f9 by A8, A37, FUNCT_1:47; A40: [g,f] in [: the carrier' of C2, the carrier' of C2:] by A34, A35, ZFMISC_1:87; [g,f] in dom the Comp of C1 by A38, A39, CAT_1:def_6; hence [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A17, A40, XBOOLE_0:def_4; ::_thesis: verum end; A41: for f, g being Morphism of CatStr(# O,M,DD,CC,Cm #) holds ( [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) iff dom g = cod f ) by A33, CAT_1:def_6; A42: CatStr(# O,M,DD,CC,Cm #) is transitive proof let f, g be Morphism of CatStr(# O,M,DD,CC,Cm #); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) ) reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def_4; assume A43: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) then A44: [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A41; A45: dom the Comp of CatStr(# O,M,DD,CC,Cm #) c= dom the Comp of C1 by RELAT_1:60; reconsider h = g (*) f as Morphism of CatStr(# O,M,DD,CC,Cm #) ; reconsider h9 = h as Morphism of C1 by XBOOLE_0:def_4; A46: h = the Comp of CatStr(# O,M,DD,CC,Cm #) . (g,f) by A44, CAT_1:def_1 .= the Comp of C1 . (g9,f9) by A44, FUNCT_1:47 .= g9 (*) f9 by A45, A44, CAT_1:def_1 ; A47: dom f = dom f9 by A7, FUNCT_1:47; A48: dom g = dom g9 by A7, FUNCT_1:47; A49: dom h = dom h9 by A7, FUNCT_1:47; A50: cod f = cod f9 by A8, FUNCT_1:47; A51: cod g = cod g9 by A8, FUNCT_1:47; A52: cod h = cod h9 by A8, FUNCT_1:47; thus dom (g (*) f) = dom f by A43, A47, A48, A49, A50, A46, CAT_1:def_7; ::_thesis: cod (g (*) f) = cod g thus cod (g (*) f) = cod g by A43, A46, A48, A50, A51, A52, CAT_1:def_7; ::_thesis: verum end; A53: for f, g being Morphism of CatStr(# O,M,DD,CC,Cm #) st dom g = cod f holds ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A42, CAT_1:def_7; A54: CatStr(# O,M,DD,CC,Cm #) is associative proof let f, g, h be Morphism of CatStr(# O,M,DD,CC,Cm #); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f ) reconsider h9 = h, g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def_4; assume that A55: dom h = cod g and A56: dom g = cod f ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f A57: [h,g] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A41, A55; A58: [g,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A41, A56; then reconsider hg = the Comp of CatStr(# O,M,DD,CC,Cm #) . (h,g), gf = the Comp of CatStr(# O,M,DD,CC,Cm #) . (g,f) as Morphism of CatStr(# O,M,DD,CC,Cm #) by A57, PARTFUN1:4; reconsider hg9 = hg, gf9 = gf as Morphism of C1 by XBOOLE_0:def_4; A59: dom hg = dom (h (*) g) by A57, CAT_1:def_1 .= dom g by A53, A55 ; A60: cod gf = cod (g (*) f) by A58, CAT_1:def_1 .= cod g by A53, A56 ; A61: [hg,f] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A41, A56, A59; A62: [h,gf] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A41, A55, A60; A63: dom h9 = dom h by A7, FUNCT_1:47; A64: cod g9 = cod g by A8, FUNCT_1:47; then A65: h9 (*) g9 = the Comp of C1 . (h9,g9) by A63, A55, CAT_1:16; A66: dom g9 = dom g by A7, FUNCT_1:47; A67: cod f9 = cod f by A8, FUNCT_1:47; then A68: g9 (*) f9 = the Comp of C1 . (g9,f9) by A66, A56, CAT_1:16; A69: cod (g9 (*) f9) = cod g9 by A56, A66, A67, CAT_1:def_7; A70: dom (h9 (*) g9) = dom g9 by A55, A63, A64, CAT_1:def_7; A71: hg = h (*) g by A57, CAT_1:def_1; gf = g (*) f by A58, CAT_1:def_1; hence h (*) (g (*) f) = the Comp of CatStr(# O,M,DD,CC,Cm #) . (h,( the Comp of CatStr(# O,M,DD,CC,Cm #) . (g,f))) by A62, CAT_1:def_1 .= the Comp of C1 . [h9,gf9] by A62, FUNCT_1:47 .= the Comp of C1 . (h9,( the Comp of C1 . (g9,f9))) by A58, FUNCT_1:47 .= h9 (*) (g9 (*) f9) by A69, A68, A55, A63, A64, CAT_1:16 .= (h9 (*) g9) (*) f9 by A55, A56, A63, A64, A66, A67, CAT_1:def_8 .= the Comp of C1 . (( the Comp of C1 . (h9,g9)),f9) by A70, A65, A56, A66, A67, CAT_1:16 .= the Comp of C1 . [hg9,f9] by A57, FUNCT_1:47 .= the Comp of CatStr(# O,M,DD,CC,Cm #) . (( the Comp of CatStr(# O,M,DD,CC,Cm #) . (h,g)),f) by A61, FUNCT_1:47 .= (h (*) g) (*) f by A71, A61, CAT_1:def_1 ; ::_thesis: verum end; A72: CatStr(# O,M,DD,CC,Cm #) is reflexive proof let b be Object of CatStr(# O,M,DD,CC,Cm #); :: according to CAT_1:def_9 ::_thesis: not Hom (b,b) = {} reconsider b1 = b as Object of C1 by XBOOLE_0:def_4; reconsider b2 = b as Object of C2 by XBOOLE_0:def_4; A73: the carrier of C1 c= the carrier of C by A1, CAT_2:def_4; b1 in the carrier of C1 ; then reconsider bb = b1 as Object of C by A73; A74: id b1 = id bb by A1, CAT_2:def_4 .= id b2 by A2, CAT_2:def_4 ; id b2 in the carrier' of C1 /\ the carrier' of C2 by A74, XBOOLE_0:def_4; then id b2 in M ; then reconsider ii = id b2 as Morphism of CatStr(# O,M,DD,CC,Cm #) ; A75: dom ii = dom (id b1) by A74, FUNCT_1:49 .= b ; cod ii = cod (id b1) by A74, FUNCT_1:49 .= b ; then ii in Hom (b,b) by A75; hence Hom (b,b) <> {} ; ::_thesis: verum end; CatStr(# O,M,DD,CC,Cm #) is with_identities proof let a be Element of CatStr(# O,M,DD,CC,Cm #); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st for b2 being Element of the carrier of CatStr(# O,M,DD,CC,Cm #) holds ( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) ) reconsider a1 = a as Object of C1 by XBOOLE_0:def_4; reconsider a2 = a as Object of C2 by XBOOLE_0:def_4; A76: the carrier of C1 c= the carrier of C by A1, CAT_2:def_4; a1 in the carrier of C1 ; then reconsider aa = a1 as Object of C by A76; A77: id a1 = id aa by A1, CAT_2:def_4 .= id a2 by A2, CAT_2:def_4 ; id a2 in the carrier' of C1 /\ the carrier' of C2 by A77, XBOOLE_0:def_4; then id a2 in M ; then reconsider ii = id a2 as Morphism of CatStr(# O,M,DD,CC,Cm #) ; A78: dom ii = dom (id a1) by A77, FUNCT_1:49 .= a ; cod ii = cod (id a1) by A77, FUNCT_1:49 .= a ; then ii in Hom (a,a) by A78; then reconsider ii = ii as Morphism of a,a by CAT_1:def_5; take ii ; ::_thesis: for b1 being Element of the carrier of CatStr(# O,M,DD,CC,Cm #) holds ( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) let b be Element of CatStr(# O,M,DD,CC,Cm #); ::_thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) ) thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) ::_thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) proof assume A79: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) ii = g let g be Morphism of a,b; ::_thesis: g (*) ii = g g in the carrier' of C1 by XBOOLE_0:def_4; then reconsider gg = g as Morphism of C1 ; A80: g in the carrier' of C2 by XBOOLE_0:def_4; A81: dom gg = the Source of C1 . g .= ( the Source of C1 | the carrier' of C2) . g by FUNCT_1:49, A80 .= dom g .= a1 by A79, CAT_1:5 ; A82: cod (id a1) = a1 ; cod ii = cod (id a1) by A77, FUNCT_1:49 .= dom g by A79, CAT_1:5 ; then A83: [g,ii] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A33, CAT_1:def_6; hence g (*) ii = Cm . (g,ii) by CAT_1:def_1 .= ( the Comp of C1 || the carrier' of C2) . (g,ii) .= the Comp of C1 . (gg,(id a1)) by A77, A83, FUNCT_1:47 .= gg (*) (id a1) by A82, A81, CAT_1:16 .= g by A81, CAT_1:22 ; ::_thesis: verum end; assume A84: Hom (b,a) <> {} ; ::_thesis: for b1 being Morphism of b,a holds ii (*) b1 = b1 let g be Morphism of b,a; ::_thesis: ii (*) g = g g in the carrier' of C1 by XBOOLE_0:def_4; then reconsider gg = g as Morphism of C1 ; A85: g in the carrier' of C2 by XBOOLE_0:def_4; A86: cod gg = the Target of C1 . g .= ( the Target of C1 | the carrier' of C2) . g by FUNCT_1:49, A85 .= cod g .= a1 by A84, CAT_1:5 ; A87: dom (id a1) = a1 ; dom ii = dom (id a1) by A77, FUNCT_1:49 .= cod g by A84, CAT_1:5 ; then A88: [ii,g] in dom the Comp of CatStr(# O,M,DD,CC,Cm #) by A33, CAT_1:def_6; hence ii (*) g = Cm . (ii,g) by CAT_1:def_1 .= ( the Comp of C1 || the carrier' of C2) . (ii,g) .= the Comp of C1 . ((id a1),gg) by A77, A88, FUNCT_1:47 .= (id a1) (*) gg by A87, A86, CAT_1:16 .= g by A86, CAT_1:21 ; ::_thesis: verum end; hence ex b1 being strict Category st ( the carrier of b1 = the carrier of C1 /\ the carrier of C2 & the carrier' of b1 = the carrier' of C1 /\ the carrier' of C2 & the Source of b1 = the Source of C1 | the carrier' of C2 & the Target of b1 = the Target of C1 | the carrier' of C2 & the Comp of b1 = the Comp of C1 || the carrier' of C2 ) by A33, A42, A54, A72; ::_thesis: verum end; uniqueness for b1, b2 being strict Category st the carrier of b1 = the carrier of C1 /\ the carrier of C2 & the carrier' of b1 = the carrier' of C1 /\ the carrier' of C2 & the Source of b1 = the Source of C1 | the carrier' of C2 & the Target of b1 = the Target of C1 | the carrier' of C2 & the Comp of b1 = the Comp of C1 || the carrier' of C2 & the carrier of b2 = the carrier of C1 /\ the carrier of C2 & the carrier' of b2 = the carrier' of C1 /\ the carrier' of C2 & the Source of b2 = the Source of C1 | the carrier' of C2 & the Target of b2 = the Target of C1 | the carrier' of C2 & the Comp of b2 = the Comp of C1 || the carrier' of C2 holds b1 = b2 ; end; :: deftheorem Def2 defines /\ CAT_5:def_2_:_ for C1, C2 being Category st ex C being Category st ( C1 is Subcategory of C & C2 is Subcategory of C ) & ex o1 being Object of C1 st o1 is Object of C2 holds for b3 being strict Category holds ( b3 = C1 /\ C2 iff ( the carrier of b3 = the carrier of C1 /\ the carrier of C2 & the carrier' of b3 = the carrier' of C1 /\ the carrier' of C2 & the Source of b3 = the Source of C1 | the carrier' of C2 & the Target of b3 = the Target of C1 | the carrier' of C2 & the Comp of b3 = the Comp of C1 || the carrier' of C2 ) ); theorem Th5: :: CAT_5:5 for C being Category for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds C1 /\ C2 = C2 /\ C1 proof let C be Category; ::_thesis: for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds C1 /\ C2 = C2 /\ C1 let C1, C2 be Subcategory of C; ::_thesis: ( the carrier of C1 meets the carrier of C2 implies C1 /\ C2 = C2 /\ C1 ) assume the carrier of C1 /\ the carrier of C2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: C1 /\ C2 = C2 /\ C1 then reconsider O = the carrier of C1 /\ the carrier of C2 as non empty set ; set o = the Element of O; set C12 = C1 /\ C2; set C21 = C2 /\ C1; set M1 = the carrier' of C1; set M2 = the carrier' of C2; set O1 = the carrier of C1; set O2 = the carrier of C2; A1: the Element of O is Object of C1 by XBOOLE_0:def_4; A2: the Element of O is Object of C2 by XBOOLE_0:def_4; then A3: the carrier of (C1 /\ C2) = O by A1, Def2; A4: the carrier of (C2 /\ C1) = O by A1, A2, Def2; A5: the carrier' of (C1 /\ C2) = the carrier' of C1 /\ the carrier' of C2 by A1, A2, Def2; A6: the Source of (C2 /\ C1) = the Source of C2 | the carrier' of C1 by A1, A2, Def2; A7: the Source of (C1 /\ C2) = the Source of C1 | the carrier' of C2 by A1, A2, Def2; A8: the Target of (C2 /\ C1) = the Target of C2 | the carrier' of C1 by A1, A2, Def2; A9: the Target of (C1 /\ C2) = the Target of C1 | the carrier' of C2 by A1, A2, Def2; A10: the Comp of (C2 /\ C1) = the Comp of C2 || the carrier' of C1 by A1, A2, Def2; A11: the Comp of (C1 /\ C2) = the Comp of C1 || the carrier' of C2 by A1, A2, Def2; A12: the Source of C1 = the Source of C | the carrier' of C1 by NATTRA_1:8; A13: the Target of C1 = the Target of C | the carrier' of C1 by NATTRA_1:8; A14: the Source of C2 = the Source of C | the carrier' of C2 by NATTRA_1:8; A15: the Target of C2 = the Target of C | the carrier' of C2 by NATTRA_1:8; A16: the Source of (C1 /\ C2) = the Source of C | ( the carrier' of C1 /\ the carrier' of C2) by A7, A12, RELAT_1:71 .= the Source of (C2 /\ C1) by A6, A14, RELAT_1:71 ; A17: the Target of (C1 /\ C2) = the Target of C | ( the carrier' of C1 /\ the carrier' of C2) by A9, A13, RELAT_1:71 .= the Target of (C2 /\ C1) by A8, A15, RELAT_1:71 ; the Comp of (C1 /\ C2) = ( the Comp of C || the carrier' of C1) || the carrier' of C2 by A11, NATTRA_1:8 .= the Comp of C | ([: the carrier' of C1, the carrier' of C1:] /\ [: the carrier' of C2, the carrier' of C2:]) by RELAT_1:71 .= ( the Comp of C || the carrier' of C2) || the carrier' of C1 by RELAT_1:71 .= the Comp of (C2 /\ C1) by A10, NATTRA_1:8 ; hence C1 /\ C2 = C2 /\ C1 by A1, A2, A3, A4, A5, A16, A17, Def2; ::_thesis: verum end; theorem Th6: :: CAT_5:6 for C being Category for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds ( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 ) proof let C be Category; ::_thesis: for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds ( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 ) let C1, C2 be Subcategory of C; ::_thesis: ( the carrier of C1 meets the carrier of C2 implies ( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 ) ) assume A1: the carrier of C1 meets the carrier of C2 ; ::_thesis: ( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 ) then A2: the carrier of C1 /\ the carrier of C2 <> {} by XBOOLE_0:def_7; A3: C1 /\ C2 = C2 /\ C1 by A1, Th5; now__::_thesis:_for_C1,_C2_being_Subcategory_of_C_st_the_carrier_of_C1_/\_the_carrier_of_C2_<>_{}_holds_ C1_/\_C2_is_Subcategory_of_C1 let C1, C2 be Subcategory of C; ::_thesis: ( the carrier of C1 /\ the carrier of C2 <> {} implies C1 /\ C2 is Subcategory of C1 ) assume A4: the carrier of C1 /\ the carrier of C2 <> {} ; ::_thesis: C1 /\ C2 is Subcategory of C1 A5: the carrier of C1 /\ the carrier of C2 c= the carrier of C1 by XBOOLE_1:17; A6: the carrier' of C1 /\ the carrier' of C2 c= the carrier' of C1 by XBOOLE_1:17; reconsider O = the carrier of C1 /\ the carrier of C2 as non empty set by A4; set o = the Element of O; A7: the Element of O is Object of C1 by XBOOLE_0:def_4; A8: the Element of O is Object of C2 by XBOOLE_0:def_4; then A9: the carrier of (C1 /\ C2) = the carrier of C1 /\ the carrier of C2 by A7, Def2; A10: the carrier' of (C1 /\ C2) = the carrier' of C1 /\ the carrier' of C2 by A7, A8, Def2; A11: the Source of (C1 /\ C2) = the Source of C1 | the carrier' of C2 by A7, A8, Def2; A12: the Target of (C1 /\ C2) = the Target of C1 | the carrier' of C2 by A7, A8, Def2; A13: the Comp of (C1 /\ C2) = the Comp of C1 || the carrier' of C2 by A7, A8, Def2; A14: the Source of C1 = the Source of C1 | (dom the Source of C1) ; dom the Source of C1 = the carrier' of C1 by FUNCT_2:def_1; then A15: the Source of (C1 /\ C2) = the Source of C1 | the carrier' of (C1 /\ C2) by A10, A11, A14, RELAT_1:71; A16: the Target of C1 = the Target of C1 | (dom the Target of C1) ; dom the Target of C1 = the carrier' of C1 by FUNCT_2:def_1; then A17: the Target of (C1 /\ C2) = the Target of C1 | the carrier' of (C1 /\ C2) by A10, A12, A16, RELAT_1:71; A18: for o being Element of C1 st o in O holds id o in the carrier' of C1 /\ the carrier' of C2 proof let o1 be Element of C1; ::_thesis: ( o1 in O implies id o1 in the carrier' of C1 /\ the carrier' of C2 ) assume o1 in O ; ::_thesis: id o1 in the carrier' of C1 /\ the carrier' of C2 then reconsider o2 = o1 as Element of C2 by XBOOLE_0:def_4; A19: the carrier of C1 c= the carrier of C by CAT_2:def_4; o1 in the carrier of C1 ; then reconsider o = o1 as Element of C by A19; A20: id o1 = id o by CAT_2:def_4; id o2 = id o by CAT_2:def_4; hence id o1 in the carrier' of C1 /\ the carrier' of C2 by A20, XBOOLE_0:def_4; ::_thesis: verum end; the Comp of C1 = the Comp of C1 || the carrier' of C1 ; then the Comp of (C1 /\ C2) = the Comp of C1 | ([: the carrier' of C1, the carrier' of C1:] /\ [: the carrier' of C2, the carrier' of C2:]) by A13, RELAT_1:71; then the Comp of (C1 /\ C2) = the Comp of C1 || the carrier' of (C1 /\ C2) by A10, ZFMISC_1:100; hence C1 /\ C2 is Subcategory of C1 by A5, A6, A9, A10, A15, A17, NATTRA_1:9, A18; ::_thesis: verum end; hence ( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 ) by A2, A3; ::_thesis: verum end; definition let C, D be Category; let F be Functor of C,D; func Image F -> strict Subcategory of D means :Def3: :: CAT_5:def 3 ( the carrier of it = rng (Obj F) & rng F c= the carrier' of it & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds it is Subcategory of E ) ); existence ex b1 being strict Subcategory of D st ( the carrier of b1 = rng (Obj F) & rng F c= the carrier' of b1 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds b1 is Subcategory of E ) ) proof set a = the Object of C; A1: dom (Obj F) = the carrier of C by FUNCT_2:def_1; then (Obj F) . the Object of C in rng (Obj F) by FUNCT_1:def_3; then reconsider O = rng (Obj F) as non empty set ; reconsider O = O as non empty Subset of the carrier of D ; set f = the Morphism of C; A2: dom F = the carrier' of C by FUNCT_2:def_1; A3: dom the Source of D = the carrier' of D by FUNCT_2:def_1; A4: dom the Target of D = the carrier' of D by FUNCT_2:def_1; defpred S1[ set ] means ( rng F c= \$1 & ex E being Subcategory of D st ( the carrier of E = O & the carrier' of E = \$1 ) ); consider MM being set such that A5: for x being set holds ( x in MM iff ( x in bool the carrier' of D & S1[x] ) ) from XBOOLE_0:sch_1(); set HH = { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } ; reconsider M0 = union { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } as non empty Subset of the carrier' of D by CAT_2:19; reconsider D0 = the Source of D | M0, C0 = the Target of D | M0 as Function of M0,O by CAT_2:20; reconsider CC = the Comp of D || M0 as PartFunc of [:M0,M0:],M0 by CAT_2:20; CatStr(# O,M0,D0,C0,CC #) is full Subcategory of D by CAT_2:21; then A6: CatStr(# O,M0,D0,C0,CC #) is Subcategory of D ; rng F c= M0 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in M0 ) assume y in rng F ; ::_thesis: y in M0 then consider x being set such that A7: x in dom F and A8: y = F . x by FUNCT_1:def_3; reconsider x = x as Morphism of C by A7; A9: (Obj F) . (dom x) in O by A1, FUNCT_1:def_3; A10: (Obj F) . (cod x) in O by A1, FUNCT_1:def_3; A11: dom (F . x) in O by A9, CAT_1:69; A12: cod (F . x) in O by A10, CAT_1:69; A13: y in Hom ((dom (F . x)),(cod (F . x))) by A8; Hom ((dom (F . x)),(cod (F . x))) in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by A11, A12; hence y in M0 by A13, TARSKI:def_4; ::_thesis: verum end; then A14: M0 in MM by A5, A6; set M = meet MM; A15: for Z being set st Z in MM holds rng F c= Z by A5; now__::_thesis:_for_X_being_set_st_X_in_MM_holds_ F_._the_Morphism_of_C_in_X let X be set ; ::_thesis: ( X in MM implies F . the Morphism of C in X ) assume X in MM ; ::_thesis: F . the Morphism of C in X then A16: rng F c= X by A5; F . the Morphism of C in rng F by A2, FUNCT_1:def_3; hence F . the Morphism of C in X by A16; ::_thesis: verum end; then reconsider M = meet MM as non empty set by A14, SETFAM_1:def_1; M c= the carrier' of D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M or x in the carrier' of D ) assume x in M ; ::_thesis: x in the carrier' of D then x in M0 by A14, SETFAM_1:def_1; hence x in the carrier' of D ; ::_thesis: verum end; then reconsider M = M as non empty Subset of the carrier' of D ; set DOM = the Source of D | M; set COD = the Target of D | M; set COMP = the Comp of D || M; A17: dom ( the Source of D | M) = M by A3, RELAT_1:62; rng ( the Source of D | M) c= O proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Source of D | M) or y in O ) assume y in rng ( the Source of D | M) ; ::_thesis: y in O then consider x being set such that A18: x in M and A19: y = ( the Source of D | M) . x by A17, FUNCT_1:def_3; reconsider x = x as Morphism of D by A18; x in M0 by A14, A18, SETFAM_1:def_1; then consider X being set such that A20: x in X and A21: X in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by TARSKI:def_4; consider a, b being Object of D such that A22: X = Hom (a,b) and A23: a in O and b in O by A21; dom x = a by A20, A22, CAT_1:1; hence y in O by A17, A18, A19, A23, FUNCT_1:47; ::_thesis: verum end; then reconsider DOM = the Source of D | M as Function of M,O by A17, FUNCT_2:def_1, RELSET_1:4; A24: dom ( the Target of D | M) = M by A4, RELAT_1:62; rng ( the Target of D | M) c= O proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Target of D | M) or y in O ) assume y in rng ( the Target of D | M) ; ::_thesis: y in O then consider x being set such that A25: x in M and A26: y = ( the Target of D | M) . x by A24, FUNCT_1:def_3; reconsider x = x as Morphism of D by A25; x in M0 by A14, A25, SETFAM_1:def_1; then consider X being set such that A27: x in X and A28: X in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by TARSKI:def_4; consider a, b being Object of D such that A29: X = Hom (a,b) and a in O and A30: b in O by A28; cod x = b by A27, A29, CAT_1:1; hence y in O by A24, A25, A26, A30, FUNCT_1:47; ::_thesis: verum end; then reconsider COD = the Target of D | M as Function of M,O by A24, FUNCT_2:def_1, RELSET_1:4; A31: dom ( the Comp of D || M) c= [:M,M:] by RELAT_1:58; rng ( the Comp of D || M) c= M proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the Comp of D || M) or y in M ) assume y in rng ( the Comp of D || M) ; ::_thesis: y in M then consider x being set such that A32: x in dom ( the Comp of D || M) and A33: y = ( the Comp of D || M) . x by FUNCT_1:def_3; reconsider x1 = x `1 , x2 = x `2 as Element of M by A31, A32, MCART_1:10; A34: x = [x1,x2] by A31, A32, MCART_1:21; now__::_thesis:_for_X_being_set_st_X_in_MM_holds_ y_in_X let X be set ; ::_thesis: ( X in MM implies y in X ) assume A35: X in MM ; ::_thesis: y in X then consider E being Subcategory of D such that the carrier of E = O and A36: the carrier' of E = X by A5; reconsider y1 = x1, y2 = x2 as Morphism of E by A35, A36, SETFAM_1:def_1; dom ( the Comp of D || M) = (dom the Comp of D) /\ [:M,M:] by RELAT_1:61; then x in dom the Comp of D by A32, XBOOLE_0:def_4; then A37: dom x1 = cod x2 by A34, CAT_1:15; A38: dom y1 = dom x1 by CAT_2:9; cod y2 = cod x2 by CAT_2:9; then A39: x in dom the Comp of E by A34, A37, A38, CAT_1:15; the Comp of E c= the Comp of D by CAT_2:def_4; then the Comp of E . x = the Comp of D . x by A39, GRFUNC_1:2 .= y by A32, A33, FUNCT_1:47 ; then y in rng the Comp of E by A39, FUNCT_1:def_3; hence y in X by A36; ::_thesis: verum end; hence y in M by A14, SETFAM_1:def_1; ::_thesis: verum end; then reconsider COMP = the Comp of D || M as PartFunc of [:M,M:],M by A31, RELSET_1:4; for o being Element of D st o in O holds id o in M proof let o be Element of D; ::_thesis: ( o in O implies id o in M ) assume A40: o in O ; ::_thesis: id o in M for X being set st X in MM holds id o in X proof let X be set ; ::_thesis: ( X in MM implies id o in X ) assume X in MM ; ::_thesis: id o in X then S1[X] by A5; then consider E being Subcategory of D such that A41: the carrier of E = O and A42: the carrier' of E = X ; o in the carrier of E by A40, A41; then reconsider oo = o as Element of E ; id oo = id o by CAT_2:def_4; hence id o in X by A42; ::_thesis: verum end; hence id o in M by SETFAM_1:def_1, A14; ::_thesis: verum end; then reconsider T = CatStr(# O,M,DOM,COD,COMP #) as strict Subcategory of D by NATTRA_1:9; take T ; ::_thesis: ( the carrier of T = rng (Obj F) & rng F c= the carrier' of T & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds T is Subcategory of E ) ) thus ( the carrier of T = rng (Obj F) & rng F c= the carrier' of T ) by A14, A15, SETFAM_1:5; ::_thesis: for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds T is Subcategory of E let E be Subcategory of D; ::_thesis: ( the carrier of E = rng (Obj F) & rng F c= the carrier' of E implies T is Subcategory of E ) assume that A43: the carrier of E = rng (Obj F) and A44: rng F c= the carrier' of E ; ::_thesis: T is Subcategory of E thus the carrier of T c= the carrier of E by A43; :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of T for b3, b4 being Element of the carrier of E holds ( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of T c= the Comp of E & ( for b1 being Element of the carrier of T for b2 being Element of the carrier of E holds ( not b1 = b2 or id b1 = id b2 ) ) ) the carrier' of E c= the carrier' of D by CAT_2:7; then the carrier' of E in MM by A5, A43, A44; then A45: M c= the carrier' of E by SETFAM_1:3; hereby ::_thesis: ( the Comp of T c= the Comp of E & ( for b1 being Element of the carrier of T for b2 being Element of the carrier of E holds ( not b1 = b2 or id b1 = id b2 ) ) ) let a, b be Object of T; ::_thesis: for a9, b9 being Object of E st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) let a9, b9 be Object of E; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) ) assume that A46: a = a9 and A47: b = b9 ; ::_thesis: Hom (a,b) c= Hom (a9,b9) thus Hom (a,b) c= Hom (a9,b9) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) ) assume x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9) then consider f being Morphism of T such that A48: x = f and A49: dom f = a and A50: cod f = b ; reconsider g = f as Morphism of D by TARSKI:def_3; reconsider f = f as Morphism of E by A45, TARSKI:def_3; A51: dom g = a by A49, CAT_2:9; A52: cod g = b by A50, CAT_2:9; A53: a9 = dom f by A46, A51, CAT_2:9; b9 = cod f by A47, A52, CAT_2:9; hence x in Hom (a9,b9) by A48, A53; ::_thesis: verum end; end; A54: dom the Comp of T c= dom the Comp of E proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom the Comp of T or x in dom the Comp of E ) assume A55: x in dom the Comp of T ; ::_thesis: x in dom the Comp of E then reconsider x1 = x `1 , x2 = x `2 as Element of M by MCART_1:10; reconsider y1 = x1, y2 = x2 as Morphism of T ; reconsider z1 = x1, z2 = x2 as Morphism of E by A45, TARSKI:def_3; A56: x = [x1,x2] by A55, MCART_1:21; then A57: dom y1 = cod y2 by A55, CAT_1:15; A58: dom y1 = dom x1 by CAT_2:9; A59: dom z1 = dom x1 by CAT_2:9; A60: cod y2 = cod x2 by CAT_2:9; cod z2 = cod x2 by CAT_2:9; hence x in dom the Comp of E by A56, A57, A58, A59, A60, CAT_1:15; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_the_Comp_of_T_holds_ the_Comp_of_T_._x_=_the_Comp_of_E_._x let x be set ; ::_thesis: ( x in dom the Comp of T implies the Comp of T . x = the Comp of E . x ) assume A61: x in dom the Comp of T ; ::_thesis: the Comp of T . x = the Comp of E . x A62: the Comp of T c= the Comp of D by CAT_2:def_4; A63: the Comp of E c= the Comp of D by CAT_2:def_4; thus the Comp of T . x = the Comp of D . x by A61, A62, GRFUNC_1:2 .= the Comp of E . x by A54, A61, A63, GRFUNC_1:2 ; ::_thesis: verum end; hence the Comp of T c= the Comp of E by A54, GRFUNC_1:2; ::_thesis: for b1 being Element of the carrier of T for b2 being Element of the carrier of E holds ( not b1 = b2 or id b1 = id b2 ) let a be Object of T; ::_thesis: for b1 being Element of the carrier of E holds ( not a = b1 or id a = id b1 ) let a9 be Object of E; ::_thesis: ( not a = a9 or id a = id a9 ) reconsider b = a as Object of D by TARSKI:def_3; assume A64: a = a9 ; ::_thesis: id a = id a9 id a = id b by CAT_2:def_4; hence id a = id a9 by A64, CAT_2:def_4; ::_thesis: verum end; uniqueness for b1, b2 being strict Subcategory of D st the carrier of b1 = rng (Obj F) & rng F c= the carrier' of b1 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds b1 is Subcategory of E ) & the carrier of b2 = rng (Obj F) & rng F c= the carrier' of b2 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds b2 is Subcategory of E ) holds b1 = b2 proof let C1, C2 be strict Subcategory of D; ::_thesis: ( the carrier of C1 = rng (Obj F) & rng F c= the carrier' of C1 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds C1 is Subcategory of E ) & the carrier of C2 = rng (Obj F) & rng F c= the carrier' of C2 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds C2 is Subcategory of E ) implies C1 = C2 ) assume that A65: the carrier of C1 = rng (Obj F) and A66: rng F c= the carrier' of C1 and A67: for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds C1 is Subcategory of E and A68: the carrier of C2 = rng (Obj F) and A69: rng F c= the carrier' of C2 and A70: for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds C2 is Subcategory of E ; ::_thesis: C1 = C2 A71: C1 is Subcategory of C2 by A67, A68, A69; C2 is Subcategory of C1 by A65, A66, A70; hence C1 = C2 by A71, Th3; ::_thesis: verum end; end; :: deftheorem Def3 defines Image CAT_5:def_3_:_ for C, D being Category for F being Functor of C,D for b4 being strict Subcategory of D holds ( b4 = Image F iff ( the carrier of b4 = rng (Obj F) & rng F c= the carrier' of b4 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds b4 is Subcategory of E ) ) ); theorem Th7: :: CAT_5:7 for C, D being Category for E being Subcategory of D for F being Functor of C,D st rng F c= the carrier' of E holds F is Functor of C,E proof let C, D be Category; ::_thesis: for E being Subcategory of D for F being Functor of C,D st rng F c= the carrier' of E holds F is Functor of C,E let E be Subcategory of D; ::_thesis: for F being Functor of C,D st rng F c= the carrier' of E holds F is Functor of C,E let F be Functor of C,D; ::_thesis: ( rng F c= the carrier' of E implies F is Functor of C,E ) assume A1: rng F c= the carrier' of E ; ::_thesis: F is Functor of C,E A2: dom F = the carrier' of C by FUNCT_2:def_1; A3: dom (Obj F) = the carrier of C by FUNCT_2:def_1; reconsider G = F as Function of the carrier' of C, the carrier' of E by A1, A2, FUNCT_2:def_1, RELSET_1:4; A4: rng (Obj F) c= the carrier of E proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Obj F) or y in the carrier of E ) assume y in rng (Obj F) ; ::_thesis: y in the carrier of E then consider x being set such that A5: x in dom (Obj F) and A6: y = (Obj F) . x by FUNCT_1:def_3; reconsider x = x as Object of C by A5; F . (id x) = id ((Obj F) . x) by CAT_1:68; then id ((Obj F) . x) in rng F by A2, FUNCT_1:def_3; then reconsider f = id ((Obj F) . x) as Morphism of E by A1; A7: dom (id ((Obj F) . x)) = y by A6; dom (id ((Obj F) . x)) = dom f by CAT_2:9; hence y in the carrier of E by A7; ::_thesis: verum end; A8: now__::_thesis:_for_c_being_Object_of_C_ex_d_being_Object_of_E_st_G_._(id_c)_=_id_d let c be Object of C; ::_thesis: ex d being Object of E st G . (id c) = id d (Obj F) . c in rng (Obj F) by A3, FUNCT_1:def_3; then reconsider d = (Obj F) . c as Object of E by A4; take d = d; ::_thesis: G . (id c) = id d thus G . (id c) = id ((Obj F) . c) by CAT_1:68 .= id d by CAT_2:def_4 ; ::_thesis: verum end; A9: now__::_thesis:_for_f_being_Morphism_of_C_holds_ (_G_._(id_(dom_f))_=_id_(dom_(G_._f))_&_G_._(id_(cod_f))_=_id_(cod_(G_._f))_) let f be Morphism of C; ::_thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) ) A10: dom (F . f) = dom (G . f) by CAT_2:9; A11: cod (F . f) = cod (G . f) by CAT_2:9; thus G . (id (dom f)) = id (F . (dom f)) by CAT_1:71 .= id (dom (F . f)) by CAT_1:72 .= id (dom (G . f)) by A10, CAT_2:def_4 ; ::_thesis: G . (id (cod f)) = id (cod (G . f)) thus G . (id (cod f)) = id (F . (cod f)) by CAT_1:71 .= id (cod (F . f)) by CAT_1:72 .= id (cod (G . f)) by A11, CAT_2:def_4 ; ::_thesis: verum end; now__::_thesis:_for_f,_g_being_Morphism_of_C_st_dom_g_=_cod_f_holds_ G_._(g_(*)_f)_=_(G_._g)_(*)_(G_._f) let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies G . (g (*) f) = (G . g) (*) (G . f) ) assume A12: dom g = cod f ; ::_thesis: G . (g (*) f) = (G . g) (*) (G . f) then A13: F . (g (*) f) = (F . g) (*) (F . f) by CAT_1:64; A14: dom (F . g) = cod (F . f) by A12, CAT_1:64; A15: dom (F . g) = dom (G . g) by CAT_2:9; cod (F . f) = cod (G . f) by CAT_2:9; hence G . (g (*) f) = (G . g) (*) (G . f) by A13, A14, A15, CAT_2:11; ::_thesis: verum end; hence F is Functor of C,E by A8, A9, CAT_1:61; ::_thesis: verum end; theorem :: CAT_5:8 for C, D being Category for F being Functor of C,D holds F is Functor of C, Image F proof let C, D be Category; ::_thesis: for F being Functor of C,D holds F is Functor of C, Image F let F be Functor of C,D; ::_thesis: F is Functor of C, Image F rng F c= the carrier' of (Image F) by Def3; hence F is Functor of C, Image F by Th7; ::_thesis: verum end; theorem Th9: :: CAT_5:9 for C, D being Category for E being Subcategory of D for F being Functor of C,E for G being Functor of C,D st F = G holds Image F = Image G proof let C, D be Category; ::_thesis: for E being Subcategory of D for F being Functor of C,E for G being Functor of C,D st F = G holds Image F = Image G let E be Subcategory of D; ::_thesis: for F being Functor of C,E for G being Functor of C,D st F = G holds Image F = Image G let F be Functor of C,E; ::_thesis: for G being Functor of C,D st F = G holds Image F = Image G let G be Functor of C,D; ::_thesis: ( F = G implies Image F = Image G ) assume A1: F = G ; ::_thesis: Image F = Image G reconsider S = Image F as strict Subcategory of D by Th4; A2: now__::_thesis:_(_dom_(Obj_F)_=_the_carrier_of_C_&_dom_(Obj_G)_=_the_carrier_of_C_&_(_for_x_being_set_st_x_in_the_carrier_of_C_holds_ (Obj_G)_._x_=_(Obj_F)_._x_)_) thus ( dom (Obj F) = the carrier of C & dom (Obj G) = the carrier of C ) by FUNCT_2:def_1; ::_thesis: for x being set st x in the carrier of C holds (Obj G) . x = (Obj F) . x let x be set ; ::_thesis: ( x in the carrier of C implies (Obj G) . x = (Obj F) . x ) assume x in the carrier of C ; ::_thesis: (Obj G) . x = (Obj F) . x then reconsider a = x as Object of C ; reconsider b = (Obj F) . a as Object of D by CAT_2:6; G . (id a) = id ((Obj F) . a) by A1, CAT_1:68 .= id b by CAT_2:def_4 ; hence (Obj G) . x = (Obj F) . x by CAT_1:67; ::_thesis: verum end; then A3: Obj F = Obj G by FUNCT_1:2; then A4: the carrier of S = rng (Obj G) by Def3; A5: rng G c= the carrier' of S by A1, Def3; now__::_thesis:_for_T_being_Subcategory_of_D_st_the_carrier_of_T_=_rng_(Obj_G)_&_rng_G_c=_the_carrier'_of_T_holds_ S_is_Subcategory_of_T let T be Subcategory of D; ::_thesis: ( the carrier of T = rng (Obj G) & rng G c= the carrier' of T implies S is Subcategory of T ) assume that A6: the carrier of T = rng (Obj G) and A7: rng G c= the carrier' of T ; ::_thesis: S is Subcategory of T set x = the Object of C; A8: (Obj G) . the Object of C in rng (Obj G) by A2, FUNCT_1:def_3; A9: (Obj G) . the Object of C = (Obj F) . the Object of C by A2; then (Obj G) . the Object of C in the carrier of T /\ the carrier of E by A6, A8, XBOOLE_0:def_4; then A10: the carrier of T meets the carrier of E by XBOOLE_0:def_7; then reconsider E1 = T /\ E as Subcategory of E by Th6; the carrier of E1 = the carrier of T /\ the carrier of E by A6, A8, A9, Def2; then A11: the carrier of E1 = rng (Obj F) by A3, A6, XBOOLE_1:28; the carrier' of E1 = the carrier' of T /\ the carrier' of E by A6, A8, A9, Def2; then rng F c= the carrier' of E1 by A1, A7, XBOOLE_1:19; then A12: Image F is Subcategory of E1 by A11, Def3; E1 is Subcategory of T by A10, Th6; hence S is Subcategory of T by A12, Th4; ::_thesis: verum end; hence Image F = Image G by A4, A5, Def3; ::_thesis: verum end; begin definition let IT be set ; attrIT is categorial means :Def4: :: CAT_5:def 4 for x being set st x in IT holds x is Category; end; :: deftheorem Def4 defines categorial CAT_5:def_4_:_ for IT being set holds ( IT is categorial iff for x being set st x in IT holds x is Category ); definition let X be non empty set ; redefine attr X is categorial means :Def5: :: CAT_5:def 5 for x being Element of X holds x is Category; compatibility ( X is categorial iff for x being Element of X holds x is Category ) proof thus ( X is categorial implies for x being Element of X holds x is Category ) by Def4; ::_thesis: ( ( for x being Element of X holds x is Category ) implies X is categorial ) assume A1: for x being Element of X holds x is Category ; ::_thesis: X is categorial let x be set ; :: according to CAT_5:def_4 ::_thesis: ( x in X implies x is Category ) thus ( x in X implies x is Category ) by A1; ::_thesis: verum end; end; :: deftheorem Def5 defines categorial CAT_5:def_5_:_ for X being non empty set holds ( X is categorial iff for x being Element of X holds x is Category ); registration cluster non empty categorial for set ; existence ex b1 being non empty set st b1 is categorial proof take X = {(1Cat (0,1))}; ::_thesis: X is categorial let x be Element of X; :: according to CAT_5:def_5 ::_thesis: x is Category thus x is Category by TARSKI:def_1; ::_thesis: verum end; end; definition let X be non empty categorial set ; :: original: Element redefine mode Element of X -> Category; coherence for b1 being Element of X holds b1 is Category by Def4; end; definition let C be Category; attrC is Categorial means :Def6: :: CAT_5:def 6 ( the carrier of C is categorial & ( for a being Object of C for A being Category st a = A holds id a = [[A,A],(id A)] ) & ( for m being Morphism of C for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ); end; :: deftheorem Def6 defines Categorial CAT_5:def_6_:_ for C being Category holds ( C is Categorial iff ( the carrier of C is categorial & ( for a being Object of C for A being Category st a = A holds id a = [[A,A],(id A)] ) & ( for m being Morphism of C for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) ); registration cluster non empty non void Category-like transitive associative reflexive with_identities Categorial -> with_triple-like_morphisms for CatStr ; coherence for b1 being Category st b1 is Categorial holds b1 is with_triple-like_morphisms proof let C be Category; ::_thesis: ( C is Categorial implies C is with_triple-like_morphisms ) assume A1: C is Categorial ; ::_thesis: C is with_triple-like_morphisms then A2: the carrier of C is categorial by Def6; let f be Morphism of C; :: according to CAT_5:def_1 ::_thesis: ex x being set st f = [[(dom f),(cod f)],x] reconsider A = dom f, B = cod f as Category by A2, Def5; ex F being Functor of A,B st f = [[A,B],F] by A1, Def6; hence ex x being set st f = [[(dom f),(cod f)],x] ; ::_thesis: verum end; end; theorem Th10: :: CAT_5:10 for C, D being Category st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) & C is Categorial holds D is Categorial proof let C, D be Category; ::_thesis: ( CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) & C is Categorial implies D is Categorial ) assume A1: CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) ; ::_thesis: ( not C is Categorial or D is Categorial ) assume that A2: the carrier of C is categorial and A3: for a being Object of C for A being Category st a = A holds id a = [[A,A],(id A)] and A4: for m being Morphism of C for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] and A5: for m1, m2 being Morphism of C for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ; :: according to CAT_5:def_6 ::_thesis: D is Categorial thus the carrier of D is categorial by A1, A2; :: according to CAT_5:def_6 ::_thesis: ( ( for a being Object of D for A being Category st a = A holds id a = [[A,A],(id A)] ) & ( for m being Morphism of D for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of D for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) thus for a being Object of D for A being Category st a = A holds id a = [[A,A],(id A)] ::_thesis: ( ( for m being Morphism of D for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of D for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) proof let a be Object of D; ::_thesis: for A being Category st a = A holds id a = [[A,A],(id A)] let A be Category; ::_thesis: ( a = A implies id a = [[A,A],(id A)] ) reconsider b = a as Object of C by A1; assume a = A ; ::_thesis: id a = [[A,A],(id A)] then [[A,A],(id A)] = id b by A3; hence id a = [[A,A],(id A)] by A1, Lm1; ::_thesis: verum end; hereby ::_thesis: for m1, m2 being Morphism of D for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let m be Morphism of D; ::_thesis: for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] reconsider m9 = m as Morphism of C by A1; let A, B be Category; ::_thesis: ( A = dom m & B = cod m implies ex F being Functor of A,B st m = [[A,B],F] ) assume that A6: A = dom m and A7: B = cod m ; ::_thesis: ex F being Functor of A,B st m = [[A,B],F] A8: A = dom m9 by A1, A6; B = cod m9 by A1, A7; hence ex F being Functor of A,B st m = [[A,B],F] by A4, A8; ::_thesis: verum end; let m1, m2 be Morphism of D; ::_thesis: for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] reconsider f1 = m1, f2 = m2 as Morphism of C by A1; let a, b, c be Category; ::_thesis: for F being Functor of a,b for G being Functor of b,c st m1 = [[a,b],F] & m2 = [[b,c],G] holds m2 (*) m1 = [[a,c],(G * F)] let F be Functor of a,b; ::_thesis: for G being Functor of b,c st m1 = [[a,b],F] & m2 = [[b,c],G] holds m2 (*) m1 = [[a,c],(G * F)] let G be Functor of b,c; ::_thesis: ( m1 = [[a,b],F] & m2 = [[b,c],G] implies m2 (*) m1 = [[a,c],(G * F)] ) assume that A9: m1 = [[a,b],F] and A10: m2 = [[b,c],G] ; ::_thesis: m2 (*) m1 = [[a,c],(G * F)] reconsider a1 = dom f1, b1 = cod f1, a2 = dom f2, b2 = cod f2 as Category by A2, Def5; A11: ex F1 being Functor of a1,b1 st f1 = [[a1,b1],F1] by A4; ex F2 being Functor of a2,b2 st f2 = [[a2,b2],F2] by A4; then A12: dom f2 = m2 `11 by MCART_1:85; A13: m2 `11 = b by A10, MCART_1:85; A14: cod f1 = m1 `12 by A11, MCART_1:85; m1 `12 = b by A9, MCART_1:85; then A15: [f2,f1] in dom the Comp of C by A12, A13, A14, CAT_1:15; hence m2 (*) m1 = the Comp of D . (m2,m1) by A1, CAT_1:def_1 .= f2 (*) f1 by A1, A15, CAT_1:def_1 .= [[a,c],(G * F)] by A5, A9, A10 ; ::_thesis: verum end; theorem Th11: :: CAT_5:11 for C being Category holds 1Cat (C,[[C,C],(id C)]) is Categorial proof let A be Category; ::_thesis: 1Cat (A,[[A,A],(id A)]) is Categorial set F = [[A,A],(id A)]; set C = 1Cat (A,[[A,A],(id A)]); thus for x being Object of (1Cat (A,[[A,A],(id A)])) holds x is Category by TARSKI:def_1; :: according to CAT_5:def_5,CAT_5:def_6 ::_thesis: ( ( for a being Object of (1Cat (A,[[A,A],(id A)])) for A being Category st a = A holds id a = [[A,A],(id A)] ) & ( for m being Morphism of (1Cat (A,[[A,A],(id A)])) for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of (1Cat (A,[[A,A],(id A)])) for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) hereby ::_thesis: ( ( for m being Morphism of (1Cat (A,[[A,A],(id A)])) for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of (1Cat (A,[[A,A],(id A)])) for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) let a be Object of (1Cat (A,[[A,A],(id A)])); ::_thesis: for D being Category st a = D holds id a = [[D,D],(id D)] let D be Category; ::_thesis: ( a = D implies id a = [[D,D],(id D)] ) assume a = D ; ::_thesis: id a = [[D,D],(id D)] then D = A by TARSKI:def_1; hence id a = [[D,D],(id D)] by TARSKI:def_1; ::_thesis: verum end; hereby ::_thesis: for m1, m2 being Morphism of (1Cat (A,[[A,A],(id A)])) for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let m be Morphism of (1Cat (A,[[A,A],(id A)])); ::_thesis: for C1, C2 being Category st C1 = dom m & C2 = cod m holds ex G being Functor of C1,C2 st m = [[C1,C2],G] let C1, C2 be Category; ::_thesis: ( C1 = dom m & C2 = cod m implies ex G being Functor of C1,C2 st m = [[C1,C2],G] ) assume that A1: C1 = dom m and A2: C2 = cod m ; ::_thesis: ex G being Functor of C1,C2 st m = [[C1,C2],G] A3: C1 = A by A1, TARSKI:def_1; A4: C2 = A by A2, TARSKI:def_1; reconsider G = id A as Functor of C1,C2 by A2, A3, TARSKI:def_1; take G = G; ::_thesis: m = [[C1,C2],G] thus m = [[C1,C2],G] by A3, A4, TARSKI:def_1; ::_thesis: verum end; let m1, m2 be Morphism of (1Cat (A,[[A,A],(id A)])); ::_thesis: for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let A1, B, C be Category; ::_thesis: for F being Functor of A1,B for G being Functor of B,C st m1 = [[A1,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A1,C],(G * F)] let F1 be Functor of A1,B; ::_thesis: for G being Functor of B,C st m1 = [[A1,B],F1] & m2 = [[B,C],G] holds m2 (*) m1 = [[A1,C],(G * F1)] let F2 be Functor of B,C; ::_thesis: ( m1 = [[A1,B],F1] & m2 = [[B,C],F2] implies m2 (*) m1 = [[A1,C],(F2 * F1)] ) assume that A5: m1 = [[A1,B],F1] and A6: m2 = [[B,C],F2] ; ::_thesis: m2 (*) m1 = [[A1,C],(F2 * F1)] A7: [[A1,B],F1] = [[A,A],(id A)] by A5, TARSKI:def_1; A8: [[B,C],F2] = [[A,A],(id A)] by A6, TARSKI:def_1; A9: [A1,B] = [A,A] by A7, XTUPLE_0:1; A10: [A,A] = [B,C] by A8, XTUPLE_0:1; A11: F1 = id A by A7, XTUPLE_0:1; A12: F2 = id A by A8, XTUPLE_0:1; A13: A1 = A by A9, XTUPLE_0:1; A14: C = A by A10, XTUPLE_0:1; F2 * F1 = id A by A11, A12, FUNCT_2:17; hence m2 (*) m1 = [[A1,C],(F2 * F1)] by A13, A14, TARSKI:def_1; ::_thesis: verum end; registration cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities Categorial for CatStr ; existence ex b1 being strict Category st b1 is Categorial proof set A = 1Cat (0,1); take 1Cat ((1Cat (0,1)),[[(1Cat (0,1)),(1Cat (0,1))],(id (1Cat (0,1)))]) ; ::_thesis: 1Cat ((1Cat (0,1)),[[(1Cat (0,1)),(1Cat (0,1))],(id (1Cat (0,1)))]) is Categorial thus 1Cat ((1Cat (0,1)),[[(1Cat (0,1)),(1Cat (0,1))],(id (1Cat (0,1)))]) is Categorial by Th11; ::_thesis: verum end; end; theorem Th12: :: CAT_5:12 for C being Categorial Category for a being Object of C holds a is Category proof let C be Categorial Category; ::_thesis: for a being Object of C holds a is Category the carrier of C is categorial by Def6; hence for a being Object of C holds a is Category by Def5; ::_thesis: verum end; theorem Th13: :: CAT_5:13 for C being Categorial Category for f being Morphism of C holds ( dom f = f `11 & cod f = f `12 ) proof let C be Categorial Category; ::_thesis: for f being Morphism of C holds ( dom f = f `11 & cod f = f `12 ) let f be Morphism of C; ::_thesis: ( dom f = f `11 & cod f = f `12 ) reconsider A = dom f, B = cod f as Category by Th12; ex F being Functor of A,B st f = [[A,B],F] by Def6; hence ( dom f = f `11 & cod f = f `12 ) by MCART_1:85; ::_thesis: verum end; definition let C be Categorial Category; let m be Morphism of C; :: original: `11 redefine funcm `11 -> Category; coherence m `11 is Category proof dom m = m `11 by Th13; hence m `11 is Category by Th12; ::_thesis: verum end; :: original: `12 redefine funcm `12 -> Category; coherence m `12 is Category proof cod m = m `12 by Th13; hence m `12 is Category by Th12; ::_thesis: verum end; end; theorem Th14: :: CAT_5:14 for C1, C2 being Categorial Category st the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 holds CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) proof let C1, C2 be Categorial Category; ::_thesis: ( the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 implies CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) ) assume that A1: the carrier of C1 = the carrier of C2 and A2: the carrier' of C1 = the carrier' of C2 ; ::_thesis: CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) A3: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def_1; A4: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def_1; A5: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def_1; A6: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_C1_holds_ the_Source_of_C1_._x_=_the_Source_of_C2_._x let x be set ; ::_thesis: ( x in the carrier' of C1 implies the Source of C1 . x = the Source of C2 . x ) assume x in the carrier' of C1 ; ::_thesis: the Source of C1 . x = the Source of C2 . x then reconsider m1 = x as Morphism of C1 ; reconsider m2 = m1 as Morphism of C2 by A2; thus the Source of C1 . x = dom m1 .= m1 `11 by Th13 .= dom m2 by Th13 .= the Source of C2 . x ; ::_thesis: verum end; then A7: the Source of C1 = the Source of C2 by A2, A3, A4, FUNCT_1:2; A8: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_C1_holds_ the_Target_of_C1_._x_=_the_Target_of_C2_._x let x be set ; ::_thesis: ( x in the carrier' of C1 implies the Target of C1 . x = the Target of C2 . x ) assume x in the carrier' of C1 ; ::_thesis: the Target of C1 . x = the Target of C2 . x then reconsider m1 = x as Morphism of C1 ; reconsider m2 = m1 as Morphism of C2 by A2; thus the Target of C1 . x = cod m1 .= m1 `12 by Th13 .= cod m2 by Th13 .= the Target of C2 . x ; ::_thesis: verum end; then A9: the Target of C1 = the Target of C2 by A2, A5, A6, FUNCT_1:2; A10: dom the Comp of C1 = dom the Comp of C2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: dom the Comp of C2 c= dom the Comp of C1 let x be set ; ::_thesis: ( x in dom the Comp of C1 implies x in dom the Comp of C2 ) assume A11: x in dom the Comp of C1 ; ::_thesis: x in dom the Comp of C2 then reconsider xx = x as Element of [: the carrier' of C1, the carrier' of C1:] ; reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A2; A12: y = [(xx `1),(xx `2)] by MCART_1:21; then dom (xx `1) = cod (xx `2) by A11, CAT_1:def_6; then dom (y `1) = cod (y `2) by A8, A7; hence x in dom the Comp of C2 by A12, CAT_1:def_6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom the Comp of C2 or x in dom the Comp of C1 ) assume A13: x in dom the Comp of C2 ; ::_thesis: x in dom the Comp of C1 then reconsider xx = x as Element of [: the carrier' of C1, the carrier' of C1:] by A2; reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A2; A14: xx = [(y `1),(y `2)] by MCART_1:21; then dom (y `1) = cod (y `2) by A13, CAT_1:def_6; then dom (xx `1) = cod (xx `2) by A8, A7; hence x in dom the Comp of C1 by A14, CAT_1:def_6; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_dom_the_Comp_of_C1_holds_ the_Comp_of_C1_._(x,y)_=_the_Comp_of_C2_._(x,y) let x, y be set ; ::_thesis: ( [x,y] in dom the Comp of C1 implies the Comp of C1 . (x,y) = the Comp of C2 . (x,y) ) assume A15: [x,y] in dom the Comp of C1 ; ::_thesis: the Comp of C1 . (x,y) = the Comp of C2 . (x,y) then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87; reconsider g2 = g1, h2 = h1 as Morphism of C2 by A2; reconsider a1 = dom g1, b1 = cod g1 as Category by Th12; consider f1 being Functor of a1,b1 such that A16: g1 = [[a1,b1],f1] by Def6; reconsider c1 = dom h1, d1 = cod h1 as Category by Th12; consider i1 being Functor of c1,d1 such that A17: h1 = [[c1,d1],i1] by Def6; A18: a1 = d1 by A15, CAT_1:15; thus the Comp of C1 . (x,y) = g1 (*) h1 by A15, CAT_1:def_1 .= [[c1,b1],(f1 * i1)] by A16, A17, A18, Def6 .= g2 (*) h2 by A16, A17, A18, Def6 .= the Comp of C2 . (x,y) by A10, A15, CAT_1:def_1 ; ::_thesis: verum end; then the Comp of C1 = the Comp of C2 by A2, A10, BINOP_1:20; hence CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) by A1, A2, A7, A9; ::_thesis: verum end; registration let C be Categorial Category; cluster -> Categorial for Subcategory of C; coherence for b1 being Subcategory of C holds b1 is Categorial proof let D be Subcategory of C; ::_thesis: D is Categorial A1: the carrier of C is categorial by Def6; thus the carrier of D is categorial :: according to CAT_5:def_6 ::_thesis: ( ( for a being Object of D for A being Category st a = A holds id a = [[A,A],(id A)] ) & ( for m being Morphism of D for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of D for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) proof let x be Object of D; :: according to CAT_5:def_5 ::_thesis: x is Category x is Object of C by CAT_2:6; hence x is Category by A1, Def4; ::_thesis: verum end; hereby ::_thesis: ( ( for m being Morphism of D for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of D for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) let a be Object of D; ::_thesis: for A being Category st a = A holds id a = [[A,A],(id A)] let A be Category; ::_thesis: ( a = A implies id a = [[A,A],(id A)] ) reconsider b = a as Object of C by CAT_2:6; assume a = A ; ::_thesis: id a = [[A,A],(id A)] then [[A,A],(id A)] = id b by Def6; hence id a = [[A,A],(id A)] by CAT_2:def_4; ::_thesis: verum end; hereby ::_thesis: for m1, m2 being Morphism of D for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let m be Morphism of D; ::_thesis: for a, b being Category st a = dom m & b = cod m holds ex F being Functor of a,b st m = [[a,b],F] reconsider m9 = m as Morphism of C by CAT_2:8; let a, b be Category; ::_thesis: ( a = dom m & b = cod m implies ex F being Functor of a,b st m = [[a,b],F] ) assume that A2: a = dom m and A3: b = cod m ; ::_thesis: ex F being Functor of a,b st m = [[a,b],F] A4: dom m9 = a by A2, CAT_2:9; cod m9 = b by A3, CAT_2:9; hence ex F being Functor of a,b st m = [[a,b],F] by A4, Def6; ::_thesis: verum end; let m1, m2 be Morphism of D; ::_thesis: for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let a, b, c be Category; ::_thesis: for F being Functor of a,b for G being Functor of b,c st m1 = [[a,b],F] & m2 = [[b,c],G] holds m2 (*) m1 = [[a,c],(G * F)] reconsider m19 = m1, m29 = m2 as Morphism of C by CAT_2:8; let f be Functor of a,b; ::_thesis: for G being Functor of b,c st m1 = [[a,b],f] & m2 = [[b,c],G] holds m2 (*) m1 = [[a,c],(G * f)] let g be Functor of b,c; ::_thesis: ( m1 = [[a,b],f] & m2 = [[b,c],g] implies m2 (*) m1 = [[a,c],(g * f)] ) assume that A5: m1 = [[a,b],f] and A6: m2 = [[b,c],g] ; ::_thesis: m2 (*) m1 = [[a,c],(g * f)] A7: dom m2 = dom m29 by CAT_2:9; A8: cod m1 = cod m19 by CAT_2:9; A9: dom m29 = m2 `11 by Th13; A10: cod m19 = m1 `12 by Th13; A11: dom m2 = b by A6, A7, A9, MCART_1:85; cod m1 = b by A5, A8, A10, MCART_1:85; hence m2 (*) m1 = m29 (*) m19 by A11, CAT_2:11 .= [[a,c],(g * f)] by A5, A6, Def6 ; ::_thesis: verum end; end; theorem Th15: :: CAT_5:15 for C, D being Categorial Category st the carrier' of C c= the carrier' of D holds C is Subcategory of D proof let C, D be Categorial Category; ::_thesis: ( the carrier' of C c= the carrier' of D implies C is Subcategory of D ) assume A1: the carrier' of C c= the carrier' of D ; ::_thesis: C is Subcategory of D thus the carrier of C c= the carrier of D :: according to CAT_2:def_4 ::_thesis: ( ( for b1, b2 being Element of the carrier of C for b3, b4 being Element of the carrier of D holds ( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of C c= the Comp of D & ( for b1 being Element of the carrier of C for b2 being Element of the carrier of D holds ( not b1 = b2 or id b1 = id b2 ) ) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of C or x in the carrier of D ) assume x in the carrier of C ; ::_thesis: x in the carrier of D then reconsider a = x as Object of C ; reconsider i = id a as Morphism of D by A1, TARSKI:def_3; A2: dom i = i `11 by Th13; dom (id a) = i `11 by Th13; hence x in the carrier of D by A2; ::_thesis: verum end; hereby ::_thesis: ( the Comp of C c= the Comp of D & ( for b1 being Element of the carrier of C for b2 being Element of the carrier of D holds ( not b1 = b2 or id b1 = id b2 ) ) ) let a, b be Object of C; ::_thesis: for a9, b9 being Object of D st a = a9 & b = b9 holds Hom (a,b) c= Hom (a9,b9) let a9, b9 be Object of D; ::_thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) ) assume that A3: a = a9 and A4: b = b9 ; ::_thesis: Hom (a,b) c= Hom (a9,b9) thus Hom (a,b) c= Hom (a9,b9) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) ) assume x in Hom (a,b) ; ::_thesis: x in Hom (a9,b9) then consider f being Morphism of C such that A5: x = f and A6: dom f = a and A7: cod f = b ; reconsider A = a, B = b as Category by Th12; A8: ex F being Functor of A,B st f = [[A,B],F] by A6, A7, Def6; reconsider f = f as Morphism of D by A1, TARSKI:def_3; A9: dom f = f `11 by Th13; A10: cod f = f `12 by Th13; A11: f `11 = A by A8, MCART_1:85; f `12 = B by A8, MCART_1:85; hence x in Hom (a9,b9) by A3, A4, A5, A9, A10, A11; ::_thesis: verum end; end; A12: dom the Comp of C c= dom the Comp of D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom the Comp of C or x in dom the Comp of D ) assume A13: x in dom the Comp of C ; ::_thesis: x in dom the Comp of D then reconsider g = x `1 , f = x `2 as Morphism of C by MCART_1:10; reconsider g9 = g, f9 = f as Morphism of D by A1, TARSKI:def_3; A14: x = [g,f] by A13, MCART_1:21; then A15: dom g = cod f by A13, CAT_1:15; A16: dom g = g `11 by Th13; A17: dom g9 = g `11 by Th13; A18: cod f = f `12 by Th13; cod f9 = f `12 by Th13; hence x in dom the Comp of D by A14, A15, A16, A17, A18, CAT_1:15; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_the_Comp_of_C_holds_ the_Comp_of_C_._x_=_the_Comp_of_D_._x let x be set ; ::_thesis: ( x in dom the Comp of C implies the Comp of C . x = the Comp of D . x ) assume A19: x in dom the Comp of C ; ::_thesis: the Comp of C . x = the Comp of D . x then reconsider g = x `1 , f = x `2 as Morphism of C by MCART_1:10; reconsider g9 = g, f9 = f as Morphism of D by A1, TARSKI:def_3; A20: x = [g,f] by A19, MCART_1:21; A21: dom g = g `11 by Th13; cod g = g `12 by Th13; then consider G being Functor of g `11 ,g `12 such that A22: g = [[(g `11),(g `12)],G] by A21, Def6; A23: dom f = f `11 by Th13; cod f = dom g by A19, A20, CAT_1:15; then consider F being Functor of f `11 ,g `11 such that A24: f = [[(f `11),(g `11)],F] by A21, A23, Def6; thus the Comp of C . x = the Comp of C . (g,f) by A19, MCART_1:21 .= g (*) f by A19, A20, CAT_1:def_1 .= [[(f `11),(g `12)],(G * F)] by A22, A24, Def6 .= g9 (*) f9 by A22, A24, Def6 .= the Comp of D . (g,f) by A12, A19, A20, CAT_1:def_1 .= the Comp of D . x by A19, MCART_1:21 ; ::_thesis: verum end; hence the Comp of C c= the Comp of D by A12, GRFUNC_1:2; ::_thesis: for b1 being Element of the carrier of C for b2 being Element of the carrier of D holds ( not b1 = b2 or id b1 = id b2 ) let a be Object of C; ::_thesis: for b1 being Element of the carrier of D holds ( not a = b1 or id a = id b1 ) let a9 be Object of D; ::_thesis: ( not a = a9 or id a = id a9 ) assume A25: a = a9 ; ::_thesis: id a = id a9 reconsider A = a as Category by Th12; thus id a = [[A,A],(id A)] by Def6 .= id a9 by A25, Def6 ; ::_thesis: verum end; definition let a be set ; assume A1: a is Category ; func cat a -> Category equals :Def7: :: CAT_5:def 7 a; correctness coherence a is Category; by A1; end; :: deftheorem Def7 defines cat CAT_5:def_7_:_ for a being set st a is Category holds cat a = a; theorem Th16: :: CAT_5:16 for C being Categorial Category for c being Object of C holds cat c = c proof let C be Categorial Category; ::_thesis: for c being Object of C holds cat c = c let c be Object of C; ::_thesis: cat c = c the carrier of C is categorial by Def6; then c is Category by Def4; hence cat c = c by Def7; ::_thesis: verum end; definition let C be Categorial Category; let m be Morphism of C; :: original: `2 redefine funcm `2 -> Functor of cat (dom m), cat (cod m); coherence m `2 is Functor of cat (dom m), cat (cod m) proof the carrier of C is categorial by Def6; then reconsider A = dom m, B = cod m as Category by Def4; consider F being Functor of A,B such that A1: m = [[A,B],F] by Def6; A2: m `2 = F by A1, MCART_1:7; cat A = A by Def7; hence m `2 is Functor of cat (dom m), cat (cod m) by A2, Def7; ::_thesis: verum end; end; theorem Th17: :: CAT_5:17 for X being non empty categorial set for Y being non empty set st ( for A, B, C being Element of X for F being Functor of A,B for G being Functor of B,C st F in Y & G in Y holds G * F in Y ) & ( for A being Element of X holds id A in Y ) holds ex C being strict Categorial Category st ( the carrier of C = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C iff F in Y ) ) ) proof let X be non empty categorial set ; ::_thesis: for Y being non empty set st ( for A, B, C being Element of X for F being Functor of A,B for G being Functor of B,C st F in Y & G in Y holds G * F in Y ) & ( for A being Element of X holds id A in Y ) holds ex C being strict Categorial Category st ( the carrier of C = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C iff F in Y ) ) ) let Y be non empty set ; ::_thesis: ( ( for A, B, C being Element of X for F being Functor of A,B for G being Functor of B,C st F in Y & G in Y holds G * F in Y ) & ( for A being Element of X holds id A in Y ) implies ex C being strict Categorial Category st ( the carrier of C = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C iff F in Y ) ) ) ) assume that A1: for A, B, C being Element of X for F being Functor of A,B for G being Functor of B,C st F in Y & G in Y holds G * F in Y and A2: for A being Element of X holds id A in Y ; ::_thesis: ex C being strict Categorial Category st ( the carrier of C = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C iff F in Y ) ) ) set B = { b where b is Element of Y : b is Function } ; set a = the Element of X; id the Element of X in Y by A2; then id the Element of X in { b where b is Element of Y : b is Function } ; then reconsider B = { b where b is Element of Y : b is Function } as non empty set ; B is functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in B or x is set ) assume x in B ; ::_thesis: x is set then ex b being Element of Y st ( x = b & b is Function ) ; hence x is set ; ::_thesis: verum end; then reconsider B = B as non empty functional set ; reconsider A = X as non empty categorial set ; defpred S1[ Element of A, Element of A, set ] means \$3 is Functor of \$1,\$2; deffunc H1( Function, Function) -> set = \$1 * \$2; A3: for a, b, c being Element of A for f, g being Element of B st S1[a,b,f] & S1[b,c,g] holds ( H1(g,f) in B & S1[a,c,H1(g,f)] ) proof let a, b, c be Element of A; ::_thesis: for f, g being Element of B st S1[a,b,f] & S1[b,c,g] holds ( H1(g,f) in B & S1[a,c,H1(g,f)] ) let f, g be Element of B; ::_thesis: ( S1[a,b,f] & S1[b,c,g] implies ( H1(g,f) in B & S1[a,c,H1(g,f)] ) ) assume that A4: S1[a,b,f] and A5: S1[b,c,g] ; ::_thesis: ( H1(g,f) in B & S1[a,c,H1(g,f)] ) reconsider f = f as Functor of a,b by A4; reconsider g = g as Functor of b,c by A5; A6: f in B ; A7: g in B ; A8: ex b being Element of Y st ( f = b & b is Function ) by A6; ex b being Element of Y st ( g = b & b is Function ) by A7; then g * f in Y by A1, A8; hence ( H1(g,f) in B & S1[a,c,H1(g,f)] ) ; ::_thesis: verum end; A9: for a being Element of A ex f being Element of B st ( S1[a,a,f] & ( for b being Element of A for g being Element of B holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) proof let a be Element of A; ::_thesis: ex f being Element of B st ( S1[a,a,f] & ( for b being Element of A for g being Element of B holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) reconsider f = id a as Element of Y by A2; f in B ; then reconsider f = f as Element of B ; take f ; ::_thesis: ( S1[a,a,f] & ( for b being Element of A for g being Element of B holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) thus S1[a,a,f] ; ::_thesis: for b being Element of A for g being Element of B holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) let b be Element of A; ::_thesis: for g being Element of B holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) let g be Element of B; ::_thesis: ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) thus ( S1[a,b,g] implies g * f = g ) by FUNCT_2:17; ::_thesis: ( S1[b,a,g] implies H1(f,g) = g ) assume S1[b,a,g] ; ::_thesis: H1(f,g) = g then reconsider G = g as Functor of b,a ; (id a) * G = G by FUNCT_2:17; hence H1(f,g) = g ; ::_thesis: verum end; A10: for a, b, c, d being Element of A for f, g, h being Element of B st S1[a,b,f] & S1[b,c,g] & S1[c,d,h] holds H1(h,H1(g,f)) = H1(H1(h,g),f) by RELAT_1:36; consider C being strict with_triple-like_morphisms Category such that A11: ( the carrier of C = A & ( for a, b being Element of A for f being Element of B st S1[a,b,f] holds [[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of A ex f being Element of B st ( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C for a1, a2, a3 being Element of A for f1, f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) ) from CAT_5:sch_1(A3, A9, A10); C is Categorial proof thus the carrier of C is categorial by A11; :: according to CAT_5:def_6 ::_thesis: ( ( for a being Object of C for A being Category st a = A holds id a = [[A,A],(id A)] ) & ( for m being Morphism of C for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) hereby ::_thesis: ( ( for m being Morphism of C for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] ) ) let a be Object of C; ::_thesis: for D being Category st a = D holds id a = [[D,D],(id D)] let D be Category; ::_thesis: ( a = D implies id a = [[D,D],(id D)] ) assume A12: a = D ; ::_thesis: id a = [[D,D],(id D)] then id D in Y by A2, A11; then id D in B ; then reconsider f = id D as Element of B ; reconsider x = a as Element of A by A11; reconsider F = [[x,x],f] as Morphism of C by A11, A12; consider b, c being Element of A, g being Element of B such that A13: id a = [[b,c],g] and A14: S1[b,c,g] by A11; A15: dom (id a) = (id a) `11 by Th2; A16: (id a) `11 = b by A13, MCART_1:85; cod F = F `12 by Th2 .= x by MCART_1:85 ; then F = (id a) (*) F by CAT_1:21 .= [[x,c],(g * (id the carrier' of D))] by A11, A13, A15, A16 .= [[x,c],g] by A12, A14, A15, A16, FUNCT_2:17 ; hence id a = [[D,D],(id D)] by A12, A13, A15, MCART_1:85; ::_thesis: verum end; hereby ::_thesis: for m1, m2 being Morphism of C for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let m be Morphism of C; ::_thesis: for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] consider a, b being Element of A, f being Element of B such that A17: m = [[a,b],f] and A18: S1[a,b,f] by A11; A19: dom m = m `11 by Th2; A20: cod m = m `12 by Th2; A21: dom m = a by A17, A19, MCART_1:85; cod m = b by A17, A20, MCART_1:85; hence for A, B being Category st A = dom m & B = cod m holds ex F being Functor of A,B st m = [[A,B],F] by A17, A18, A21; ::_thesis: verum end; let m1, m2 be Morphism of C; ::_thesis: for A, B, C being Category for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] consider a1, b1 being Element of A, f1 being Element of B such that A22: m1 = [[a1,b1],f1] and S1[a1,b1,f1] by A11; consider a2, b2 being Element of A, f2 being Element of B such that A23: m2 = [[a2,b2],f2] and S1[a2,b2,f2] by A11; let A, B, C be Category; ::_thesis: for F being Functor of A,B for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let F be Functor of A,B; ::_thesis: for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds m2 (*) m1 = [[A,C],(G * F)] let G be Functor of B,C; ::_thesis: ( m1 = [[A,B],F] & m2 = [[B,C],G] implies m2 (*) m1 = [[A,C],(G * F)] ) assume that A24: m1 = [[A,B],F] and A25: m2 = [[B,C],G] ; ::_thesis: m2 (*) m1 = [[A,C],(G * F)] A26: [A,B] = [a1,b1] by A22, A24, XTUPLE_0:1; A27: [B,C] = [a2,b2] by A23, A25, XTUPLE_0:1; A28: f1 = F by A22, A24, XTUPLE_0:1; A29: f2 = G by A23, A25, XTUPLE_0:1; A30: A = a1 by A26, XTUPLE_0:1; A31: B = b1 by A26, XTUPLE_0:1; C = b2 by A27, XTUPLE_0:1; hence m2 (*) m1 = [[A,C],(G * F)] by A11, A22, A25, A28, A29, A30, A31; ::_thesis: verum end; then reconsider C = C as strict Categorial Category ; take C ; ::_thesis: ( the carrier of C = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C iff F in Y ) ) ) thus the carrier of C = X by A11; ::_thesis: for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C iff F in Y ) let A9, B9 be Element of X; ::_thesis: for F being Functor of A9,B9 holds ( [[A9,B9],F] is Morphism of C iff F in Y ) let F be Functor of A9,B9; ::_thesis: ( [[A9,B9],F] is Morphism of C iff F in Y ) hereby ::_thesis: ( F in Y implies [[A9,B9],F] is Morphism of C ) assume [[A9,B9],F] is Morphism of C ; ::_thesis: F in Y then reconsider m = [[A9,B9],F] as Morphism of C ; consider a, b being Element of A, f being Element of B such that A32: m = [[a,b],f] and S1[a,b,f] by A11; A33: m `2 = F by MCART_1:7; m `2 = f by A32, MCART_1:7; then F in B by A33; then ex b being Element of Y st ( F = b & b is Function ) ; hence F in Y ; ::_thesis: verum end; assume F in Y ; ::_thesis: [[A9,B9],F] is Morphism of C then F in B ; hence [[A9,B9],F] is Morphism of C by A11; ::_thesis: verum end; theorem Th18: :: CAT_5:18 for X being non empty categorial set for Y being non empty set for C1, C2 being strict Categorial Category st the carrier of C1 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C2 iff F in Y ) ) holds C1 = C2 proof let X be non empty categorial set ; ::_thesis: for Y being non empty set for C1, C2 being strict Categorial Category st the carrier of C1 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C2 iff F in Y ) ) holds C1 = C2 let Y be non empty set ; ::_thesis: for C1, C2 being strict Categorial Category st the carrier of C1 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C2 iff F in Y ) ) holds C1 = C2 let C1, C2 be strict Categorial Category; ::_thesis: ( the carrier of C1 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C2 iff F in Y ) ) implies C1 = C2 ) assume that A1: the carrier of C1 = X and A2: for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C1 iff F in Y ) and A3: the carrier of C2 = X and A4: for A, B being Element of X for F being Functor of A,B holds ( [[A,B],F] is Morphism of C2 iff F in Y ) ; ::_thesis: C1 = C2 the carrier' of C1 = the carrier' of C2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier' of C2 c= the carrier' of C1 let x be set ; ::_thesis: ( x in the carrier' of C1 implies x in the carrier' of C2 ) assume x in the carrier' of C1 ; ::_thesis: x in the carrier' of C2 then reconsider m = x as Morphism of C1 ; reconsider a = dom m, b = cod m as Category by Th12; consider f being Functor of a,b such that A5: m = [[a,b],f] by Def6; f in Y by A1, A2, A5; then x is Morphism of C2 by A1, A4, A5; hence x in the carrier' of C2 ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of C2 or x in the carrier' of C1 ) assume x in the carrier' of C2 ; ::_thesis: x in the carrier' of C1 then reconsider m = x as Morphism of C2 ; reconsider a = dom m, b = cod m as Category by Th12; consider f being Functor of a,b such that A6: m = [[a,b],f] by Def6; f in Y by A3, A4, A6; then x is Morphism of C1 by A2, A3, A6; hence x in the carrier' of C1 ; ::_thesis: verum end; hence C1 = C2 by A1, A3, Th14; ::_thesis: verum end; definition let IT be Categorial Category; attrIT is full means :Def8: :: CAT_5:def 8 for a, b being Category st a is Object of IT & b is Object of IT holds for F being Functor of a,b holds [[a,b],F] is Morphism of IT; end; :: deftheorem Def8 defines full CAT_5:def_8_:_ for IT being Categorial Category holds ( IT is full iff for a, b being Category st a is Object of IT & b is Object of IT holds for F being Functor of a,b holds [[a,b],F] is Morphism of IT ); registration cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities with_triple-like_morphisms Categorial full for CatStr ; existence ex b1 being strict Categorial Category st b1 is full proof set A = 1Cat (0,1); reconsider C = 1Cat ((1Cat (0,1)),[[(1Cat (0,1)),(1Cat (0,1))],(id (1Cat (0,1)))]) as strict Categorial Category by Th11; take C ; ::_thesis: C is full let a, b be Category; :: according to CAT_5:def_8 ::_thesis: ( a is Object of C & b is Object of C implies for F being Functor of a,b holds [[a,b],F] is Morphism of C ) assume that A1: a is Object of C and A2: b is Object of C ; ::_thesis: for F being Functor of a,b holds [[a,b],F] is Morphism of C let F be Functor of a,b; ::_thesis: [[a,b],F] is Morphism of C A3: a = 1Cat (0,1) by A1, TARSKI:def_1; A4: b = 1Cat (0,1) by A2, TARSKI:def_1; then id (1Cat (0,1)) = F by A3, FUNCT_2:51; hence [[a,b],F] is Morphism of C by A3, A4, TARSKI:def_1; ::_thesis: verum end; end; theorem :: CAT_5:19 for C1, C2 being Categorial full Category st the carrier of C1 = the carrier of C2 holds CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) proof let C1, C2 be Categorial full Category; ::_thesis: ( the carrier of C1 = the carrier of C2 implies CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) ) assume A1: the carrier of C1 = the carrier of C2 ; ::_thesis: CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) reconsider A = the carrier of C1 as non empty categorial set by Def6; set B = { (m `2) where m is Morphism of C1 : verum } ; set m = the Morphism of C1; the Morphism of C1 `2 in { (m `2) where m is Morphism of C1 : verum } ; then reconsider B = { (m `2) where m is Morphism of C1 : verum } as non empty set ; reconsider D1 = CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #), D2 = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) as strict Category by Th1; A2: D1 is Categorial by Th10; A3: D2 is Categorial by Th10; A4: now__::_thesis:_for_a,_b_being_Element_of_A for_F_being_Functor_of_a,b_holds_ (_[[a,b],F]_is_Morphism_of_CatStr(#_the_carrier_of_C1,_the_carrier'_of_C1,_the_Source_of_C1,_the_Target_of_C1,_the_Comp_of_C1_#)_iff_F_in_B_) let a, b be Element of A; ::_thesis: for F being Functor of a,b holds ( [[a,b],F] is Morphism of CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) iff F in B ) let F be Functor of a,b; ::_thesis: ( [[a,b],F] is Morphism of CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) iff F in B ) reconsider m = [[a,b],F] as Morphism of C1 by Def8; m `2 = F by MCART_1:7; hence ( [[a,b],F] is Morphism of CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) iff F in B ) ; ::_thesis: verum end; now__::_thesis:_for_a,_b_being_Element_of_A for_F_being_Functor_of_a,b_holds_ (_[[a,b],F]_is_Morphism_of_CatStr(#_the_carrier_of_C2,_the_carrier'_of_C2,_the_Source_of_C2,_the_Target_of_C2,_the_Comp_of_C2_#)_iff_F_in_B_) let a, b be Element of A; ::_thesis: for F being Functor of a,b holds ( [[a,b],F] is Morphism of CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) iff F in B ) let F be Functor of a,b; ::_thesis: ( [[a,b],F] is Morphism of CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) iff F in B ) reconsider a9 = a, b9 = b as Object of C2 by A1; A5: cat a9 = a by Th16; cat b9 = b by Th16; then reconsider m2 = [[a,b],F] as Morphism of C2 by A5, Def8; reconsider m = [[a,b],F] as Morphism of C1 by Def8; A6: m `2 = F by MCART_1:7; m2 = m2 ; hence ( [[a,b],F] is Morphism of CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) iff F in B ) by A6; ::_thesis: verum end; hence CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) by A1, A2, A3, A4, Th18; ::_thesis: verum end; theorem Th20: :: CAT_5:20 for A being non empty categorial set ex C being strict Categorial full Category st the carrier of C = A proof let AA be non empty categorial set ; ::_thesis: ex C being strict Categorial full Category st the carrier of C = AA set dFF = { (Funct (a,b)) where a, b is Element of AA : verum } ; set a = the Element of AA; set f = the Functor of the Element of AA, the Element of AA; A1: the Functor of the Element of AA, the Element of AA in Funct ( the Element of AA, the Element of AA) by CAT_2:def_2; Funct ( the Element of AA, the Element of AA) in { (Funct (a,b)) where a, b is Element of AA : verum } ; then reconsider FF = union { (Funct (a,b)) where a, b is Element of AA : verum } as non empty set by A1, TARSKI:def_4; A2: now__::_thesis:_for_A,_B,_C_being_Element_of_AA for_F_being_Functor_of_A,B for_G_being_Functor_of_B,C_st_F_in_FF_&_G_in_FF_holds_ G_*_F_in_FF let A, B, C be Element of AA; ::_thesis: for F being Functor of A,B for G being Functor of B,C st F in FF & G in FF holds G * F in FF let F be Functor of A,B; ::_thesis: for G being Functor of B,C st F in FF & G in FF holds G * F in FF let G be Functor of B,C; ::_thesis: ( F in FF & G in FF implies G * F in FF ) assume that F in FF and G in FF ; ::_thesis: G * F in FF A3: G * F in Funct (A,C) by CAT_2:def_2; Funct (A,C) in { (Funct (a,b)) where a, b is Element of AA : verum } ; hence G * F in FF by A3, TARSKI:def_4; ::_thesis: verum end; now__::_thesis:_for_A_being_Element_of_AA_holds_id_A_in_FF let A be Element of AA; ::_thesis: id A in FF A4: id A in Funct (A,A) by CAT_2:def_2; Funct (A,A) in { (Funct (a,b)) where a, b is Element of AA : verum } ; hence id A in FF by A4, TARSKI:def_4; ::_thesis: verum end; then consider C being strict Categorial Category such that A5: the carrier of C = AA and A6: for A, B being Element of AA for F being Functor of A,B holds ( [[A,B],F] is Morphism of C iff F in FF ) by A2, Th17; C is full proof let a, b be Category; :: according to CAT_5:def_8 ::_thesis: ( a is Object of C & b is Object of C implies for F being Functor of a,b holds [[a,b],F] is Morphism of C ) assume that A7: a is Object of C and A8: b is Object of C ; ::_thesis: for F being Functor of a,b holds [[a,b],F] is Morphism of C reconsider A = a, B = b as Element of AA by A5, A7, A8; let F be Functor of a,b; ::_thesis: [[a,b],F] is Morphism of C A9: F in Funct (A,B) by CAT_2:def_2; Funct (A,B) in { (Funct (a,b)) where a, b is Element of AA : verum } ; then F in FF by A9, TARSKI:def_4; then [[A,B],F] is Morphism of C by A6; hence [[a,b],F] is Morphism of C ; ::_thesis: verum end; hence ex C being strict Categorial full Category st the carrier of C = AA by A5; ::_thesis: verum end; theorem Th21: :: CAT_5:21 for C being Categorial Category for D being Categorial full Category st the carrier of C c= the carrier of D holds C is Subcategory of D proof let C be Categorial Category; ::_thesis: for D being Categorial full Category st the carrier of C c= the carrier of D holds C is Subcategory of D let D be Categorial full Category; ::_thesis: ( the carrier of C c= the carrier of D implies C is Subcategory of D ) assume A1: the carrier of C c= the carrier of D ; ::_thesis: C is Subcategory of D the carrier' of C c= the carrier' of D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier' of C or x in the carrier' of D ) assume x in the carrier' of C ; ::_thesis: x in the carrier' of D then reconsider x = x as Morphism of C ; reconsider y1 = dom x, y2 = cod x as Category by Th12; consider F being Functor of y1,y2 such that A2: x = [[y1,y2],F] by Def6; A3: y1 is Object of D by A1, TARSKI:def_3; y2 is Object of D by A1, TARSKI:def_3; then [[y1,y2],F] is Morphism of D by A3, Def8; hence x in the carrier' of D by A2; ::_thesis: verum end; hence C is Subcategory of D by Th15; ::_thesis: verum end; theorem :: CAT_5:22 for C being Category for D1, D2 being Categorial Category for F1 being Functor of C,D1 for F2 being Functor of C,D2 st F1 = F2 holds Image F1 = Image F2 proof let C be Category; ::_thesis: for D1, D2 being Categorial Category for F1 being Functor of C,D1 for F2 being Functor of C,D2 st F1 = F2 holds Image F1 = Image F2 let D1, D2 be Categorial Category; ::_thesis: for F1 being Functor of C,D1 for F2 being Functor of C,D2 st F1 = F2 holds Image F1 = Image F2 let F1 be Functor of C,D1; ::_thesis: for F2 being Functor of C,D2 st F1 = F2 holds Image F1 = Image F2 let F2 be Functor of C,D2; ::_thesis: ( F1 = F2 implies Image F1 = Image F2 ) assume A1: F1 = F2 ; ::_thesis: Image F1 = Image F2 reconsider DD = the carrier of D1 \/ the carrier of D2 as non empty set ; DD is categorial proof let d be Element of DD; :: according to CAT_5:def_5 ::_thesis: d is Category ( d is Object of D1 or d is Object of D2 ) by XBOOLE_0:def_3; hence d is Category by Th12; ::_thesis: verum end; then reconsider DD = the carrier of D1 \/ the carrier of D2 as non empty categorial set ; consider D being strict Categorial full Category such that A2: the carrier of D = DD by Th20; reconsider D1 = D1, D2 = D2 as Subcategory of D by A2, Th21, XBOOLE_1:7; reconsider F1 = F1 as Functor of C,D1 ; reconsider F2 = F2 as Functor of C,D2 ; rng F1 c= the carrier' of D1 ; then F1 = (incl D1) * F1 by RELAT_1:53; then reconsider G1 = F1 as Functor of C,D ; Image F1 = Image G1 by Th9 .= Image F2 by A1, Th9 ; hence Image F1 = Image F2 ; ::_thesis: verum end; begin definition let C be Category; let o be Object of C; func Hom o -> Subset of the carrier' of C equals :: CAT_5:def 9 the Target of C " {o}; coherence the Target of C " {o} is Subset of the carrier' of C ; funco Hom -> Subset of the carrier' of C equals :: CAT_5:def 10 the Source of C " {o}; coherence the Source of C " {o} is Subset of the carrier' of C ; end; :: deftheorem defines Hom CAT_5:def_9_:_ for C being Category for o being Object of C holds Hom o = the Target of C " {o}; :: deftheorem defines Hom CAT_5:def_10_:_ for C being Category for o being Object of C holds o Hom = the Source of C " {o}; registration let C be Category; let o be Object of C; cluster Hom o -> non empty ; coherence not Hom o is empty proof A1: the Target of C . (id o) = cod (id o) .= o ; A2: o in {o} by TARSKI:def_1; dom the Target of C = the carrier' of C by FUNCT_2:def_1; hence not Hom o is empty by A1, A2, FUNCT_1:def_7; ::_thesis: verum end; clustero Hom -> non empty ; coherence not o Hom is empty proof A3: the Source of C . (id o) = dom (id o) .= o ; A4: o in {o} by TARSKI:def_1; dom the Source of C = the carrier' of C by FUNCT_2:def_1; hence not o Hom is empty by A3, A4, FUNCT_1:def_7; ::_thesis: verum end; end; theorem Th23: :: CAT_5:23 for C being Category for a being Object of C for f being Morphism of C holds ( f in Hom a iff cod f = a ) proof let C be Category; ::_thesis: for a being Object of C for f being Morphism of C holds ( f in Hom a iff cod f = a ) let a be Object of C; ::_thesis: for f being Morphism of C holds ( f in Hom a iff cod f = a ) let f be Morphism of C; ::_thesis: ( f in Hom a iff cod f = a ) ( cod f in {a} iff cod f = a ) by TARSKI:def_1; hence ( f in Hom a iff cod f = a ) by FUNCT_2:38; ::_thesis: verum end; theorem Th24: :: CAT_5:24 for C being Category for a being Object of C for f being Morphism of C holds ( f in a Hom iff dom f = a ) proof let C be Category; ::_thesis: for a being Object of C for f being Morphism of C holds ( f in a Hom iff dom f = a ) let a be Object of C; ::_thesis: for f being Morphism of C holds ( f in a Hom iff dom f = a ) let f be Morphism of C; ::_thesis: ( f in a Hom iff dom f = a ) ( dom f in {a} iff dom f = a ) by TARSKI:def_1; hence ( f in a Hom iff dom f = a ) by FUNCT_2:38; ::_thesis: verum end; theorem :: CAT_5:25 for C being Category for a, b being Object of C holds Hom (a,b) = (a Hom) /\ (Hom b) proof let C be Category; ::_thesis: for a, b being Object of C holds Hom (a,b) = (a Hom) /\ (Hom b) let a, b be Object of C; ::_thesis: Hom (a,b) = (a Hom) /\ (Hom b) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (a Hom) /\ (Hom b) c= Hom (a,b) let x be set ; ::_thesis: ( x in Hom (a,b) implies x in (a Hom) /\ (Hom b) ) assume A1: x in Hom (a,b) ; ::_thesis: x in (a Hom) /\ (Hom b) then reconsider f = x as Morphism of C ; A2: dom f = a by A1, CAT_1:1; A3: cod f = b by A1, CAT_1:1; A4: f in a Hom by A2, Th24; f in Hom b by A3, Th23; hence x in (a Hom) /\ (Hom b) by A4, XBOOLE_0:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (a Hom) /\ (Hom b) or x in Hom (a,b) ) assume A5: x in (a Hom) /\ (Hom b) ; ::_thesis: x in Hom (a,b) then A6: x in a Hom by XBOOLE_0:def_4; A7: x in Hom b by A5, XBOOLE_0:def_4; reconsider f = x as Morphism of C by A5; A8: dom f = a by A6, Th24; cod f = b by A7, Th23; hence x in Hom (a,b) by A8; ::_thesis: verum end; theorem :: CAT_5:26 for C being Category for f being Morphism of C holds ( f in (dom f) Hom & f in Hom (cod f) ) by Th23, Th24; theorem Th27: :: CAT_5:27 for C being Category for f being Morphism of C for g being Element of Hom (dom f) holds f (*) g in Hom (cod f) proof let C be Category; ::_thesis: for f being Morphism of C for g being Element of Hom (dom f) holds f (*) g in Hom (cod f) let f be Morphism of C; ::_thesis: for g being Element of Hom (dom f) holds f (*) g in Hom (cod f) let g be Element of Hom (dom f); ::_thesis: f (*) g in Hom (cod f) cod g = dom f by Th23; then cod (f (*) g) = cod f by CAT_1:17; hence f (*) g in Hom (cod f) by Th23; ::_thesis: verum end; theorem Th28: :: CAT_5:28 for C being Category for f being Morphism of C for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom proof let C be Category; ::_thesis: for f being Morphism of C for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom let f be Morphism of C; ::_thesis: for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom let g be Element of (cod f) Hom ; ::_thesis: g (*) f in (dom f) Hom cod f = dom g by Th24; then dom (g (*) f) = dom f by CAT_1:17; hence g (*) f in (dom f) Hom by Th24; ::_thesis: verum end; definition let C be Category; let o be Object of C; set A = Hom o; set B = the carrier' of C; defpred S1[ Element of Hom o, Element of Hom o, Element of the carrier' of C] means ( dom \$2 = cod \$3 & \$1 = \$2 (*) \$3 ); deffunc H1( Morphism of C, Morphism of C) -> Element of the carrier' of C = \$1 (*) \$2; A1: for a, b, c being Element of Hom o for f, g being Element of the carrier' of C st S1[a,b,f] & S1[b,c,g] holds ( H1(g,f) in the carrier' of C & S1[a,c,H1(g,f)] ) proof let a, b, c be Element of Hom o; ::_thesis: for f, g being Element of the carrier' of C st S1[a,b,f] & S1[b,c,g] holds ( H1(g,f) in the carrier' of C & S1[a,c,H1(g,f)] ) let f, g be Morphism of C; ::_thesis: ( S1[a,b,f] & S1[b,c,g] implies ( H1(g,f) in the carrier' of C & S1[a,c,H1(g,f)] ) ) assume that A2: dom b = cod f and A3: a = b (*) f and A4: dom c = cod g and A5: b = c (*) g ; ::_thesis: ( H1(g,f) in the carrier' of C & S1[a,c,H1(g,f)] ) dom g = cod f by A2, A4, A5, CAT_1:17; hence ( H1(g,f) in the carrier' of C & S1[a,c,H1(g,f)] ) by A3, A4, A5, CAT_1:17, CAT_1:18; ::_thesis: verum end; A6: for a being Element of Hom o ex f being Element of the carrier' of C st ( S1[a,a,f] & ( for b being Element of Hom o for g being Element of the carrier' of C holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) proof let a be Element of Hom o; ::_thesis: ex f being Element of the carrier' of C st ( S1[a,a,f] & ( for b being Element of Hom o for g being Element of the carrier' of C holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) take f = id (dom a); ::_thesis: ( S1[a,a,f] & ( for b being Element of Hom o for g being Element of the carrier' of C holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) ) thus ( dom a = cod f & a = a (*) f ) by CAT_1:58, CAT_1:22; ::_thesis: for b being Element of Hom o for g being Element of the carrier' of C holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) let b be Element of Hom o; ::_thesis: for g being Element of the carrier' of C holds ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) let g be Morphism of C; ::_thesis: ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) hereby ::_thesis: ( S1[b,a,g] implies H1(f,g) = g ) assume that A7: dom b = cod g and A8: a = b (*) g ; ::_thesis: g (*) f = g dom a = dom g by A7, A8, CAT_1:17; hence g (*) f = g by CAT_1:22; ::_thesis: verum end; thus ( S1[b,a,g] implies H1(f,g) = g ) by CAT_1:21; ::_thesis: verum end; A9: for a, b, c, d being Element of Hom o for f, g, h being Element of the carrier' of C st S1[a,b,f] & S1[b,c,g] & S1[c,d,h] holds H1(h,H1(g,f)) = H1(H1(h,g),f) proof let a, b, c, d be Element of Hom o; ::_thesis: for f, g, h being Element of the carrier' of C st S1[a,b,f] & S1[b,c,g] & S1[c,d,h] holds H1(h,H1(g,f)) = H1(H1(h,g),f) let f, g, h be Morphism of C; ::_thesis: ( S1[a,b,f] & S1[b,c,g] & S1[c,d,h] implies H1(h,H1(g,f)) = H1(H1(h,g),f) ) assume that A10: dom b = cod f and a = b (*) f and A11: dom c = cod g and A12: b = c (*) g and A13: dom d = cod h and A14: c = d (*) h ; ::_thesis: H1(h,H1(g,f)) = H1(H1(h,g),f) A15: dom g = cod f by A10, A11, A12, CAT_1:17; dom h = cod g by A11, A13, A14, CAT_1:17; hence H1(h,H1(g,f)) = H1(H1(h,g),f) by A15, CAT_1:18; ::_thesis: verum end; funcC -SliceCat o -> strict with_triple-like_morphisms Category means :Def11: :: CAT_5:def 11 ( the carrier of it = Hom o & ( for a, b being Element of Hom o for f being Morphism of C st dom b = cod f & a = b (*) f holds [[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of it for a1, a2, a3 being Element of Hom o for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ); existence ex b1 being strict with_triple-like_morphisms Category st ( the carrier of b1 = Hom o & ( for a, b being Element of Hom o for f being Morphism of C st dom b = cod f & a = b (*) f holds [[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b1 for a1, a2, a3 being Element of Hom o for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) proof thus ex F being strict with_triple-like_morphisms Category st ( the carrier of F = Hom o & ( for a, b being Element of Hom o for f being Element of the carrier' of C st S1[a,b,f] holds [[a,b],f] is Morphism of F ) & ( for m being Morphism of F ex a, b being Element of Hom o ex f being Element of the carrier' of C st ( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of F for a1, a2, a3 being Element of Hom o for f1, f2 being Element of the carrier' of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) ) from CAT_5:sch_1(A1, A6, A9); ::_thesis: verum end; uniqueness for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = Hom o & ( for a, b being Element of Hom o for f being Morphism of C st dom b = cod f & a = b (*) f holds [[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b1 for a1, a2, a3 being Element of Hom o for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) & the carrier of b2 = Hom o & ( for a, b being Element of Hom o for f being Morphism of C st dom b = cod f & a = b (*) f holds [[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b2 for a1, a2, a3 being Element of Hom o for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) holds b1 = b2 proof thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = Hom o & ( for a, b being Element of Hom o for f being Element of the carrier' of C st S1[a,b,f] holds [[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of Hom o ex f being Element of the carrier' of C st ( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C1 for a1, a2, a3 being Element of Hom o for f1, f2 being Element of the carrier' of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) & the carrier of C2 = Hom o & ( for a, b being Element of Hom o for f being Element of the carrier' of C st S1[a,b,f] holds [[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of Hom o ex f being Element of the carrier' of C st ( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of C2 for a1, a2, a3 being Element of Hom o for f1, f2 being Element of the carrier' of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) holds C1 = C2 from CAT_5:sch_2(A6); ::_thesis: verum end; set X = o Hom ; defpred S2[ Element of o Hom , Element of o Hom , Element of the carrier' of C] means ( dom \$3 = cod \$1 & \$2 = \$3 (*) \$1 ); A16: for a, b, c being Element of o Hom for f, g being Element of the carrier' of C st S2[a,b,f] & S2[b,c,g] holds ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] ) proof let a, b, c be Element of o Hom ; ::_thesis: for f, g being Element of the carrier' of C st S2[a,b,f] & S2[b,c,g] holds ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] ) let f, g be Morphism of C; ::_thesis: ( S2[a,b,f] & S2[b,c,g] implies ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] ) ) assume that A17: dom f = cod a and A18: f (*) a = b and A19: dom g = cod b and A20: g (*) b = c ; ::_thesis: ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] ) dom g = cod f by A17, A18, A19, CAT_1:17; hence ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] ) by A17, A18, A20, CAT_1:17, CAT_1:18; ::_thesis: verum end; A21: for a being Element of o Hom ex f being Element of the carrier' of C st ( S2[a,a,f] & ( for b being Element of o Hom for g being Element of the carrier' of C holds ( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) ) ) proof let a be Element of o Hom ; ::_thesis: ex f being Element of the carrier' of C st ( S2[a,a,f] & ( for b being Element of o Hom for g being Element of the carrier' of C holds ( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) ) ) take f = id (cod a); ::_thesis: ( S2[a,a,f] & ( for b being Element of o Hom for g being Element of the carrier' of C holds ( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) ) ) thus ( dom f = cod a & f (*) a = a ) by CAT_1:58, CAT_1:21; ::_thesis: for b being Element of o Hom for g being Element of the carrier' of C holds ( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) let b be Element of o Hom ; ::_thesis: for g being Element of the carrier' of C holds ( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) let g be Morphism of C; ::_thesis: ( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) thus ( dom g = cod a & g (*) a = b implies g (*) f = g ) by CAT_1:22; ::_thesis: ( S2[b,a,g] implies H1(f,g) = g ) assume that A22: dom g = cod b and A23: g (*) b = a ; ::_thesis: H1(f,g) = g cod g = cod a by A22, A23, CAT_1:17; hence H1(f,g) = g by CAT_1:21; ::_thesis: verum end; A24: for a, b, c, d being Element of o Hom for f, g, h being Element of the carrier' of C st S2[a,b,f] & S2[b,c,g] & S2[c,d,h] holds H1(h,H1(g,f)) = H1(H1(h,g),f) proof let a, b, c, d be Element of o Hom ; ::_thesis: for f, g, h being Element of the carrier' of C st S2[a,b,f] & S2[b,c,g] & S2[c,d,h] holds H1(h,H1(g,f)) = H1(H1(h,g),f) let f, g, h be Morphism of C; ::_thesis: ( S2[a,b,f] & S2[b,c,g] & S2[c,d,h] implies H1(h,H1(g,f)) = H1(H1(h,g),f) ) assume that A25: dom f = cod a and A26: f (*) a = b and A27: dom g = cod b and A28: g (*) b = c and A29: dom h = cod c and h (*) c = d ; ::_thesis: H1(h,H1(g,f)) = H1(H1(h,g),f) A30: dom g = cod f by A25, A26, A27, CAT_1:17; dom h = cod g by A27, A28, A29, CAT_1:17; hence H1(h,H1(g,f)) = H1(H1(h,g),f) by A30, CAT_1:18; ::_thesis: verum end; funco -SliceCat C -> strict with_triple-like_morphisms Category means :Def12: :: CAT_5:def 12 ( the carrier of it = o Hom & ( for a, b being Element of o Hom for f being Morphism of C st dom f = cod a & f (*) a = b holds [[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of it for a1, a2, a3 being Element of o Hom for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ); existence ex b1 being strict with_triple-like_morphisms Category st ( the carrier of b1 = o Hom & ( for a, b being Element of o Hom for f being Morphism of C st dom f = cod a & f (*) a = b holds [[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b1 for a1, a2, a3 being Element of o Hom for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) proof thus ex F being strict with_triple-like_morphisms Category st ( the carrier of F = o Hom & ( for a, b being Element of o Hom for f being Element of the carrier' of C st S2[a,b,f] holds [[a,b],f] is Morphism of F ) & ( for m being Morphism of F ex a, b being Element of o Hom ex f being Element of the carrier' of C st ( m = [[a,b],f] & S2[a,b,f] ) ) & ( for m1, m2 being Morphism of F for a1, a2, a3 being Element of o Hom for f1, f2 being Element of the carrier' of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) ) from CAT_5:sch_1(A16, A21, A24); ::_thesis: verum end; uniqueness for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = o Hom & ( for a, b being Element of o Hom for f being Morphism of C st dom f = cod a & f (*) a = b holds [[a,b],f] is Morphism of b1 ) & ( for m being Morphism of b1 ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b1 for a1, a2, a3 being Element of o Hom for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) & the carrier of b2 = o Hom & ( for a, b being Element of o Hom for f being Morphism of C st dom f = cod a & f (*) a = b holds [[a,b],f] is Morphism of b2 ) & ( for m being Morphism of b2 ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b2 for a1, a2, a3 being Element of o Hom for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) holds b1 = b2 proof thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = o Hom & ( for a, b being Element of o Hom for f being Element of the carrier' of C st S2[a,b,f] holds [[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of o Hom ex f being Element of the carrier' of C st ( m = [[a,b],f] & S2[a,b,f] ) ) & ( for m1, m2 being Morphism of C1 for a1, a2, a3 being Element of o Hom for f1, f2 being Element of the carrier' of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) & the carrier of C2 = o Hom & ( for a, b being Element of o Hom for f being Element of the carrier' of C st S2[a,b,f] holds [[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of o Hom ex f being Element of the carrier' of C st ( m = [[a,b],f] & S2[a,b,f] ) ) & ( for m1, m2 being Morphism of C2 for a1, a2, a3 being Element of o Hom for f1, f2 being Element of the carrier' of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) holds C1 = C2 from CAT_5:sch_2(A21); ::_thesis: verum end; end; :: deftheorem Def11 defines -SliceCat CAT_5:def_11_:_ for C being Category for o being Object of C for b3 being strict with_triple-like_morphisms Category holds ( b3 = C -SliceCat o iff ( the carrier of b3 = Hom o & ( for a, b being Element of Hom o for f being Morphism of C st dom b = cod f & a = b (*) f holds [[a,b],f] is Morphism of b3 ) & ( for m being Morphism of b3 ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b3 for a1, a2, a3 being Element of Hom o for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) ); :: deftheorem Def12 defines -SliceCat CAT_5:def_12_:_ for C being Category for o being Object of C for b3 being strict with_triple-like_morphisms Category holds ( b3 = o -SliceCat C iff ( the carrier of b3 = o Hom & ( for a, b being Element of o Hom for f being Morphism of C st dom f = cod a & f (*) a = b holds [[a,b],f] is Morphism of b3 ) & ( for m being Morphism of b3 ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b3 for a1, a2, a3 being Element of o Hom for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) ); definition let C be Category; let o be Object of C; let m be Morphism of (C -SliceCat o); :: original: `2 redefine funcm `2 -> Morphism of C; coherence m `2 is Morphism of C proof ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) by Def11; hence m `2 is Morphism of C by MCART_1:7; ::_thesis: verum end; :: original: `11 redefine funcm `11 -> Element of Hom o; coherence m `11 is Element of Hom o proof ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) by Def11; hence m `11 is Element of Hom o by MCART_1:85; ::_thesis: verum end; :: original: `12 redefine funcm `12 -> Element of Hom o; coherence m `12 is Element of Hom o proof ex a, b being Element of Hom o ex f being Morphism of C st ( m = [[a,b],f] & dom b = cod f & a = b (*) f ) by Def11; hence m `12 is Element of Hom o by MCART_1:85; ::_thesis: verum end; end; theorem Th29: :: CAT_5:29 for C being Category for a being Object of C for m being Morphism of (C -SliceCat a) holds ( m = [[(m `11),(m `12)],(m `2)] & dom (m `12) = cod (m `2) & m `11 = (m `12) (*) (m `2) & dom m = m `11 & cod m = m `12 ) proof let C be Category; ::_thesis: for a being Object of C for m being Morphism of (C -SliceCat a) holds ( m = [[(m `11),(m `12)],(m `2)] & dom (m `12) = cod (m `2) & m `11 = (m `12) (*) (m `2) & dom m = m `11 & cod m = m `12 ) let o be Object of C; ::_thesis: for m being Morphism of (C -SliceCat o) holds ( m = [[(m `11),(m `12)],(m `2)] & dom (m `12) = cod (m `2) & m `11 = (m `12) (*) (m `2) & dom m = m `11 & cod m = m `12 ) let m be Morphism of (C -SliceCat o); ::_thesis: ( m = [[(m `11),(m `12)],(m `2)] & dom (m `12) = cod (m `2) & m `11 = (m `12) (*) (m `2) & dom m = m `11 & cod m = m `12 ) consider a, b being Element of Hom o, f being Morphism of C such that A1: m = [[a,b],f] and A2: dom b = cod f and A3: a = b (*) f by Def11; A4: m `11 = a by A1, MCART_1:85; m `12 = b by A1, MCART_1:85; hence ( m = [[(m `11),(m `12)],(m `2)] & dom (m `12) = cod (m `2) & m `11 = (m `12) (*) (m `2) & dom m = m `11 & cod m = m `12 ) by A1, A2, A3, A4, Th2, MCART_1:7; ::_thesis: verum end; theorem Th30: :: CAT_5:30 for C being Category for o being Object of C for f being Element of Hom o for a being Object of (C -SliceCat o) st a = f holds id a = [[a,a],(id (dom f))] proof let C be Category; ::_thesis: for o being Object of C for f being Element of Hom o for a being Object of (C -SliceCat o) st a = f holds id a = [[a,a],(id (dom f))] let o be Object of C; ::_thesis: for f being Element of Hom o for a being Object of (C -SliceCat o) st a = f holds id a = [[a,a],(id (dom f))] let f be Element of Hom o; ::_thesis: for a being Object of (C -SliceCat o) st a = f holds id a = [[a,a],(id (dom f))] let a be Object of (C -SliceCat o); ::_thesis: ( a = f implies id a = [[a,a],(id (dom f))] ) assume A1: a = f ; ::_thesis: id a = [[a,a],(id (dom f))] consider b, c being Element of Hom o, g being Morphism of C such that A2: id a = [[b,c],g] and A3: dom c = cod g and b = c (*) g by Def11; A4: cod (id (dom f)) = dom f ; f = f (*) (id (dom f)) by CAT_1:22; then reconsider h = [[f,f],(id (dom f))] as Morphism of (C -SliceCat o) by A4, Def11; A5: (id a) `11 = b by A2, MCART_1:85; A6: (id a) `12 = c by A2, MCART_1:85; A7: dom (id a) = b by A5, Th2; A8: cod (id a) = c by A6, Th2; A9: b = a by A7; A10: c = a by A8; dom h = h `11 by Th2 .= a by A1, MCART_1:85 ; then h = h (*) (id a) by CAT_1:22 .= [[f,f],((id (dom f)) (*) g)] by A1, A2, A9, A10, Def11 .= [[f,f],g] by A1, A3, A10, CAT_1:21 ; hence id a = [[a,a],(id (dom f))] by A1, A2, A7, A10; ::_thesis: verum end; definition let C be Category; let o be Object of C; let m be Morphism of (o -SliceCat C); :: original: `2 redefine funcm `2 -> Morphism of C; coherence m `2 is Morphism of C proof ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) by Def12; hence m `2 is Morphism of C by MCART_1:7; ::_thesis: verum end; :: original: `11 redefine funcm `11 -> Element of o Hom ; coherence m `11 is Element of o Hom proof ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) by Def12; hence m `11 is Element of o Hom by MCART_1:85; ::_thesis: verum end; :: original: `12 redefine funcm `12 -> Element of o Hom ; coherence m `12 is Element of o Hom proof ex a, b being Element of o Hom ex f being Morphism of C st ( m = [[a,b],f] & dom f = cod a & f (*) a = b ) by Def12; hence m `12 is Element of o Hom by MCART_1:85; ::_thesis: verum end; end; theorem Th31: :: CAT_5:31 for C being Category for a being Object of C for m being Morphism of (a -SliceCat C) holds ( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 ) proof let C be Category; ::_thesis: for a being Object of C for m being Morphism of (a -SliceCat C) holds ( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 ) let o be Object of C; ::_thesis: for m being Morphism of (o -SliceCat C) holds ( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 ) let m be Morphism of (o -SliceCat C); ::_thesis: ( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 ) consider a, b being Element of o Hom , f being Morphism of C such that A1: m = [[a,b],f] and A2: dom f = cod a and A3: f (*) a = b by Def12; A4: m `11 = a by A1, MCART_1:85; m `12 = b by A1, MCART_1:85; hence ( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 ) by A1, A2, A3, A4, Th2, MCART_1:7; ::_thesis: verum end; theorem Th32: :: CAT_5:32 for C being Category for o being Object of C for f being Element of o Hom for a being Object of (o -SliceCat C) st a = f holds id a = [[a,a],(id (cod f))] proof let C be Category; ::_thesis: for o being Object of C for f being Element of o Hom for a being Object of (o -SliceCat C) st a = f holds id a = [[a,a],(id (cod f))] let o be Object of C; ::_thesis: for f being Element of o Hom for a being Object of (o -SliceCat C) st a = f holds id a = [[a,a],(id (cod f))] let f be Element of o Hom ; ::_thesis: for a being Object of (o -SliceCat C) st a = f holds id a = [[a,a],(id (cod f))] let a be Object of (o -SliceCat C); ::_thesis: ( a = f implies id a = [[a,a],(id (cod f))] ) assume A1: a = f ; ::_thesis: id a = [[a,a],(id (cod f))] consider b, c being Element of o Hom , g being Morphism of C such that A2: id a = [[b,c],g] and A3: dom g = cod b and g (*) b = c by Def12; A4: dom (id (cod f)) = cod f ; f = (id (cod f)) (*) f by CAT_1:21; then reconsider h = [[f,f],(id (cod f))] as Morphism of (o -SliceCat C) by A4, Def12; A5: (id a) `11 = b by A2, MCART_1:85; A6: (id a) `12 = c by A2, MCART_1:85; A7: dom (id a) = b by A5, Th2; A8: cod (id a) = c by A6, Th2; A9: b = a by A7; A10: c = a by A8; cod h = h `12 by Th2 .= a by A1, MCART_1:85 ; then h = (id a) (*) h by CAT_1:21 .= [[f,f],(g (*) (id (cod f)))] by A1, A2, A9, A10, Def12 .= [[f,f],g] by A1, A3, A9, CAT_1:22 ; hence id a = [[a,a],(id (cod f))] by A1, A2, A8, A9; ::_thesis: verum end; begin definition let C be Category; let f be Morphism of C; func SliceFunctor f -> Functor of C -SliceCat (dom f),C -SliceCat (cod f) means :Def13: :: CAT_5:def 13 for m being Morphism of (C -SliceCat (dom f)) holds it . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)]; existence ex b1 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st for m being Morphism of (C -SliceCat (dom f)) holds b1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] proof set C1 = C -SliceCat (dom f); set C2 = C -SliceCat (cod f); deffunc H1( Morphism of (C -SliceCat (dom f))) -> Element of the carrier' of [:[:C,C:],C:] = [[(f (*) (\$1 `11)),(f (*) (\$1 `12))],(\$1 `2)]; consider F being Function of the carrier' of (C -SliceCat (dom f)), the carrier' of [:[:C,C:],C:] such that A1: for m being Morphism of (C -SliceCat (dom f)) holds F . m = H1(m) from FUNCT_2:sch_4(); A2: dom F = the carrier' of (C -SliceCat (dom f)) by FUNCT_2:def_1; rng F c= the carrier' of (C -SliceCat (cod f)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in the carrier' of (C -SliceCat (cod f)) ) assume x in rng F ; ::_thesis: x in the carrier' of (C -SliceCat (cod f)) then consider m being set such that A3: m in dom F and A4: x = F . m by FUNCT_1:def_3; reconsider m = m as Morphism of (C -SliceCat (dom f)) by A3; A5: x = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] by A1, A4; A6: dom (m `12) = cod (m `2) by Th29; A7: m `11 = (m `12) (*) (m `2) by Th29; A8: cod (m `12) = dom f by Th23; A9: f (*) (m `11) in Hom (cod f) by Th27; A10: f (*) (m `12) in Hom (cod f) by Th27; A11: dom (f (*) (m `12)) = cod (m `2) by A6, A8, CAT_1:17; f (*) (m `11) = (f (*) (m `12)) (*) (m `2) by A6, A7, A8, CAT_1:18; then x is Morphism of (C -SliceCat (cod f)) by A5, A9, A10, A11, Def11; hence x in the carrier' of (C -SliceCat (cod f)) ; ::_thesis: verum end; then reconsider F = F as Function of the carrier' of (C -SliceCat (dom f)), the carrier' of (C -SliceCat (cod f)) by A2, FUNCT_2:def_1, RELSET_1:4; A12: now__::_thesis:_for_c_being_Object_of_(C_-SliceCat_(dom_f))_ex_d_being_Object_of_(C_-SliceCat_(cod_f))_st_F_._(id_c)_=_id_d let c be Object of (C -SliceCat (dom f)); ::_thesis: ex d being Object of (C -SliceCat (cod f)) st F . (id c) = id d reconsider g = c as Element of Hom (dom f) by Def11; reconsider h = f (*) g as Element of Hom (cod f) by Th27; reconsider d = h as Object of (C -SliceCat (cod f)) by Def11; take d = d; ::_thesis: F . (id c) = id d A13: id c = [[c,c],(id (dom g))] by Th30; A14: id d = [[d,d],(id (dom h))] by Th30; A15: (id c) `11 = c by A13, MCART_1:85; A16: (id c) `12 = c by A13, MCART_1:85; A17: (id c) `2 = id (dom g) by A13, MCART_1:7; A18: cod g = dom f by Th23; thus F . (id c) = [[h,h],((id c) `2)] by A1, A15, A16 .= id d by A14, A17, A18, CAT_1:17 ; ::_thesis: verum end; A19: now__::_thesis:_for_m_being_Morphism_of_(C_-SliceCat_(dom_f))_holds_ (_F_._(id_(dom_m))_=_id_(dom_(F_._m))_&_F_._(id_(cod_m))_=_id_(cod_(F_._m))_) let m be Morphism of (C -SliceCat (dom f)); ::_thesis: ( F . (id (dom m)) = id (dom (F . m)) & F . (id (cod m)) = id (cod (F . m)) ) reconsider g1 = f (*) (m `11), g2 = f (*) (m `12) as Element of Hom (cod f) by Th27; A20: dom f = cod (m `11) by Th23; A21: dom f = cod (m `12) by Th23; F . m = [[g1,g2],(m `2)] by A1; then dom (F . m) = [[g1,g2],(m `2)] `11 by Th29 .= g1 by MCART_1:85 ; then A22: id (dom (F . m)) = [[g1,g1],(id (dom g1))] by Th30; dom m = m `11 by Th29; then A23: id (dom m) = [[(m `11),(m `11)],(id (dom (m `11)))] by Th30; then A24: (id (dom m)) `11 = m `11 by MCART_1:85; A25: (id (dom m)) `12 = m `11 by A23, MCART_1:85; (id (dom m)) `2 = id (dom (m `11)) by A23, MCART_1:7; hence F . (id (dom m)) = [[g1,g1],(id (dom (m `11)))] by A1, A24, A25 .= id (dom (F . m)) by A20, A22, CAT_1:17 ; ::_thesis: F . (id (cod m)) = id (cod (F . m)) F . m = [[g1,g2],(m `2)] by A1; then cod (F . m) = [[g1,g2],(m `2)] `12 by Th29 .= g2 by MCART_1:85 ; then A26: id (cod (F . m)) = [[g2,g2],(id (dom g2))] by Th30; cod m = m `12 by Th29; then A27: id (cod m) = [[(m `12),(m `12)],(id (dom (m `12)))] by Th30; then A28: (id (cod m)) `11 = m `12 by MCART_1:85; A29: (id (cod m)) `12 = m `12 by A27, MCART_1:85; (id (cod m)) `2 = id (dom (m `12)) by A27, MCART_1:7; hence F . (id (cod m)) = [[g2,g2],(id (dom (m `12)))] by A1, A28, A29 .= id (cod (F . m)) by A21, A26, CAT_1:17 ; ::_thesis: verum end; now__::_thesis:_for_f1,_f2_being_Morphism_of_(C_-SliceCat_(dom_f))_st_dom_f2_=_cod_f1_holds_ F_._(f2_(*)_f1)_=_(F_._f2)_(*)_(F_._f1) let f1, f2 be Morphism of (C -SliceCat (dom f)); ::_thesis: ( dom f2 = cod f1 implies F . (f2 (*) f1) = (F . f2) (*) (F . f1) ) consider a1, b1 being Element of Hom (dom f), g1 being Morphism of C such that A30: f1 = [[a1,b1],g1] and dom b1 = cod g1 and a1 = b1 (*) g1 by Def11; consider a2, b2 being Element of Hom (dom f), g2 being Morphism of C such that A31: f2 = [[a2,b2],g2] and dom b2 = cod g2 and a2 = b2 (*) g2 by Def11; A32: dom f2 = f2 `11 by Th2; A33: cod f1 = f1 `12 by Th2; A34: dom f2 = a2 by A31, A32, MCART_1:85; A35: cod f1 = b1 by A30, A33, MCART_1:85; reconsider ha1 = f (*) a1, ha2 = f (*) a2, hb1 = f (*) b1, hb2 = f (*) b2 as Element of Hom (cod f) by Th27; A36: f1 `11 = a1 by A30, MCART_1:85; A37: f1 `12 = b1 by A30, MCART_1:85; A38: f1 `2 = g1 by A30, MCART_1:7; A39: f2 `11 = a2 by A31, MCART_1:85; A40: f2 `12 = b2 by A31, MCART_1:85; A41: f2 `2 = g2 by A31, MCART_1:7; A42: F . f1 = [[ha1,hb1],g1] by A1, A36, A37, A38; A43: F . f2 = [[ha2,hb2],g2] by A1, A39, A40, A41; assume A44: dom f2 = cod f1 ; ::_thesis: F . (f2 (*) f1) = (F . f2) (*) (F . f1) then A45: f2 (*) f1 = [[a1,b2],(g2 (*) g1)] by A30, A31, A34, A35, Def11; A46: (F . f2) (*) (F . f1) = [[ha1,hb2],(g2 (*) g1)] by A34, A35, A42, A43, A44, Def11; A47: (f2 (*) f1) `11 = a1 by A45, MCART_1:85; A48: (f2 (*) f1) `12 = b2 by A45, MCART_1:85; (f2 (*) f1) `2 = g2 (*) g1 by A45, MCART_1:7; hence F . (f2 (*) f1) = (F . f2) (*) (F . f1) by A1, A46, A47, A48; ::_thesis: verum end; then reconsider F = F as Functor of C -SliceCat (dom f),C -SliceCat (cod f) by A12, A19, CAT_1:61; take F ; ::_thesis: for m being Morphism of (C -SliceCat (dom f)) holds F . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] thus for m being Morphism of (C -SliceCat (dom f)) holds F . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] by A1; ::_thesis: verum end; uniqueness for b1, b2 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st ( for m being Morphism of (C -SliceCat (dom f)) holds b1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) & ( for m being Morphism of (C -SliceCat (dom f)) holds b2 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) holds b1 = b2 proof let F1, F2 be Functor of C -SliceCat (dom f),C -SliceCat (cod f); ::_thesis: ( ( for m being Morphism of (C -SliceCat (dom f)) holds F1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) & ( for m being Morphism of (C -SliceCat (dom f)) holds F2 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) implies F1 = F2 ) assume that A49: for m being Morphism of (C -SliceCat (dom f)) holds F1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] and A50: for m being Morphism of (C -SliceCat (dom f)) holds F2 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ; ::_thesis: F1 = F2 now__::_thesis:_for_m_being_Morphism_of_(C_-SliceCat_(dom_f))_holds_F1_._m_=_F2_._m let m be Morphism of (C -SliceCat (dom f)); ::_thesis: F1 . m = F2 . m thus F1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] by A49 .= F2 . m by A50 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; func SliceContraFunctor f -> Functor of (cod f) -SliceCat C,(dom f) -SliceCat C means :Def14: :: CAT_5:def 14 for m being Morphism of ((cod f) -SliceCat C) holds it . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)]; existence ex b1 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st for m being Morphism of ((cod f) -SliceCat C) holds b1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] proof set C1 = (cod f) -SliceCat C; set C2 = (dom f) -SliceCat C; deffunc H1( Morphism of ((cod f) -SliceCat C)) -> Element of the carrier' of [:[:C,C:],C:] = [[((\$1 `11) (*) f),((\$1 `12) (*) f)],(\$1 `2)]; consider F being Function of the carrier' of ((cod f) -SliceCat C), the carrier' of [:[:C,C:],C:] such that A51: for m being Morphism of ((cod f) -SliceCat C) holds F . m = H1(m) from FUNCT_2:sch_4(); A52: dom F = the carrier' of ((cod f) -SliceCat C) by FUNCT_2:def_1; rng F c= the carrier' of ((dom f) -SliceCat C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in the carrier' of ((dom f) -SliceCat C) ) assume x in rng F ; ::_thesis: x in the carrier' of ((dom f) -SliceCat C) then consider m being set such that A53: m in dom F and A54: x = F . m by FUNCT_1:def_3; reconsider m = m as Morphism of ((cod f) -SliceCat C) by A53; A55: x = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] by A51, A54; A56: dom (m `2) = cod (m `11) by Th31; A57: m `12 = (m `2) (*) (m `11) by Th31; A58: dom (m `11) = cod f by Th24; A59: (m `11) (*) f in (dom f) Hom by Th28; A60: (m `12) (*) f in (dom f) Hom by Th28; A61: cod ((m `11) (*) f) = dom (m `2) by A56, A58, CAT_1:17; (m `12) (*) f = (m `2) (*) ((m `11) (*) f) by A56, A57, A58, CAT_1:18; then x is Morphism of ((dom f) -SliceCat C) by A55, A59, A60, A61, Def12; hence x in the carrier' of ((dom f) -SliceCat C) ; ::_thesis: verum end; then reconsider F = F as Function of the carrier' of ((cod f) -SliceCat C), the carrier' of ((dom f) -SliceCat C) by A52, FUNCT_2:def_1, RELSET_1:4; A62: now__::_thesis:_for_c_being_Object_of_((cod_f)_-SliceCat_C)_ex_d_being_Object_of_((dom_f)_-SliceCat_C)_st_F_._(id_c)_=_id_d let c be Object of ((cod f) -SliceCat C); ::_thesis: ex d being Object of ((dom f) -SliceCat C) st F . (id c) = id d reconsider g = c as Element of (cod f) Hom by Def12; reconsider h = g (*) f as Element of (dom f) Hom by Th28; reconsider d = h as Object of ((dom f) -SliceCat C) by Def12; take d = d; ::_thesis: F . (id c) = id d A63: id c = [[c,c],(id (cod g))] by Th32; A64: id d = [[d,d],(id (cod h))] by Th32; A65: (id c) `11 = c by A63, MCART_1:85; A66: (id c) `12 = c by A63, MCART_1:85; A67: (id c) `2 = id (cod g) by A63, MCART_1:7; A68: dom g = cod f by Th24; thus F . (id c) = [[h,h],((id c) `2)] by A51, A65, A66 .= id d by A64, A67, A68, CAT_1:17 ; ::_thesis: verum end; A69: now__::_thesis:_for_m_being_Morphism_of_((cod_f)_-SliceCat_C)_holds_ (_F_._(id_(dom_m))_=_id_(dom_(F_._m))_&_F_._(id_(cod_m))_=_id_(cod_(F_._m))_) let m be Morphism of ((cod f) -SliceCat C); ::_thesis: ( F . (id (dom m)) = id (dom (F . m)) & F . (id (cod m)) = id (cod (F . m)) ) reconsider g1 = (m `11) (*) f, g2 = (m `12) (*) f as Element of (dom f) Hom by Th28; A70: cod f = dom (m `11) by Th24; A71: cod f = dom (m `12) by Th24; F . m = [[g1,g2],(m `2)] by A51; then dom (F . m) = [[g1,g2],(m `2)] `11 by Th31 .= g1 by MCART_1:85 ; then A72: id (dom (F . m)) = [[g1,g1],(id (cod g1))] by Th32; dom m = m `11 by Th31; then A73: id (dom m) = [[(m `11),(m `11)],(id (cod (m `11)))] by Th32; then A74: (id (dom m)) `11 = m `11 by MCART_1:85; A75: (id (dom m)) `12 = m `11 by A73, MCART_1:85; (id (dom m)) `2 = id (cod (m `11)) by A73, MCART_1:7; hence F . (id (dom m)) = [[g1,g1],(id (cod (m `11)))] by A51, A74, A75 .= id (dom (F . m)) by A70, A72, CAT_1:17 ; ::_thesis: F . (id (cod m)) = id (cod (F . m)) F . m = [[g1,g2],(m `2)] by A51; then cod (F . m) = [[g1,g2],(m `2)] `12 by Th31 .= g2 by MCART_1:85 ; then A76: id (cod (F . m)) = [[g2,g2],(id (cod g2))] by Th32; cod m = m `12 by Th31; then A77: id (cod m) = [[(m `12),(m `12)],(id (cod (m `12)))] by Th32; then A78: (id (cod m)) `11 = m `12 by MCART_1:85; A79: (id (cod m)) `12 = m `12 by A77, MCART_1:85; (id (cod m)) `2 = id (cod (m `12)) by A77, MCART_1:7; hence F . (id (cod m)) = [[g2,g2],(id (cod (m `12)))] by A51, A78, A79 .= id (cod (F . m)) by A71, A76, CAT_1:17 ; ::_thesis: verum end; now__::_thesis:_for_f1,_f2_being_Morphism_of_((cod_f)_-SliceCat_C)_st_dom_f2_=_cod_f1_holds_ F_._(f2_(*)_f1)_=_(F_._f2)_(*)_(F_._f1) let f1, f2 be Morphism of ((cod f) -SliceCat C); ::_thesis: ( dom f2 = cod f1 implies F . (f2 (*) f1) = (F . f2) (*) (F . f1) ) consider a1, b1 being Element of (cod f) Hom , g1 being Morphism of C such that A80: f1 = [[a1,b1],g1] and dom g1 = cod a1 and g1 (*) a1 = b1 by Def12; consider a2, b2 being Element of (cod f) Hom , g2 being Morphism of C such that A81: f2 = [[a2,b2],g2] and dom g2 = cod a2 and g2 (*) a2 = b2 by Def12; A82: dom f2 = f2 `11 by Th2; A83: cod f1 = f1 `12 by Th2; A84: dom f2 = a2 by A81, A82, MCART_1:85; A85: cod f1 = b1 by A80, A83, MCART_1:85; reconsider ha1 = a1 (*) f, ha2 = a2 (*) f, hb1 = b1 (*) f, hb2 = b2 (*) f as Element of (dom f) Hom by Th28; A86: f1 `11 = a1 by A80, MCART_1:85; A87: f1 `12 = b1 by A80, MCART_1:85; A88: f1 `2 = g1 by A80, MCART_1:7; A89: f2 `11 = a2 by A81, MCART_1:85; A90: f2 `12 = b2 by A81, MCART_1:85; A91: f2 `2 = g2 by A81, MCART_1:7; A92: F . f1 = [[ha1,hb1],g1] by A51, A86, A87, A88; A93: F . f2 = [[ha2,hb2],g2] by A51, A89, A90, A91; assume A94: dom f2 = cod f1 ; ::_thesis: F . (f2 (*) f1) = (F . f2) (*) (F . f1) then A95: f2 (*) f1 = [[a1,b2],(g2 (*) g1)] by A80, A81, A84, A85, Def12; A96: (F . f2) (*) (F . f1) = [[ha1,hb2],(g2 (*) g1)] by A84, A85, A92, A93, A94, Def12; A97: (f2 (*) f1) `11 = a1 by A95, MCART_1:85; A98: (f2 (*) f1) `12 = b2 by A95, MCART_1:85; (f2 (*) f1) `2 = g2 (*) g1 by A95, MCART_1:7; hence F . (f2 (*) f1) = (F . f2) (*) (F . f1) by A51, A96, A97, A98; ::_thesis: verum end; then reconsider F = F as Functor of (cod f) -SliceCat C,(dom f) -SliceCat C by A62, A69, CAT_1:61; take F ; ::_thesis: for m being Morphism of ((cod f) -SliceCat C) holds F . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] thus for m being Morphism of ((cod f) -SliceCat C) holds F . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] by A51; ::_thesis: verum end; uniqueness for b1, b2 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st ( for m being Morphism of ((cod f) -SliceCat C) holds b1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) & ( for m being Morphism of ((cod f) -SliceCat C) holds b2 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) holds b1 = b2 proof let F1, F2 be Functor of (cod f) -SliceCat C,(dom f) -SliceCat C; ::_thesis: ( ( for m being Morphism of ((cod f) -SliceCat C) holds F1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) & ( for m being Morphism of ((cod f) -SliceCat C) holds F2 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) implies F1 = F2 ) assume that A99: for m being Morphism of ((cod f) -SliceCat C) holds F1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] and A100: for m being Morphism of ((cod f) -SliceCat C) holds F2 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ; ::_thesis: F1 = F2 now__::_thesis:_for_m_being_Morphism_of_((cod_f)_-SliceCat_C)_holds_F1_._m_=_F2_._m let m be Morphism of ((cod f) -SliceCat C); ::_thesis: F1 . m = F2 . m thus F1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] by A99 .= F2 . m by A100 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def13 defines SliceFunctor CAT_5:def_13_:_ for C being Category for f being Morphism of C for b3 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) holds ( b3 = SliceFunctor f iff for m being Morphism of (C -SliceCat (dom f)) holds b3 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ); :: deftheorem Def14 defines SliceContraFunctor CAT_5:def_14_:_ for C being Category for f being Morphism of C for b3 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C holds ( b3 = SliceContraFunctor f iff for m being Morphism of ((cod f) -SliceCat C) holds b3 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ); theorem :: CAT_5:33 for C being Category for f, g being Morphism of C st dom g = cod f holds SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f) proof let C be Category; ::_thesis: for f, g being Morphism of C st dom g = cod f holds SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f) let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f) ) assume A1: dom g = cod f ; ::_thesis: SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f) then A2: dom (g (*) f) = dom f by CAT_1:17; set A1 = C -SliceCat (dom f); set A3 = C -SliceCat (cod g); set F = SliceFunctor f; reconsider G = SliceFunctor g as Functor of C -SliceCat (cod f),C -SliceCat (cod g) by A1; reconsider GF = SliceFunctor (g (*) f) as Functor of C -SliceCat (dom f),C -SliceCat (cod g) by A1, A2, CAT_1:17; now__::_thesis:_for_m_being_Morphism_of_(C_-SliceCat_(dom_f))_holds_(G_*_(SliceFunctor_f))_._m_=_GF_._m let m be Morphism of (C -SliceCat (dom f)); ::_thesis: (G * (SliceFunctor f)) . m = GF . m A3: (SliceFunctor f) . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] by Def13; then A4: ((SliceFunctor f) . m) `11 = f (*) (m `11) by MCART_1:85; A5: ((SliceFunctor f) . m) `12 = f (*) (m `12) by A3, MCART_1:85; A6: ((SliceFunctor f) . m) `2 = m `2 by A3, MCART_1:7; A7: dom f = cod (m `11) by Th23; A8: dom f = cod (m `12) by Th23; A9: g (*) (f (*) (m `11)) = (g (*) f) (*) (m `11) by A1, A7, CAT_1:18; A10: g (*) (f (*) (m `12)) = (g (*) f) (*) (m `12) by A1, A8, CAT_1:18; thus (G * (SliceFunctor f)) . m = G . ((SliceFunctor f) . m) by FUNCT_2:15 .= [[(g (*) (f (*) (m `11))),(g (*) (f (*) (m `12)))],(m `2)] by A1, A4, A5, A6, Def13 .= GF . m by A2, A9, A10, Def13 ; ::_thesis: verum end; hence SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f) by FUNCT_2:63; ::_thesis: verum end; theorem :: CAT_5:34 for C being Category for f, g being Morphism of C st dom g = cod f holds SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g) proof let C be Category; ::_thesis: for f, g being Morphism of C st dom g = cod f holds SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g) let f, g be Morphism of C; ::_thesis: ( dom g = cod f implies SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g) ) assume A1: dom g = cod f ; ::_thesis: SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g) then A2: cod (g (*) f) = cod g by CAT_1:17; set A1 = (dom f) -SliceCat C; set A2 = (cod f) -SliceCat C; set A3 = (cod g) -SliceCat C; reconsider F = SliceContraFunctor f as Functor of (cod f) -SliceCat C,(dom f) -SliceCat C ; reconsider G = SliceContraFunctor g as Functor of (cod g) -SliceCat C,(cod f) -SliceCat C by A1; reconsider FG = SliceContraFunctor (g (*) f) as Functor of (cod g) -SliceCat C,(dom f) -SliceCat C by A1, A2, CAT_1:17; now__::_thesis:_for_m_being_Morphism_of_((cod_g)_-SliceCat_C)_holds_(F_*_G)_._m_=_FG_._m let m be Morphism of ((cod g) -SliceCat C); ::_thesis: (F * G) . m = FG . m A3: G . m = [[((m `11) (*) g),((m `12) (*) g)],(m `2)] by Def14; then A4: (G . m) `11 = (m `11) (*) g by MCART_1:85; A5: (G . m) `12 = (m `12) (*) g by A3, MCART_1:85; A6: (G . m) `2 = m `2 by A3, MCART_1:7; A7: cod g = dom (m `11) by Th24; A8: cod g = dom (m `12) by Th24; A9: (m `11) (*) (g (*) f) = ((m `11) (*) g) (*) f by A1, A7, CAT_1:18; A10: (m `12) (*) (g (*) f) = ((m `12) (*) g) (*) f by A1, A8, CAT_1:18; thus (F * G) . m = F . (G . m) by FUNCT_2:15 .= [[(((m `11) (*) g) (*) f),(((m `12) (*) g) (*) f)],(m `2)] by A4, A5, A6, Def14 .= FG . m by A2, A9, A10, Def14 ; ::_thesis: verum end; hence SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g) by FUNCT_2:63; ::_thesis: verum end;