:: by Grzegorz Bancerek and Agata Darmochwa\l

::

:: Received February 20, 1992

:: Copyright (c) 1992-2017 Association of Mizar Users

deffunc H

deffunc H

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

{ [[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:]

end;
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)) } ;

{ [[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:]

proof 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)) } ;

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) )

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

{ [[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:]:]

end;
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) ) } ;

{ [[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:]:]

proof 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) ) } ;

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)

redefine func k `12 -> Element of commaObjs (F,G);

coherence

k `12 is Element of commaObjs (F,G)

end;
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: `12redefine func k `12 -> Element of commaObjs (F,G);

coherence

k `12 is Element of commaObjs (F,G)

proof 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) )

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 ;

[[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] is Element of commaMorphs (F,G)

end;
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 :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))]];

[[(k1 `11),(k2 `12)],[((k2 `21) (*) (k1 `21)),((k2 `22) (*) (k1 `22))]] is Element of commaMorphs (F,G)

proof 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))]];

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;

ex b_{1} being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) st

( dom b_{1} = { [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 b_{1} holds

b_{1} . [k,k9] = k * k9 ) )

for b_{1}, b_{2} being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) st dom b_{1} = { [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 b_{1} holds

b_{1} . [k,k9] = k * k9 ) & dom b_{2} = { [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 b_{2} holds

b_{2} . [k,k9] = k * k9 ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{6} being PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) holds

( b_{6} = commaComp (F,G) iff ( dom b_{6} = { [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 b_{6} holds

b_{6} . [k,k9] = k * k9 ) ) );

for C, D, E being Category

for F being Functor of C,E

for G being Functor of D,E

for b

( b

b

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

ex b_{1} being strict Category st

( the carrier of b_{1} = commaObjs (F,G) & the carrier' of b_{1} = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b_{1} . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b_{1} . k = k `12 ) & the Comp of b_{1} = commaComp (F,G) )

for b_{1}, b_{2} being strict Category st the carrier of b_{1} = commaObjs (F,G) & the carrier' of b_{1} = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b_{1} . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b_{1} . k = k `12 ) & the Comp of b_{1} = commaComp (F,G) & the carrier of b_{2} = commaObjs (F,G) & the carrier' of b_{2} = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b_{2} . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b_{2} . k = k `12 ) & the Comp of b_{2} = commaComp (F,G) holds

b_{1} = b_{2}

end;
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 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 ( 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) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof 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 b_{6} being strict Category holds

( b_{6} = F comma G iff ( the carrier of b_{6} = commaObjs (F,G) & the carrier' of b_{6} = commaMorphs (F,G) & ( for k being Element of commaMorphs (F,G) holds the Source of b_{6} . k = k `11 ) & ( for k being Element of commaMorphs (F,G) holds the Target of b_{6} . k = k `12 ) & the Comp of b_{6} = commaComp (F,G) ) );

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 b

( b

theorem :: COMMACAT:3

definition

let C be Category;

let c be Object of C;

coherence

1Cat (c,(id c)) is strict Subcategory of C

end;
let c be Object of C;

coherence

1Cat (c,(id c)) is strict Subcategory of C

proof end;

:: deftheorem defines 1Cat COMMACAT:def 6 :

for C being Category

for c being Object of C holds 1Cat c = 1Cat (c,(id c));

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;

coherence

(incl (1Cat c)) comma (id C) is strict Category ;

coherence

(id C) comma (incl (1Cat c)) is strict Category ;

end;
let c be Object of C;

coherence

(incl (1Cat c)) comma (id C) is strict Category ;

coherence

(id C) comma (incl (1Cat c)) is strict Category ;

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

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

for C being Category

for c being Object of C holds C comma c = (id C) comma (incl (1Cat c));