:: Comma Category
:: by Grzegorz Bancerek and Agata Darmochwa\l
::
:: Received February 20, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

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

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

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 carrier of C, the carrier of D:], the carrier' of E:] equals :Def1: :: COMMACAT:def 1
 {  [[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 carrier of C, the carrier of D:], the carrier' of E:]
proofend;
end;

:: deftheorem Def1 defines commaObjs COMMACAT:def_1_:_
 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 Th1: :: COMMACAT:1
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) )
proofend;

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 carrier' of C, the carrier' of D:]:] equals :Def2: :: COMMACAT:def 2
 {  [[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 carrier' of C, the carrier' of D:]:]
proofend;
end;

:: deftheorem Def2 defines commaMorphs COMMACAT:def_2_:_
 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 funck `11  ->  Element of commaObjs (F,G);
coherence
 k `11 is Element of commaObjs (F,G)
proofend;
:: original:`12
redefine funck `12  ->  Element of commaObjs (F,G);
coherence
 k `12 is Element of commaObjs (F,G)
proofend;
end;

theorem Th2: :: COMMACAT:2
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) )
proofend;

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 ;
funck2 * k1 ->  Element of commaMorphs (F,G) equals :Def3: :: COMMACAT:def 3
[[(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)
proofend;
end;

:: deftheorem Def3 defines * COMMACAT:def_3_:_
 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 :Def4: :: COMMACAT:def 4
( dom it =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom it holds
it . [k,k9] = k * k9 ) );
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, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b1 holds
b1 . [k,k9] = k * k9 ) )
proofend;
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, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b1 holds
b1 . [k,k9] = k * k9 ) & dom b2 =  {  [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12  }  & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b2 holds
b2 . [k,k9] = k * k9 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines commaComp COMMACAT:def_4_:_
 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, k9 being Element of commaMorphs (F,G) st [k,k9] in dom b6 holds
b6 . [k,k9] = k * k9 ) ) );

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)) ;
funcF comma G ->  strict Category means :: COMMACAT:def 5
( the carrier of it = commaObjs (F,G) & the carrier' of it = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of it . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of it . k = k `12 ) & the Comp of it = commaComp (F,G) );
existence
 ex b1 being strict Category st
( the carrier of b1 = commaObjs (F,G) & the carrier' of b1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b1 . k = k `12 ) & the Comp of b1 = commaComp (F,G) )
proofend;
uniqueness
 for b1, b2 being strict Category st the carrier of b1 = commaObjs (F,G) & the carrier' of b1 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b1 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b1 . k = k `12 ) & the Comp of b1 = commaComp (F,G) & the carrier of b2 = commaObjs (F,G) & the carrier' of b2 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b2 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b2 . k = k `12 ) & the Comp of b2 = commaComp (F,G) holds
b1 = b2
proofend;
end;

:: deftheorem  defines comma 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
for b6 being strict Category holds
( b6 = F comma G iff ( the carrier of b6 = commaObjs (F,G) & the carrier' of b6 = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b6 . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b6 . k = k `12 ) & the Comp of b6 = commaComp (F,G) ) );

theorem :: COMMACAT:3
for y, x being set holds
( the carrier of (1Cat (x,y)) = {x} & the carrier' of (1Cat (x,y)) = {y} ) ;

theorem Th4: :: COMMACAT:4
for y, x being set
for a, b being Object of (1Cat (x,y)) holds Hom (a,b) = {y}
proofend;

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

:: deftheorem  defines 1Cat COMMACAT:def_6_:_
 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;
funcc comma C ->  strict Category equals :: COMMACAT:def 7
(incl (1Cat c)) comma (id C);
coherence
 (incl (1Cat c)) comma (id C) is strict Category ;
funcC comma c ->  strict Category equals :: COMMACAT:def 8
(id C) comma (incl (1Cat c));
coherence
 (id C) comma (incl (1Cat c)) is strict Category ;
end;

:: deftheorem  defines comma COMMACAT:def_7_:_
 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_8_:_
 for C being Category
for c being Object of C holds C comma c = (id C) comma (incl (1Cat c));