begin
definition
let A be non
empty set ;
func MSSCat A -> non
empty strict AltCatStr means :
Def1:
( the
carrier of
it = MSS_set A & ( for
i,
j being
Element of
MSS_set A holds the
Arrows of
it . (
i,
j)
= MSS_morph (
i,
j) ) & ( for
i,
j,
k being
object of
it st
i in MSS_set A &
j in MSS_set A &
k in MSS_set A holds
for
f1,
f2,
g1,
g2 being
Function st
[f1,f2] in the
Arrows of
it . (
i,
j) &
[g1,g2] in the
Arrows of
it . (
j,
k) holds
( the Comp of it . (i,j,k)) . (
[g1,g2],
[f1,f2])
= [(g1 * f1),(g2 * f2)] ) );
existence
ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) )
uniqueness
for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) holds
b1 = b2
end;
:: deftheorem Def1 defines MSSCat MSINST_1:def 1 :
for A being non empty set
for b2 being non empty strict AltCatStr holds
( b2 = MSSCat A iff ( the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) );
theorem
:: deftheorem Def2 defines MSAlg_set MSINST_1:def 2 :
for S being non empty non void ManySortedSign
for A being non empty set
for b3 being set holds
( b3 = MSAlg_set (S,A) iff for x being set holds
( x in b3 iff ex M being strict feasible MSAlgebra of S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) );
begin
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
definition
let S be non
empty non
void ManySortedSign ;
let A be non
empty set ;
let i,
j be
set ;
assume that A1:
i in MSAlg_set (
S,
A)
and A2:
j in MSAlg_set (
S,
A)
;
func MSAlg_morph (
S,
A,
i,
j)
-> set means :
Def3:
for
x being
set holds
(
x in it iff ex
M,
N being
strict feasible MSAlgebra of
S ex
f being
ManySortedFunction of
M,
N st
(
M = i &
N = j &
f = x & the
Sorts of
M is_transformable_to the
Sorts of
N &
f is_homomorphism M,
N ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra of S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra of S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds
( x in b2 iff ex M, N being strict feasible MSAlgebra of S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines MSAlg_morph MSINST_1:def 3 :
for S being non empty non void ManySortedSign
for A being non empty set
for i, j being set st i in MSAlg_set (S,A) & j in MSAlg_set (S,A) holds
for b5 being set holds
( b5 = MSAlg_morph (S,A,i,j) iff for x being set holds
( x in b5 iff ex M, N being strict feasible MSAlgebra of S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) );
definition
let S be non
empty non
void ManySortedSign ;
let A be non
empty set ;
func MSAlgCat (
S,
A)
-> non
empty strict AltCatStr means :
Def4:
( the
carrier of
it = MSAlg_set (
S,
A) & ( for
i,
j being
Element of
MSAlg_set (
S,
A) holds the
Arrows of
it . (
i,
j)
= MSAlg_morph (
S,
A,
i,
j) ) & ( for
i,
j,
k being
object of
it for
f,
g being
Function-yielding Function st
f in the
Arrows of
it . (
i,
j) &
g in the
Arrows of
it . (
j,
k) holds
( the Comp of it . (i,j,k)) . (
g,
f)
= g ** f ) );
existence
ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) )
uniqueness
for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) & the carrier of b2 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b2 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b2
for f, g being Function-yielding Function st f in the Arrows of b2 . (i,j) & g in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . (g,f) = g ** f ) holds
b1 = b2
end;
:: deftheorem Def4 defines MSAlgCat MSINST_1:def 4 :
for S being non empty non void ManySortedSign
for A being non empty set
for b3 being non empty strict AltCatStr holds
( b3 = MSAlgCat (S,A) iff ( the carrier of b3 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b3 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being object of b3
for f, g being Function-yielding Function st f in the Arrows of b3 . (i,j) & g in the Arrows of b3 . (j,k) holds
( the Comp of b3 . (i,j,k)) . (g,f) = g ** f ) ) );
theorem