:: CAT_5 semantic presentation

definition

let D1, D2, D be non empty set ;
let x be Element of [:[:D1,D2:],D:];
:: original: `11
redefine func x `11 -> Element of D1;
coherence

proof end;

:: original: `12
redefine func x `12 -> Element of D2;
coherence

proof end;

end;

definition

let D1, D2 be non empty set ;
let x be Element of [:D1,D2:];
:: original: `2
redefine func x `2 -> Element of D2;
coherence

proof end;

end;

theorem Th1: :: CAT_5:1

for C, D being CatStr st CatStr(# the Objects of C,the Morphisms of C,the Dom of C,the Cod of C,the Comp of C,the Id of C #) = CatStr(# the Objects of D,the Morphisms of D,the Dom of D,the Cod of D,the Comp of D,the Id of D #) & C is Category-like holds
D is Category-like

proof end;

definition

let IT be CatStr ;
attr IT 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 :

registration

cluster strict with_triple-like_morphisms CatStr ;
existence

proof end;

end;

theorem Th2: :: CAT_5:2

for C being 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 end;

definition

let C be with_triple-like_morphisms CatStr ;
let f be Morphism of C;
:: original: `11
redefine func f `11 -> Object of C;
coherence

proof end;

:: original: `12
redefine func f `12 -> Object of C;
coherence

proof end;

end;

scheme :: CAT_5:sch 1
CatEx{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set , set ], F₃( set , set ) -> set } :

ex C being strict with_triple-like_morphisms Category st
( the Objects of C = F₁() & ( for a, b being Element of F₁()
for f being Element of F₂() st P₁[a,b,f] holds
[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F₁() ex f being Element of F₂() st
( m = [[a,b],f] & P₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of F₁()
for f1, f2 being Element of F₂() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],F₃(f2,f1)] ) )

provided

A1: for a, b, c being Element of F₁()
for f, g being Element of F₂() st P₁[a,b,f] & P₁[b,c,g] holds
( F₃(g,f) in F₂() & P₁[a,c,F₃(g,f)] ) and
A2: for a being Element of F₁() ex f being Element of F₂() st
( P₁[a,a,f] & ( for b being Element of F₁()
for g being Element of F₂() holds
( ( P₁[a,b,g] implies F₃(g,f) = g ) & ( P₁[b,a,g] implies F₃(f,g) = g ) ) ) ) and
A3: for a, b, c, d being Element of F₁()
for f, g, h being Element of F₂() st P₁[a,b,f] & P₁[b,c,g] & P₁[c,d,h] holds
F₃(h,F₃(g,f)) = F₃(F₃(h,g),f)

proof end;

scheme :: CAT_5:sch 2
CatUniq{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set , set ], F₃( set , set ) -> set } :

for C1, C2 being strict with_triple-like_morphisms Category st the Objects of C1 = F₁() & ( for a, b being Element of F₁()
for f being Element of F₂() st P₁[a,b,f] holds
[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F₁() ex f being Element of F₂() st
( m = [[a,b],f] & P₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C1
for a1, a2, a3 being Element of F₁()
for f1, f2 being Element of F₂() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],F₃(f2,f1)] ) & the Objects of C2 = F₁() & ( for a, b being Element of F₁()
for f being Element of F₂() st P₁[a,b,f] holds
[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F₁() ex f being Element of F₂() st
( m = [[a,b],f] & P₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C2
for a1, a2, a3 being Element of F₁()
for f1, f2 being Element of F₂() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],F₃(f2,f1)] ) holds
C1 = C2

provided

A1: for a being Element of F₁() ex f being Element of F₂() st
( P₁[a,a,f] & ( for b being Element of F₁()
for g being Element of F₂() holds
( ( P₁[a,b,g] implies F₃(g,f) = g ) & ( P₁[b,a,g] implies F₃(f,g) = g ) ) ) )

proof end;

scheme :: CAT_5:sch 3
FunctorEx{ F₁() -> Category, F₂() -> Category, F₃( set ) -> Object of F₂(), F₄( set ) -> set } :

ex F being Functor of F₁(),F₂() st
for f being Morphism of F₁() holds F . f = F₄(f)

provided

A1: for f being Morphism of F₁() holds
( F₄(f) is Morphism of F₂() & ( for g being Morphism of F₂() st g = F₄(f) holds
( dom g = F₃((dom f)) & cod g = F₃((cod f)) ) ) ) and
A2: for a being Object of F₁() holds F₄((id a)) = id F₃(a) and
A3: for f1, f2 being Morphism of F₁()
for g1, g2 being Morphism of F₂() st g1 = F₄(f1) & g2 = F₄(f2) & dom f2 = cod f1 holds
F₄((f2 * f1)) = g2 * g1

