:: COMMACAT semantic presentation

deffunc H₁( CatStr ) -> set = the Objects of a₁;

deffunc H₂( CatStr ) -> set = the Morphisms of a₁;

definition

canceled;
canceled;
canceled;
canceled;

end;

:: deftheorem Def1 COMMACAT:def 1 :

:: deftheorem Def2 COMMACAT:def 2 :

:: deftheorem Def3 COMMACAT:def 3 :

:: deftheorem Def4 COMMACAT:def 4 :

theorem Th1: :: COMMACAT:1

canceled;

Lemma1: for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( [[b₁,b₂],b₃] `11 = b₁ & [[b₁,b₂],b₃] `12 = b₂ & [b₄,[b₅,b₆]] `21 = b₅ & [b₄,[b₅,b₆]] `22 = b₆ )
by MCART_1:89;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₃;
let c₅ be Functor of c₂,c₃;
given c₆ being Object of c₁, c₇ being Object of c₂, c₈ being Morphism of c₃ such that E2: c₈ in Hom (c₄ . c₆),(c₅ . c₇) ;
func commaObjs c₄,c₅ -> non empty Subset of [:[:the Objects of a₁,the Objects of a₂:],the Morphisms of a₃:] equals :Def5: :: COMMACAT:def 5
{ [[b₁,b₂],b₃] where B is Object of a₁, B is Object of a₂, B is Morphism of a₃ : b₃ in Hom (a₄ . b₁),(a₅ . b₂) } ;
coherence

proof end;

end;

:: deftheorem Def5 defines commaObjs COMMACAT:def 5 :

