:: The Correspondence Between Homomorphisms of Universal Algebra &
:: Many Sorted Algebra
::  by Adam Grabowski
::
:: Received December 13, 1994
:: Copyright (c) 1994-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, FUNCT_1, RELAT_1, TARSKI, SUBSET_1,
      FINSEQ_1, FUNCOP_1, PBOOLE, CARD_3, MSUALG_1, XXREAL_0, STRUCT_0,
      FINSEQ_2, PARTFUN1, CQC_SIM1, CARD_1, UNIALG_2, MARGREL1, NUMBERS,
      MSUALG_3, MEMBER_1, MSUHOM_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
      PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, CARD_3, FUNCOP_1, FINSEQ_1,
      STRUCT_0, UNIALG_1, UNIALG_2, FINSEQ_2, ALG_1, MSUALG_3, MSUALG_1,
      XXREAL_0;
 constructors FINSEQOP, ALG_1, MSUALG_3, XREAL_0, RELSET_1, NAT_1, NUMBERS;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
      XREAL_0, PRE_CIRC, STRUCT_0, MSUALG_1, MSUALG_3, RELAT_1, PBOOLE,
      FINSEQ_1;
 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 S,S9 be non empty ManySortedSign;
  pred S <= S9 means
:: MSUHOM_1:def 1

  the carrier of S c= the carrier of S9 & the
carrier' of S c= the carrier' of S9 & (the Arity of S9)|the carrier' of S = the
  Arity of S & (the ResultSort of S9)|the carrier' of S = the ResultSort of S;
  reflexivity;
end;

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

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

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,S9 be strict non void non empty ManySortedSign;
  let A be non-empty strict MSAlgebra over S9;
  assume
 S <= S9;
  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 carrier' 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 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 implies MSAlg h is_epimorphism MSAlg U1,
  (MSAlg U2 Over MSSign U1);

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

theorem :: MSUHOM_1:20
  h is_isomorphism 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;

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;

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
;

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;

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);