proof 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 Objects of C1,the Morphisms of C1,the Dom of C1,the Cod of C1,the Comp of C1,the Id of C1 #) = CatStr(# the Objects of C2,the Morphisms of C2,the Dom of C2,the Cod of C2,the Comp of C2,the Id of C2 #)

proof 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 end;

definition

let C1, C2 be Category;
given C being Category such that A1: ( C1 is Subcategory of C & C2 is Subcategory of C ) ;
given o1 being Object of C1 such that A2: o1 is Object of C2 ;
func C1 /\ C2 -> strict Category means :Def2: :: CAT_5:def 2
( the Objects of it = the Objects of C1 /\ the Objects of C2 & the Morphisms of it = the Morphisms of C1 /\ the Morphisms of C2 & the Dom of it = the Dom of C1 | the Morphisms of C2 & the Cod of it = the Cod of C1 | the Morphisms of C2 & the Comp of it = the Comp of C1 || the Morphisms of C2 & the Id of it = the Id of C1 | the Objects of C2 );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines /\ CAT_5:def 2 :

theorem Th5: :: CAT_5:5

for C being Category
for C1, C2 being Subcategory of C st the Objects of C1 meets the Objects of C2 holds
C1 /\ C2 = C2 /\ C1

proof end;

theorem Th6: :: CAT_5:6

for C being Category
for C1, C2 being Subcategory of C st the Objects of C1 meets the Objects of C2 holds
( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 )

