Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Equations in Many Sorted Algebras

**by****Artur Kornilowicz**- Received May 30, 1997
- MML identifier: EQUATION

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, PBOOLE, ZF_REFLE, PRALG_1, MSUALG_3, FUNCT_2, PRALG_2, BOOLE, NATTRA_1, FUNCT_6, MSUALG_2, REALSET1, AMI_1, MSUALG_1, UNIALG_2, TDGROUP, FINSEQ_4, CARD_3, RLVECT_2, PRELAMB, MSAFREE, PRE_CIRC, MSAFREE2, FREEALG, MSUALG_6, QC_LANG1, ALG_1, GROUP_6, FINSET_1, CLOSURE2, TARSKI, FINSEQ_1, PRALG_3, FUNCT_4, FUNCOP_1, ZF_LANG, MCART_1, ZF_MODEL, WELLORD1, MSUALG_4, BORSUK_1, EQUATION; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, STRUCT_0, FUNCT_2, MCART_1, FINSET_1, FINSEQ_1, FUNCT_4, CARD_3, PBOOLE, MSUALG_1, PRALG_1, PRALG_2, FINSEQ_4, PRE_CIRC, MSUALG_2, PRALG_3, MSUALG_3, MSUALG_4, EXTENS_1, MSAFREE, MSAFREE2, AUTALG_1, CLOSURE2, MSUALG_6; constructors AUTALG_1, PRALG_3, MSAFREE2, PRE_CIRC, CLOSURE2, FINSEQ_4, MSUALG_6, EXTENS_1; clusters MSUALG_6, FINSET_1, EXTENS_1, CANTOR_1, FUNCT_1, MSAFREE, MSUALG_1, MSUALG_2, MSUALG_9, PBOOLE, PRALG_1, PRALG_2, PRALG_3, STRUCT_0, CLOSURE2, PRELAMB, MSUALG_4, FINSEQ_1, RELSET_1, SUBSET_1, MEMBERED, ORDINAL2; 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; canceled; theorem :: EQUATION:5 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:6 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:7 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 set st i in I holds it.i = (F.i)"(A.i); end; theorem :: EQUATION:8 for A, B, C being ManySortedSet of I, F being ManySortedFunction of A, B holds F.:.:C is ManySortedSubset of B; theorem :: EQUATION:9 for A, B, C being ManySortedSet of I, F being ManySortedFunction of A, B holds F""C is ManySortedSubset of A; theorem :: EQUATION:10 for A, B being ManySortedSet of I, F being ManySortedFunction of A, B st F is "onto" holds F.:.:A = B; theorem :: EQUATION:11 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:12 for A being ManySortedSet of I, F being ManySortedFunction of I st A c= rngs F holds F.:.:(F""A) = A; theorem :: EQUATION:13 for f being ManySortedFunction of I for X being ManySortedSet of I holds f.:.:X c= rngs f; theorem :: EQUATION:14 for f being ManySortedFunction of I holds f.:.:(doms f) = rngs f; theorem :: EQUATION:15 for f being ManySortedFunction of I holds f""(rngs f) = doms f; theorem :: EQUATION:16 for A being ManySortedSet of I holds (id A).:.:A = A; theorem :: EQUATION:17 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; canceled; theorem :: EQUATION:19 for A being MSAlgebra over S holds A is MSSubAlgebra of the MSAlgebra of A; theorem :: EQUATION:20 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:21 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:22 for F being MSAlgebra-Family of I, S, B being MSSubAlgebra of product F for o being OperSymbol of S, x being set 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 means :: EQUATION:def 2 for x being set holds x in it iff ex C being strict MSSubAlgebra of A st x = C & B is MSSubAlgebra of C; end; definition let S be non void non empty ManySortedSign, A be MSAlgebra over S, B be MSSubAlgebra of A; cluster SuperAlgebraSet B -> non empty; end; definition let S be non empty non void ManySortedSign; cluster strict non-empty free MSAlgebra over S; end; definition let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty locally-finite MSSubset of A; cluster GenMSAlg X -> finitely-generated; end; definition let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S; cluster strict non-empty finitely-generated MSSubAlgebra of A; end; definition let S be non empty non void ManySortedSign, A be feasible MSAlgebra over S; cluster feasible MSSubAlgebra of A; end; theorem :: EQUATION:23 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:24 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:25 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:26 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:27 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:28 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:29 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 set 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:30 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; definition 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; definition 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; 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; synonym x '=' y; end; theorem :: EQUATION:31 e`1 in (the Sorts of TermAlg S).s; theorem :: EQUATION:32 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:33 for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e; theorem :: EQUATION:34 for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E; theorem :: EQUATION:35 U0, U1 are_isomorphic & U0 |= e implies U1 |= e; theorem :: EQUATION:36 U0, U1 are_isomorphic & U0 |= E implies U1 |= E; theorem :: EQUATION:37 for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e; theorem :: EQUATION:38 for R being MSCongruence of U0 st U0 |= E holds QuotMSAlg (U0,R) |= E; theorem :: EQUATION:39 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:40 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;

Back to top