:: More on Products of Many Sorted Algebras :: by Mariusz Giero :: :: Received April 29, 1996 :: Copyright (c) 1996-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, 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;