:: Equations in Many Sorted Algebras
:: by Artur Korni{\l}owicz
::
:: Received May 30, 1997
:: Copyright (c) 1997-2019 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, NUMERALS;
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;