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