begin
theorem Th1:
for
C,
D being
CatStr st
CatStr(# the
carrier of
C,the
carrier' of
C,the
Source of
C,the
Target of
C,the
Comp of
C,the
Id of
C #)
= CatStr(# the
carrier of
D,the
carrier' of
D,the
Source of
D,the
Target of
D,the
Comp of
D,the
Id of
D #) &
C is
Category-like holds
D is
Category-like
:: deftheorem Def1 defines with_triple-like_morphisms CAT_5:def 1 :
theorem Th2:
scheme
CatEx{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
P1[
set ,
set ,
set ],
F3(
set ,
set )
-> set } :
ex
C being
strict with_triple-like_morphisms Category st
( the
carrier of
C = F1() & ( for
a,
b being
Element of
F1()
for
f being
Element of
F2() st
P1[
a,
b,
f] holds
[[a,b],f] is
Morphism of ) & ( for
m being
Morphism of ex
a,
b being
Element of
F1() ex
f being
Element of
F2() st
(
m = [[a,b],f] &
P1[
a,
b,
f] ) ) & ( for
m1,
m2 being
Morphism of
for
a1,
a2,
a3 being
Element of
F1()
for
f1,
f2 being
Element of
F2() st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],F3(f2,f1)] ) )
provided
A1:
for
a,
b,
c being
Element of
F1()
for
f,
g being
Element of
F2() st
P1[
a,
b,
f] &
P1[
b,
c,
g] holds
(
F3(
g,
f)
in F2() &
P1[
a,
c,
F3(
g,
f)] )
and A2:
for
a being
Element of
F1() ex
f being
Element of
F2() st
(
P1[
a,
a,
f] & ( for
b being
Element of
F1()
for
g being
Element of
F2() holds
( (
P1[
a,
b,
g] implies
F3(
g,
f)
= g ) & (
P1[
b,
a,
g] implies
F3(
f,
g)
= g ) ) ) )
and A3:
for
a,
b,
c,
d being
Element of
F1()
for
f,
g,
h being
Element of
F2() st
P1[
a,
b,
f] &
P1[
b,
c,
g] &
P1[
c,
d,
h] holds
F3(
h,
F3(
g,
f))
= F3(
F3(
h,
g),
f)
scheme
CatUniq{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
P1[
set ,
set ,
set ],
F3(
set ,
set )
-> set } :
for
C1,
C2 being
strict with_triple-like_morphisms Category st the
carrier of
C1 = F1() & ( for
a,
b being
Element of
F1()
for
f being
Element of
F2() st
P1[
a,
b,
f] holds
[[a,b],f] is
Morphism of ) & ( for
m being
Morphism of ex
a,
b being
Element of
F1() ex
f being
Element of
F2() st
(
m = [[a,b],f] &
P1[
a,
b,
f] ) ) & ( for
m1,
m2 being
Morphism of
for
a1,
a2,
a3 being
Element of
F1()
for
f1,
f2 being
Element of
F2() st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],F3(f2,f1)] ) & the
carrier of
C2 = F1() & ( for
a,
b being
Element of
F1()
for
f being
Element of
F2() st
P1[
a,
b,
f] holds
[[a,b],f] is
Morphism of ) & ( for
m being
Morphism of ex
a,
b being
Element of
F1() ex
f being
Element of
F2() st
(
m = [[a,b],f] &
P1[
a,
b,
f] ) ) & ( for
m1,
m2 being
Morphism of
for
a1,
a2,
a3 being
Element of
F1()
for
f1,
f2 being
Element of
F2() st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],F3(f2,f1)] ) holds
C1 = C2
provided
A1:
for
a being
Element of
F1() ex
f being
Element of
F2() st
(
P1[
a,
a,
f] & ( for
b being
Element of
F1()
for
g being
Element of
F2() holds
( (
P1[
a,
b,
g] implies
F3(
g,
f)
= g ) & (
P1[
b,
a,
g] implies
F3(
f,
g)
= g ) ) ) )
theorem Th3:
for
C1 being
Category for
C2 being
Subcategory of
C1 st
C1 is
Subcategory of
C2 holds
CatStr(# the
carrier of
C1,the
carrier' of
C1,the
Source of
C1,the
Target of
C1,the
Comp of
C1,the
Id of
C1 #)
= CatStr(# the
carrier of
C2,the
carrier' of
C2,the
Source of
C2,the
Target of
C2,the
Comp of
C2,the
Id of
C2 #)
theorem Th4:
:: deftheorem Def2 defines /\ CAT_5:def 2 :
theorem Th5:
theorem Th6:
:: deftheorem Def3 defines Image CAT_5:def 3 :
theorem Th7:
theorem
theorem Th9:
begin
:: deftheorem Def4 defines categorial CAT_5:def 4 :
:: deftheorem Def5 defines categorial CAT_5:def 5 :
definition
let C be
Category;
attr C is
Categorial means :
Def6:
( the
carrier of
C is
categorial & ( for
a being
Object of
for
A being
Category st
a = A holds
id a = [[A,A],(id A)] ) & ( for
m being
Morphism of
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
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 :
for
C being
Category holds
(
C is
Categorial iff ( the
carrier of
C is
categorial & ( for
a being
Object of
for
A being
Category st
a = A holds
id a = [[A,A],(id A)] ) & ( for
m being
Morphism of
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
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)] ) ) );
theorem Th10:
for
C,
D being
Category st
CatStr(# the
carrier of
C,the
carrier' of
C,the
Source of
C,the
Target of
C,the
Comp of
C,the
Id of
C #)
= CatStr(# the
carrier of
D,the
carrier' of
D,the
Source of
D,the
Target of
D,the
Comp of
D,the
Id of
D #) &
C is
Categorial holds
D is
Categorial
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
for
C1,
C2 being
Categorial Category st the
carrier of
C1 = the
carrier of
C2 & the
carrier' of
C1 = the
carrier' of
C2 holds
CatStr(# the
carrier of
C1,the
carrier' of
C1,the
Source of
C1,the
Target of
C1,the
Comp of
C1,the
Id of
C1 #)
= CatStr(# the
carrier of
C2,the
carrier' of
C2,the
Source of
C2,the
Target of
C2,the
Comp of
C2,the
Id of
C2 #)
theorem Th15:
:: deftheorem Def7 defines cat CAT_5:def 7 :
theorem Th16:
theorem Th17:
theorem Th18:
:: deftheorem Def8 defines full CAT_5:def 8 :
theorem
for
C1,
C2 being
Categorial full Category st the
carrier of
C1 = the
carrier of
C2 holds
CatStr(# the
carrier of
C1,the
carrier' of
C1,the
Source of
C1,the
Target of
C1,the
Comp of
C1,the
Id of
C1 #)
= CatStr(# the
carrier of
C2,the
carrier' of
C2,the
Source of
C2,the
Target of
C2,the
Comp of
C2,the
Id of
C2 #)
theorem Th20:
theorem Th21:
theorem
begin
:: deftheorem defines Hom CAT_5:def 9 :
:: deftheorem defines Hom CAT_5:def 10 :
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem Th28:
definition
let C be
Category;
let o be
Object of ;
set A =
Hom o;
set B = the
carrier' of
C;
defpred S1[
Element of
Hom o,
Element of
Hom o,
Element of the
carrier' of
C]
means (
dom $2
= cod $3 & $1
= $2
* $3 );
deffunc H1(
Morphism of ,
Morphism of )
-> Element of the
carrier' of
C = $1
* $2;
A1:
for
a,
b,
c being
Element of
Hom o for
f,
g being
Element of the
carrier' of
C st
S1[
a,
b,
f] &
S1[
b,
c,
g] holds
(
H1(
g,
f)
in the
carrier' of
C &
S1[
a,
c,
H1(
g,
f)] )
A6:
for
a being
Element of
Hom o ex
f being
Element of the
carrier' of
C st
(
S1[
a,
a,
f] & ( for
b being
Element of
Hom o for
g being
Element of the
carrier' of
C holds
( (
S1[
a,
b,
g] implies
H1(
g,
f)
= g ) & (
S1[
b,
a,
g] implies
H1(
f,
g)
= g ) ) ) )
A9:
for
a,
b,
c,
d being
Element of
Hom o for
f,
g,
h being
Element of the
carrier' of
C st
S1[
a,
b,
f] &
S1[
b,
c,
g] &
S1[
c,
d,
h] holds
H1(
h,
H1(
g,
f))
= H1(
H1(
h,
g),
f)
func C -SliceCat o -> strict with_triple-like_morphisms Category means :
Def11:
( the
carrier of
it = Hom o & ( for
a,
b being
Element of
Hom o for
f being
Morphism of st
dom b = cod f &
a = b * f holds
[[a,b],f] is
Morphism of ) & ( for
m being
Morphism of ex
a,
b being
Element of
Hom o ex
f being
Morphism of st
(
m = [[a,b],f] &
dom b = cod f &
a = b * f ) ) & ( for
m1,
m2 being
Morphism of
for
a1,
a2,
a3 being
Element of
Hom o for
f1,
f2 being
Morphism of st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) );
existence
ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = Hom o & ( for a, b being Element of Hom o
for f being Morphism of st dom b = cod f & a = b * f holds
[[a,b],f] is Morphism of ) & ( for m being Morphism of ex a, b being Element of Hom o ex f being Morphism of st
( m = [[a,b],f] & dom b = cod f & a = b * f ) ) & ( for m1, m2 being Morphism of
for a1, a2, a3 being Element of Hom o
for f1, f2 being Morphism of st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) )
uniqueness
for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = Hom o & ( for a, b being Element of Hom o
for f being Morphism of st dom b = cod f & a = b * f holds
[[a,b],f] is Morphism of ) & ( for m being Morphism of ex a, b being Element of Hom o ex f being Morphism of st
( m = [[a,b],f] & dom b = cod f & a = b * f ) ) & ( for m1, m2 being Morphism of
for a1, a2, a3 being Element of Hom o
for f1, f2 being Morphism of st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) & the carrier of b2 = Hom o & ( for a, b being Element of Hom o
for f being Morphism of st dom b = cod f & a = b * f holds
[[a,b],f] is Morphism of ) & ( for m being Morphism of ex a, b being Element of Hom o ex f being Morphism of st
( m = [[a,b],f] & dom b = cod f & a = b * f ) ) & ( for m1, m2 being Morphism of
for a1, a2, a3 being Element of Hom o
for f1, f2 being Morphism of st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) holds
b1 = b2
set X =
o Hom ;
defpred S2[
Element of
o Hom ,
Element of
o Hom ,
Element of the
carrier' of
C]
means (
dom $3
= cod $1 & $2
= $3
* $1 );
A16:
for
a,
b,
c being
Element of
o Hom for
f,
g being
Element of the
carrier' of
C st
S2[
a,
b,
f] &
S2[
b,
c,
g] holds
(
H1(
g,
f)
in the
carrier' of
C &
S2[
a,
c,
H1(
g,
f)] )
A21:
for
a being
Element of
o Hom ex
f being
Element of the
carrier' of
C st
(
S2[
a,
a,
f] & ( for
b being
Element of
o Hom for
g being
Element of the
carrier' of
C holds
( (
S2[
a,
b,
g] implies
H1(
g,
f)
= g ) & (
S2[
b,
a,
g] implies
H1(
f,
g)
= g ) ) ) )
A24:
for
a,
b,
c,
d being
Element of
o Hom for
f,
g,
h being
Element of the
carrier' of
C st
S2[
a,
b,
f] &
S2[
b,
c,
g] &
S2[
c,
d,
h] holds
H1(
h,
H1(
g,
f))
= H1(
H1(
h,
g),
f)
func o -SliceCat C -> strict with_triple-like_morphisms Category means :
Def12:
( the
carrier of
it = o Hom & ( for
a,
b being
Element of
o Hom for
f being
Morphism of st
dom f = cod a &
f * a = b holds
[[a,b],f] is
Morphism of ) & ( for
m being
Morphism of ex
a,
b being
Element of
o Hom ex
f being
Morphism of st
(
m = [[a,b],f] &
dom f = cod a &
f * a = b ) ) & ( for
m1,
m2 being
Morphism of
for
a1,
a2,
a3 being
Element of
o Hom for
f1,
f2 being
Morphism of st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) );
existence
ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = o Hom & ( for a, b being Element of o Hom
for f being Morphism of st dom f = cod a & f * a = b holds
[[a,b],f] is Morphism of ) & ( for m being Morphism of ex a, b being Element of o Hom ex f being Morphism of st
( m = [[a,b],f] & dom f = cod a & f * a = b ) ) & ( for m1, m2 being Morphism of
for a1, a2, a3 being Element of o Hom
for f1, f2 being Morphism of st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) )
uniqueness
for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = o Hom & ( for a, b being Element of o Hom
for f being Morphism of st dom f = cod a & f * a = b holds
[[a,b],f] is Morphism of ) & ( for m being Morphism of ex a, b being Element of o Hom ex f being Morphism of st
( m = [[a,b],f] & dom f = cod a & f * a = b ) ) & ( for m1, m2 being Morphism of
for a1, a2, a3 being Element of o Hom
for f1, f2 being Morphism of st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) & the carrier of b2 = o Hom & ( for a, b being Element of o Hom
for f being Morphism of st dom f = cod a & f * a = b holds
[[a,b],f] is Morphism of ) & ( for m being Morphism of ex a, b being Element of o Hom ex f being Morphism of st
( m = [[a,b],f] & dom f = cod a & f * a = b ) ) & ( for m1, m2 being Morphism of
for a1, a2, a3 being Element of o Hom
for f1, f2 being Morphism of st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) holds
b1 = b2
end;
:: deftheorem Def11 defines -SliceCat CAT_5:def 11 :
for
C being
Category for
o being
Object of
for
b3 being
strict with_triple-like_morphisms Category holds
(
b3 = C -SliceCat o iff ( the
carrier of
b3 = Hom o & ( for
a,
b being
Element of
Hom o for
f being
Morphism of st
dom b = cod f &
a = b * f holds
[[a,b],f] is
Morphism of ) & ( for
m being
Morphism of ex
a,
b being
Element of
Hom o ex
f being
Morphism of st
(
m = [[a,b],f] &
dom b = cod f &
a = b * f ) ) & ( for
m1,
m2 being
Morphism of
for
a1,
a2,
a3 being
Element of
Hom o for
f1,
f2 being
Morphism of st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) ) );
:: deftheorem Def12 defines -SliceCat CAT_5:def 12 :
for
C being
Category for
o being
Object of
for
b3 being
strict with_triple-like_morphisms Category holds
(
b3 = o -SliceCat C iff ( the
carrier of
b3 = o Hom & ( for
a,
b being
Element of
o Hom for
f being
Morphism of st
dom f = cod a &
f * a = b holds
[[a,b],f] is
Morphism of ) & ( for
m being
Morphism of ex
a,
b being
Element of
o Hom ex
f being
Morphism of st
(
m = [[a,b],f] &
dom f = cod a &
f * a = b ) ) & ( for
m1,
m2 being
Morphism of
for
a1,
a2,
a3 being
Element of
o Hom for
f1,
f2 being
Morphism of st
m1 = [[a1,a2],f1] &
m2 = [[a2,a3],f2] holds
m2 * m1 = [[a1,a3],(f2 * f1)] ) ) );
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
begin
definition
let C be
Category;
let f be
Morphism of ;
func SliceFunctor f -> Functor of
C -SliceCat (dom f),
C -SliceCat (cod f) means :
Def13:
for
m being
Morphism of holds
it . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )];
existence
ex b1 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st
for m being Morphism of holds b1 . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )]
uniqueness
for b1, b2 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st ( for m being Morphism of holds b1 . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )] ) & ( for m being Morphism of holds b2 . m = [[(f * (m `11 )),(f * (m `12 ))],(m `2 )] ) holds
b1 = b2
func SliceContraFunctor f -> Functor of
(cod f) -SliceCat C,
(dom f) -SliceCat C means :
Def14:
for
m being
Morphism of holds
it . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )];
existence
ex b1 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st
for m being Morphism of holds b1 . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )]
uniqueness
for b1, b2 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st ( for m being Morphism of holds b1 . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )] ) & ( for m being Morphism of holds b2 . m = [[((m `11 ) * f),((m `12 ) * f)],(m `2 )] ) holds
b1 = b2
end;
:: deftheorem Def13 defines SliceFunctor CAT_5:def 13 :
:: deftheorem Def14 defines SliceContraFunctor CAT_5:def 14 :
theorem
theorem