proof 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 Objects of it = rng (Obj F) & rng F c= the Morphisms of it & ( for E being Subcategory of D st the Objects of E = rng (Obj F) & rng F c= the Morphisms of E holds
it is Subcategory of E ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Image CAT_5:def 3 :

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 Morphisms of E holds
F is Functor of C,E

proof 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 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 end;

definition

let IT be set ;
attr IT 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 :

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

proof end;

end;

:: deftheorem Def5 defines categorial CAT_5:def 5 :

registration

cluster non empty categorial set ;
existence

proof end;

end;

definition

let X be non empty categorial set ;
:: original: Element
redefine mode Element of X -> Category;
coherence by Def4;

end;

definition

let C be Category;
attr C is Categorial means :Def6: :: CAT_5:def 6
( the Objects 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 :

registration

cluster Categorial -> with_triple-like_morphisms CatStr ;
coherence

proof end;

end;

theorem Th10: :: CAT_5:10

for C, D being Category st CatStr(# the Objects of C,the Morphisms of C,the Dom of C,the Cod of C,the Comp of C,the Id of C #) = CatStr(# the Objects of D,the Morphisms of D,the Dom of D,the Cod of D,the Comp of D,the Id of D #) & C is Categorial holds
D is Categorial

proof end;

theorem Th11: :: CAT_5:11

for C being Category holds 1Cat C,[[C,C],(id C)] is Categorial

proof end;

registration

cluster strict with_triple-like_morphisms Categorial CatStr ;
existence

proof end;

end;

theorem Th12: :: CAT_5:12

for C being Categorial Category
for a being Object of C holds a is Category

proof 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 end;

definition

let C be Categorial Category;
let m be Morphism of C;
:: original: `11
redefine func m `11 -> Category;
coherence

proof end;

:: original: `12
redefine func m `12 -> Category;
coherence

proof end;

end;

theorem Th14: :: CAT_5:14

for C1, C2 being Categorial Category st the Objects of C1 = the Objects of C2 & the Morphisms of C1 = the Morphisms of C2 holds
CatStr(# the Objects of C1,the Morphisms of C1,the Dom of C1,the Cod of C1,the Comp of C1,the Id of C1 #) = CatStr(# the Objects of C2,the Morphisms of C2,the Dom of C2,the Cod of C2,the Comp of C2,the Id of C2 #)

proof end;

registration

let C be Categorial Category;
cluster -> Categorial Subcategory of C;
coherence

proof end;

end;

theorem Th15: :: CAT_5:15

for C, D being Categorial Category st the Morphisms of C c= the Morphisms of D holds
C is Subcategory of D

proof end;

definition

let a be set ;
assume A1: a is Category ;
func cat a -> Category equals :Def7: :: CAT_5:def 7
a;
correctness by A1;

end;

:: deftheorem Def7 defines cat CAT_5:def 7 :

theorem Th16: :: CAT_5:16

for C being Categorial Category
for c being Object of C holds cat c = c

proof end;

definition

let C be Categorial Category;
let m be Morphism of C;
:: original: `2
redefine func m `2 -> Functor of cat (dom m), cat (cod m);
coherence

proof 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 Objects 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 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 Objects 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 Objects 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 end;

definition

let IT be Categorial Category;
attr IT 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 :

registration

cluster strict with_triple-like_morphisms Categorial full CatStr ;
existence

proof end;

end;

theorem :: CAT_5:19

for C1, C2 being Categorial full Category st the Objects of C1 = the Objects of C2 holds
CatStr(# the Objects of C1,the Morphisms of C1,the Dom of C1,the Cod of C1,the Comp of C1,the Id of C1 #) = CatStr(# the Objects of C2,the Morphisms of C2,the Dom of C2,the Cod of C2,the Comp of C2,the Id of C2 #)

proof end;

theorem Th20: :: CAT_5:20

for A being non empty categorial set ex C being strict Categorial full Category st the Objects of C = A

proof end;

theorem Th21: :: CAT_5:21

for C being Categorial Category
for D being Categorial full Category st the Objects of C c= the Objects of D holds
C is Subcategory of D

proof 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 end;

definition

let C be Category;
let o be Object of C;
func Hom o -> Subset of the Morphisms of C equals :: CAT_5:def 9
the Cod of C " {o};
coherence ;
func o Hom -> Subset of the Morphisms of C equals :: CAT_5:def 10
the Dom of C " {o};
coherence ;

end;

:: deftheorem defines Hom CAT_5:def 9 :

:: deftheorem defines Hom CAT_5:def 10 :

registration

let C be Category;
let o be Object of C;
cluster Hom o -> non empty ;
coherence

proof end;

cluster o Hom -> non empty ;
coherence

proof 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 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 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 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 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 end;

definition

let C be Category;
let o be Object of C;
set A = Hom o;
set B = the Morphisms of C;
defpred S₁[ Element of Hom o, Element of Hom o, Element of the Morphisms of C] means ( dom $2 = cod $3 & $1 = $2 * $3 );
deffunc H₁( Morphism of C, Morphism of C) -> Element of the Morphisms of C = $1 * $2;
A1: for a, b, c being Element of Hom o
for f, g being Element of the Morphisms of C st S₁[a,b,f] & S₁[b,c,g] holds
( H₁(g,f) in the Morphisms of C & S₁[a,c,H₁(g,f)] )

proof end;

A3: for a being Element of Hom o ex f being Element of the Morphisms of C st
( S₁[a,a,f] & ( for b being Element of Hom o
for g being Element of the Morphisms of C holds
( ( S₁[a,b,g] implies H₁(g,f) = g ) & ( S₁[b,a,g] implies H₁(f,g) = g ) ) ) )

proof end;

A4: for a, b, c, d being Element of Hom o
for f, g, h being Element of the Morphisms of C st S₁[a,b,f] & S₁[b,c,g] & S₁[c,d,h] holds
H₁(h,H₁(g,f)) = H₁(H₁(h,g),f)

proof end;

func C -SliceCat o -> strict with_triple-like_morphisms Category means :Def11: :: CAT_5:def 11
( the Objects 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

proof end;

uniqueness

proof end;

set X = o Hom ;
defpred S₂[ Element of o Hom , Element of o Hom , Element of the Morphisms of C] means ( dom $3 = cod $1 & $2 = $3 * $1 );
A5: for a, b, c being Element of o Hom
for f, g being Element of the Morphisms of C st S₂[a,b,f] & S₂[b,c,g] holds
( H₁(g,f) in the Morphisms of C & S₂[a,c,H₁(g,f)] )

proof end;

A7: for a being Element of o Hom ex f being Element of the Morphisms of C st
( S₂[a,a,f] & ( for b being Element of o Hom
for g being Element of the Morphisms of C holds
( ( S₂[a,b,g] implies H₁(g,f) = g ) & ( S₂[b,a,g] implies H₁(f,g) = g ) ) ) )

proof end;

A8: for a, b, c, d being Element of o Hom
for f, g, h being Element of the Morphisms of C st S₂[a,b,f] & S₂[b,c,g] & S₂[c,d,h] holds
H₁(h,H₁(g,f)) = H₁(H₁(h,g),f)

proof end;

func o -SliceCat C -> strict with_triple-like_morphisms Category means :Def12: :: CAT_5:def 12
( the Objects 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines -SliceCat CAT_5:def 11 :

:: deftheorem Def12 defines -SliceCat CAT_5:def 12 :

definition

let C be Category;
let o be Object of C;
let m be Morphism of (C -SliceCat o);
:: original: `2
redefine func m `2 -> Morphism of C;
coherence

proof end;

:: original: `11
redefine func m `11 -> Element of Hom o;
coherence

proof end;

:: original: `12
redefine func m `12 -> Element of Hom o;
coherence

proof 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 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 end;

definition

let C be Category;
let o be Object of C;
let m be Morphism of (o -SliceCat C);
:: original: `2
redefine func m `2 -> Morphism of C;
coherence

proof end;

:: original: `11
redefine func m `11 -> Element of o Hom ;
coherence

proof end;

:: original: `12
redefine func m `12 -> Element of o Hom ;
coherence

proof 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 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 end;

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

proof end;

uniqueness

proof 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines SliceFunctor CAT_5:def 13 :

:: deftheorem Def14 defines SliceContraFunctor CAT_5:def 14 :

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