Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Product of Family of Universal Algebras

by

MML identifier: PRALG_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_2, FINSEQ_1, UNIALG_1, FUNCT_3, RELAT_1, FUNCT_1, MCART_1,
FUNCT_2, PARTFUN1, TARSKI, CQC_SIM1, UNIALG_2, BOOLE, ZF_REFLE, FINSEQ_4,
ORDINAL2, PBOOLE, FUNCOP_1, RLVECT_2, CARD_3, FUNCT_5, PRALG_1, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS,
NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, FUNCOP_1, MCART_1,
DOMAIN_1, PARTFUN1, FINSEQ_2, FUNCT_4, FUNCT_5, CARD_3, DTCONSTR,
UNIALG_1, UNIALG_2, PBOOLE;
constructors DOMAIN_1, FRAENKEL, FUNCT_4, FUNCT_5, CARD_3, DTCONSTR, UNIALG_2,
PBOOLE, MEMBERED, XBOOLE_0;
clusters SUBSET_1, UNIALG_1, PRVECT_1, PBOOLE, FUNCT_1, RELAT_1, RELSET_1,
STRUCT_0, FINSEQ_2, PARTFUN1, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1,
XBOOLE_0, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET;

begin

theorem :: PRALG_1:1
for D1,D2 be non empty set,n,m be Nat st n-tuples_on D1 = m-tuples_on D2
holds n = m;

::
:: Product of Two Algebras
::

reserve U1,U2,U3 for Universal_Algebra,
k,n,m,i for Nat,
x,y,z for set,
A,B for non empty set,
h1 for FinSequence of [:A,B:];

definition let A,B; let 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;
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:2
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:3
for A,B be non empty set holds rng (Inv (A,B)) = [:B,A:];

theorem :: PRALG_1:4
for A,B be non empty set holds Inv (A,B) is one-to-one;

theorem :: PRALG_1:5
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:6
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:7
U1,U2 are_similar implies [:U1,U2:],U1 are_similar;

theorem :: PRALG_1:8
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 natural number;
func TrivialOp(k) -> PartFunc of {{}}*,{{}}
means
:: PRALG_1:def 7
dom it = { k |-> {}} & rng it = {{}};
end;

definition
let k be natural number;
cluster TrivialOp k -> homogeneous quasi_total non empty;
end;

theorem :: PRALG_1:9
for k being natural number 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:10
for f be FinSequence of NAT holds TrivialOps(f) is homogeneous quasi_total
non-empty;

theorem :: PRALG_1:11
for f be FinSequence of NAT st f <> {} holds UAStr (#{{}},TrivialOps(f)#) is
strict Universal_Algebra;

definition let D be non empty set;
cluster non empty FinSequence of D;
cluster non empty 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 Function;
attr IT is 1-sorted-yielding means
:: PRALG_1:def 11
for x st x in dom IT holds IT.x is 1-sorted;
end;

definition
cluster Univ_Alg-yielding Function;
end;

definition
cluster Univ_Alg-yielding -> 1-sorted-yielding Function;
end;

definition
let I be set;
cluster 1-sorted-yielding ManySortedSet of I;
end;

definition let IT be Function;
attr IT is equal-signature means
:: PRALG_1:def 12
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;

definition
let J be non empty set;
cluster equal-signature Univ_Alg-yielding ManySortedSet of J;
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 J be set, A be 1-sorted-yielding ManySortedSet of J;
func Carrier A -> ManySortedSet of J means
:: PRALG_1:def 13
for j be set st j in J
ex R being 1-sorted st R = A.j & it.j = the carrier of R;
end;

definition
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 14
for j be Element of J holds it = signature (A.j);
end;

definition let IT be Function;
attr IT is Function-yielding means
:: PRALG_1:def 15
for x st x in dom IT holds IT.x is Function;
end;

definition
cluster Function-yielding Function;
end;

definition
let I be set;
cluster Function-yielding ManySortedSet of I;
end;

definition
let I be set;
mode ManySortedFunction of I is Function-yielding ManySortedSet of I;
end;

definition
let B be Function-yielding Function, j be set;
cluster B.j -> Function-like Relation-like;
end;

definition
let J be non empty set,
B be non-empty ManySortedSet of J,
j be Element of J;
cluster B.j -> non empty;
end;

definition
let F be Function-yielding Function, f be Function;
cluster F * f -> Function-yielding;
end;

definition
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 16
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 17
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;

definition
let J be non empty set,
B be non-empty ManySortedSet of J;
cluster equal-arity ManySortedOperation of B;
end;

theorem :: PRALG_1:12
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 18
dom it = dom F &
for x be set st x in dom F holds it.x = (F.x).(f.x);
end;

definition
let I be set,
f be ManySortedFunction of I,
x be ManySortedSet of I;
redefine func f..x -> ManySortedSet of I means
:: PRALG_1:def 19
for i be set st i in I holds for g be Function st g = f.i holds it.i = g.(x.i);
end;

definition
let J be non empty set,
B be non-empty ManySortedSet of J,
p be FinSequence of product B;
redefine func uncurry p -> ManySortedSet of [:dom p, J:];
end;

definition
let I,J be set,
X be ManySortedSet of [:I,J:];
redefine func ~X -> ManySortedSet of [:J,I:];
end;

definition
let X be set,
Y be non empty set,
f be ManySortedSet of [:X,Y:];
redefine func curry f -> ManySortedSet of X;
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 20
for j be Element of J holds it = arity (O.j);
end;

definition
let I be set,
A be ManySortedSet of I;
func EmptySeq(A) -> ManySortedSet of I means
:: PRALG_1:def 21
for i be set st i in I holds it.i = {}(A.i);
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..(EmptySeq B) ) &
( 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 natural number;
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;

```