Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

Homomorphisms of Order Sorted Algebras

by
Josef Urban

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;