:: Homomorphisms of Many Sorted Algebras
::  by Ma{\l}gorzata Korolkiewicz
::
:: Received April 25, 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 STRUCT_0, XBOOLE_0, MSUALG_1, NAT_1, PBOOLE, SUBSET_1, FUNCT_1,
      RELAT_1, MEMBER_1, CARD_3, MARGREL1, TARSKI, FUNCT_6, NUMBERS, FINSEQ_4,
      PARTFUN1, WELLORD1, GROUP_6, MSUALG_2, UNIALG_2, MSUALG_3;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
      RELAT_1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3,
      FUNCT_6, STRUCT_0, PRALG_1, MSUALG_1, MSUALG_2, PRALG_2;
 constructors PRALG_1, MSUALG_2, PRALG_2, RELSET_1, FINSEQ_2, XTUPLE_0;
 registrations FUNCT_2, FUNCOP_1, CARD_3, FUNCT_1, STRUCT_0, MSUALG_1,
      MSUALG_2, ORDINAL1, RELAT_1, RELSET_1, PBOOLE, FINSEQ_1;
 requirements BOOLE, SUBSET;


begin

reserve S for non void non empty ManySortedSign,
  U1,U2 for MSAlgebra over S,
  o for OperSymbol of S,
  n for Nat;

::    PRELIMINARIES - MANY SORTED FUNCTIONS

definition
  let I be non empty set, A,B be ManySortedSet of I, F be ManySortedFunction
  of A,B, i be Element of I;
  redefine func F.i -> Function of A.i,B.i;
end;

definition
  let S be non empty ManySortedSign;
  let U1,U2 be MSAlgebra over S;
  mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1,
    the Sorts of U2;
end;

definition
  let I be set,A be ManySortedSet of I;
  func id A -> ManySortedFunction of A,A means
:: MSUALG_3:def 1

  for i be set st i in I holds it.i = id (A.i);
end;

definition
  let IT be Function;
  attr IT is "1-1" means
:: MSUALG_3:def 2

  for i be set, f be Function st i in dom IT & IT.i = f holds f is one-to-one;
end;

registration
  let I be set;
  cluster "1-1" for ManySortedFunction of I;
end;

theorem :: MSUALG_3:1
  for I be set,F be ManySortedFunction of I holds F is "1-1" iff
  for i be set st i in I holds F.i is one-to-one;

definition
  let I be set, A,B be ManySortedSet of I;
  let IT be ManySortedFunction of A,B;
  attr IT is "onto" means
:: MSUALG_3:def 3

  for i be set st i in I holds rng(IT.i) = B.i;
end;

theorem :: MSUALG_3:2
  for I be set, A,B,C be ManySortedSet of I, F be
ManySortedFunction of A,B, G be ManySortedFunction of B,C holds dom (G ** F) =
  I & for i be set st i in I holds (G**F).i = (G.i)*(F.i);

definition
  let I be set, A be ManySortedSet of I, B,C be non-empty ManySortedSet of I,
  F be ManySortedFunction of A,B, G be ManySortedFunction of B,C;
  redefine func G**F -> ManySortedFunction of A,C;
end;

theorem :: MSUALG_3:3
  for I be set,A,B be ManySortedSet of I, F be ManySortedFunction of A,B
  holds F**(id A) = F;

theorem :: MSUALG_3:4
  for I be set, A,B be ManySortedSet of I for F be
  ManySortedFunction of A, B holds (id B)**F = F;

definition
  let I be set, A,B be ManySortedSet of I, F be ManySortedFunction of A,B;
  assume that
 F is "1-1" and
 F is "onto";
  func F"" -> ManySortedFunction of B,A means
:: MSUALG_3:def 4

  for i be set st i in I holds it.i = (F.i)";
end;

theorem :: MSUALG_3:5
  for I be set,A,B be non-empty ManySortedSet of I, H be
ManySortedFunction of A,B, H1 be ManySortedFunction of B,A st H is "1-1" "onto"
  & H1 = H"" holds H**H1 = id B & H1**H = id A;

registration
  let S;
  let U1 be non-empty MSAlgebra over S;
  let o;
  cluster Args(o,U1) -> functional;
end;

begin :: Homomorphisms of Many Sorted Algebras

theorem :: MSUALG_3:6
  for U1 being MSAlgebra over S
  for x be Function st x in Args(o,U1) holds
  dom x = dom the_arity_of o &
  for y be set st y in dom ((the Sorts of U1) * (the_arity_of o)) holds
    x.y in ((the Sorts of U1) * (the_arity_of o)).y;

definition
  let S;
  let U1,U2 be MSAlgebra over S;
  let o;
  let F be ManySortedFunction of U1,U2;
  let x be Element of Args(o,U1);
  assume that
 Args(o,U1) <> {} and
 Args(o,U2) <> {};
  func F # x -> Element of Args(o,U2) equals
:: MSUALG_3:def 5

  (Frege(F*the_arity_of o)).
  x;
end;

definition
  let S;
  let U1,U2 be non-empty MSAlgebra over S;
  let o;
  let F be ManySortedFunction of U1,U2;
  let x be Element of Args(o,U1);
  redefine func F # x means
:: MSUALG_3:def 6
  for n st n in dom x holds it.n = (F.((the_arity_of o)/.n)).(x.n);
end;

