The abstract of the Mizar article:

Homomorphisms of Order Sorted Algebras

by

Josef Urban

Received September 19, 2002

MML identifier: OSALG_3

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_1, MSUALG_1, PBOOLE, PRALG_1, FUNCT_1, RELAT_1, BOOLE,
      ZF_REFLE, CARD_3, QC_LANG1, TDGROUP, FINSEQ_1, FINSEQ_4, ALG_1, SEQM_3,
      GROUP_6, MSUALG_2, UNIALG_2, MSUALG_3, OSALG_1, ORDERS_1, OSALG_2,
      OSALG_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, RELAT_1, RELSET_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_4, STRUCT_0, ORDERS_1, PRALG_1,
      MSUALG_1, MSUALG_2, YELLOW18, OSALG_1, OSALG_2, MSUALG_3;
 constructors ORDERS_3, FINSEQ_4, OSALG_2, MSUALG_3, YELLOW18, MEMBERED;
 clusters DTCONSTR, FINSEQ_1, MSAFREE, MSUALG_1, ORDERS_3, OSALG_1, PRALG_1,
      RELSET_1, STRUCT_0, MSUALG_9, PARTFUN1;
 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
canceled;

theorem :: OSALG_3:2
  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:3
  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:4
    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:5
  for A being OrderSortedSet of R holds
  id A is order-sorted;

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

theorem :: OSALG_3:6
 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:7
  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:8
  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:9
  for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic;

theorem :: OSALG_3:10
 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:11
  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:12
  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:13
  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:14
  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:15
  for U1 being monotone OSAlgebra of S1,
      U2 being OSSubAlgebra of U1 holds
  U2 is monotone;

definition let S1;
  let U1 be monotone OSAlgebra of S1;
  cluster monotone OSSubAlgebra of U1;
end;

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

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 G be ManySortedFunction of U1,Image F
  st F = G & G is order-sorted & G is_epimorphism U1,Image F;

theorem :: OSALG_3:17
    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;

definition 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:18
    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:19
    for U1,U2 being strict non-empty OSAlgebra of S1 st
  U1,U2 are_os_isomorphic holds
  U1 is monotone iff U2 is monotone;