:: COMMACAT semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

deffunc H1( CatStr ) -> set = the Objects of $1;

deffunc H2( CatStr ) -> set = the Morphisms of $1;

definition
canceled;
canceled;
canceled;
canceled;
end;

:: deftheorem COMMACAT:def 1 :
canceled;

:: deftheorem COMMACAT:def 2 :
canceled;

:: deftheorem COMMACAT:def 3 :
canceled;

:: deftheorem COMMACAT:def 4 :
canceled;

theorem :: COMMACAT:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

Lm1: for x1, x2, y, x, y1, y2 being set holds
( [[x1,x2],y] `11 = x1 & [[x1,x2],y] `12 = x2 & [x,[y1,y2]] `21 = y1 & [x,[y1,y2]] `22 = y2 )
by MCART_1:89;

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom (F . c1),(G . d1) ;
func commaObjs F,G -> non empty Subset of [:[:the Objects of C,the Objects of D:],the Morphisms of E:] equals :Def5: :: COMMACAT:def 5
{ [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } ;
coherence
{ [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } is non empty Subset of [:[:the Objects of C,the Objects of D:],the Morphisms of E:]
proof end;
end;

:: deftheorem Def5 defines commaObjs COMMACAT:def 5 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom (F . c1),(G . d1) holds
commaObjs F,G = { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } ;

theorem Th2: :: COMMACAT:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for o being Element of commaObjs F,G st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom (F . c),(G . d) holds
( o = [[(o `11 ),(o `12 )],(o `2 )] & o `2 in Hom (F . (o `11 )),(G . (o `12 )) & dom (o `2 ) = F . (o `11 ) & cod (o `2 ) = G . (o `12 ) )
proof end;

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom (F . c1),(G . d1) ;
func commaMorphs F,G -> non empty Subset of [:[:(commaObjs F,G),(commaObjs F,G):],[:the Morphisms of C,the Morphisms of D:]:] equals :Def6: :: COMMACAT:def 6
{ [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } ;
coherence
{ [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } is non empty Subset of [:[:(commaObjs F,G),(commaObjs F,G):],[:the Morphisms of C,the Morphisms of D:]:]
proof end;
end;

:: deftheorem Def6 defines commaMorphs COMMACAT:def 6 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom (F . c1),(G . d1) holds
commaMorphs F,G = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } ;

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
let k be Element of commaMorphs F,G;
:: original: `11
redefine func k `11 -> Element of commaObjs F,G;
coherence
k `11 is Element of commaObjs F,G
proof end;
:: original: `12
redefine func k `12 -> Element of commaObjs F,G;
coherence
k `12 is Element of commaObjs F,G
proof end;
end;

theorem Th3: :: COMMACAT:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for k being Element of commaMorphs F,G st ex c being Object of C ex d being Object of D ex f being Morphism of E st f in Hom (F . c),(G . d) holds
( k = [[(k `11 ),(k `12 )],[(k `21 ),(k `22 )]] & dom (k `21 ) = (k `11 ) `11 & cod (k `21 ) = (k `12 ) `11 & dom (k `22 ) = (k `11 ) `12 & cod (k `22 ) = (k `12 ) `12 & ((k `12 ) `2 ) * (F . (k `21 )) = (G . (k `22 )) * ((k `11 ) `2 ) )
proof end;

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
let k1, k2 be Element of commaMorphs F,G;
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom (F . c1),(G . d1) ;
assume A2: k1 `12 = k2 `11 ;
func k2 * k1 -> Element of commaMorphs F,G equals :Def7: :: COMMACAT:def 7
[[(k1 `11 ),(k2 `12 )],[((k2 `21 ) * (k1 `21 )),((k2 `22 ) * (k1 `22 ))]];
coherence
[[(k1 `11 ),(k2 `12 )],[((k2 `21 ) * (k1 `21 )),((k2 `22 ) * (k1 `22 ))]] is Element of commaMorphs F,G
proof end;
end;

:: deftheorem Def7 defines * COMMACAT:def 7 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for k1, k2 being Element of commaMorphs F,G st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom (F . c1),(G . d1) & k1 `12 = k2 `11 holds
k2 * k1 = [[(k1 `11 ),(k2 `12 )],[((k2 `21 ) * (k1 `21 )),((k2 `22 ) * (k1 `22 ))]];

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
func commaComp F,G -> PartFunc of [:(commaMorphs F,G),(commaMorphs F,G):], commaMorphs F,G means :Def8: :: COMMACAT:def 8
( dom it = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } & ( for k, k' being Element of commaMorphs F,G st [k,k'] in dom it holds
it . [k,k'] = k * k' ) );
existence
ex b1 being PartFunc of [:(commaMorphs F,G),(commaMorphs F,G):], commaMorphs F,G st
( dom b1 = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } & ( for k, k' being Element of commaMorphs F,G st [k,k'] in dom b1 holds
b1 . [k,k'] = k * k' ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(commaMorphs F,G),(commaMorphs F,G):], commaMorphs F,G st dom b1 = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } & ( for k, k' being Element of commaMorphs F,G st [k,k'] in dom b1 holds
b1 . [k,k'] = k * k' ) & dom b2 = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } & ( for k, k' being Element of commaMorphs F,G st [k,k'] in dom b2 holds
b2 . [k,k'] = k * k' ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines commaComp COMMACAT:def 8 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E
for b6 being PartFunc of [:(commaMorphs F,G),(commaMorphs F,G):], commaMorphs F,G holds
( b6 = commaComp F,G iff ( dom b6 = { [k1,k2] where k1, k2 is Element of commaMorphs F,G : k1 `11 = k2 `12 } & ( for k, k' being Element of commaMorphs F,G st [k,k'] in dom b6 holds
b6 . [k,k'] = k * k' ) ) );

definition
let C, D, E be Category;
let F be Functor of C,E;
let G be Functor of D,E;
given c1 being Object of C, d1 being Object of D, f1 being Morphism of E such that A1: f1 in Hom (F . c1),(G . d1) ;
func F comma G -> strict Category means :: COMMACAT:def 9
( the Objects of it = commaObjs F,G & the Morphisms of it = commaMorphs F,G & ( for k being Element of commaMorphs F,G holds the Dom of it . k = k `11 ) & ( for k being Element of commaMorphs F,G holds the Cod of it . k = k `12 ) & ( for o being Element of commaObjs F,G holds the Id of it . o = [[o,o],[(id (o `11 )),(id (o `12 ))]] ) & the Comp of it = commaComp F,G );
existence
ex b1 being strict Category st
( the Objects of b1 = commaObjs F,G & the Morphisms of b1 = commaMorphs F,G & ( for k being Element of commaMorphs F,G holds the Dom of b1 . k = k `11 ) & ( for k being Element of commaMorphs F,G holds the Cod of b1 . k = k `12 ) & ( for o being Element of commaObjs F,G holds the Id of b1 . o = [[o,o],[(id (o `11 )),(id (o `12 ))]] ) & the Comp of b1 = commaComp F,G )
proof end;
uniqueness
for b1, b2 being strict Category st the Objects of b1 = commaObjs F,G & the Morphisms of b1 = commaMorphs F,G & ( for k being Element of commaMorphs F,G holds the Dom of b1 . k = k `11 ) & ( for k being Element of commaMorphs F,G holds the Cod of b1 . k = k `12 ) & ( for o being Element of commaObjs F,G holds the Id of b1 . o = [[o,o],[(id (o `11 )),(id (o `12 ))]] ) & the Comp of b1 = commaComp F,G & the Objects of b2 = commaObjs F,G & the Morphisms of b2 = commaMorphs F,G & ( for k being Element of commaMorphs F,G holds the Dom of b2 . k = k `11 ) & ( for k being Element of commaMorphs F,G holds the Cod of b2 . k = k `12 ) & ( for o being Element of commaObjs F,G holds the Id of b2 . o = [[o,o],[(id (o `11 )),(id (o `12 ))]] ) & the Comp of b2 = commaComp F,G holds
b1 = b2
proof end;
end;

:: deftheorem defines comma COMMACAT:def 9 :
for C, D, E being Category
for F being Functor of C,E
for G being Functor of D,E st ex c1 being Object of C ex d1 being Object of D ex f1 being Morphism of E st f1 in Hom (F . c1),(G . d1) holds
for b6 being strict Category holds
( b6 = F comma G iff ( the Objects of b6 = commaObjs F,G & the Morphisms of b6 = commaMorphs F,G & ( for k being Element of commaMorphs F,G holds the Dom of b6 . k = k `11 ) & ( for k being Element of commaMorphs F,G holds the Cod of b6 . k = k `12 ) & ( for o being Element of commaObjs F,G holds the Id of b6 . o = [[o,o],[(id (o `11 )),(id (o `12 ))]] ) & the Comp of b6 = commaComp F,G ) );

theorem Th4: :: COMMACAT:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x being set holds
( the Objects of (1Cat x,y) = {x} & the Morphisms of (1Cat x,y) = {y} )
proof end;

theorem Th5: :: COMMACAT:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x being set
for a, b being Object of (1Cat x,y) holds Hom a,b = {y}
proof end;

definition
let C be Category;
let c be Object of C;
func 1Cat c -> strict Subcategory of C equals :: COMMACAT:def 10
1Cat c,(id c);
coherence
1Cat c,(id c) is strict Subcategory of C
proof end;
end;

:: deftheorem defines 1Cat COMMACAT:def 10 :
for C being Category
for c being Object of C holds 1Cat c = 1Cat c,(id c);

definition
let C be Category;
let c be Object of C;
func c comma C -> strict Category equals :: COMMACAT:def 11
(incl (1Cat c)) comma (id C);
coherence
(incl (1Cat c)) comma (id C) is strict Category
;
func C comma c -> strict Category equals :: COMMACAT:def 12
(id C) comma (incl (1Cat c));
coherence
(id C) comma (incl (1Cat c)) is strict Category
;
end;

:: deftheorem defines comma COMMACAT:def 11 :
for C being Category
for c being Object of C holds c comma C = (incl (1Cat c)) comma (id C);

:: deftheorem defines comma COMMACAT:def 12 :
for C being Category
for c being Object of C holds C comma c = (id C) comma (incl (1Cat c));