:: Homomorphisms of Order Sorted Algebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2026 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;
definitions TARSKI, OSALG_1;
expansions TARSKI, OSALG_1;
theorems XBOOLE_1, FUNCT_1, FUNCT_2, PBOOLE, CARD_3, MSUALG_1, ZFMISC_1,
MSUALG_9, FINSEQ_3, MSUALG_2, RELAT_1, OSALG_1, OSALG_2, MSUALG_3,
MSAFREE3, ORDINAL1, PARTFUN1, FINSEQ_2, XTUPLE_0;
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
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 Th1:
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
proof
let F be ManySortedFunction of the carrier of R such that
A1: F is order-sorted;
let s1,s2 be Element of R such that
A2: s1 <= s2;
thus dom (F.s1) c= dom (F.s2)
by A1,A2;
for a,b being object holds [a,b] in F.s1 implies [a,b] in F.s2
proof
let y,z be object such that
A3: [y,z] in F.s1;
y in dom (F.s1) by A3,XTUPLE_0:def 12;
then
A4: y in dom (F.s2) & (F.s1).y = (F.s2).y by A1,A2;
(F.s1).y = z by A3,FUNCT_1:1;
hence thesis by A4,FUNCT_1:1;
end;
hence thesis by RELAT_1:def 3;
end;
theorem Th2:
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
proof
let A be OrderSortedSet of R, B be non-empty OrderSortedSet of R, F be
ManySortedFunction of A,B;
hereby
assume
A1: F is order-sorted;
let s1,s2 be Element of R such that
A2: s1 <= s2;
let a1 be set;
assume a1 in A.s1;
then a1 in dom (F.s1) by FUNCT_2:def 1;
hence (F.s1).a1 = (F.s2).a1 by A1,A2;
end;
assume
A3: 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;
let s1,s2 be Element of R such that
A4: s1 <= s2;
A5: dom (F.s1) = A.s1 & dom (F.s2) = A.s2 by FUNCT_2:def 1;
let a1 be set such that
A6: a1 in dom (F.s1);
A.s1 c= A.s2 by A4,OSALG_1:def 16;
hence a1 in dom (F.s2) by A6,A5;
thus (F.s1).a1 = (F.s2).a1 by A3,A4,A6;
end;
theorem
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
proof
let F be ManySortedFunction of the carrier of R such that
A1: F is order-sorted;
let w1,w2 be Element of (the carrier of R)* such that
A2: w1 <= w2;
A3: len w1 = len w2 by A2;
then
A4: dom w1 = dom w2 by FINSEQ_3:29;
thus F#.w1 c= F#.w2
proof
set a = F#.w1, b = F#.w2;
A5: a = product(F*w1) by FINSEQ_2:def 5;
let x be object;
assume x in F#.w1;
then consider g being Function such that
A6: x = g & dom g = dom (F*w1) and
A7: for y being object st y in dom (F*w1) holds g.y in (F*w1).y
by A5,CARD_3:def 5;
A8: dom F = the carrier of R by PARTFUN1:def 2;
rng w2 c= the carrier of R;
then
A9: dom (F*w2) = dom w2 by A8,RELAT_1:27;
rng w1 c= the carrier of R;
then
A10: dom (F*w1) = dom w1 by A8,RELAT_1:27;
A11: for z being object st z in dom (F*w2) holds g.z in (F*w2).z
proof
let z be object such that
A12: z in dom (F*w2);
A13: (F*w2).z = F.(w2.z) by A12,FUNCT_1:12;
w1.z in rng w1 & w2.z in rng w2 by A4,A9,A12,FUNCT_1:3;
then reconsider s1 = w1.z, s2 = w2.z as Element of R;
z in dom (F*w1) by A3,A10,A9,A12,FINSEQ_3:29;
then s1 <= s2 by A2,A10;
then
A14: F.s1 c= F.s2 by A1,Th1;
g.z in (F*w1).z & (F*w1).z = F.(w1.z) by A4,A7,A10,A9,A12,FUNCT_1:12;
hence thesis by A13,A14;
end;
b = product(F*w2) by FINSEQ_2:def 5;
hence thesis by A4,A6,A10,A9,A11,CARD_3:def 5;
end;
end;
theorem Th4:
for A being OrderSortedSet of R holds id A is order-sorted
proof
let A be OrderSortedSet of R;
set F = id A;
let s1,s2 be Element of R;
assume s1 <= s2;
then
A1: A.s1 c= A.s2 by OSALG_1:def 16;
let a1 be set such that
A2: a1 in dom (F.s1);
A.s2 = {} implies A.s2 = {};
then dom (F.s2) = A.s2 by FUNCT_2:def 1;
hence a1 in dom (F.s2) by A2,A1;
(F.s1).a1 = (id (A.s1)).a1 by MSUALG_3:def 1
.= a1 by A2,FUNCT_1:18
.= (id (A.s2)).a1 by A2,A1,FUNCT_1:18
.= (F.s2).a1 by MSUALG_3:def 1;
hence thesis;
end;
registration
let R;
let A be OrderSortedSet of R;
cluster id A -> order-sorted;
coherence by Th4;
end;
theorem Th5:
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
proof
let A be OrderSortedSet of R, B,C be non-empty OrderSortedSet of R, F be
ManySortedFunction of A,B, G be ManySortedFunction of B,C;
assume that
A1: F is order-sorted and
A2: G is order-sorted;
for s1,s2 being Element of R st s1 <= s2 holds for a1 being set st a1 in
A.s1 holds ((G**F).s1).a1 = ((G**F).s2).a1
proof
let s1,s2 be Element of R such that
A3: s1 <= s2;
A4: A.s1 c= A.s2 by A3,OSALG_1:def 16;
let a1 be set such that
A5: a1 in A.s1;
A6: (F.s1).a1 = (F.s2).a1 by A1,A3,A5,Th2;
(F.s1).a1 in B.s1 by A5,FUNCT_2:5;
then
A7: (G.s1).((F.s2).a1) = (G.s2).((F.s2).a1) by A2,A3,A6,Th2;
((G**F).s1).a1 = ((G.s1)*(F.s1)).a1 by MSUALG_3:2
.= (G.s1).((F.s2).a1) by A5,A6,FUNCT_2:15
.= ((G.s2)*(F.s2)).a1 by A5,A4,A7,FUNCT_2:15
.= ((G**F).s2).a1 by MSUALG_3:2;
hence thesis;
end;
hence thesis by Th2;
end;
theorem Th6:
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
proof
let A,B be OrderSortedSet of R;
let F be ManySortedFunction of A,B such that
A1: F is "1-1" and
A2: F is "onto" and
A3: F is order-sorted;
let s1,s2 be Element of R such that
A4: s1 <= s2;
A5: B.s1 c= B.s2 by A4,OSALG_1:def 16;
A6: F"".s2 = (F.s2)" by A1,A2,MSUALG_3:def 4;
A7: A.s1 c= A.s2 by A4,OSALG_1:def 16;
s1 in the carrier of R;
then s1 in dom F by PARTFUN1:def 2;
then
A8: F.s1 is one-to-one by A1,MSUALG_3:def 2;
s2 in the carrier of R;
then s2 in dom F by PARTFUN1:def 2;
then
A9: F.s2 is one-to-one by A1,MSUALG_3:def 2;
let a1 be set such that
A10: a1 in dom (F"".s1);
A11: a1 in B.s1 by A10;
then
A12: dom (F.s2) = A.s2 by A5,FUNCT_2:def 1;
set c1 = ((F.s1)").a1, c2 = ((F.s2)").a1;
A13: dom (F.s1) = A.s1 by A10,FUNCT_2:def 1;
A14: F"".s1 = (F.s1)" by A1,A2,MSUALG_3:def 4;
then
A15: ((F.s1)").a1 in rng ((F.s1)") by A10,FUNCT_1:3;
A16: rng(F.s1) = B.s1 by A2,MSUALG_3:def 3;
then (F.s1)" is Function of B.s1,A.s1 by A8,FUNCT_2:25;
then
A17: rng ((F.s1)") c= A.s1 by RELAT_1:def 19;
then
A18: ((F.s1)").a1 in A.s1 by A15;
A19: rng (F.s2) = B.s2 by A2,MSUALG_3:def 3;
then
A20: (F.s2).c2 = a1 by A5,A9,A11,FUNCT_1:35
.= (F.s1).c1 by A10,A16,A8,FUNCT_1:35
.= (F.s2). c1 by A3,A4,A15,A17,A13;
a1 in B.s2 by A5,A11;
hence a1 in dom (F"".s2) by A7,A18,FUNCT_2:def 1;
(F.s2)" is Function of B.s2,A.s2 by A19,A9,FUNCT_2:25;
then c2 in dom (F.s2) by A5,A7,A11,A18,A12,FUNCT_2:5;
hence thesis by A7,A9,A14,A6,A18,A12,A20,FUNCT_1:def 4;
end;
:: this could be done via by cluster, when non clusterable attrs removed
theorem Th7:
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
proof
let A be OrderSortedSet of R;
let F be ManySortedFunction of the carrier of R such that
A1: F is order-sorted;
reconsider C1 = F.:.:A as ManySortedSet of R;
C1 is order-sorted
proof
let s1,s2 be Element of R;
assume s1 <= s2;
then
A2: A.s1 c= A.s2 & F.s1 c= F.s2 by A1,Th1,OSALG_1:def 16;
C1.s1 = (F.s1).:(A.s1) & C1.s2 = (F.s2).:(A.s2) by PBOOLE:def 20;
hence thesis by A2,RELAT_1:125;
end;
hence thesis;
end;
definition
let S1;
let U1,U2 be OSAlgebra of S1;
pred U1,U2 are_os_isomorphic means
ex F be ManySortedFunction of U1,
U2 st F is_isomorphism U1,U2 & F is order-sorted;
end;
theorem Th8:
for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic
proof
let U1 be OSAlgebra of S1;
take id (the Sorts of U1);
the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
hence thesis by MSUALG_3:16;
end;
theorem Th9:
for U1,U2 being non-empty OSAlgebra of S1 holds U1,U2
are_os_isomorphic implies U2,U1 are_os_isomorphic
proof
let U1,U2 be non-empty OSAlgebra of S1;
A1: the Sorts of U1 is OrderSortedSet of S1 & the Sorts of U2 is
OrderSortedSet of S1 by OSALG_1:17;
assume U1,U2 are_os_isomorphic;
then consider F be ManySortedFunction of U1,U2 such that
A2: F is_isomorphism U1,U2 and
A3: F is order-sorted;
reconsider G = F"" as ManySortedFunction of U2,U1;
A4: G is_isomorphism U2,U1 by A2,MSUALG_3:14;
F is "onto" & F is "1-1" by A2,MSUALG_3:13;
then F"" is order-sorted by A3,A1,Th6;
hence thesis by A4;
end;
definition
let S1;
let U1, U2 be OSAlgebra of S1;
redefine pred U1, U2 are_os_isomorphic; :: redefines are_os_isomorphic (OSALG_3, definition)
reflexivity by Th8;
end;
definition
let S1;
let U1, U2 be non-empty OSAlgebra of S1;
redefine pred U1, U2 are_os_isomorphic; :: redefines are_os_isomorphic (OSALG_3, definition)
symmetry by Th9;
end;
:: prove for order-sorted
theorem
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
proof
let U1,U2,U3 be non-empty OSAlgebra of S1;
assume that
A1: U1,U2 are_os_isomorphic and
A2: U2,U3 are_os_isomorphic;
consider F be ManySortedFunction of U1,U2 such that
A3: F is_isomorphism U1,U2 and
A4: F is order-sorted by A1;
consider G be ManySortedFunction of U2,U3 such that
A5: G is_isomorphism U2,U3 and
A6: G is order-sorted by A2;
reconsider H = G**F as ManySortedFunction of U1,U3;
A7: H is_isomorphism U1,U3 by A3,A5,MSUALG_3:15;
A8: the Sorts of U3 is non-empty OrderSortedSet of S1 by OSALG_1:17;
the Sorts of U1 is non-empty OrderSortedSet of S1 & the Sorts of U2 is
non-empty OrderSortedSet of S1 by OSALG_1:17;
then H is order-sorted by A4,A6,A8,Th5;
hence thesis by A7;
end;
:: again, should be done as cluster or redefine
theorem Th11:
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
proof
let U1,U2 be non-empty OSAlgebra of S1;
let F be ManySortedFunction of U1,U2 such that
A1: F is order-sorted and
A2: F is_homomorphism U1,U2;
reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1:17;
F.:.:O1 is OrderSortedSet of S1 by A1,Th7;
then the Sorts of Image F is OrderSortedSet of S1 by A2,MSUALG_3:def 12;
hence thesis by OSALG_1:17;
end;
theorem Th12:
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
proof
let U1,U2 be non-empty OSAlgebra of S1;
let F be ManySortedFunction of U1,U2 such that
A1: F is order-sorted;
let o1,o2 be OperSymbol of S1 such that
A2: o1 <= o2;
let x be Element of Args(o1,U1), x1 be Element of Args(o2,U1) such that
A3: x = x1;
A4: dom x = dom (the_arity_of o1) by MSUALG_3:6;
A5: for n being object st n in dom x holds (F # x).n = (F # x1).n
proof
let n1 be object such that
A6: n1 in dom x;
reconsider n2 = n1 as Nat by A6,ORDINAL1:def 12;
reconsider pi1 = (the_arity_of o1)/.n2, pi2 = (the_arity_of o2)/.n2 as
Element of S1;
A7: (the_arity_of o1)/.n2 = (the_arity_of o1).n2 by A4,A6,PARTFUN1:def 6;
A8: the_arity_of o1 <= the_arity_of o2 by A2;
then len (the_arity_of o1) = len (the_arity_of o2);
then dom (the_arity_of o1) = dom (the_arity_of o2) by FINSEQ_3:29;
then (the_arity_of o2)/.n2 = (the_arity_of o2).n2 by A4,A6,PARTFUN1:def 6;
then
A9: pi1 <= pi2 by A4,A6,A8,A7;
rng (the_arity_of o1) c= the carrier of S1;
then rng (the_arity_of o1) c= dom (the Sorts of U1) by PARTFUN1:def 2;
then
A10: n2 in dom ((the Sorts of U1) * (the_arity_of o1)) by A4,A6,RELAT_1:27;
dom (F.pi1) = (the Sorts of U1).pi1 by FUNCT_2:def 1
.= (the Sorts of U1).((the_arity_of o1).n2) by A4,A6,PARTFUN1:def 6
.= ((the Sorts of U1) * (the_arity_of o1)).n2 by A4,A6,FUNCT_1:13;
then
A11: x1.n2 in dom (F.pi1) by A3,A10,MSUALG_3:6;
(F # x).n2 = (F.((the_arity_of o1)/.n2)).(x1.n2) by A3,A6,MSUALG_3:def 6
.= (F.pi2).(x1.n2) by A1,A11,A9
.= (F # x1).n2 by A3,A6,MSUALG_3:def 6;
hence thesis;
end;
dom x1 = dom (the_arity_of o2) by MSUALG_3:6;
then
A12: dom (F # x1) = dom x1 by MSUALG_3:6;
dom (F # x) = dom x by A4,MSUALG_3:6;
hence thesis by A3,A12,A5,FUNCT_1:2;
end;
theorem Th13:
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
proof
let U1 be monotone non-empty OSAlgebra of S1, U2 be non-empty OSAlgebra of
S1;
let F be ManySortedFunction of U1,U2 such that
A1: F is order-sorted and
A2: F is_homomorphism U1,U2;
reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1:17;
F.:.:O1 is OrderSortedSet of S1 by A1,Th7;
then
A3: the Sorts of Image F is OrderSortedSet of S1 by A2,MSUALG_3:def 12;
then reconsider I = Image F as non-empty OSAlgebra of S1 by OSALG_1:17;
thus Image F is order-sorted by A3,OSALG_1:17;
consider G being ManySortedFunction of U1,I such that
A4: F = G and
A5: G is_epimorphism U1,I by A2,MSUALG_3:21;
A6: G is_homomorphism U1,I by A5,MSUALG_3:def 8;
A7: G is "onto" by A5,MSUALG_3:def 8;
for o1,o2 being OperSymbol of S1 st o1 <= o2 holds Den(o1,I) c= Den(o2,I )
proof
let o1,o2 be OperSymbol of S1 such that
A8: o1 <= o2;
A9: Args(o1,I) c= Args(o2,I) by A8,OSALG_1:26;
A10: Args(o1,U1) c= Args(o2,U1) by A8,OSALG_1:26;
A11: dom Den(o2,I) = Args(o2,I) by FUNCT_2:def 1;
A12: Den(o2,U1)|Args(o1,U1) = Den(o1,U1) by A8,OSALG_1:def 21;
A13: the_result_sort_of o1 <= the_result_sort_of o2 by A8;
for a,b being object holds [a,b] in Den(o1,I) implies [a,b] in Den(o2,I)
proof
set s1 = the_result_sort_of o1, s2 = the_result_sort_of o2;
o1 in the carrier' of S1;
then
A14: o1 in dom the ResultSort of S1 by FUNCT_2:def 1;
let a,b be object such that
A15: [a,b] in Den(o1,I);
A16: a in Args(o1,I) by A15,ZFMISC_1:87;
then consider y being Element of Args(o1,U1) such that
A17: G # y = a by A7,MSUALG_9:17;
reconsider y1 = y as Element of Args(o2,U1) by A10;
A18: G # y1 = G # y & Den(o2,U1).y = Den(o1,U1).y by A1,A4,A8,A12,Th12,
FUNCT_1:49;
set x = Den(o1,U1).y;
(G.s1).x = Den(o1,I).a by A6,A17,MSUALG_3:def 7;
then
A19: b = (G.s1).x by A15,FUNCT_1:1;
Result(o1,U1) = (O1 * (the ResultSort of S1)).o1 by MSUALG_1:def 5
.= O1.((the ResultSort of S1).o1) by A14,FUNCT_1:13
.= O1.s1 by MSUALG_1:def 2
.= dom (G.s1) by FUNCT_2:def 1;
then (G.s1).x = (G.s2).x by A1,A4,A13;
then b = Den(o2,I).a by A6,A17,A19,A18,MSUALG_3:def 7;
hence thesis by A9,A11,A16,FUNCT_1:1;
end;
hence thesis by RELAT_1:def 3;
end;
hence thesis by OSALG_1:27;
end;
theorem Th14:
for U1 being monotone OSAlgebra of S1, U2 being OSSubAlgebra of
U1 holds U2 is monotone
proof
let U1 be monotone OSAlgebra of S1, U2 be OSSubAlgebra of U1;
let o1,o2 be OperSymbol of S1 such that
A1: o1 <= o2;
A2: Args(o1,U2) c= Args(o2,U2) by A1,OSALG_1:26;
the Sorts of U2 is MSSubset of U1 & the Sorts of U2 is OrderSortedSet of
S1 by MSUALG_2:def 9,OSALG_1:17;
then reconsider B = the Sorts of U2 as OSSubset of U1 by OSALG_2:def 2;
A3: B is opers_closed by MSUALG_2:def 9;
then
A4: B is_closed_on o1 by MSUALG_2:def 6;
A5: B is_closed_on o2 by A3,MSUALG_2:def 6;
A6: Den(o2,U2) = (the Charact of U2).o2 by MSUALG_1:def 6
.= Opers(U1,B).o2 by MSUALG_2:def 9
.= o2/.B by MSUALG_2:def 8
.= (Den(o2,U1)) | ((B# * the Arity of S1).o2) by A5,MSUALG_2:def 7
.= (Den(o2,U1)) | Args(o2,U2) by MSUALG_1:def 4;
A7: Den(o1,U2) = (the Charact of U2).o1 by MSUALG_1:def 6
.= Opers(U1,B).o1 by MSUALG_2:def 9
.= o1/.B by MSUALG_2:def 8
.= (Den(o1,U1)) | ((B# * the Arity of S1).o1) by A4,MSUALG_2:def 7
.= (Den(o1,U1)) | Args(o1,U2) by MSUALG_1:def 4;
Den(o2,U1)|Args(o1,U1) = Den(o1,U1) by A1,OSALG_1:def 21;
then Den(o1,U2) = Den(o2,U1)| ( Args(o1,U1) /\ Args(o1,U2)) by A7,RELAT_1:71
.= Den(o2,U1) | Args(o1,U2) by MSAFREE3:37,XBOOLE_1:28
.= Den(o2,U1) | ( Args(o2,U2) /\ Args(o1,U2) ) by A2,XBOOLE_1:28
.= Den(o2,U2) | Args(o1,U2) by A6,RELAT_1:71;
hence thesis;
end;
registration
let S1;
let U1 be monotone OSAlgebra of S1;
cluster monotone for OSSubAlgebra of U1;
existence
proof
set U2 = the OSSubAlgebra of U1;
take U2;
thus thesis by Th14;
end;
end;
registration
let S1;
let U1 be monotone OSAlgebra of S1;
cluster -> monotone for OSSubAlgebra of U1;
coherence by Th14;
end;
theorem Th15:
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
proof
let U1,U2 be non-empty OSAlgebra of S1;
let F be ManySortedFunction of U1,U2;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted;
consider G being ManySortedFunction of U1,Image F such that
A3: F = G & G is_epimorphism U1,Image F by A1,MSUALG_3:21;
take G;
thus thesis by A2,A3;
end;
theorem
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
proof
let U1,U2 be non-empty OSAlgebra of S1;
let F be ManySortedFunction of U1,U2;
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted;
for H be ManySortedFunction of Image F,Image F holds H is
ManySortedFunction of Image F,U2
proof
let H be ManySortedFunction of Image F,Image F;
for i be object st i in the carrier of S1 holds H.i is Function of (the
Sorts of Image F).i,(the Sorts of U2).i
proof
let i be object;
assume
A3: i in the carrier of S1;
then reconsider
f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).
i by PBOOLE:def 15;
reconsider h = H.i as Function of (the Sorts of Image F).i,(the Sorts of
Image F).i by A3,PBOOLE:def 15;
A4: dom f = (the Sorts of U1).i by A3,FUNCT_2:def 1;
the Sorts of Image F = F.:.:(the Sorts of U1) by A1,MSUALG_3:def 12;
then (the Sorts of Image F).i = f.:((the Sorts of U1).i) by A3,
PBOOLE:def 20
.= rng f by A4,RELAT_1:113;
then h is Function of (the Sorts of Image F).i,(the Sorts of U2).i by
FUNCT_2:7;
hence thesis;
end;
hence thesis by PBOOLE:def 15;
end;
then reconsider
F2 = id (the Sorts of Image F) as ManySortedFunction of Image F,
U2;
consider F1 being ManySortedFunction of U1,Image F such that
A5: F1 = F & F1 is order-sorted and
A6: F1 is_epimorphism U1,Image F by A1,A2,Th15;
take F1,F2;
thus F1 is_epimorphism U1,Image F by A6;
thus F2 is_monomorphism Image F,U2 by MSUALG_3:22;
thus F = F2**F1 & F1 is order-sorted by A5,MSUALG_3:4;
Image F is order-sorted by A1,A2,Th11;
then (the Sorts of Image F) is OrderSortedSet of S1 by OSALG_1:17;
hence thesis;
end;
registration
let S1;
let U1 be OSAlgebra of S1;
cluster MSAlgebra(# the Sorts of U1, the Charact of U1 #) -> order-sorted;
coherence
proof
the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
hence thesis by OSALG_1:17;
end;
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
for U1 being OSAlgebra of S1 holds (U1 is monotone iff MSAlgebra(# the
Sorts of U1, the Charact of U1 #) is monotone)
proof
let U1 be OSAlgebra of S1;
set U2 = MSAlgebra(# the Sorts of U1, the Charact of U1 #);
A1: now
let o1 being OperSymbol of S1;
thus Den(o1,U1) = (the Charact of U2).o1 by MSUALG_1:def 6
.= Den(o1,U2) by MSUALG_1:def 6;
thus Args(o1,U1) = ((the Sorts of U2)# * the Arity of S1).o1 by
MSUALG_1:def 4
.= Args(o1,U2) by MSUALG_1:def 4;
end;
thus U1 is monotone implies U2 is monotone
proof
assume
A2: U1 is monotone;
let o1,o2 be OperSymbol of S1;
assume o1 <= o2;
then
A3: Den(o2,U1)|Args(o1,U1) = Den(o1,U1) by A2;
thus Den(o2,U2)|Args(o1,U2) = Den(o2,U1)|Args(o1,U2) by A1
.= Den(o1,U1) by A1,A3
.= Den(o1,U2) by A1;
end;
assume
A4: U2 is monotone;
let o1,o2 be OperSymbol of S1;
assume o1 <= o2;
then
A5: Den(o2,U2)|Args(o1,U2) = Den(o1,U2) by A4;
thus Den(o2,U1)|Args(o1,U1) = Den(o2,U2)|Args(o1,U1) by A1
.= Den(o1,U2) by A1,A5
.= Den(o1,U1) by A1;
end;
:: proving the non strict version is painful, I'll do it only
:: if it is necessary, see TWiki.StructureImplementation for some suggestions
theorem
for U1,U2 being strict non-empty OSAlgebra of S1 st U1,U2
are_os_isomorphic holds U1 is monotone iff U2 is monotone
proof
let U1,U2 be strict non-empty OSAlgebra of S1;
assume U1,U2 are_os_isomorphic;
then consider F be ManySortedFunction of U1,U2 such that
A1: F is_isomorphism U1,U2 and
A2: F is order-sorted;
reconsider O1 = the Sorts of U1, O2 = the Sorts of U2 as OrderSortedSet of
S1 by OSALG_1:17;
reconsider F1 = F as ManySortedFunction of O1,O2;
F is "onto" & F is "1-1" by A1,MSUALG_3:13;
then
A3: F1"" is order-sorted by A2,Th6;
A4: F is_epimorphism U1,U2 by A1,MSUALG_3:def 10;
then
A5: F is_homomorphism U1,U2 by MSUALG_3:def 8;
then Image F = U2 by A4,MSUALG_3:19;
hence U1 is monotone implies U2 is monotone by A2,A5,Th13;
reconsider F2 = F1"" as ManySortedFunction of U2,U1;
assume
A6: U2 is monotone;
F"" is_isomorphism U2,U1 by A1,MSUALG_3:14;
then
A7: F2 is_epimorphism U2,U1 by MSUALG_3:def 10;
then
A8: F2 is_homomorphism U2,U1 by MSUALG_3:def 8;
then Image F2 = U1 by A7,MSUALG_3:19;
hence thesis by A3,A8,A6,Th13;
end;