theorem :: MSUALG_3:7
  for S,o for U1 being MSAlgebra over S st Args(o,U1) <> {}
  for x be Element of Args(o,U1) holds x = ((id (the Sorts of U1))#x);

theorem :: MSUALG_3:8
  for U1,U2,U3 being non-empty MSAlgebra over S
  for H1 be ManySortedFunction of U1,U2,
      H2 be ManySortedFunction of U2,U3,
      x be Element of Args(o,U1) holds (H2**H1)#x = H2#(H1#x);

definition
  let S;
  let U1,U2 be MSAlgebra over S;
  let F be ManySortedFunction of U1,U2;
  pred F is_homomorphism U1,U2 means
:: MSUALG_3:def 7
  for o be OperSymbol of S st Args(o,U1) <> {}
  for x be Element of Args(o,U1) holds
  (F.(the_result_sort_of o)).(Den (o,U1).x) = Den(o,U2).(F#x);
end;

theorem :: MSUALG_3:9
  for U1 being MSAlgebra over S holds
    id (the Sorts of U1) is_homomorphism U1,U1;

theorem :: MSUALG_3:10
  for U1,U2,U3 being non-empty MSAlgebra over S for H1 be
  ManySortedFunction of U1,U2, H2 be ManySortedFunction of U2,U3 st H1
is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism
  U1,U3;

definition
  let S;
  let U1,U2 be MSAlgebra over S;
  let F be ManySortedFunction of U1,U2;
  pred F is_epimorphism U1,U2 means
:: MSUALG_3:def 8
  F is_homomorphism U1,U2 & F is "onto";
end;

theorem :: MSUALG_3:11
  for U1,U2,U3 being non-empty MSAlgebra over S
  for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st
  F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
  G**F is_epimorphism U1,U3;

definition
  let S;
  let U1,U2 be MSAlgebra over S;
  let F be ManySortedFunction of U1,U2;
  pred F is_monomorphism U1,U2 means
:: MSUALG_3:def 9
  F is_homomorphism U1,U2 & F is "1-1";
end;

theorem :: MSUALG_3:12
  for U1,U2,U3 being non-empty MSAlgebra over S for F be
  ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st F
is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G**F is_monomorphism U1,
  U3;

definition
  let S;
  let U1,U2 be MSAlgebra over S;
  let F be ManySortedFunction of U1,U2;
  pred F is_isomorphism U1,U2 means
:: MSUALG_3:def 10

  F is_epimorphism U1,U2 & F is_monomorphism U1,U2;
end;

theorem :: MSUALG_3:13
  for F be ManySortedFunction of U1,U2 holds F is_isomorphism U1,
  U2 iff F is_homomorphism U1,U2 & F is "onto" & F is "1-1";

theorem :: MSUALG_3:14
  for U1,U2 being non-empty MSAlgebra over S for H be
  ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U1 st H
  is_isomorphism U1,U2 & H1 = H"" holds H1 is_isomorphism U2,U1;

theorem :: MSUALG_3:15
  for U1,U2,U3 being non-empty MSAlgebra over S for H be
  ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U3 st H
is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,
  U3;

definition
  let S;
  let U1,U2 be MSAlgebra over S;
  pred U1,U2 are_isomorphic means
:: MSUALG_3:def 11

  ex F be ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;
end;

theorem :: MSUALG_3:16
  for U1 being MSAlgebra over S holds id the Sorts of U1
  is_isomorphism U1,U1 & U1,U1 are_isomorphic;

definition
  let S;
  let U1, U2 be MSAlgebra over S;
  redefine pred U1, U2 are_isomorphic;
  reflexivity;
end;

theorem :: MSUALG_3:17
  for U1,U2 being non-empty MSAlgebra over S holds U1,U2 are_isomorphic
  implies U2,U1 are_isomorphic;

theorem :: MSUALG_3:18
  for U1,U2,U3 being non-empty MSAlgebra over S holds U1,U2
  are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic;

definition
  let S;
  let U1,U2 be non-empty MSAlgebra over S;
  let F be ManySortedFunction of U1,U2;
  assume
 F is_homomorphism U1,U2;
  func Image F -> strict non-empty MSSubAlgebra of U2 means
:: MSUALG_3:def 12

  the Sorts of it = F.:.:(the Sorts of U1);
end;

theorem :: MSUALG_3:19
  for U1 being non-empty MSAlgebra over S, U2 being non-empty
  MSAlgebra over S, F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2
  holds F is_epimorphism U1,U2 iff Image F = the MSAlgebra of U2;

theorem :: MSUALG_3:20
  for U1,U2 being non-empty MSAlgebra over S for F be
ManySortedFunction of U1,U2, G be ManySortedFunction of U1,Image F st F = G & F
  is_homomorphism U1,U2 holds G is_epimorphism U1,Image F;

theorem :: MSUALG_3:21
  for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction
of U1,U2 st F is_homomorphism U1,U2 ex G be ManySortedFunction of U1,Image F st
  F = G & G is_epimorphism U1,Image F;

theorem :: MSUALG_3:22
  for U1 being non-empty MSAlgebra over S for U2 be non-empty
MSSubAlgebra of U1, G be ManySortedFunction of U2,U1 st G = id (the Sorts of U2
  ) holds G is_monomorphism U2,U1;

theorem :: MSUALG_3:23
  for U1,U2 being non-empty MSAlgebra over S for F be ManySortedFunction
of U1,U2 st F is_homomorphism U1,U2 ex F1 be ManySortedFunction of U1,Image F,
  F2 be ManySortedFunction of Image F,U2 st F1 is_epimorphism U1,Image F & F2
  is_monomorphism Image F,U2 & F = F2**F1;

theorem :: MSUALG_3:24
  for S for U1,U2 being MSAlgebra over S for o for F being
  ManySortedFunction of U1,U2 for x being Element of Args(o,U1), f,u being
  Function st x = f & x in Args(o,U1) & u in Args(o,U2) holds u = F#x iff for n
  st n in dom f holds u.n = (F.((the_arity_of o)/.n)).(f.n);