:: Product of Family of Universal Algebras :: by Beata Madras :: :: Received October 12, 1993 :: Copyright (c) 1993-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 UNIALG_1, NAT_1, XBOOLE_0, FINSEQ_1, ZFMISC_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, FINSEQ_2, SUBSET_1, TARSKI, NUMBERS, STRUCT_0, CQC_SIM1, UNIALG_2, PBOOLE, FUNCOP_1, RLVECT_2, CARD_3, CARD_1, FINSEQ_4, FUNCT_5, PRALG_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, BINOP_1, FUNCOP_1, MCART_1, DOMAIN_1, PARTFUN1, FINSEQ_2, FUNCT_4, FUNCT_5, CARD_3, MARGREL1, DTCONSTR, UNIALG_1, UNIALG_2, PBOOLE; constructors BINOP_1, DOMAIN_1, FUNCT_4, FUNCT_5, CARD_3, PBOOLE, UNIALG_2, DTCONSTR, STRUCT_0, RELSET_1, XTUPLE_0, NUMBERS; registrations SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_2, CARD_3, PBOOLE, STRUCT_0, UNIALG_1, CARD_1, RELSET_1, MARGREL1, XTUPLE_0; requirements BOOLE, SUBSET; begin :: :: Product of Two Algebras :: reserve U1,U2,U3 for Universal_Algebra, n,m for Nat, x,y,z for object, A,B for non empty set, h1 for FinSequence of [:A,B:]; definition let A,B,h1; redefine func pr1 h1 -> FinSequence of A means :: PRALG_1:def 1 len it = len h1 & for n st n in dom it holds it.n = (h1.n)`1; redefine func pr2 h1 -> FinSequence of B means :: PRALG_1:def 2 len it = len h1 & for n st n in dom it holds it.n = (h1.n)`2; end; definition let A,B; let f1 be homogeneous quasi_total non empty PartFunc of A*,A; let f2 be homogeneous quasi_total non empty PartFunc of B*,B; assume arity (f1) = arity (f2); func [[:f1,f2:]] -> homogeneous quasi_total non empty PartFunc of ([:A,B:])* ,[:A,B:] means :: PRALG_1:def 3 dom it = (arity f1)-tuples_on [:A,B:] & for h be FinSequence of [:A,B:] st h in dom it holds it.h = [f1.pr1 h,f2.pr2 h]; end; reserve h1 for homogeneous quasi_total non empty PartFunc of (the carrier of U1)*,the carrier of U1, h2 for homogeneous quasi_total non empty PartFunc of ( the carrier of U2)*,the carrier of U2; definition let U1,U2; assume U1,U2 are_similar; func Opers(U1,U2) -> PFuncFinSequence of [:the carrier of U1,the carrier of U2:] means :: PRALG_1:def 4 len it = len the charact of(U1) & for n st n in dom it holds for h1,h2 st h1=(the charact of(U1)).n & h2=(the charact of(U2)).n holds it.n = [[:h1,h2:]]; end; theorem :: PRALG_1:1 U1,U2 are_similar implies UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1,U2) #) is strict Universal_Algebra; definition let U1,U2; assume U1,U2 are_similar; func [:U1,U2:] -> strict Universal_Algebra equals :: PRALG_1:def 5 UAStr (# [:the carrier of U1,the carrier of U2:], Opers(U1,U2) #); end; definition let A,B be non empty set; func Inv (A,B) -> Function of [:A,B:],[:B,A:] means :: PRALG_1:def 6 for a be Element of [:A,B:] holds it.a = [a`2,a`1]; end; theorem :: PRALG_1:2 for A,B be non empty set holds rng (Inv (A,B)) = [:B,A:]; theorem :: PRALG_1:3 for A,B be non empty set holds Inv (A,B) is one-to-one; theorem :: PRALG_1:4 U1,U2 are_similar implies Inv (the carrier of U1,the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:]; theorem :: PRALG_1:5 U1,U2 are_similar implies for o1 be operation of U1,o2 be operation of U2,o be operation of [:U1,U2:], n be Nat st o1 = (the charact of U1).n & o2 = (the charact of U2).n & o = (the charact of [:U1,U2:]).n & n in dom the charact of(U1) holds arity o = arity o1 & arity o = arity o2 & o = [[: o1,o2:]]; theorem :: PRALG_1:6 U1,U2 are_similar implies [:U1,U2:],U1 are_similar; theorem :: PRALG_1:7 for U1,U2,U3,U4 be Universal_Algebra st U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar holds [:U1,U3:] is SubAlgebra of [:U2,U4:] ; begin :: :: Trivial Algebra :: definition let k be Nat; func TrivialOp(k) -> PartFunc of {{}}*,{{}} means :: PRALG_1:def 7 dom it = { k |-> {} } & rng it = {{}}; end; registration let k be Nat; cluster TrivialOp k -> homogeneous quasi_total non empty; end; theorem :: PRALG_1:8 for k being Nat holds arity TrivialOp(k) = k; definition let f be FinSequence of NAT; func TrivialOps(f) -> PFuncFinSequence of {{}} means :: PRALG_1:def 8 len it = len f & for n st n in dom it for m st m = f.n holds it.n=TrivialOp(m); end; theorem :: PRALG_1:9 for f be FinSequence of NAT holds TrivialOps(f) is homogeneous quasi_total non-empty; theorem :: PRALG_1:10 for f be FinSequence of NAT st f <> {} holds UAStr (#{{}}, TrivialOps(f)#) is strict Universal_Algebra; registration let D be non empty set; cluster non empty for Element of D*; end; definition let f be non empty FinSequence of NAT; func Trivial_Algebra(f) -> strict Universal_Algebra equals :: PRALG_1:def 9 UAStr (#{{}}, TrivialOps(f)#); end; begin :: :: Product of Universal Algebras :: definition let IT be Function; attr IT is Univ_Alg-yielding means :: PRALG_1:def 10 for x st x in dom IT holds IT.x is Universal_Algebra; end; definition let IT be Relation; attr IT is 1-sorted-yielding means :: PRALG_1:def 11 for x st x in rng IT holds x is 1-sorted; end; definition let IT be Function; redefine attr IT is 1-sorted-yielding means :: PRALG_1:def 12 for x st x in dom IT holds IT.x is 1-sorted; end; registration cluster Univ_Alg-yielding for Function; end; registration cluster Univ_Alg-yielding -> 1-sorted-yielding for Function; end; registration let I be set; cluster 1-sorted-yielding for ManySortedSet of I; end; definition let IT be Function; attr IT is equal-signature means :: PRALG_1:def 13 for x,y st x in dom IT & y in dom IT holds for U1,U2 st U1 = IT.x & U2 = IT.y holds signature U1 = signature U2; end; registration let J be non empty set; cluster equal-signature Univ_Alg-yielding for ManySortedSet of J; end; definition let A be 1-sorted-yielding non empty Function, j be Element of dom A; redefine func A.j -> 1-sorted; end; definition let J be non empty set, A be 1-sorted-yielding ManySortedSet of J, j be Element of J; redefine func A.j -> 1-sorted; end; definition let J be non empty set, A be Univ_Alg-yielding ManySortedSet of J, j be Element of J; redefine func A.j -> Universal_Algebra; end; definition let A be 1-sorted-yielding Function; func Carrier A -> Function means :: PRALG_1:def 14 dom it = dom A & for j be set st j in dom A ex R being 1-sorted st R = A.j & it.j = the carrier of R; end; definition let J be set, A be 1-sorted-yielding ManySortedSet of J; redefine func Carrier A -> ManySortedSet of J means :: PRALG_1:def 15 for j be set st j in J ex R being 1-sorted st R = A.j & it.j = the carrier of R; end; registration let J be non empty set, A be Univ_Alg-yielding ManySortedSet of J; cluster Carrier A -> non-empty; end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J; func ComSign A -> FinSequence of NAT means :: PRALG_1:def 16 for j be Element of J holds it = signature (A.j); end; registration let J be non empty set, B be non-empty ManySortedSet of J; cluster product B -> non empty; end; definition let J be non empty set, B be non-empty ManySortedSet of J; mode ManySortedOperation of B -> ManySortedFunction of J means :: PRALG_1:def 17 for j be Element of J holds it.j is homogeneous quasi_total non empty PartFunc of (B.j)*,B.j; end; definition let J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B, j be Element of J; redefine func O.j -> homogeneous quasi_total non empty PartFunc of (B.j)*,B.j; end; definition let IT be Function; attr IT is equal-arity means :: PRALG_1:def 18 for x,y be set st x in dom IT & y in dom IT for f,g be Function st IT.x = f & IT.y = g holds for n,m be Nat for X,Y be non empty set st dom f = n-tuples_on X & dom g = m-tuples_on Y holds for o1 be homogeneous quasi_total non empty PartFunc of X*,X, o2 be homogeneous quasi_total non empty PartFunc of Y*,Y st f = o1 & g = o2 holds arity o1 = arity o2; end; registration let J be non empty set, B be non-empty ManySortedSet of J; cluster equal-arity for ManySortedOperation of B; end; theorem :: PRALG_1:11 for J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B holds O is equal-arity iff for i,j be Element of J holds arity (O.i) = arity (O.j); definition let F be Function-yielding Function, f be Function; func F..f -> Function means :: PRALG_1:def 19 dom it = dom F /\ dom f & for x be set st x in dom it holds it.x = (F.x).(f.x); end; registration let I be set, f be (ManySortedFunction of I), x be ManySortedSet of I; cluster f..x -> I-defined; end; registration let I be set, f be (ManySortedFunction of I), x be ManySortedSet of I; cluster f..x -> total for I-defined Function; end; definition let I be set, f be (ManySortedFunction of I), x be ManySortedSet of I; redefine func f..x means :: PRALG_1:def 20 dom it = I & for i be set st i in I holds for g be Function st g = f.i holds it.i = g.(x.i); end; registration let J be non empty set, B be non-empty ManySortedSet of J, p be FinSequence of product B; cluster uncurry p -> [:dom p, J:]-defined; end; registration let J be non empty set, B be non-empty ManySortedSet of J, p be FinSequence of product B; cluster uncurry p -> total for [:dom p, J:]-defined Function; end; registration let I,J be set, X be ManySortedSet of [:I,J:]; cluster ~X -> [:J,I:]-defined; end; registration let I,J be set, X be ManySortedSet of [:I,J:]; cluster ~X -> total for [:J,I:]-defined Function; end; registration let X be set, Y be non empty set, f be ManySortedSet of [:X,Y:]; cluster curry f -> X-defined; end; registration let X be set, Y be non empty set, f be ManySortedSet of [:X,Y:]; cluster curry f -> total for X-defined Function; end; definition let J be non empty set, B be non-empty ManySortedSet of J, O be equal-arity ManySortedOperation of B; func ComAr(O) -> Nat means :: PRALG_1:def 21 for j be Element of J holds it = arity (O .j); end; definition let J be non empty set, B be non-empty ManySortedSet of J, O be equal-arity ManySortedOperation of B; func [[: O :]] -> homogeneous quasi_total non empty PartFunc of (product B)* ,(product B) means :: PRALG_1:def 22 dom it = (ComAr O)-tuples_on (product B) & for p being Element of (product B)* st p in dom it holds ( dom p = {} implies it.p = O..( EmptyMS J) ) & ( dom p <> {} implies for Z be non empty set, w be ManySortedSet of [:J,Z:] st Z = dom p & w = ~uncurry p holds it.p = O..(curry w )); end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J, n be Nat; assume n in dom (ComSign A); func ProdOp(A,n) -> equal-arity ManySortedOperation of Carrier A means :: PRALG_1:def 23 for j be Element of J holds for o be operation of A.j st (the charact of A.j).n = o holds it.j = o; end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J; func ProdOpSeq(A) -> PFuncFinSequence of product Carrier A means :: PRALG_1:def 24 len it = len (ComSign A) & for n st n in dom it holds it.n = [[: ProdOp(A,n) :]]; end; definition let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J; func ProdUnivAlg A -> strict Universal_Algebra equals :: PRALG_1:def 25 UAStr (# product Carrier A, ProdOpSeq(A) #); end;