The abstract of the Mizar article:

The Correspondence Between Homomorphisms of Universal Algebra \& Many Sorted Algebra

by

Adam Grabowski

Received December 13, 1994

MML identifier: MSUHOM_1

[ Mizar article, MML identifier index ]

environ

 vocabulary UNIALG_1, FUNCT_1, RELAT_1, FINSEQ_1, PRALG_1, PBOOLE, TDGROUP,
      CARD_3, FINSEQ_2, MSUALG_1, BOOLE, CAT_1, AMI_1, ZF_REFLE, CQC_SIM1,
      FUNCOP_1, UNIALG_2, QC_LANG1, ALG_1, GROUP_6, MSUALG_3, MSUHOM_1,
      FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, RELAT_1, FUNCT_1,
      RELSET_1, STRUCT_0, PARTFUN1, FUNCT_2, PBOOLE, CARD_3, CQC_LANG,
      UNIALG_1, FINSEQ_1, UNIALG_2, PRALG_1, FINSEQ_2, FINSEQ_4, TOPREAL1,
      ALG_1, MSUALG_3, PRE_CIRC, MSUALG_1;
 constructors XREAL_0, CQC_LANG, ALG_1, MSUALG_3, PRE_CIRC, FINSEQ_4, FINSEQOP,
      XCMPLX_0, MEMBERED, XBOOLE_0;
 clusters MSUALG_1, MSUALG_3, PRE_CIRC, FUNCT_1, RELSET_1, STRUCT_0, CQC_LANG,
      ARYTM_3, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0, SUBSET_1,
      NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE;


begin

 reserve U1,U2,U3 for Universal_Algebra,
         m,n for Nat,
         a for set,
         A for non empty set,
         h for Function of U1,U2;

theorem :: MSUHOM_1:1
 for f,g be Function, C be set st rng f c= C holds (g|C)*f = g*f;

theorem :: MSUHOM_1:2
 for I be set, C be Subset of I holds C* c= I*;

theorem :: MSUHOM_1:3
   for f be Function, C be set st f is Function-yielding holds
  f|C is Function-yielding;

theorem :: MSUHOM_1:4
 for I be set, C be Subset of I, M be ManySortedSet of I holds (M|C)# = M#|(C*)
;

definition let A, n; let a be Element of A;
 redefine func n |-> a -> FinSequence of A;
end;

definition
  let S,S' be non empty ManySortedSign;
  pred S <= S' means
:: MSUHOM_1:def 1
   the carrier of S c= the carrier of S' &
   the OperSymbols of S c= the OperSymbols of S' &
   (the Arity of S')|the OperSymbols of S = the Arity of S &
   (the ResultSort of S')|the OperSymbols of S = the ResultSort of S;
  reflexivity;
end;

theorem :: MSUHOM_1:5
   for S,S',S'' be non empty ManySortedSign st S <= S' & S' <= S'' holds S <=
S'';

theorem :: MSUHOM_1:6
   for S,S' be strict non empty ManySortedSign st S <= S' & S' <= S holds S =
S';

theorem :: MSUHOM_1:7
   for g be Function, a be Element of A
  for k be Nat st 1 <= k & k <= n holds
    (a .--> g).((n |-> a)/.k) = g;

theorem :: MSUHOM_1:8
 for I be set,I0 be Subset of I, A,B be ManySortedSet of I,
     F be ManySortedFunction of A,B
  for A0,B0 be ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds
    F|I0 is ManySortedFunction of A0,B0;

definition let S,S' be strict non void non empty ManySortedSign;
 let A be non-empty strict MSAlgebra over S';
 assume  S <= S';
 func A Over S -> non-empty strict MSAlgebra over S means
:: MSUHOM_1:def 2
  the Sorts of it = (the Sorts of A)|the carrier of S &
  the Charact of it = (the Charact of A)|the OperSymbols of S;
end;

theorem :: MSUHOM_1:9
 for S be strict non void non empty ManySortedSign,
     A be non-empty strict MSAlgebra over S holds A = A Over S;

theorem :: MSUHOM_1:10
 for U1,U2 st U1,U2 are_similar holds MSSign U1 = MSSign U2;

definition let U1,U2 be Universal_Algebra, h be Function of U1,U2;
 assume   MSSign U1 = MSSign U2;
 func MSAlg h -> ManySortedFunction of MSAlg U1, ((MSAlg U2) Over MSSign U1)
 equals
:: MSUHOM_1:def 3
{0} --> h;
end;

theorem :: MSUHOM_1:11
 for U1,U2,h st U1,U2 are_similar
  for o be OperSymbol of MSSign U1
    holds ((MSAlg h).(the_result_sort_of o)) = h;

theorem :: MSUHOM_1:12
 for o be OperSymbol of MSSign U1 holds
  Den(o,MSAlg U1) = (the charact of U1).o;

theorem :: MSUHOM_1:13
 for o be OperSymbol of MSSign U1 holds
  Den(o,MSAlg U1) is operation of U1;

theorem :: MSUHOM_1:14
 for o be OperSymbol of MSSign U1
  for y be Element of Args(o,MSAlg U1) holds
    y is FinSequence of the carrier of U1;

theorem :: MSUHOM_1:15
 for U1,U2,h st U1,U2 are_similar
  for o be OperSymbol of MSSign U1,y be Element of Args(o,MSAlg U1)
      holds (MSAlg h)#y = h * y;

theorem :: MSUHOM_1:16
 h is_homomorphism U1,U2 implies
  MSAlg h is_homomorphism MSAlg U1,(MSAlg U2 Over MSSign U1);

theorem :: MSUHOM_1:17
 U1,U2 are_similar implies MSAlg h is ManySortedSet of {0};

theorem :: MSUHOM_1:18
 h is_epimorphism U1, U2 implies
  MSAlg h is_epimorphism MSAlg U1, (MSAlg U2 Over MSSign U1);

theorem :: MSUHOM_1:19
 h is_monomorphism U1, U2 implies
  MSAlg h is_monomorphism MSAlg U1,(MSAlg U2 Over MSSign U1);

theorem :: MSUHOM_1:20
   h is_isomorphism U1,U2 implies
  MSAlg h is_isomorphism MSAlg U1,(MSAlg U2 Over MSSign U1);

theorem :: MSUHOM_1:21
 for U1,U2,h st U1,U2 are_similar holds
  MSAlg h is_homomorphism MSAlg U1,(MSAlg U2 Over MSSign U1) implies
   h is_homomorphism U1,U2;

theorem :: MSUHOM_1:22
 for U1,U2,h st U1, U2 are_similar holds
  MSAlg h is_epimorphism MSAlg U1, (MSAlg U2 Over MSSign U1) implies
   h is_epimorphism U1, U2;

theorem :: MSUHOM_1:23
 for U1, U2, h st U1, U2 are_similar holds
  MSAlg h is_monomorphism MSAlg U1, (MSAlg U2 Over MSSign U1) implies
   h is_monomorphism U1, U2;

theorem :: MSUHOM_1:24
   for U1, U2, h st U1, U2 are_similar holds
  MSAlg h is_isomorphism MSAlg U1, (MSAlg U2 Over MSSign U1) implies
   h is_isomorphism U1, U2;

theorem :: MSUHOM_1:25
   MSAlg (id the carrier of U1) = (id the Sorts of MSAlg U1);

theorem :: MSUHOM_1:26
   for U1,U2,U3 st U1,U2 are_similar & U2,U3 are_similar
  for h1 be Function of U1,U2, h2 be Function of U2,U3 holds
   (MSAlg h2) ** (MSAlg h1) = MSAlg (h2*h1);