:: Institution of Many-sorted Algebras, Part { I } : Signature Reduct
:: of an Algebra
:: by Grzegorz Bancerek
::
:: Received December 30, 1996
:: Copyright (c) 1996-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, STRUCT_0, MSUALG_1, RELAT_1, PBOOLE, MSATERM, MSAFREE,
SUBSET_1, DTCONSTR, FINSEQ_1, TDGROUP, TREES_3, TARSKI, FUNCT_1, NUMBERS,
MARGREL1, PARTFUN1, PZFMISC1, TREES_4, FUNCT_6, MSUALG_3, MSUALG_6,
PUA2MSS1, CARD_3, RLTOPSP1, FUNCT_4, REWRITE1, REALSET1, CAT_1, ZFMISC_1,
NAT_1, MEMBER_1, INSTALG1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1,
NUMBERS, FINSEQ_1, STRUCT_0, FINSEQ_2, CARD_3, LANG1, TREES_3, TREES_4,
DTCONSTR, REWRITE1, FUNCT_7, PBOOLE, PZFMISC1, MSUALG_1, PARTFUN1,
FUNCT_2, PRALG_2, MSUALG_3, PUA2MSS1, MSAFREE, MSATERM, MSUALG_6;
constructors NAT_1, REWRITE1, PZFMISC1, FUNCT_7, PRALG_2, MSUALG_3, MSATERM,
PUA2MSS1, MSUALG_6, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, TREES_3,
STRUCT_0, MSUALG_1, MSUALG_3, MSAFREE, MSATERM, MSUALG_9, RELSET_1,
FINSEQ_1, ORDINAL1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
theorem :: INSTALG1:1
for S being non empty non void ManySortedSign for o being
OperSymbol of S for V being non-empty ManySortedSet of the carrier of S for x
being set holds x is ArgumentSeq of Sym(o,V) iff x is Element of Args(o,
FreeMSA V);
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let o be OperSymbol of S;
cluster -> DTree-yielding for Element of Args(o, FreeMSA V);
end;
theorem :: INSTALG1:2
for S 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 for o
being OperSymbol of S st Args(o,A1) <> {} holds Args(o,A2) <> {};
theorem :: INSTALG1:3
for S being non empty non void ManySortedSign for o being
OperSymbol of S for V being non-empty ManySortedSet of the carrier of S for x
being Element of Args(o, FreeMSA V) holds Den(o,FreeMSA V).x = [o, the carrier
of S]-tree x;
theorem :: INSTALG1:4
for S being non empty non void ManySortedSign for A,B being MSAlgebra
over S st the MSAlgebra of A = the MSAlgebra of B for o being OperSymbol of S
holds Den(o,A) = Den(o,B);
theorem :: INSTALG1:5
for S being non empty non void ManySortedSign for A1,A2,B1,B2
being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the
MSAlgebra of A2 = the MSAlgebra of B2 for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g for o being OperSymbol of S st
Args(o,A1) <> {} & Args(o,A2) <> {} 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 :: INSTALG1:6
for S being non empty non void ManySortedSign for A1,A2,B1,B2 being
MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra
of A2 = the MSAlgebra of B2 & the Sorts of A1 is_transformable_to the Sorts of
A2 for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 ex h9
being ManySortedFunction of B1,B2 st h9 = h & h9 is_homomorphism B1,B2;
definition
let S be ManySortedSign;
attr S is feasible means
:: INSTALG1:def 1
the carrier of S = {} implies the carrier' of S = {};
end;
theorem :: INSTALG1:7
for S being ManySortedSign holds
S is feasible iff dom the ResultSort of S = the carrier' of S;
registration
cluster non empty -> feasible for ManySortedSign;
cluster void -> feasible for ManySortedSign;
cluster empty feasible -> void for ManySortedSign;
cluster non void feasible -> non empty for ManySortedSign;
end;
registration
cluster non void non empty for ManySortedSign;
end;
theorem :: INSTALG1:8
for S being feasible ManySortedSign holds id the carrier of S, id
the carrier' of S form_morphism_between S,S;
theorem :: INSTALG1:9
for S1,S2 being ManySortedSign for f,g being Function st f,g
form_morphism_between S1,S2 holds f is Function of the carrier of S1, the
carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2;
begin :: Subsignature
definition
let S be feasible ManySortedSign;
mode Subsignature of S -> ManySortedSign means
:: INSTALG1:def 2
id the carrier of it, id the carrier' of it form_morphism_between it,S;
end;
theorem :: INSTALG1:10
for S being feasible ManySortedSign, T being Subsignature of S
holds the carrier of T c= the carrier of S & the carrier' of T c= the carrier'
of S;
registration
let S be feasible ManySortedSign;
cluster -> feasible for Subsignature of S;
end;
theorem :: INSTALG1:11
for S being feasible ManySortedSign, T being Subsignature of S
holds the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity
of S;
theorem :: INSTALG1:12
for S being feasible ManySortedSign, T being Subsignature of S
holds the Arity of T = (the Arity of S)|the carrier' of T & the ResultSort of T
= (the ResultSort of S)|the carrier' of T;
theorem :: INSTALG1:13
for S,T being feasible ManySortedSign st the carrier of T c= the
carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the
ResultSort of S holds T is Subsignature of S;
theorem :: INSTALG1:14
for S,T being feasible ManySortedSign st the carrier of T c= the
carrier of S & the Arity of T = (the Arity of S)|the carrier' of T & the
ResultSort of T = (the ResultSort of S)|the carrier' of T holds T is
Subsignature of S;
theorem :: INSTALG1:15
for S being feasible ManySortedSign holds S is Subsignature of S;
theorem :: INSTALG1:16
for S1 being feasible ManySortedSign for S2 being Subsignature of S1
for S3 being Subsignature of S2 holds S3 is Subsignature of S1;
theorem :: INSTALG1:17
for S1 being feasible ManySortedSign for S2 being Subsignature of S1
st S1 is Subsignature of S2 holds the ManySortedSign of S1 = the ManySortedSign
of S2;
registration
let S be non empty ManySortedSign;
cluster non empty for Subsignature of S;
end;
registration
let S be non void feasible ManySortedSign;
cluster non void for Subsignature of S;
end;
theorem :: INSTALG1:18
for S being feasible ManySortedSign, S9 being Subsignature of S for T
being ManySortedSign, f,g being Function st f,g form_morphism_between S,T holds
f|the carrier of S9, g|the carrier' of S9 form_morphism_between S9,T;
theorem :: INSTALG1:19
for S being ManySortedSign, T being feasible ManySortedSign for T9
being Subsignature of T, f,g being Function st f,g form_morphism_between S,T9
holds f,g form_morphism_between S,T;
theorem :: INSTALG1:20
for S being ManySortedSign, T being feasible ManySortedSign for T9
being Subsignature of T, f,g being Function st f,g form_morphism_between S,T &
rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds f,g
form_morphism_between S,T9;
begin :: Signature reduct
definition
let S1,S2 be non empty ManySortedSign;
let A be MSAlgebra over S2;
let f,g be Function such that
f,g form_morphism_between S1,S2;
func A|(S1,f,g) -> strict MSAlgebra over S1 means
:: INSTALG1:def 3
the Sorts of it =
(the Sorts of A)*f & the Charact of it = (the Charact of A)*g;
end;
definition
let S2,S1 be non empty ManySortedSign;
let A be MSAlgebra over S2;
func A|S1 -> strict MSAlgebra over S1 equals
:: INSTALG1:def 4
A|(S1, id the carrier of S1, id
the carrier' of S1);
end;
theorem :: INSTALG1:21
for S1,S2 being non empty ManySortedSign for A,B being MSAlgebra over
S2 st the MSAlgebra of A = the MSAlgebra of B for f,g being Function st f,g
form_morphism_between S1,S2 holds A|(S1,f,g) = B|(S1,f,g);
theorem :: INSTALG1:22
for S1,S2 being non empty ManySortedSign for A being non-empty
MSAlgebra over S2 for f,g being Function st f,g form_morphism_between S1,S2
holds A|(S1,f,g) is non-empty;
registration
let S2 be non empty ManySortedSign;
let S1 be non empty Subsignature of S2;
let A be non-empty MSAlgebra over S2;
cluster A|S1 -> non-empty;
end;
theorem :: INSTALG1:23
for S1,S2 being non void non empty ManySortedSign for f,g being
Function st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 for
o1 being OperSymbol of S1, o2 being OperSymbol of S2 st o2 = g.o1 holds Den(o1,
A|(S1,f,g)) = Den(o2,A);
theorem :: INSTALG1:24
for S1,S2 being non void non empty ManySortedSign for f,g being
Function st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 for
o1 being OperSymbol of S1, 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 :: INSTALG1:25
for S being non empty ManySortedSign for A being MSAlgebra over
S holds A|(S, id the carrier of S, id the carrier' of S) = the MSAlgebra of A
;
theorem :: INSTALG1:26
for S being non empty ManySortedSign for A being MSAlgebra over S
holds A|S = the MSAlgebra of A;
theorem :: INSTALG1:27
for S1,S2,S3 being non empty ManySortedSign for f1,g1 being
Function st f1,g1 form_morphism_between S1,S2 for f2,g2 being Function st f2,g2
form_morphism_between S2,S3 for A being MSAlgebra over S3 holds A|(S1,f2*f1,g2*
g1) = (A|(S2,f2,g2))|(S1,f1,g1);
theorem :: INSTALG1:28
for S1 being non empty feasible ManySortedSign for S2 being non empty
Subsignature of S1 for S3 being non empty Subsignature of S2 for A being
MSAlgebra over S1 holds A|S3 = (A|S2)|S3;
theorem :: INSTALG1:29
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 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 :: INSTALG1:30
for S1 being non empty ManySortedSign for S2 being non empty
Subsignature of S1 for A1,A2 being MSAlgebra over S1 for h being
ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h|the carrier of
S2 is ManySortedFunction of the Sorts of A1|S2, the Sorts of A2|S2;
theorem :: INSTALG1:31
for S1,S2 being non empty ManySortedSign for f,g being Function
st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 holds (id the
Sorts of A)*f = id the Sorts of A|(S1,f,g);
theorem :: INSTALG1:32
for S1 being non empty ManySortedSign for S2 being non empty
Subsignature of S1 for A being MSAlgebra over S1 holds (id the Sorts of A)|the
carrier of S2 = id the Sorts of A|S2;
theorem :: INSTALG1:33
for S1,S2 being non void non empty ManySortedSign for f,g being
Function st f,g form_morphism_between S1,S2 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 for o1 being OperSymbol of S1, o2 being OperSymbol of
S2 st o2 = g.o1 & Args(o2,A) <> {} & Args(o2,B) <> {} 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 :: INSTALG1:34
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 for h
being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 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 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 :: INSTALG1:35
for S being non void feasible ManySortedSign for S9 being non void
Subsignature of S for A1,A2 being MSAlgebra over S st the Sorts of A1
is_transformable_to the Sorts of A2 for h being ManySortedFunction of A1,A2 st
h is_homomorphism A1,A2 ex h9 being ManySortedFunction of A1|S9, A2|S9 st h9 =
h|the carrier of S9 & h9 is_homomorphism A1|S9, A2|S9;
theorem :: INSTALG1:36
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 for B being
non-empty MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9,
t being Function st t is_e.translation_of B, s1, s2 holds t is_e.translation_of
A, f.s1, f.s2;
theorem :: INSTALG1:37
for S,S9 being non empty non void ManySortedSign 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 for s1,s2 being SortSymbol of S9 st TranslationRel
S9 reduces s1,s2 holds TranslationRel S reduces f.s1, f.s2;
theorem :: INSTALG1:38
for S,S9 being non void non empty 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 for B being non-empty
MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9 st
TranslationRel S9 reduces s1,s2 for t being Translation of B, s1, s2 holds t is
Translation of A, f.s1, f.s2;
begin :: Translating homomorphism
scheme :: INSTALG1:sch 1
GenFuncEx{S() -> non empty non void ManySortedSign, A() -> non-empty
MSAlgebra over S(), X() -> non-empty ManySortedSet of the carrier of S(),
F(object,object) -> set}:
ex h being ManySortedFunction of FreeMSA X(), A() st h
is_homomorphism FreeMSA X(), A() & for s being SortSymbol of S() for x being
Element of X().s holds h.s.root-tree [x,s] = F(x,s)
provided
for s being SortSymbol of S() for x being Element of X().s holds F(x
,s) in (the Sorts of A()).s;
theorem :: INSTALG1:39
for I being set, A,B being ManySortedSet of I for C being
ManySortedSubset of A for F being ManySortedFunction of A,B for i being set st
i in I for f,g being Function st f = F.i & g = (F||C).i for x being set st x in
C.i holds g.x = f.x;
registration
let S be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
cluster FreeGen X -> non-empty;
end;
definition
let S1,S2 be non empty non void ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S2;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function such that
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
:: INSTALG1:def 5
it is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) & for
s being SortSymbol of S1, x being Element of (X*f).s holds it.s.root-tree [x,s]
= root-tree [x,f.s];
end;
theorem :: INSTALG1:40
for S1,S2 being non void non empty ManySortedSign for X being
non-empty 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 for o being OperSymbol of S1, 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 :: INSTALG1:41
for S1,S2 being non void non empty ManySortedSign for X being
non-empty 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 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 :: INSTALG1:42
for S1,S2 being non void non empty ManySortedSign for X being
non-empty 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 :: INSTALG1:43
for S being non void non empty ManySortedSign for X being non-empty
ManySortedSet of the carrier of S holds hom(id the carrier of S, id the
carrier' of S, X, S, S) = id the Sorts of FreeMSA X;
theorem :: INSTALG1:44
for S1,S2,S3 being non void non empty ManySortedSign for X being
non-empty 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 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);