:: Order Sorted Quotient Algebra
:: 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 NUMBERS, XBOOLE_0, ORDERS_2, MSUALG_4, OSALG_1, RELAT_1,
STRUCT_0, FUNCOP_1, PBOOLE, SUBSET_1, XXREAL_0, FUNCT_1, MSUALG_1,
TARSKI, EQREL_1, NAT_1, MARGREL1, PARTFUN1, FINSEQ_1, ARYTM_3, ARYTM_1,
ZFMISC_1, FINSEQ_5, CARD_1, RELAT_2, ORDINAL4, NATTRA_1, YELLOW15,
SETFAM_1, COH_SP, YELLOW18, WAYBEL_0, CARD_3, MSUALG_3, WELLORD1, SEQM_3,
OSALG_4;
notations ZFMISC_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
RELSET_1, PARTFUN1, EQREL_1, SETFAM_1, XCMPLX_0, ORDERS_2, ORDERS_3,
ORDINAL1, NUMBERS, FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_2, FINSEQ_4,
FINSEQ_5, FUNCOP_1, PBOOLE, STRUCT_0, WAYBEL_0, MSUALG_1, MSUALG_3,
OSALG_1, OSALG_3, MSUALG_4, XXREAL_0;
constructors REAL_1, NAT_1, NAT_D, EQREL_1, FINSEQ_4, FINSEQ_5, MSUALG_3,
MSUALG_4, ORDERS_3, WAYBEL_0, OSALG_3, RELSET_1;
registrations SUBSET_1, RELAT_1, PARTFUN1, FUNCOP_1, XREAL_0, INT_1, FINSEQ_1,
EQREL_1, FUNCT_1, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_3, MSUALG_4,
ORDERS_3, OSALG_1, ORDINAL1, CARD_3, TOLER_1, RELSET_1, FINSEQ_2;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin
registration
let R be non empty Poset;
cluster Relation-yielding for OrderSortedSet of R;
end;
:: this is a stronger condition for relation than just being order-sorted
definition
let R be non empty Poset;
let A,B be ManySortedSet of the carrier of R;
let IT be ManySortedRelation of A,B;
attr IT is os-compatible means
:: OSALG_4:def 1
for s1,s2 being Element of R st s1 <=
s2 for x,y being set st x in A.s1 & y in B.s1 holds [x,y] in IT.s1 iff [x,y] in
IT.s2;
end;
registration
let R be non empty Poset;
let A,B be ManySortedSet of the carrier of R;
cluster os-compatible for ManySortedRelation of A,B;
end;
definition
let R be non empty Poset;
let A,B be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A,B is os-compatible ManySortedRelation of A,B;
end;
theorem :: OSALG_4:1
for R being non empty Poset, A,B being ManySortedSet of the
carrier of R, OR being ManySortedRelation of A,B holds OR is os-compatible
implies OR is OrderSortedSet of R;
registration
let R be non empty Poset;
let A,B be ManySortedSet of R;
cluster os-compatible -> order-sorted for ManySortedRelation of A,B;
end;
definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
mode OrderSortedRelation of A is OrderSortedRelation of A,A;
end;
definition
let S be OrderSortedSign, U1 be OSAlgebra of S;
mode OrderSortedRelation of U1 -> ManySortedRelation of U1 means
:: OSALG_4:def 2
it is os-compatible;
end;
:: REVISE: the definition of ManySorted diagonal from MSUALG_6
:: should be moved to MSUALG_4; the "compatible" attr from MSUALG_6
:: should replace the MSCongruence-like
registration
let S be OrderSortedSign, U1 be OSAlgebra of S;
cluster MSEquivalence-like for OrderSortedRelation of U1;
end;
:: REVISE: we need the fact that id has the type,
:: the original prf can be simplified
registration
let S be OrderSortedSign, U1 be non-empty OSAlgebra of S;
cluster MSCongruence-like for MSEquivalence-like OrderSortedRelation of U1;
end;
definition
let S be OrderSortedSign, U1 be non-empty OSAlgebra of S;
mode OSCongruence of U1 is MSCongruence-like MSEquivalence-like
OrderSortedRelation of U1;
end;
:: TODO: a smooth transition between Relations and Graphs would
:: be useful here, the FinSequence approach seemed to me faster than
:: transitive closure of R \/ R" .. maybe not, can be later a theorem
:: all could be done generally for reflexive (or with small
:: modification even non reflexive) Relations
:: I found ex post that attributes disconnected and connected defined
:: in ORDERS_3 have st. in common here, but the theory there is not developed
:: suggested improvements: f connects x,y; x is_connected_with y;
:: connected iff for x,y holds x is_connected_with y
:: finally I found this is the EqCl from MSUALG_5 - should be merged
definition
let R be non empty Poset;
func Path_Rel R -> Equivalence_Relation of the carrier of R means
:: OSALG_4:def 3
for x,y being object
holds [x,y] in it iff x in the carrier of R & y in the carrier of
R & ex p being FinSequence of the carrier of R st 1 < len p & p.1 = x & p.(len
p) = y & for n being Nat st 2 <= n & n <= len p holds [p.n,p.(n-1)] in the
InternalRel of R or [p.(n-1),p.n] in the InternalRel of R;
end;
theorem :: OSALG_4:2
for R being non empty Poset, s1,s2 being Element of R st s1 <= s2
holds [s1,s2] in Path_Rel R;
:: again, should be defined for Relations probably
definition
let R be non empty Poset;
let s1,s2 be Element of R;
pred s1 ~= s2 means
:: OSALG_4:def 4
[s1,s2] in Path_Rel R;
reflexivity;
symmetry;
end;
theorem :: OSALG_4:3
for R being non empty Poset, s1,s2,s3 being Element of R holds s1 ~=
s2 & s2 ~= s3 implies s1 ~= s3;
:: do for Relations
definition
let R be non empty Poset;
func Components R -> non empty (Subset-Family of R) equals
:: OSALG_4:def 5
Class Path_Rel R;
end;
registration
let R be non empty Poset;
cluster -> non empty for Element of Components R;
end;
definition
let R be non empty Poset;
mode Component of R is Element of Components R;
end;
definition
let R be non empty Poset;
let s1 be Element of R;
func CComp s1 -> Component of R equals
:: OSALG_4:def 6
Class(Path_Rel R,s1);
end;
theorem :: OSALG_4:4
for R being non empty Poset, s1,s2 being Element of R st s1 <= s2
holds CComp(s1) = CComp(s2);
definition
let R be non empty Poset;
let A be ManySortedSet of the carrier of R;
let C be Component of R;
func A-carrier_of C -> set equals
:: OSALG_4:def 7
union {A.s where s is Element of R: s in C};
end;
theorem :: OSALG_4:5
for R being non empty Poset, A being ManySortedSet of the carrier
of R, s being (Element of R), x being set st x in A.s holds x in A-carrier_of
CComp(s);
definition
let R be non empty Poset;
attr R is locally_directed means
:: OSALG_4:def 8
for C being Component of R holds C is directed;
end;
theorem :: OSALG_4:6
for R being discrete non empty Poset holds for x,y being Element
of R st [x,y] in Path_Rel R holds x = y;
theorem :: OSALG_4:7
for R being discrete non empty Poset, C being Component of R ex x
being Element of R st C = {x};
theorem :: OSALG_4:8
for R being discrete non empty Poset holds R is locally_directed;
:: the system could generate this one from the following
registration
cluster locally_directed for non empty Poset;
end;
registration
cluster locally_directed for OrderSortedSign;
end;
registration
cluster discrete -> locally_directed for non empty Poset;
end;
registration
let S be locally_directed non empty Poset;
cluster -> directed for Component of S;
end;
theorem :: OSALG_4:9
{} is Equivalence_Relation of {};
:: Much of what follows can be done generally for OrderSortedRelations
:: of OrderSortedSets (and not just OrderSortedRelations of OSAlgebras),
:: unfortunately, multiple inheritence would be needed to widen the
:: latter to the former
:: Classes on connected components
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let C be Component of S;
func CompClass(E,C) -> Equivalence_Relation of (the Sorts of A)-carrier_of C
means
:: OSALG_4:def 9
for x,y being object holds [x,y] in it iff ex s1 being Element of S
st s1 in C & [x,y] in E.s1;
end;
:: we could give a name to Class CompClass(E,C)
:: restriction of Class CompClass(E,C) to A.s1
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
func OSClass(E,s1) -> Subset of Class(CompClass(E,CComp(s1))) means
:: OSALG_4:def 10
for z being set holds z in it iff ex x being set st x in (the Sorts of A).s1 &
z = Class( CompClass(E,CComp(s1)), x);
end;
registration
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
let s1 be Element of S;
cluster OSClass(E,s1) -> non empty;
end;
theorem :: OSALG_4:10
for S being locally_directed OrderSortedSign, A being OSAlgebra
of S, E being MSEquivalence-like (OrderSortedRelation of A), s1,s2 being
Element of S st s1 <= s2 holds OSClass(E,s1) c= OSClass(E,s2);
:: finally, this is analogy of the Many-Sorted Class E for order-sorted E
:: this definition should work for order-sorted MSCongruence too
:: if non-empty not needed, prove the following cluster
definition
let S be locally_directed OrderSortedSign;
let A be OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
func OSClass E -> OrderSortedSet of S means
:: OSALG_4:def 11
for s1 being Element of S holds it.s1 = OSClass(E,s1);
end;
registration
let S be locally_directed OrderSortedSign;
let A be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of A;
cluster OSClass E -> non-empty;
end;
:: order-sorted equiv of Class(R,x)
definition
let S be locally_directed OrderSortedSign;
let U1 be non-empty OSAlgebra of S;
let E be MSEquivalence-like OrderSortedRelation of U1;
let s be Element of S;
let x be Element of (the Sorts of U1).s;
func OSClass(E,x) -> Element of OSClass(E,s) equals
:: OSALG_4:def 12
Class( CompClass(E,
CComp(s)), x);
end;
theorem :: OSALG_4:11
for R being locally_directed non empty Poset, x,y being Element of R
st (ex z being Element of R st z <= x & z <= y) holds ex u being Element of R
st x <= u & y <= u;
theorem :: OSALG_4:12
for S be locally_directed OrderSortedSign, U1 be non-empty
OSAlgebra of S, E be MSEquivalence-like (OrderSortedRelation of U1),
s be Element of S, x,y be Element of (the Sorts of U1).s holds OSClass(E,x) =
OSClass(E,y) iff [x,y] in E.s;
theorem :: OSALG_4:13
for S be locally_directed OrderSortedSign, U1 be non-empty OSAlgebra
of S, E be MSEquivalence-like (OrderSortedRelation of U1), s1,s2 be Element of
S, x be Element of (the Sorts of U1).s1 st s1 <= s2 holds for y being Element
of (the Sorts of U1).s2 st y = x holds OSClass(E,x) = OSClass(E,y);
begin :: Order Sorted Quotient Algebra
:: take care (or even prove counterexample) - order-sorted
:: ManySortedFunction generaly does not exist
reserve S for locally_directed OrderSortedSign;
reserve o for Element of the carrier' of S;
:: multiclasses
definition
let S,o;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
let x be Element of Args(o,A);
func R #_os x -> Element of product ((OSClass R) * (the_arity_of o)) means
:: OSALG_4:def 13
for n be Nat st n in dom (the_arity_of o) ex y being Element of (the
Sorts of A).((the_arity_of o)/.n) st y = x.n & it.n = OSClass(R, y);
end;
:: the quotient will be different for order-sorted;
:: this def seems ok for order-sorted
definition
let S,o;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes(R,o) -> Function of ((the Sorts of A) * the ResultSort of S).
o, ((OSClass R) * the ResultSort of S).o means
:: OSALG_4:def 14
for x being Element of (
the Sorts of A).(the_result_sort_of o) holds it.x = OSClass(R,x);
func OSQuotArgs(R,o) -> Function of ((the Sorts of A)# * the Arity of S).o,
((OSClass R)# * the Arity of S).o means
:: OSALG_4:def 15
for x be Element of Args(o,A) holds it. x = R #_os x;
end;
definition
let S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotRes R -> ManySortedFunction of ((the Sorts of A) * the ResultSort
of S), ((OSClass R) * the ResultSort of S) means
:: OSALG_4:def 16
for o being OperSymbol of S holds it.o = OSQuotRes(R,o);
func OSQuotArgs R -> ManySortedFunction of (the Sorts of A)# * the Arity of
S, (OSClass R)# * the Arity of S means
:: OSALG_4:def 17
for o be OperSymbol of S holds it.o = OSQuotArgs(R,o);
end;
theorem :: OSALG_4:14
for A be non-empty OSAlgebra of S, R be OSCongruence of A, x be
set st x in ((OSClass R)# * the Arity of S).o ex a be Element of Args(o,A) st x
= R #_os a;
definition
let S,o;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact(R,o) -> Function of ((OSClass R)# * the Arity of S).o, ((
OSClass R) * the ResultSort of S).o means
:: OSALG_4:def 18
for a be Element of Args(o,A)
st R #_os a in ((OSClass R)# * the Arity of S).o holds it.(R #_os a) = ((
OSQuotRes(R,o)) * (Den(o,A))).a;
end;
definition
let S;
let A be non-empty OSAlgebra of S;
let R be OSCongruence of A;
func OSQuotCharact R -> ManySortedFunction of (OSClass R)# * the Arity of S,
(OSClass R) * the ResultSort of S means
:: OSALG_4:def 19
for o be OperSymbol of S holds it.o = OSQuotCharact(R,o);
end;
definition
let S;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func QuotOSAlg(U1,R) -> OSAlgebra of S equals
:: OSALG_4:def 20
MSAlgebra(# OSClass R,
OSQuotCharact R #);
end;
:: we could note that for discrete the QuotOSAlg and QuotMsAlg are equal
registration
let S;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
cluster QuotOSAlg (U1,R) -> strict non-empty;
end;
definition
let S;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
let s be Element of S;
func OSNat_Hom(U1,R,s) -> Function of (the Sorts of U1).s,OSClass(R,s) means
:: OSALG_4:def 21
for x being Element of (the Sorts of U1).s holds it.x = OSClass(R,x);
end;
definition
let S;
let U1 be non-empty OSAlgebra of S;
let R be OSCongruence of U1;
func OSNat_Hom(U1,R) -> ManySortedFunction of U1, QuotOSAlg (U1,R) means
:: OSALG_4:def 22
for s be Element of S holds it.s = OSNat_Hom(U1,R,s);
end;
theorem :: OSALG_4:15
for U1 be non-empty OSAlgebra of S, R be OSCongruence of U1 holds
OSNat_Hom(U1,R) is_epimorphism U1, QuotOSAlg (U1,R) & OSNat_Hom(U1,R) is
order-sorted;
theorem :: OSALG_4:16
for U1,U2 being non-empty OSAlgebra of S, F being
ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted
holds MSCng(F) is OSCongruence of U1;
:: just a casting func, currently no other way how to employ the type system
definition
let S;
let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
assume
F is_homomorphism U1,U2 & F is order-sorted;
func OSCng(F) -> OSCongruence of U1 equals
:: OSALG_4:def 23
MSCng(F);
end;
definition
let S;
let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let s be Element of S;
assume that
F is_homomorphism U1,U2 and
F is order-sorted;
func OSHomQuot(F,s) -> Function of (the Sorts of (QuotOSAlg (U1,OSCng F))).s
,(the Sorts of U2).s means
:: OSALG_4:def 24
for x be Element of (the Sorts of U1).s
holds it.(OSClass(OSCng(F),x)) = (F.s).x;
end;
:: this seems a bit too permissive, but same as the original
:: we should assume F order-sorted probably
definition
let S;
let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
func OSHomQuot(F) -> ManySortedFunction of (QuotOSAlg (U1, OSCng F)),U2
means
:: OSALG_4:def 25
for s be Element of S holds it.s = OSHomQuot(F,s);
end;
theorem :: OSALG_4:17
for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction
of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds OSHomQuot(F)
is_monomorphism QuotOSAlg (U1,OSCng F),U2 & OSHomQuot(F) is order-sorted;
theorem :: OSALG_4:18
for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction
of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds OSHomQuot(F)
is_isomorphism QuotOSAlg (U1,OSCng F),U2;
theorem :: OSALG_4:19
for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,
U2 st F is_epimorphism U1,U2 & F is order-sorted holds QuotOSAlg (U1,OSCng F),
U2 are_isomorphic;
:: monotone OSCongruence ... monotonicity is properly stronger
:: than MSCongruence, so we define it more broadly and prove the
:: ccluster then, however if used for other things than OSCongruences
:: the name of the attribute should be changed
:: this condition is nontrivial only for nonmonotone osas (see further),
:: where Den(o1,U1).x1 can differ from Den(o2,U2).x1
:: is OK for constants ... their Args is always {{}}, so o1 <= o2
:: implies for them [Den(o1,U1).{},Den(o2,U1).{}] in R
definition
let S be OrderSortedSign, U1 be non-empty OSAlgebra of S, R be
MSEquivalence-like OrderSortedRelation of U1;
attr R is monotone means
:: OSALG_4:def 26
for o1,o2 being OperSymbol of S st o1 <= o2
for x1 being Element of Args(o1,U1) for x2 being Element of Args(o2,U1) st (
for y being Nat st y in dom x1 holds [x1.y,x2.y] in R.((the_arity_of o2)/.y) )
holds [Den(o1,U1).x1,Den(o2,U1).x2] in R.(the_result_sort_of o2);
end;
theorem :: OSALG_4:20
for S being OrderSortedSign, U1 being non-empty OSAlgebra of S
holds [| the Sorts of U1, the Sorts of U1 |] is OSCongruence of U1;
theorem :: OSALG_4:21
for S being OrderSortedSign, U1 being non-empty OSAlgebra of S,
R being OSCongruence of U1 st R = [| (the Sorts of U1), (the Sorts of U1) |]
holds R is monotone;
registration
let S be OrderSortedSign, U1 be non-empty OSAlgebra of S;
cluster monotone for OSCongruence of U1;
end;
registration
let S be OrderSortedSign, U1 be non-empty OSAlgebra of S;
cluster monotone for MSEquivalence-like OrderSortedRelation of U1;
end;
theorem :: OSALG_4:22
for S being OrderSortedSign, U1 being non-empty OSAlgebra of S,
R being monotone MSEquivalence-like OrderSortedRelation of U1 holds R is
MSCongruence-like;
registration
let S be OrderSortedSign, U1 be non-empty OSAlgebra of S;
cluster monotone -> MSCongruence-like for MSEquivalence-like
OrderSortedRelation of U1;
end;
theorem :: OSALG_4:23
for S being OrderSortedSign, U1 being monotone non-empty
OSAlgebra of S, R being OSCongruence of U1 holds R is monotone;
registration
let S be OrderSortedSign, U1 be monotone non-empty OSAlgebra of S;
cluster -> monotone for OSCongruence of U1;
end;
:: monotonicity of quotient by monotone oscongruence
registration
let S;
let U1 be non-empty OSAlgebra of S;
let R be monotone OSCongruence of U1;
cluster QuotOSAlg(U1,R) -> monotone;
end;
theorem :: OSALG_4:24
for U1 being non-empty OSAlgebra of S, U2 being monotone non-empty
OSAlgebra of S, F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2
& F is order-sorted holds OSCng(F) is monotone;
:: these are a bit more general versions of OSHomQuot, that
:: I need for OSAFREE; more proper way how to do this is restating
:: the MSUALG_9 quotient theorems for OSAs, but that's more work
definition
let S;
let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
let s be Element of S;
assume that
F is_homomorphism U1,U2 and
F is order-sorted and
R c= OSCng F;
func OSHomQuot(F,R,s) -> Function of (the Sorts of (QuotOSAlg (U1,R))).s,(
the Sorts of U2).s means
:: OSALG_4:def 27
for x be Element of (the Sorts of U1).s holds it.(OSClass(R,x)) = (F.s).x;
end;
:: this seems a bit too permissive, but same as the original
:: we should assume F order-sorted probably
definition
let S;
let U1,U2 be non-empty OSAlgebra of S;
let F be ManySortedFunction of U1,U2;
let R be OSCongruence of U1;
func OSHomQuot(F,R) -> ManySortedFunction of (QuotOSAlg (U1, R)),U2 means
:: OSALG_4:def 28
for s be Element of S holds it.s = OSHomQuot(F,R,s);
end;
theorem :: OSALG_4:25
for U1,U2 be non-empty OSAlgebra of S, F be ManySortedFunction of U1,
U2, R be OSCongruence of U1 st F is_homomorphism U1,U2 & F is order-sorted & R
c= OSCng F holds OSHomQuot(F,R) is_homomorphism QuotOSAlg (U1,R),U2 & OSHomQuot
(F,R) is order-sorted;