:: More on Products of Many Sorted Algebras
:: by Mariusz Giero
::
:: Received April 29, 1996
:: Copyright (c) 1996-2016 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, PBOOLE, STRUCT_0, MSUALG_1, SUBSET_1, PRALG_2, EQREL_1,
FUNCT_1, CARD_3, RELAT_1, SETFAM_1, RLVECT_2, FUNCT_6, TARSKI, FUNCT_2,
MARGREL1, UNIALG_2, FUNCT_5, FUNCOP_1, FINSEQ_4, PARTFUN1, MSUALG_3,
MEMBER_1, ARYTM_3, WELLORD1, PRALG_3;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, STRUCT_0, FUNCT_2, FUNCOP_1, EQREL_1, FUNCT_5, FUNCT_6, CARD_3,
PBOOLE, MSUALG_1, MSUALG_3, PRALG_2, PRALG_1, MSUALG_2;
constructors EQREL_1, PRALG_1, PRALG_2, MSUALG_3, RELSET_1, FUNCT_5;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCOP_1, EQREL_1, PBOOLE, STRUCT_0, MSUALG_1, PRALG_2, MSUALG_3, CARD_3,
RELSET_1;
requirements BOOLE, SUBSET;
begin ::Preliminaries
::-------------------------------------------------------------------
:: Acknowledgements:
:: ================
::
:: I would like to thank Professor A.Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------
reserve I for non empty set,
J for ManySortedSet of I,
S for non void non empty ManySortedSign,
i for Element of I,
c for set,
A for MSAlgebra-Family of I,S,
EqR for Equivalence_Relation of I,
U0,U1,U2 for MSAlgebra over S,
s for SortSymbol of S,
o for OperSymbol of S,
f for Function;
registration
let I be set, S;
let AF be MSAlgebra-Family of I,S;
cluster product AF -> non-empty;
end;
registration
let X be with_non-empty_elements set;
cluster id X -> non-empty;
end;
theorem :: PRALG_3:1
for f,F being Function, A being set st f in product F holds f|A
in product(F|A);
theorem :: PRALG_3:2
for A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non
empty Subset of I, Aa be MSAlgebra-Family of a,S st A|a = Aa holds Carrier(Aa,s
) = (Carrier(A,s))|a;
theorem :: PRALG_3:3
for i be set, I be non empty set, EqR be Equivalence_Relation of
I, c1,c2 be Element of Class EqR st i in c1 & i in c2 holds c1 = c2;
theorem :: PRALG_3:4
for D being non empty set for F being ManySortedFunction of D for C
being with_common_domain functional non empty set st C = rng F for d being
Element of D,e being set st e in DOM C holds F.d.e = (commute F).e.d;
begin :: Constants of Many Sorted Algebras
definition
let S,U0;
let o be OperSymbol of S;
func const(o,U0) -> set equals
:: PRALG_3:def 1
Den(o,U0).{};
end;
theorem :: PRALG_3:5
the_arity_of o = {} & Result(o,U0) <> {} implies const(o,U0) in Result(o,U0);
theorem :: PRALG_3:6
(the Sorts of U0).s <> {} implies Constants(U0,s) = { const(o,U0)
where o is Element of the carrier' of S : the_result_sort_of o = s &
the_arity_of o = {} };
theorem :: PRALG_3:7
the_arity_of o = {} implies (commute (OPER A)).o in Funcs(I,Funcs
({{}}, union the set of all Result(o,A.i9) where i9 is Element of I));
theorem :: PRALG_3:8
the_arity_of o = {} implies const(o,product A) in Funcs(I, union
the set of all Result(o,A.i9) where i9 is Element of I);
registration
let S,I,o,A;
cluster const (o,product A) -> Relation-like Function-like;
end;
theorem :: PRALG_3:9
for o be OperSymbol of S st the_arity_of o = {} holds (const (o,
product A)).i = const (o,A.i);
theorem :: PRALG_3:10
the_arity_of o = {} & dom f = I & (for i be Element of I holds f.i =
const(o,A.i)) implies f = const(o,product A);
theorem :: PRALG_3:11
for e be Element of Args(o,U1) st e = {} & the_arity_of o = {} &
Args(o,U1) <> {} & Args(o,U2) <> {} for F be ManySortedFunction of U1,U2 holds
F#e = {};
begin :: Properties of Arguments of operations in Many Sorted Algebras
theorem :: PRALG_3:12
for U1,U2 be non-empty MSAlgebra over S for F be
ManySortedFunction of U1,U2 for x be Element of Args(o,U1) holds x in product
doms (F*the_arity_of o);
theorem :: PRALG_3:13
for U1,U2 be non-empty MSAlgebra over S for F be
ManySortedFunction of U1,U2 for x be Element of Args(o,U1) for n be set st n in
dom (the_arity_of o) holds (F#x).n = F.((the_arity_of o)/.n).(x.n);
theorem :: PRALG_3:14
for x be Element of Args(o,product A) holds x in Funcs (dom (
the_arity_of o),Funcs (I,union the set of all
(the Sorts of A.i9).s9 where i9 is Element of
I,s9 is Element of (the carrier of S) ));
theorem :: PRALG_3:15
for x be Element of Args(o,product A) for n be set st n in dom (
the_arity_of o) holds x.n in product Carrier(A,(the_arity_of o)/.n);
theorem :: PRALG_3:16
for i be Element of I for n be set st n in dom(the_arity_of o)
for s be SortSymbol of S st s = (the_arity_of o).n for y be Element of Args(o,
product A) for g be Function st g = y.n holds g.i in (the Sorts of A.i).s;
theorem :: PRALG_3:17
for y be Element of Args(o,product A) st (the_arity_of o) <> {}
holds (commute y) in product doms (A?.o);
theorem :: PRALG_3:18
for y be Element of Args(o,product A) st the_arity_of o <> {}
holds y in dom (Commute Frege(A?.o));
theorem :: PRALG_3:19
for I be set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S for x be Element of Args(o,
product A) holds Den(o,product A).x in product Carrier(A,the_result_sort_of o);
theorem :: PRALG_3:20
for I,S,A,i for o be OperSymbol of S st (the_arity_of o) <> {}
for U1 be non-empty MSAlgebra over S for x be Element of Args(o,product A)
holds (commute x).i is Element of Args(o,A.i);
theorem :: PRALG_3:21
for I,S,A,i,o for x be Element of Args(o,product A) for n be set
st n in dom(the_arity_of o) for f be Function st f = x.n holds ((commute x).i).
n = f.i;
theorem :: PRALG_3:22
for o be OperSymbol of S st (the_arity_of o) <> {} for y be
Element of Args(o,product A), i9 be Element of I for g be Function st g = Den(o
,product A).y holds g.i9 = Den(o,A.i9).((commute y).i9);
begin :: The Projection of Family of Many Sorted Algebras
definition
let I,S;
let A be MSAlgebra-Family of I,S, i be Element of I;
func proj(A,i) -> ManySortedFunction of product A,A.i means
:: PRALG_3:def 2
for s be Element of S holds it.s = proj (Carrier(A,s), i);
end;
theorem :: PRALG_3:23
for x be Element of Args(o,product A) st the_arity_of o <> {}
for i be Element of I holds proj(A,i)#x = (commute x).i;
theorem :: PRALG_3:24
for i be Element of I for A be MSAlgebra-Family of I,S holds proj(A,i)
is_homomorphism product A,A.i;
theorem :: PRALG_3:25
for U1 be non-empty MSAlgebra over S for F being
ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds F
in Funcs(I,Funcs(the carrier of S, the set of all
F.i9.s1 where s1 is SortSymbol of S,i9 is
Element of I )) & (commute F).s.i = F.i.s;
theorem :: PRALG_3:26
for U1 be non-empty MSAlgebra over S for F being
ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds (
commute F).s in Funcs(I,Funcs((the Sorts of U1).s, union the set of all
(the Sorts of A.i9).
s1 where i9 is Element of I,s1 is SortSymbol of S ));
theorem :: PRALG_3:27
for U1 be non-empty MSAlgebra over S for F being
ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for F9 be
ManySortedFunction of U1,A.i st F9 = F.i for x be set st x in (the Sorts of U1)
.s for f be Function st f = (commute((commute F).s)).x holds f.i = F9.s.x;
theorem :: PRALG_3:28
for U1 be non-empty MSAlgebra over S for F being
ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for x be
set st x in (the Sorts of U1).s holds (commute ((commute F).s)).x in product (
Carrier(A,s));
theorem :: PRALG_3:29
for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of
I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
F1 = F.i & F1 is_homomorphism U1,A.i) holds ex H being ManySortedFunction of U1
,(product A) st H is_homomorphism U1,(product A) & for i be Element of I holds
proj(A,i) ** H = F.i;
begin :: The Class of Family of Many Sorted Algebras
definition
let I,J,S;
mode MSAlgebra-Class of S,J -> ManySortedSet of I means
:: PRALG_3:def 3
for i be set st i in I holds it.i is MSAlgebra-Family of J.i,S;
end;
definition
let I,S,A,EqR;
func A / EqR -> MSAlgebra-Class of S,id Class EqR means
:: PRALG_3:def 4
for c st c in Class EqR holds it.c = A|c;
end;
definition
let I,S;
let J be non-empty ManySortedSet of I;
let C be MSAlgebra-Class of S,J;
func product C -> MSAlgebra-Family of I,S means
:: PRALG_3:def 5
for i st i in I ex Ji
be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & it.i
= product Cs;
end;
theorem :: PRALG_3:30
for A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I
holds product A, product (product (A/EqR)) are_isomorphic;