:: 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;