Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Institution of Many Sorted Algebras. Part I: Signature Reduct of an Algebra

**by****Grzegorz Bancerek**- Received December 30, 1996
- MML identifier: INSTALG1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, PRALG_1, RELAT_1, MSUALG_3, BOOLE, AMI_1, MSUALG_1, ZF_REFLE, PBOOLE, MSATERM, FREEALG, MSAFREE, TDGROUP, FINSEQ_1, DTCONSTR, QC_LANG1, TREES_3, NATTRA_1, TREES_4, CARD_3, FUNCT_6, ALG_1, MSUALG_6, PUA2MSS1, FUNCT_4, REWRITE1, REALSET1, MSUALG_2, CAT_1, GROUP_6, INSTALG1, FINSEQ_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, STRUCT_0, FINSEQ_2, CARD_3, FINSEQ_4, LANG1, TREES_3, TREES_4, DTCONSTR, REWRITE1, FUNCT_7, PBOOLE, MSUALG_1, PARTFUN1, FUNCT_2, MSUALG_2, PRALG_2, MSUALG_3, PUA2MSS1, MSAFREE, MSATERM, AUTALG_1, MSUALG_6; constructors NAT_1, REWRITE1, MSATERM, PUA2MSS1, FUNCT_7, AUTALG_1, MSUALG_6, FINSEQ_4; clusters STRUCT_0, RELSET_1, FUNCT_1, TREES_3, PRALG_1, PBOOLE, MSUALG_1, MSAFREE, PRE_CIRC, MSUALG_9, MSATERM, FUNCT_2, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries canceled; theorem :: INSTALG1:2 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); definition 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 Element of Args(o, FreeMSA V); end; theorem :: INSTALG1:3 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:4 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; definition let S be non empty non void ManySortedSign; let A be non-empty MSAlgebra over S; cluster the MSAlgebra of A -> non-empty; end; theorem :: INSTALG1:5 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: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 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:7 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 h' being ManySortedFunction of B1,B2 st h' = h & h' is_homomorphism B1,B2; definition let S be ManySortedSign; attr S is feasible means :: INSTALG1:def 1 the carrier of S = {} implies the OperSymbols of S = {}; end; theorem :: INSTALG1:8 for S being ManySortedSign holds S is feasible iff dom the ResultSort of S = the OperSymbols of S; definition cluster non empty -> feasible ManySortedSign; cluster void -> feasible ManySortedSign; cluster empty feasible -> void ManySortedSign; cluster non void feasible -> non empty ManySortedSign; end; definition cluster non void non empty ManySortedSign; end; theorem :: INSTALG1:9 for S being feasible ManySortedSign holds id the carrier of S, id the OperSymbols of S form_morphism_between S,S; theorem :: INSTALG1:10 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 OperSymbols of S1, the OperSymbols 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 OperSymbols of it form_morphism_between it,S; end; theorem :: INSTALG1:11 for S being feasible ManySortedSign, T being Subsignature of S holds the carrier of T c= the carrier of S & the OperSymbols of T c= the OperSymbols of S; definition let S be feasible ManySortedSign; cluster -> feasible Subsignature of S; end; theorem :: INSTALG1:12 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:13 for S being feasible ManySortedSign, T being Subsignature of S holds the Arity of T = (the Arity of S)|the OperSymbols of T & the ResultSort of T = (the ResultSort of S)|the OperSymbols of T; theorem :: INSTALG1:14 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:15 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 OperSymbols of T & the ResultSort of T = (the ResultSort of S)|the OperSymbols of T holds T is Subsignature of S; theorem :: INSTALG1:16 for S being feasible ManySortedSign holds S is Subsignature of S; theorem :: INSTALG1:17 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:18 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; definition let S be non empty ManySortedSign; cluster non empty Subsignature of S; end; definition let S be non void feasible ManySortedSign; cluster non void Subsignature of S; end; theorem :: INSTALG1:19 for S being feasible ManySortedSign, S' 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 S', g|the OperSymbols of S' form_morphism_between S',T ; theorem :: INSTALG1:20 for S being ManySortedSign, T being feasible ManySortedSign for T' being Subsignature of T, f,g being Function st f,g form_morphism_between S,T' holds f,g form_morphism_between S,T; theorem :: INSTALG1:21 for S being ManySortedSign, T being feasible ManySortedSign for T' being Subsignature of T, f,g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T' & rng g c= the OperSymbols of T' holds f,g form_morphism_between S,T'; 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 OperSymbols of S1); end; theorem :: INSTALG1:22 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:23 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; definition 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: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 Den(o1,A|(S1,f,g)) = Den(o2,A); theorem :: INSTALG1:25 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:26 for S being non empty ManySortedSign for A being MSAlgebra over S holds A|(S, id the carrier of S, id the OperSymbols of S) = the MSAlgebra of A; theorem :: INSTALG1:27 for S being non empty ManySortedSign for A being MSAlgebra over S holds A|S = the MSAlgebra of A; theorem :: INSTALG1:28 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:29 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:30 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:31 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:32 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:33 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:34 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:35 for S,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 h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for f being Function of the carrier of S', the carrier of S for g being Function st f,g form_morphism_between S',S ex h' being ManySortedFunction of A1|(S',f,g), A2|(S',f,g) st h' = h*f & h' is_homomorphism A1|(S',f,g), A2|(S',f,g); theorem :: INSTALG1:36 for S being non void feasible ManySortedSign for S' 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 h' being ManySortedFunction of A1|S', A2|S' st h' = h|the carrier of S' & h' is_homomorphism A1|S', A2|S'; theorem :: INSTALG1:37 for S,S' being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for f being Function of the carrier of S', the carrier of S for g being Function st f,g form_morphism_between S',S for B being non-empty MSAlgebra over S' st B = A|(S',f,g) for s1,s2 being SortSymbol of S', 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:38 for S,S' being non empty non void ManySortedSign for f being Function of the carrier of S', the carrier of S for g being Function st f,g form_morphism_between S',S for s1,s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds TranslationRel S reduces f.s1, f.s2; theorem :: INSTALG1:39 for S,S' being non void non empty ManySortedSign for A being non-empty MSAlgebra over S for f being Function of the carrier of S', the carrier of S for g being Function st f,g form_morphism_between S',S for B being non-empty MSAlgebra over S' st B = A|(S',f,g) for s1,s2 being SortSymbol of S' st TranslationRel S' 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 GenFuncEx{S() -> non empty non void ManySortedSign, A() -> non-empty MSAlgebra over S(), X() -> non-empty ManySortedSet of the carrier of S(), F(set,set) -> 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:40 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; definition 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: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 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: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 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:43 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:44 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 OperSymbols of S, X, S, S) = id the Sorts of FreeMSA X; theorem :: INSTALG1:45 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);

Back to top