:: Institution of Many-sorted Algebras, Part { I } : Signature Reduct :: of an Algebra :: by Grzegorz Bancerek :: :: Received December 30, 1996 :: Copyright (c) 1996-2021 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);