The abstract of the Mizar article:

Product of Family of Universal Algebras

by

Beata Madras

Received October 12, 1993

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;