begin
:: deftheorem Def1 defines -MSF CATALG_1:def 1 :
for I being set
for A, f being Function
for b4 being ManySortedFunction of I holds
( b4 = f -MSF I,A iff for i being set st i in I holds
b4 . i = f | (A . i) );
theorem
theorem
theorem
:: deftheorem CATALG_1:def 2 :
canceled;
:: deftheorem Def3 defines empty CATALG_1:def 3 :
for S being non empty ManySortedSign
for A being MSAlgebra of S holds
( A is empty iff the Sorts of A is empty-yielding );
begin
definition
let A be
set ;
canceled;func CatSign A -> strict ManySortedSign means :
Def5:
( the
carrier of
it = [:{0 },(2 -tuples_on A):] & the
carrier' of
it = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for
a being
set st
a in A holds
( the
Arity of
it . [1,<*a*>] = {} & the
ResultSort of
it . [1,<*a*>] = [0 ,<*a,a*>] ) ) & ( for
a,
b,
c being
set st
a in A &
b in A &
c in A holds
( the
Arity of
it . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the
ResultSort of
it . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ) );
existence
ex b1 being strict ManySortedSign st
( the carrier of b1 = [:{0 },(2 -tuples_on A):] & the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [1,<*a*>] = [0 ,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds
( the Arity of b1 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ) )
correctness
uniqueness
for b1, b2 being strict ManySortedSign st the carrier of b1 = [:{0 },(2 -tuples_on A):] & the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [1,<*a*>] = [0 ,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds
( the Arity of b1 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ) & the carrier of b2 = [:{0 },(2 -tuples_on A):] & the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [1,<*a*>] = [0 ,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds
( the Arity of b2 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ) holds
b1 = b2;
end;
:: deftheorem CATALG_1:def 4 :
canceled;
:: deftheorem Def5 defines CatSign CATALG_1:def 5 :
for A being set
for b2 being strict ManySortedSign holds
( b2 = CatSign A iff ( the carrier of b2 = [:{0 },(2 -tuples_on A):] & the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [1,<*a*>] = [0 ,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds
( the Arity of b2 . [2,<*a,b,c*>] = <*[0 ,<*b,c*>],[0 ,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0 ,<*a,c*>] ) ) ) );
:: deftheorem Def6 defines Categorial CATALG_1:def 6 :
for S being Signature holds
( S is Categorial iff ex A being set st
( CatSign A is Subsignature of S & the carrier of S = [:{0 },(2 -tuples_on A):] ) );
:: deftheorem Def7 defines CatSignature CATALG_1:def 7 :
for A being set
for b2 being Signature holds
( b2 is CatSignature of A iff ( CatSign A is Subsignature of b2 & the carrier of b2 = [:{0 },(2 -tuples_on A):] ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def8 defines underlay CATALG_1:def 8 :
for S being ManySortedSign
for b2 being set holds
( b2 = underlay S iff for x being set holds
( x in b2 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) );
theorem Th15:
:: deftheorem Def9 defines delta-concrete CATALG_1:def 9 :
for S being ManySortedSign holds
( S is delta-concrete iff ex f being Function of NAT ,NAT st
( ( for s being set st s in the carrier of S holds
ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) & ( for o being set st o in the carrier' of S holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) ) );
theorem Th16:
theorem
theorem
theorem
begin
definition
let a be
set ;
func idsym a -> set equals
[1,<*a*>];
correctness
coherence
[1,<*a*>] is set ;
;
let b be
set ;
func homsym a,
b -> set equals
[0 ,<*a,b*>];
correctness
coherence
[0 ,<*a,b*>] is set ;
;
let c be
set ;
func compsym a,
b,
c -> set equals
[2,<*a,b,c*>];
correctness
coherence
[2,<*a,b,c*>] is set ;
;
end;
:: deftheorem defines idsym CATALG_1:def 10 :
for a being set holds idsym a = [1,<*a*>];
:: deftheorem defines homsym CATALG_1:def 11 :
for a, b being set holds homsym a,b = [0 ,<*a,b*>];
:: deftheorem defines compsym CATALG_1:def 12 :
for a, b, c being set holds compsym a,b,c = [2,<*a,b,c*>];
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
for
a1,
b1,
a2,
b2,
a3,
b3 being
set st
compsym a1,
a2,
a3 = compsym b1,
b2,
b3 holds
(
a1 = b1 &
a2 = b2 &
a3 = b3 )
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
for
A being non
empty set for
a,
b,
c being
Element of
A holds
(
the_arity_of (compsym a,b,c) = <*(homsym b,c),(homsym a,b)*> &
the_result_sort_of (compsym a,b,c) = homsym a,
c )
by Def5;
begin
definition
let C1,
C2 be
Category;
let F be
Functor of
C1,
C2;
func Upsilon F -> Function of the
carrier of
(CatSign the carrier of C1),the
carrier of
(CatSign the carrier of C2) means :
Def13:
for
s being
SortSymbol of
(CatSign the carrier of C1) holds
it . s = [0 ,((Obj F) * (s `2 ))];
uniqueness
for b1, b2 being Function of the carrier of (CatSign the carrier of C1),the carrier of (CatSign the carrier of C2) st ( for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0 ,((Obj F) * (s `2 ))] ) & ( for s being SortSymbol of (CatSign the carrier of C1) holds b2 . s = [0 ,((Obj F) * (s `2 ))] ) holds
b1 = b2
existence
ex b1 being Function of the carrier of (CatSign the carrier of C1),the carrier of (CatSign the carrier of C2) st
for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0 ,((Obj F) * (s `2 ))]
func Psi F -> Function of the
carrier' of
(CatSign the carrier of C1),the
carrier' of
(CatSign the carrier of C2) means :
Def14:
for
o being
OperSymbol of
(CatSign the carrier of C1) holds
it . o = [(o `1 ),((Obj F) * (o `2 ))];
uniqueness
for b1, b2 being Function of the carrier' of (CatSign the carrier of C1),the carrier' of (CatSign the carrier of C2) st ( for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1 ),((Obj F) * (o `2 ))] ) & ( for o being OperSymbol of (CatSign the carrier of C1) holds b2 . o = [(o `1 ),((Obj F) * (o `2 ))] ) holds
b1 = b2
existence
ex b1 being Function of the carrier' of (CatSign the carrier of C1),the carrier' of (CatSign the carrier of C2) st
for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1 ),((Obj F) * (o `2 ))]
end;
:: deftheorem Def13 defines Upsilon CATALG_1:def 13 :
for C1, C2 being Category
for F being Functor of C1,C2
for b4 being Function of the carrier of (CatSign the carrier of C1),the carrier of (CatSign the carrier of C2) holds
( b4 = Upsilon F iff for s being SortSymbol of (CatSign the carrier of C1) holds b4 . s = [0 ,((Obj F) * (s `2 ))] );
:: deftheorem Def14 defines Psi CATALG_1:def 14 :
for C1, C2 being Category
for F being Functor of C1,C2
for b4 being Function of the carrier' of (CatSign the carrier of C1),the carrier' of (CatSign the carrier of C2) holds
( b4 = Psi F iff for o being OperSymbol of (CatSign the carrier of C1) holds b4 . o = [(o `1 ),((Obj F) * (o `2 ))] );
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
begin
theorem Th34:
Lm3:
for C being Category
for A being MSAlgebra of CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of A . (homsym a,b) = Hom a,b ) holds
for a, b, c being Object of C holds
( Args (compsym a,b,c),A = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),A = Hom a,c )
scheme
CatAlgEx{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3(
set ,
set )
-> set ,
F4(
set ,
set ,
set ,
set ,
set )
-> set ,
F5(
set )
-> set } :
ex
A being
strict MSAlgebra of
CatSign F1() st
( ( for
a,
b being
Element of
F1() holds the
Sorts of
A . (homsym a,b) = F3(
a,
b) ) & ( for
a being
Element of
F1() holds
(Den (idsym a),A) . {} = F5(
a) ) & ( for
a,
b,
c being
Element of
F1()
for
f,
g being
Element of
F2() st
f in F3(
a,
b) &
g in F3(
b,
c) holds
(Den (compsym a,b,c),A) . <*g,f*> = F4(
a,
b,
c,
g,
f) ) )
provided
A1:
for
a,
b being
Element of
F1() holds
F3(
a,
b)
c= F2()
and A2:
for
a being
Element of
F1() holds
F5(
a)
in F3(
a,
a)
and A3:
for
a,
b,
c being
Element of
F1()
for
f,
g being
Element of
F2() st
f in F3(
a,
b) &
g in F3(
b,
c) holds
F4(
a,
b,
c,
g,
f)
in F3(
a,
c)
definition
let C be
Category;
func MSAlg C -> strict MSAlgebra of
CatSign the
carrier of
C means :
Def15:
( ( for
a,
b being
Object of
C holds the
Sorts of
it . (homsym a,b) = Hom a,
b ) & ( for
a being
Object of
C holds
(Den (idsym a),it) . {} = id a ) & ( for
a,
b,
c being
Object of
C for
f,
g being
Morphism of
C st
dom f = a &
cod f = b &
dom g = b &
cod g = c holds
(Den (compsym a,b,c),it) . <*g,f*> = g * f ) );
uniqueness
for b1, b2 being strict MSAlgebra of CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of b1 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b1) . {} = id a ) & ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den (compsym a,b,c),b1) . <*g,f*> = g * f ) & ( for a, b being Object of C holds the Sorts of b2 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b2) . {} = id a ) & ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den (compsym a,b,c),b2) . <*g,f*> = g * f ) holds
b1 = b2
correctness
existence
ex b1 being strict MSAlgebra of CatSign the carrier of C st
( ( for a, b being Object of C holds the Sorts of b1 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b1) . {} = id a ) & ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den (compsym a,b,c),b1) . <*g,f*> = g * f ) );
end;
:: deftheorem Def15 defines MSAlg CATALG_1:def 15 :
for C being Category
for b2 being strict MSAlgebra of CatSign the carrier of C holds
( b2 = MSAlg C iff ( ( for a, b being Object of C holds the Sorts of b2 . (homsym a,b) = Hom a,b ) & ( for a being Object of C holds (Den (idsym a),b2) . {} = id a ) & ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a & cod f = b & dom g = b & cod g = c holds
(Den (compsym a,b,c),b2) . <*g,f*> = g * f ) ) );
theorem
canceled;
theorem Th36:
theorem Th37:
for
A being
Category for
a,
b,
c being
Object of
A holds
(
Args (compsym a,b,c),
(MSAlg A) = product <*(Hom b,c),(Hom a,b)*> &
Result (compsym a,b,c),
(MSAlg A) = Hom a,
c )
theorem Th38:
theorem Th39:
theorem Th40:
for
C1,
C2 being
Category for
F being
Functor of
C1,
C2 for
a,
b,
c being
Object of
C1 for
f,
g being
Morphism of
C1 st
f in Hom a,
b &
g in Hom b,
c holds
for
x being
Element of
Args (compsym a,b,c),
(MSAlg C1) st
x = <*g,f*> holds
for
H being
ManySortedFunction of
(MSAlg C1),
((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) st
H = F -MSF the
carrier of
(CatSign the carrier of C1),the
Sorts of
(MSAlg C1) holds
H # x = <*(F . g),(F . f)*>
theorem
canceled;
theorem Th42:
theorem
for
C being
Category for
a,
b,
c,
d being
Object of
C for
f,
g,
h being
Morphism of
C st
f in Hom a,
b &
g in Hom b,
c &
h in Hom c,
d holds
(Den (compsym a,c,d),(MSAlg C)) . <*h,((Den (compsym a,b,c),(MSAlg C)) . <*g,f*>)*> = (Den (compsym a,b,d),(MSAlg C)) . <*((Den (compsym b,c,d),(MSAlg C)) . <*h,g*>),f*>
theorem
for
C being
Category for
a,
b being
Object of
C for
f being
Morphism of
C st
f in Hom a,
b holds
(
(Den (compsym a,b,b),(MSAlg C)) . <*(id b),f*> = f &
(Den (compsym a,a,b),(MSAlg C)) . <*f,(id a)*> = f )
theorem