:: Equations in Many Sorted Algebras :: by Artur Korni{\l}owicz :: :: Received May 30, 1997 :: Copyright (c) 1997-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, FUNCT_1, RELAT_1, TARSKI, PBOOLE, MEMBER_1, MSUALG_3, FUNCT_2, FUNCT_6, PZFMISC1, SUBSET_1, REALSET1, STRUCT_0, MSUALG_1, MSUALG_2, UNIALG_2, PARTFUN1, PRALG_2, CARD_3, RLVECT_2, PRELAMB, MSAFREE, FINSET_1, MSAFREE2, MSUALG_6, MARGREL1, NAT_1, GROUP_6, CLOSURE2, ZFMISC_1, FINSEQ_1, CARD_1, PRALG_3, FUNCT_4, FUNCOP_1, NUMBERS, ZF_LANG, MCART_1, ZF_MODEL, WELLORD1, MSUALG_4, EQUATION, AFINSQ_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, STRUCT_0, FUNCT_2, MCART_1, FINSET_1, FINSEQ_1, FINSEQ_2, FUNCT_4, FUNCT_6, PZFMISC1, CARD_3, AFINSQ_1, MSUALG_1, PRALG_2, FUNCOP_1, MSUALG_2, PRALG_3, MSUALG_3, MSUALG_4, MSAFREE, MSAFREE2, CLOSURE2, MSUALG_6; constructors FUNCT_4, PZFMISC1, MSUALG_3, MSAFREE2, CLOSURE2, MSUALG_6, PRALG_3, RELSET_1, XTUPLE_0, NUMBERS, AFINSQ_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, FINSET_1, FINSEQ_1, STRUCT_0, MSUALG_1, MSUALG_2, RELAT_1, FUNCT_1, PRALG_2, MSUALG_3, MSAFREE, MSUALG_4, EXTENS_1, CLOSURE2, MSUALG_6, PRALG_3, MSUALG_9, MSSUBFAM, PBOOLE, AUTALG_1, AFINSQ_1; requirements SUBSET, BOOLE; begin :: On the Functions and Many Sorted Functions reserve I for set; theorem :: EQUATION:1 for A being set, B, C being non empty set for f being Function of A, B, g being Function of B, C st rng (g * f) = C holds rng g = C; theorem :: EQUATION:2 for A being ManySortedSet of I, B, C being non-empty ManySortedSet of I for f being ManySortedFunction of A, B, g being ManySortedFunction of B, C st g ** f is "onto" holds g is "onto"; theorem :: EQUATION:3 :: see PRALG_2:5 for A, B being non empty set, C, y being set for f being Function st f in Funcs(A,Funcs(B,C)) & y in B holds dom ((commute f).y) = A & rng (( commute f).y) c= C; theorem :: EQUATION:4 for A, B being ManySortedSet of I st A is_transformable_to B for f being ManySortedFunction of I st doms f = A & rngs f c= B holds f is ManySortedFunction of A, B; theorem :: EQUATION:5 for A, B being ManySortedSet of I, F being ManySortedFunction of A, B for C, E being ManySortedSubset of A, D being ManySortedSubset of C st E = D holds (F || C) || D = F || E; theorem :: EQUATION:6 for B being non-empty ManySortedSet of I, C being ManySortedSet of I for A being ManySortedSubset of C, F being ManySortedFunction of A, B ex G being ManySortedFunction of C, B st G || A = F; definition let I be set, A be ManySortedSet of I, F be ManySortedFunction of I; func F""A -> ManySortedSet of I means :: EQUATION:def 1 for i being object st i in I holds it.i = (F.i)"(A.i); end; theorem :: EQUATION:7 for A, B, C being ManySortedSet of I, F being ManySortedFunction of A, B holds F.:.:C is ManySortedSubset of B; theorem :: EQUATION:8 for A, B, C being ManySortedSet of I, F being ManySortedFunction of A, B holds F""C is ManySortedSubset of A; theorem :: EQUATION:9 for A, B being ManySortedSet of I, F being ManySortedFunction of A, B st F is "onto" holds F.:.:A = B; theorem :: EQUATION:10 for A, B being ManySortedSet of I, F being ManySortedFunction of A, B st A is_transformable_to B holds F""B = A; theorem :: EQUATION:11 for A being ManySortedSet of I, F being ManySortedFunction of I st A c= rngs F holds F.:.:(F""A) = A; theorem :: EQUATION:12 for f being ManySortedFunction of I for X being ManySortedSet of I holds f.:.:X c= rngs f; theorem :: EQUATION:13 for f being ManySortedFunction of I holds f.:.:(doms f) = rngs f; theorem :: EQUATION:14 for f being ManySortedFunction of I holds f""(rngs f) = doms f; theorem :: EQUATION:15 for A being ManySortedSet of I holds (id A).:.:A = A; theorem :: EQUATION:16 for A being ManySortedSet of I holds (id A)""A = A; begin :: On the Many Sorted Algebras reserve S for non empty non void ManySortedSign, U0, U1 for non-empty MSAlgebra over S; theorem :: EQUATION:17 for A being MSAlgebra over S holds A is MSSubAlgebra of the MSAlgebra of A; theorem :: EQUATION:18 for U0 being MSAlgebra over S, A being MSSubAlgebra of U0 for o being OperSymbol of S, x being set st x in Args(o,A) holds x in Args(o,U0); theorem :: EQUATION:19 for U0 being MSAlgebra over S, A being MSSubAlgebra of U0 for o being OperSymbol of S, x being set st x in Args(o,A) holds Den(o,A).x = Den(o, U0).x; theorem :: EQUATION:20 for F being MSAlgebra-Family of I, S, B being MSSubAlgebra of product F for o being OperSymbol of S, x being object st x in Args(o,B) holds Den(o,B).x is Function & Den(o,product F).x is Function; definition let S be non void non empty ManySortedSign, A be MSAlgebra over S, B be MSSubAlgebra of A; func SuperAlgebraSet B -> set means :: EQUATION:def 2 for x being object holds x in it iff ex C being strict MSSubAlgebra of A st x = C & B is MSSubAlgebra of C; end; registration let S be non void non empty ManySortedSign, A be MSAlgebra over S, B be MSSubAlgebra of A; cluster SuperAlgebraSet B -> non empty; end; registration let S be non empty non void ManySortedSign; cluster strict non-empty free for MSAlgebra over S; end; registration let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty finite-yielding MSSubset of A; cluster GenMSAlg X -> finitely-generated; end; registration let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S; cluster strict non-empty finitely-generated for MSSubAlgebra of A; end; registration let S be non empty non void ManySortedSign, A be feasible MSAlgebra over S; cluster feasible for MSSubAlgebra of A; end; theorem :: EQUATION:21 for A being MSAlgebra over S, C being MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C for h being ManySortedFunction of A, U0 for g being ManySortedFunction of C, U0 st g = h || D for o being OperSymbol of S, x being Element of Args(o,A) for y being Element of Args(o,C) st Args(o,C) <> {} & x = y holds h#x = g#y; theorem :: EQUATION:22 for A being feasible MSAlgebra over S, C being feasible MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C for h being ManySortedFunction of A, U0 st h is_homomorphism A, U0 for g being ManySortedFunction of C, U0 st g = h || D holds g is_homomorphism C , U0; theorem :: EQUATION:23 for B being strict non-empty MSAlgebra over S for G being GeneratorSet of U0, H being non-empty GeneratorSet of B for f being ManySortedFunction of U0 , B st H c= f.:.:G & f is_homomorphism U0, B holds f is_epimorphism U0, B; theorem :: EQUATION:24 for W being strict free non-empty MSAlgebra over S for F being ManySortedFunction of U0, U1 st F is_epimorphism U0, U1 for G being ManySortedFunction of W, U1 st G is_homomorphism W, U1 holds ex H being ManySortedFunction of W, U0 st H is_homomorphism W, U0 & G = F ** H; theorem :: EQUATION:25 for I being non empty finite set, A being non-empty MSAlgebra over S for F being MSAlgebra-Family of I, S st for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F.i ex B being strict non-empty finitely-generated MSSubAlgebra of A st for i being Element of I holds F.i is MSSubAlgebra of B; theorem :: EQUATION:26 for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st A is MSSubAlgebra of M & B is MSSubAlgebra of M; theorem :: EQUATION:27 for SG being non empty non void ManySortedSign for AG being non-empty MSAlgebra over SG for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } for F being MSAlgebra-Family of C, SG st for c being object st c in C holds c = F. c ex PS being strict non-empty MSSubAlgebra of product F, BA being ManySortedFunction of PS, AG st BA is_epimorphism PS, AG; theorem :: EQUATION:28 for U0 being feasible free MSAlgebra over S, A being free GeneratorSet of U0 for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds GenMSAlg Z is free; begin :: Equations in Many Sorted Algebras definition let S be non empty non void ManySortedSign; func TermAlg S -> MSAlgebra over S equals :: EQUATION:def 3 FreeMSA ((the carrier of S) --> NAT); end; registration let S be non empty non void ManySortedSign; cluster TermAlg S -> strict non-empty free; end; definition let S be non empty non void ManySortedSign; func Equations S -> ManySortedSet of the carrier of S equals :: EQUATION:def 4 [|the Sorts of TermAlg S, the Sorts of TermAlg S|]; end; registration let S be non empty non void ManySortedSign; cluster Equations S -> non-empty; end; definition let S be non empty non void ManySortedSign; mode EqualSet of S is ManySortedSubset of Equations S; end; reserve s for SortSymbol of S; reserve e for Element of (Equations S).s; reserve E for EqualSet of S; notation let S be non empty non void ManySortedSign, s be SortSymbol of S, x, y be Element of (the Sorts of TermAlg S).s; synonym x '=' y for [x,y]; end; definition let S be non empty non void ManySortedSign, s be SortSymbol of S, x, y be Element of (the Sorts of TermAlg S).s; redefine func x '=' y -> Element of (Equations S).s; end; theorem :: EQUATION:29 e`1 in (the Sorts of TermAlg S).s; theorem :: EQUATION:30 e`2 in (the Sorts of TermAlg S).s; definition let S be non empty non void ManySortedSign, A be MSAlgebra over S, s be SortSymbol of S, e be Element of (Equations S).s; pred A |= e means :: EQUATION:def 5 for h being ManySortedFunction of TermAlg S, A st h is_homomorphism TermAlg S, A holds h.s.(e`1) = h.s.(e`2); end; definition let S be non empty non void ManySortedSign, A be MSAlgebra over S, E be EqualSet of S; pred A |= E means :: EQUATION:def 6 for s being SortSymbol of S for e being Element of (Equations S).s st e in E.s holds A |= e; end; theorem :: EQUATION:31 for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e; theorem :: EQUATION:32 for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E; theorem :: EQUATION:33 U0, U1 are_isomorphic & U0 |= e implies U1 |= e; theorem :: EQUATION:34 U0, U1 are_isomorphic & U0 |= E implies U1 |= E; theorem :: EQUATION:35 for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e; theorem :: EQUATION:36 for R being MSCongruence of U0 st U0 |= E holds QuotMSAlg (U0,R) |= E; theorem :: EQUATION:37 for F being MSAlgebra-Family of I, S st (for i being set st i in I ex A being MSAlgebra over S st A = F.i & A |= e) holds product F |= e; theorem :: EQUATION:38 for F being MSAlgebra-Family of I, S st (for i being set st i in I ex A being MSAlgebra over S st A = F.i & A |= E) holds product F |= E;