begin
theorem Th5:
for
S being non
empty non
void ManySortedSign for
A1,
A2,
B1,
B2 being
MSAlgebra over
S st
MSAlgebra(# the
Sorts of
A1, the
Charact of
A1 #)
= MSAlgebra(# the
Sorts of
B1, the
Charact of
B1 #) &
MSAlgebra(# the
Sorts of
A2, the
Charact of
A2 #)
= MSAlgebra(# the
Sorts of
B2, the
Charact of
B2 #) holds
for
f being
ManySortedFunction of
A1,
A2 for
g being
ManySortedFunction of
B1,
B2 st
f = g holds
for
o being
OperSymbol of
S st
Args (
o,
A1)
<> {} &
Args (
o,
A2)
<> {} holds
for
x being
Element of
Args (
o,
A1)
for
y being
Element of
Args (
o,
B1) st
x = y holds
f # x = g # y
theorem
for
S being non
empty non
void ManySortedSign for
A1,
A2,
B1,
B2 being
MSAlgebra over
S st
MSAlgebra(# the
Sorts of
A1, the
Charact of
A1 #)
= MSAlgebra(# the
Sorts of
B1, the
Charact of
B1 #) &
MSAlgebra(# the
Sorts of
A2, the
Charact of
A2 #)
= MSAlgebra(# the
Sorts of
B2, the
Charact of
B2 #) & the
Sorts of
A1 is_transformable_to the
Sorts of
A2 holds
for
h being
ManySortedFunction of
A1,
A2 st
h is_homomorphism A1,
A2 holds
ex
h9 being
ManySortedFunction of
B1,
B2 st
(
h9 = h &
h9 is_homomorphism B1,
B2 )
begin
begin
theorem
for
S1,
S2 being non
empty ManySortedSign for
A,
B being
MSAlgebra over
S2 st
MSAlgebra(# the
Sorts of
A, the
Charact of
A #)
= MSAlgebra(# the
Sorts of
B, the
Charact of
B #) holds
for
f,
g being
Function st
f,
g form_morphism_between S1,
S2 holds
A | (
S1,
f,
g)
= B | (
S1,
f,
g)
theorem Th24:
for
S1,
S2 being non
empty non
void ManySortedSign for
f,
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
A being
MSAlgebra over
S2 for
o1 being
OperSymbol of
S1 for
o2 being
OperSymbol of
S2 st
o2 = g . o1 holds
(
Args (
o2,
A)
= Args (
o1,
(A | (S1,f,g))) &
Result (
o1,
(A | (S1,f,g)))
= Result (
o2,
A) )
theorem Th27:
for
S1,
S2,
S3 being non
empty ManySortedSign for
f1,
g1 being
Function st
f1,
g1 form_morphism_between S1,
S2 holds
for
f2,
g2 being
Function st
f2,
g2 form_morphism_between S2,
S3 holds
for
A being
MSAlgebra over
S3 holds
A | (
S1,
(f2 * f1),
(g2 * g1))
= (A | (S2,f2,g2)) | (
S1,
f1,
g1)
theorem Th29:
for
S1,
S2 being non
empty ManySortedSign for
f being
Function of the
carrier of
S1, the
carrier of
S2 for
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
A1,
A2 being
MSAlgebra over
S2 for
h being
ManySortedFunction of the
Sorts of
A1, the
Sorts of
A2 holds
h * f is
ManySortedFunction of the
Sorts of
(A1 | (S1,f,g)), the
Sorts of
(A2 | (S1,f,g))
theorem Th33:
for
S1,
S2 being non
empty non
void ManySortedSign for
f,
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
A,
B being
MSAlgebra over
S2 for
h2 being
ManySortedFunction of
A,
B for
h1 being
ManySortedFunction of
(A | (S1,f,g)),
(B | (S1,f,g)) st
h1 = h2 * f holds
for
o1 being
OperSymbol of
S1 for
o2 being
OperSymbol of
S2 st
o2 = g . o1 &
Args (
o2,
A)
<> {} &
Args (
o2,
B)
<> {} holds
for
x2 being
Element of
Args (
o2,
A)
for
x1 being
Element of
Args (
o1,
(A | (S1,f,g))) st
x2 = x1 holds
h1 # x1 = h2 # x2
theorem Th34:
for
S,
S9 being non
empty non
void ManySortedSign for
A1,
A2 being
MSAlgebra over
S st the
Sorts of
A1 is_transformable_to the
Sorts of
A2 holds
for
h being
ManySortedFunction of
A1,
A2 st
h is_homomorphism A1,
A2 holds
for
f being
Function of the
carrier of
S9, the
carrier of
S for
g being
Function st
f,
g form_morphism_between S9,
S holds
ex
h9 being
ManySortedFunction of
(A1 | (S9,f,g)),
(A2 | (S9,f,g)) st
(
h9 = h * f &
h9 is_homomorphism A1 | (
S9,
f,
g),
A2 | (
S9,
f,
g) )
theorem Th36:
for
S,
S9 being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra over
S for
f being
Function of the
carrier of
S9, the
carrier of
S for
g being
Function st
f,
g form_morphism_between S9,
S holds
for
B being
non-empty MSAlgebra over
S9 st
B = A | (
S9,
f,
g) holds
for
s1,
s2 being
SortSymbol of
S9 for
t being
Function st
t is_e.translation_of B,
s1,
s2 holds
t is_e.translation_of A,
f . s1,
f . s2
Lm1:
for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
theorem
for
S,
S9 being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra over
S for
f being
Function of the
carrier of
S9, the
carrier of
S for
g being
Function st
f,
g form_morphism_between S9,
S holds
for
B being
non-empty MSAlgebra over
S9 st
B = A | (
S9,
f,
g) holds
for
s1,
s2 being
SortSymbol of
S9 st
TranslationRel S9 reduces s1,
s2 holds
for
t being
Translation of
B,
s1,
s2 holds
t is
Translation of
A,
f . s1,
f . s2 by Lm1;
begin
definition
let S1,
S2 be non
empty non
void ManySortedSign ;
let X be
V16()
ManySortedSet of the
carrier of
S2;
let f be
Function of the
carrier of
S1, the
carrier of
S2;
let g be
Function;
assume B1:
f,
g form_morphism_between S1,
S2
;
func hom (
f,
g,
X,
S1,
S2)
-> ManySortedFunction of
(FreeMSA (X * f)),
((FreeMSA X) | (S1,f,g)) means :
Def5:
(
it is_homomorphism FreeMSA (X * f),
(FreeMSA X) | (
S1,
f,
g) & ( for
s being
SortSymbol of
S1 for
x being
Element of
(X * f) . s holds
(it . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) );
existence
ex b1 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st
( b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )
uniqueness
for b1, b2 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & b2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) holds
b1 = b2
end;
::
deftheorem Def5 defines
hom INSTALG1:def 5 :
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for b6 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) holds
( b6 = hom (f,g,X,S1,S2) iff ( b6 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b6 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) );
theorem Th40:
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V16()
ManySortedSet of the
carrier of
S2 for
f being
Function of the
carrier of
S1, the
carrier of
S2 for
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
o being
OperSymbol of
S1 for
p being
Element of
Args (
o,
(FreeMSA (X * f)))
for
q being
FinSequence st
q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
theorem Th41:
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V16()
ManySortedSet of the
carrier of
S2 for
f being
Function of the
carrier of
S1, the
carrier of
S2 for
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
t being
Term of
S1,
(X * f) holds
(
((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is
CompoundTerm of
S2,
X iff
t is
CompoundTerm of
S1,
X * f )
theorem
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V16()
ManySortedSet of the
carrier of
S2 for
f being
Function of the
carrier of
S1, the
carrier of
S2 for
g being
one-to-one Function st
f,
g form_morphism_between S1,
S2 holds
hom (
f,
g,
X,
S1,
S2)
is_monomorphism FreeMSA (X * f),
(FreeMSA X) | (
S1,
f,
g)
theorem
for
S1,
S2,
S3 being non
empty non
void ManySortedSign for
X being
V16()
ManySortedSet of the
carrier of
S3 for
f1 being
Function of the
carrier of
S1, the
carrier of
S2 for
g1 being
Function st
f1,
g1 form_morphism_between S1,
S2 holds
for
f2 being
Function of the
carrier of
S2, the
carrier of
S3 for
g2 being
Function st
f2,
g2 form_morphism_between S2,
S3 holds
hom (
(f2 * f1),
(g2 * g1),
X,
S1,
S3)
= ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))