theorem Th2: :: COMMACAT:2

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₃
for b₅ being Functor of b₂,b₃
for b₆ being Element of commaObjs b₄,b₅ st ex b₇ being Object of b₁ex b₈ being Object of b₂ex b₉ being Morphism of b₃ st b₉ in Hom (b₄ . b₇),(b₅ . b₈) holds
( b₆ = [[(b₆ `11 ),(b₆ `12 )],(b₆ `2 )] & b₆ `2 in Hom (b₄ . (b₆ `11 )),(b₅ . (b₆ `12 )) & dom (b₆ `2 ) = b₄ . (b₆ `11 ) & cod (b₆ `2 ) = b₅ . (b₆ `12 ) )

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₃;
let c₅ be Functor of c₂,c₃;
given c₆ being Object of c₁, c₇ being Object of c₂, c₈ being Morphism of c₃ such that E4: c₈ in Hom (c₄ . c₆),(c₅ . c₇) ;
func commaMorphs c₄,c₅ -> non empty Subset of [:[:(commaObjs a₄,a₅),(commaObjs a₄,a₅):],[:the Morphisms of a₁,the Morphisms of a₂:]:] equals :Def6: :: COMMACAT:def 6
{ [[b₃,b₄],[b₁,b₂]] where B is Morphism of a₁, B is Morphism of a₂, B is Element of commaObjs a₄,a₅, B is Element of commaObjs a₄,a₅ : ( dom b₁ = b₃ `11 & cod b₁ = b₄ `11 & dom b₂ = b₃ `12 & cod b₂ = b₄ `12 & (b₄ `2 ) * (a₄ . b₁) = (a₅ . b₂) * (b₃ `2 ) ) } ;
coherence

proof end;

end;

:: deftheorem Def6 defines commaMorphs COMMACAT:def 6 :

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₃;
let c₅ be Functor of c₂,c₃;
let c₆ be Element of commaMorphs c₄,c₅;
redefine func `11 as c₆ `11 -> Element of commaObjs a₄,a₅;
coherence

proof end;

redefine func `12 as c₆ `12 -> Element of commaObjs a₄,a₅;
coherence

proof end;

end;

theorem Th3: :: COMMACAT:3

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₃
for b₅ being Functor of b₂,b₃
for b₆ being Element of commaMorphs b₄,b₅ st ex b₇ being Object of b₁ex b₈ being Object of b₂ex b₉ being Morphism of b₃ st b₉ in Hom (b₄ . b₇),(b₅ . b₈) holds
( b₆ = [[(b₆ `11 ),(b₆ `12 )],[(b₆ `21 ),(b₆ `22 )]] & dom (b₆ `21 ) = (b₆ `11 ) `11 & cod (b₆ `21 ) = (b₆ `12 ) `11 & dom (b₆ `22 ) = (b₆ `11 ) `12 & cod (b₆ `22 ) = (b₆ `12 ) `12 & ((b₆ `12 ) `2 ) * (b₄ . (b₆ `21 )) = (b₅ . (b₆ `22 )) * ((b₆ `11 ) `2 ) )

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₃;
let c₅ be Functor of c₂,c₃;
let c₆, c₇ be Element of commaMorphs c₄,c₅;
given c₈ being Object of c₁, c₉ being Object of c₂, c₁₀ being Morphism of c₃ such that E6: c₁₀ in Hom (c₄ . c₈),(c₅ . c₉) ;
assume E7: c₆ `12 = c₇ `11 ;
func c₇ * c₆ -> Element of commaMorphs a₄,a₅ equals :Def7: :: COMMACAT:def 7
[[(a₆ `11 ),(a₇ `12 )],[((a₇ `21 ) * (a₆ `21 )),((a₇ `22 ) * (a₆ `22 ))]];
coherence

proof end;

end;

:: deftheorem Def7 defines * COMMACAT:def 7 :

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₃;
let c₅ be Functor of c₂,c₃;
func commaComp c₄,c₅ -> PartFunc of [:(commaMorphs a₄,a₅),(commaMorphs a₄,a₅):], commaMorphs a₄,a₅ means :Def8: :: COMMACAT:def 8
( dom a₆ = { [b₁,b₂] where B is Element of commaMorphs a₄,a₅, B is Element of commaMorphs a₄,a₅ : b₁ `11 = b₂ `12 } & ( for b₁, b₂ being Element of commaMorphs a₄,a₅ st [b₁,b₂] in dom a₆ holds
a₆ . [b₁,b₂] = b₁ * b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines commaComp COMMACAT:def 8 :

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₃;
let c₅ be Functor of c₂,c₃;
given c₆ being Object of c₁, c₇ being Object of c₂, c₈ being Morphism of c₃ such that E8: c₈ in Hom (c₄ . c₆),(c₅ . c₇) ;
func c₄ comma c₅ -> strict Category means :: COMMACAT:def 9
( the Objects of a₆ = commaObjs a₄,a₅ & the Morphisms of a₆ = commaMorphs a₄,a₅ & ( for b₁ being Element of commaMorphs a₄,a₅ holds the Dom of a₆ . b₁ = b₁ `11 ) & ( for b₁ being Element of commaMorphs a₄,a₅ holds the Cod of a₆ . b₁ = b₁ `12 ) & ( for b₁ being Element of commaObjs a₄,a₅ holds the Id of a₆ . b₁ = [[b₁,b₁],[(id (b₁ `11 )),(id (b₁ `12 ))]] ) & the Comp of a₆ = commaComp a₄,a₅ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines comma COMMACAT:def 9 :

theorem Th4: :: COMMACAT:4

for b₁, b₂ being set holds
( the Objects of (1Cat b₂,b₁) = {b₂} & the Morphisms of (1Cat b₂,b₁) = {b₁} )

proof end;

theorem Th5: :: COMMACAT:5

for b₁, b₂ being set
for b₃, b₄ being Object of (1Cat b₂,b₁) holds Hom b₃,b₄ = {b₁}

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
func 1Cat c₂ -> strict Subcategory of a₁ equals :: COMMACAT:def 10
1Cat a₂,(id a₂);
coherence

proof end;

end;

:: deftheorem Def10 defines 1Cat COMMACAT:def 10 :

definition

let c₁ be Category;
let c₂ be Object of c₁;
func c₂ comma c₁ -> strict Category equals :: COMMACAT:def 11
(incl (1Cat a₂)) comma (id a₁);
coherence ;
func c₁ comma c₂ -> strict Category equals :: COMMACAT:def 12
(id a₁) comma (incl (1Cat a₂));
coherence ;

end;

:: deftheorem Def11 defines comma COMMACAT:def 11 :

:: deftheorem Def12 defines comma COMMACAT:def 12 :