:: Homomorphisms of Order Sorted Algebras
::  by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-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 XBOOLE_0, ORDERS_2, OSALG_1, PBOOLE, STRUCT_0, SUBSET_1,
      XXREAL_0, RELAT_1, FUNCT_1, TARSKI, FINSEQ_1, CARD_3, MEMBER_1, MSUALG_3,
      MSUALG_1, GROUP_6, MARGREL1, NAT_1, PARTFUN1, SEQM_3, OSALG_2, MSUALG_2,
      UNIALG_2, OSALG_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, CARD_3, ORDERS_2, PBOOLE,
      STRUCT_0, MSUALG_1, MSUALG_2, OSALG_1, OSALG_2, MSUALG_3;
 constructors MSUALG_3, ORDERS_3, OSALG_2, CARD_3, RELSET_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, PBOOLE, STRUCT_0,
      MSUALG_1, MSUALG_3, ORDERS_3, MSUALG_9, OSALG_1, RELAT_1;
 requirements BOOLE, SUBSET;


begin

reserve R for non empty Poset,
  S1 for OrderSortedSign;

definition
  let R;
  let F be ManySortedFunction of the carrier of R;
  attr F is order-sorted means
:: OSALG_3:def 1

  for s1,s2 being Element of R st s1 <= s2
holds for a1 being set st a1 in dom (F.s1) holds a1 in dom (F.s2) & (F.s1).a1 =
  (F.s2).a1;
end;

:: maybe later cluster 1-1 order-sorted (when clusterable)
:: REVISE the prf of cluster in MSUALG_3

theorem :: OSALG_3:1
  for F being ManySortedFunction of the carrier of R st F is
order-sorted for s1,s2 being Element of R st s1 <= s2 holds dom (F.s1) c= dom (
  F.s2) & F.s1 c= F.s2;

theorem :: OSALG_3:2
  for A be OrderSortedSet of R, B be non-empty OrderSortedSet of R,
  F be ManySortedFunction of A,B holds F is order-sorted iff for s1,s2 being
Element of R st s1 <= s2 holds for a1 being set st a1 in A.s1 holds (F.s1).a1 =
  (F.s2).a1;

theorem :: OSALG_3:3
  for F being ManySortedFunction of the carrier of R st F is
order-sorted for w1,w2 being Element of (the carrier of R)* st w1 <= w2 holds F
  #.w1 c= F#.w2;

theorem :: OSALG_3:4
  for A being OrderSortedSet of R holds id A is order-sorted;

registration
  let R;
  let A be OrderSortedSet of R;
  cluster id A -> order-sorted;
end;

theorem :: OSALG_3:5
  for A be OrderSortedSet of R for B,C be non-empty OrderSortedSet
of R, F be ManySortedFunction of A,B, G be ManySortedFunction of B,C holds F is
  order-sorted & G is order-sorted implies G**F is order-sorted;

theorem :: OSALG_3:6
  for A,B being OrderSortedSet of R, F being ManySortedFunction of
  A,B st F is "1-1" & F is "onto" & F is order-sorted holds F"" is order-sorted
;

:: this could be done via by cluster, when non clusterable attrs removed

theorem :: OSALG_3:7
  for A being OrderSortedSet of R, F being ManySortedFunction of
  the carrier of R st F is order-sorted holds F.:.:A is OrderSortedSet of R;

definition
  let S1;
  let U1,U2 be OSAlgebra of S1;
  pred U1,U2 are_os_isomorphic means
:: OSALG_3:def 2

  ex F be ManySortedFunction of U1,
  U2 st F is_isomorphism U1,U2 & F is order-sorted;
end;

theorem :: OSALG_3:8
  for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic;

theorem :: OSALG_3:9
  for U1,U2 being non-empty OSAlgebra of S1 holds U1,U2
  are_os_isomorphic implies U2,U1 are_os_isomorphic;

definition
  let S1;
  let U1, U2 be OSAlgebra of S1;
  redefine pred U1, U2 are_os_isomorphic;
  reflexivity;
end;

definition
  let S1;
  let U1, U2 be non-empty OSAlgebra of S1;
  redefine pred U1, U2 are_os_isomorphic;
  symmetry;
end;

:: prove for order-sorted

theorem :: OSALG_3:10
  for U1,U2,U3 being non-empty OSAlgebra of S1 holds U1,U2
  are_os_isomorphic & U2,U3 are_os_isomorphic implies U1,U3 are_os_isomorphic;

:: again, should be done as cluster or redefine

theorem :: OSALG_3:11
  for U1,U2 being non-empty OSAlgebra of S1 for F being
  ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2
  holds Image F is order-sorted;

theorem :: OSALG_3:12
  for U1,U2 being non-empty OSAlgebra of S1 for F being
ManySortedFunction of U1,U2 st F is order-sorted for o1,o2 being OperSymbol of
S1 st o1 <= o2 for x being Element of Args(o1,U1), x1 be Element of Args(o2,U1)
  st x = x1 holds F # x = F # x1;

theorem :: OSALG_3:13
  for U1 being monotone non-empty OSAlgebra of S1, U2 being
  non-empty OSAlgebra of S1 for F being ManySortedFunction of U1,U2 st F is
order-sorted & F is_homomorphism U1,U2 holds Image F is order-sorted & Image F
  is monotone OSAlgebra of S1;

theorem :: OSALG_3:14
  for U1 being monotone OSAlgebra of S1, U2 being OSSubAlgebra of
  U1 holds U2 is monotone;

registration
  let S1;
  let U1 be monotone OSAlgebra of S1;
  cluster monotone for OSSubAlgebra of U1;
end;

registration
  let S1;
  let U1 be monotone OSAlgebra of S1;
  cluster -> monotone for OSSubAlgebra of U1;
end;

theorem :: OSALG_3:15
  for U1,U2 being non-empty OSAlgebra of S1 for F be
ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted ex G
  be ManySortedFunction of U1,Image F st F = G & G is order-sorted & G
  is_epimorphism U1,Image F;

theorem :: OSALG_3:16
  for U1,U2 being non-empty OSAlgebra of S1 for F be ManySortedFunction
  of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is
  order-sorted & F2 is order-sorted;

registration
  let S1;
  let U1 be OSAlgebra of S1;
  cluster MSAlgebra(# the Sorts of U1, the Charact of U1 #) -> order-sorted;
end;

:: very strange, the "strict" attribute is quite unfriendly
:: could Grzegorz's suggestion for struct implementation fix this?
:: hard to generalize to some useful scheme

theorem :: OSALG_3:17
  for U1 being OSAlgebra of S1 holds (U1 is monotone iff MSAlgebra(# the
    Sorts of U1, the Charact of U1 #) is monotone);

:: proving the non strict version is painful, I'll do it only
:: if it is necessary, see TWiki.StructureImplementation for some suggestions

theorem :: OSALG_3:18
  for U1,U2 being strict non-empty OSAlgebra of S1 st U1,U2
  are_os_isomorphic holds U1 is monotone iff U2 is monotone;