:: Quantales
:: by Grzegorz Bancerek
::
:: Received May 9, 1994
:: Copyright (c) 1994-2016 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, SUBSET_1, TARSKI, LATTICES, STRUCT_0, ALGSTR_0,
EQREL_1, PBOOLE, LATTICE3, BINOP_1, FUNCT_1, WAYBEL_0, FINSET_1, RELAT_1,
VECTSP_1, FINSEQ_1, GROUP_1, REWRITE1, SETWISEO, ZFMISC_1, SEQM_3,
GRAPH_1, FUNCT_3, SETFAM_1, QUANTAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1,
SETWISEO, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, FINSET_1,
DOMAIN_1, LATTICES, LATTICE3, MONOID_0;
constructors SETFAM_1, BINOP_1, DOMAIN_1, SETWISEO, VECTSP_1, LATTICE3,
RELSET_1, GROUP_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
STRUCT_0, LATTICES, LATTICE3, ALGSTR_0, RELSET_1;
requirements BOOLE, SUBSET;
begin
scheme :: QUANTAL1:sch 1
DenestFraenkel {A()->non empty set, B()->non empty set, F(set)->set, G(set)
->Element of B(), P[set]}: {F(a) where a is Element of B(): a in {G(b) where b
is Element of A(): P[b]}} = {F(G(a)) where a is Element of A(): P[a]};
scheme :: QUANTAL1:sch 2
EmptyFraenkel {A() -> non empty set, f(set) -> set, P[set]}: {f(a) where a
is Element of A(): P[a]} = {}
provided
not ex a being Element of A() st P[a];
theorem :: QUANTAL1:1
for L1,L2 being non empty LattStr st the LattStr of L1 = the
LattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 =
a2 & b1 = b2 holds a1"\/"b1 = a2"\/"b2 & a1"/\"b1 = a2"/\"b2 & (a1 [= b1 iff a2
[= b2);
theorem :: QUANTAL1:2
for L1,L2 being non empty LattStr st the LattStr of L1 = the
LattStr of L2 for a being Element of L1, b being Element of L2, X being set st
a = b holds (a is_less_than X iff b is_less_than X) & (a is_greater_than X iff
b is_greater_than X);
definition
let L be 1-sorted;
mode UnOp of L is Function of L,L;
end;
definition
let L be non empty LattStr, X be Subset of L;
attr X is directed means
:: QUANTAL1:def 1
for Y being finite Subset of X ex x being Element
of L st "\/"(Y, L) [= x & x in X;
end;
theorem :: QUANTAL1:3
for L being non empty LattStr, X being Subset of L st X is directed
holds X is non empty;
definition
struct (LattStr, multMagma) QuantaleStr (# carrier -> set, L_join, L_meet,
multF -> BinOp of the carrier #);
end;
registration
cluster non empty for QuantaleStr;
end;
definition
struct (QuantaleStr, multLoopStr) QuasiNetStr (# carrier -> set, L_join,
L_meet, multF -> (BinOp of the carrier), OneF -> Element of the carrier #);
end;
registration
cluster non empty for QuasiNetStr;
end;
definition
let IT be non empty multMagma;
attr IT is with_left-zero means
:: QUANTAL1:def 2
ex a being Element of IT st for b being Element of IT holds a*b = a;
attr IT is with_right-zero means
:: QUANTAL1:def 3
ex b being Element of IT st for a being Element of IT holds a*b = b;
end;
definition
let IT be non empty multMagma;
attr IT is with_zero means
:: QUANTAL1:def 4
IT is with_left-zero with_right-zero;
end;
registration
cluster with_zero -> with_left-zero with_right-zero for
non empty multMagma;
cluster with_left-zero with_right-zero -> with_zero for
non empty multMagma;
end;
registration
cluster with_zero for non empty multMagma;
end;
definition
let IT be non empty QuantaleStr;
attr IT is right-distributive means
:: QUANTAL1:def 5
for a being Element of IT, X
being set holds a [*] "\/"(X,IT) = "\/"({a [*] b where b is Element of IT: b in
X},IT);
attr IT is left-distributive means
:: QUANTAL1:def 6
for a being Element of IT, X
being set holds "\/"(X,IT) [*] a = "\/"({b [*] a where b is Element of IT: b in
X},IT);
attr IT is times-additive means
:: QUANTAL1:def 7
for a,b,c being Element of IT holds (a"\/"b)
[*]c = (a[*]c)"\/"(b[*]c) & c[*](a"\/"b) = (c[*]a)"\/"(c[*]b);
attr IT is times-continuous means
:: QUANTAL1:def 8
for X1, X2 being Subset of IT st X1 is
directed & X2 is directed holds ("\/"X1)[*]("\/"X2) = "\/"({a [*] b where a is
Element of IT, b is Element of IT: a in X1 & b in X2},IT);
end;
reserve x,y,z for set;
theorem :: QUANTAL1:4
for Q being non empty QuantaleStr st the LattStr of Q = BooleLatt
{} holds Q is associative commutative unital with_zero complete
right-distributive left-distributive Lattice-like;
registration
let A be non empty set, b1,b2,b3 be BinOp of A;
cluster QuantaleStr(#A,b1,b2,b3#) -> non empty;
end;
registration
cluster associative commutative unital with_zero left-distributive
right-distributive complete Lattice-like for non empty QuantaleStr;
end;
scheme :: QUANTAL1:sch 3
LUBFraenkelDistr {Q() -> complete Lattice-like non empty QuantaleStr, f(
set, set) -> Element of Q(), X, Y() -> set}: "\/"({"\/"({f(a,b) where b is
Element of Q(): b in Y()},Q()) where a is Element of Q(): a in X()}, Q()) =
"\/"({f(a,b) where a is Element of Q(), b is Element of Q(): a in X() & b in Y(
)}, Q());
reserve Q for left-distributive right-distributive complete Lattice-like non
empty QuantaleStr,
a, b, c, d for Element of Q;
theorem :: QUANTAL1:5
for Q for X,Y being set holds "\/"(X,Q) [*] "\/"(Y,Q) = "\/"({a
[*] b: a in X & b in Y}, Q);
theorem :: QUANTAL1:6
(a"\/"b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a"\/"b) = (c
[*] a) "\/" (c [*] b);
registration
let A be non empty set, b1,b2,b3 be (BinOp of A), e be Element of A;
cluster QuasiNetStr(#A,b1,b2,b3,e#) -> non empty;
end;
registration
cluster complete Lattice-like for non empty QuasiNetStr;
end;
registration
cluster left-distributive right-distributive -> times-continuous
times-additive for complete Lattice-like non empty QuasiNetStr;
end;
registration
cluster associative commutative unital with_zero with_left-zero
left-distributive right-distributive complete Lattice-like for non empty
QuasiNetStr;
end;
definition
mode Quantale is associative left-distributive right-distributive complete
Lattice-like non empty QuantaleStr;
mode QuasiNet is unital associative with_left-zero times-continuous
times-additive complete Lattice-like non empty QuasiNetStr;
end;
definition
mode BlikleNet is with_zero non empty QuasiNet;
end;
theorem :: QUANTAL1:7
for Q being unital non empty QuasiNetStr st Q is Quantale holds Q is
BlikleNet;
reserve Q for Quantale,
a,a9,b,b9,c,d,d1,d2,D for Element of Q;
theorem :: QUANTAL1:8
a [= b implies a [*] c [= b [*] c & c [*] a [= c [*] b;
theorem :: QUANTAL1:9
a [= b & c [= d implies a [*] c [= b [*] d;
definition
let f be Function;
attr f is idempotent means
:: QUANTAL1:def 9
f * f = f;
end;
definition
let L be non empty LattStr;
let IT be UnOp of L;
attr IT is inflationary means
:: QUANTAL1:def 10
for p being Element of L holds p [= IT.p;
attr IT is deflationary means
:: QUANTAL1:def 11
for p being Element of L holds IT.p [= p;
attr IT is monotone means
:: QUANTAL1:def 12
for p,q being Element of L st p [= q holds IT.p [= IT.q;
attr IT is \/-distributive means
:: QUANTAL1:def 13
for X being Subset of L holds IT."\/"X [=
"\/"({IT.a where a is Element of L: a in X}, L);
end;
registration
let L be Lattice;
cluster inflationary deflationary monotone for UnOp of L;
end;
theorem :: QUANTAL1:10
for L being complete Lattice, j being UnOp of L st j is monotone
holds j is \/-distributive iff for X being Subset of L holds j."\/"X = "\/"({j.
a where a is Element of L: a in X}, L);
definition
let Q be non empty QuantaleStr;
let IT be UnOp of Q;
attr IT is times-monotone means
:: QUANTAL1:def 14
for a,b being Element of Q holds IT.a [*] IT .b [= IT.(a [*] b);
end;
definition
let Q be non empty QuantaleStr, a,b be Element of Q;
func a -r> b -> Element of Q equals
:: QUANTAL1:def 15
"\/"({ c where c is Element of Q: c [*]
a [= b }, Q);
func a -l> b -> Element of Q equals
:: QUANTAL1:def 16
"\/"({ c where c is Element of Q: a [*]
c [= b }, Q);
end;
theorem :: QUANTAL1:11
a [*] b [= c iff b [= a -l> c;
theorem :: QUANTAL1:12
a [*] b [= c iff a [= b -r> c;
theorem :: QUANTAL1:13
for Q being Quantale, s,a,b being Element of Q st a [= b holds b
-r>s [= a-r>s & b-l>s [= a-l>s;
theorem :: QUANTAL1:14
for Q being Quantale, s being Element of Q, j being UnOp of Q st for a
being Element of Q holds j.a = (a-r>s)-r>s holds j is monotone;
definition
let Q be non empty QuantaleStr;
let IT be Element of Q;
attr IT is dualizing means
:: QUANTAL1:def 17
for a being Element of Q holds (a-r>IT) -l>IT = a & (a-l>IT)-r>IT = a;
attr IT is cyclic means
:: QUANTAL1:def 18
for a being Element of Q holds a -r> IT = a -l> IT;
end;
theorem :: QUANTAL1:15
c is cyclic iff for a,b st a [*] b [= c holds b [*] a [= c;
theorem :: QUANTAL1:16
for Q being Quantale, s,a being Element of Q st s is cyclic
holds a [= (a-r>s)-r>s & a [= (a-l>s)-l>s;
theorem :: QUANTAL1:17
for Q being Quantale, s,a being Element of Q st s is cyclic holds a-r>
s = ((a-r>s)-r>s)-r>s & a-l>s = ((a-l>s)-l>s)-l>s;
theorem :: QUANTAL1:18
for Q being Quantale, s,a,b being Element of Q holds ((a-r>s)-r>s)[*](
(b-r>s)-r>s) [= ((a[*]b)-r>s)-r>s;
theorem :: QUANTAL1:19
D is dualizing implies Q is unital & the_unity_wrt the multF of
Q = D -r> D & the_unity_wrt the multF of Q = D -l> D;
theorem :: QUANTAL1:20
a is dualizing implies b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = (
(c -r> a) [*] b) -l> a;
definition
struct (QuasiNetStr) Girard-QuantaleStr (# carrier -> set, L_join, L_meet,
multF -> (BinOp of the carrier), OneF, absurd -> Element of the carrier #);
end;
registration
cluster non empty for Girard-QuantaleStr;
end;
definition
let IT be non empty Girard-QuantaleStr;
attr IT is cyclic means
:: QUANTAL1:def 19
the absurd of IT is cyclic;
attr IT is dualized means
:: QUANTAL1:def 20
the absurd of IT is dualizing;
end;
theorem :: QUANTAL1:21
for Q being non empty Girard-QuantaleStr st the LattStr of Q =
BooleLatt {} holds Q is cyclic dualized;
registration
let A be non empty set, b1,b2,b3 be (BinOp of A), e1,e2 be Element of A;
cluster Girard-QuantaleStr(#A,b1,b2,b3,e1,e2#) -> non empty;
end;
registration
cluster associative commutative unital left-distributive right-distributive
complete Lattice-like cyclic dualized strict for
non empty Girard-QuantaleStr;
end;
definition
mode Girard-Quantale is associative unital left-distributive
right-distributive complete Lattice-like cyclic dualized non empty
Girard-QuantaleStr;
end;
definition
let G be Girard-QuantaleStr;
func Bottom G -> Element of G equals
:: QUANTAL1:def 21
the absurd of G;
end;
definition
let G be non empty Girard-QuantaleStr;
func Top G -> Element of G equals
:: QUANTAL1:def 22
(Bottom G) -r> Bottom G;
let a be Element of G;
func Bottom a -> Element of G equals
:: QUANTAL1:def 23
a -r> Bottom G;
end;
definition
let G be non empty Girard-QuantaleStr;
func Negation G -> UnOp of G means
:: QUANTAL1:def 24
for a being Element of G holds it.a = Bottom a;
end;
definition
let G be non empty Girard-QuantaleStr, u be UnOp of G;
func Bottom u -> UnOp of G equals
:: QUANTAL1:def 25
Negation(G)*u;
end;
definition
let G be non empty Girard-QuantaleStr, o be BinOp of G;
func Bottom o -> BinOp of G equals
:: QUANTAL1:def 26
Negation(G)*o;
end;
reserve Q for Girard-Quantale,
a,a1,a2,b,b1,b2,c,d for Element of Q,
X for set;
theorem :: QUANTAL1:22
Bottom Bottom a = a;
theorem :: QUANTAL1:23
a [= b implies Bottom b [= Bottom a;
theorem :: QUANTAL1:24
Bottom "\/"(X,Q) = "/\"({Bottom a: a in X}, Q);
theorem :: QUANTAL1:25
Bottom "/\"(X,Q) = "\/"({Bottom a: a in X}, Q);
theorem :: QUANTAL1:26
Bottom (a"\/"b) = Bottom a"/\"Bottom b & Bottom (a"/\"b) =
Bottom a"\/"Bottom b;
definition
let Q,a,b;
func a delta b -> Element of Q equals
:: QUANTAL1:def 27
Bottom (Bottom a [*] Bottom b);
end;
theorem :: QUANTAL1:27
a [*] "\/"(X,Q) = "\/"({a [*] b: b in X}, Q) & a delta "/\"(X,Q) =
"/\"({a delta c: c in X}, Q);
theorem :: QUANTAL1:28
"\/"(X,Q) [*] a = "\/"({b [*] a: b in X}, Q) & "/\"(X,Q) delta a =
"/\"({c delta a: c in X}, Q);
theorem :: QUANTAL1:29
a delta (b"/\"c) = (a delta b)"/\"(a delta c) & (b"/\"c) delta a = (b
delta a)"/\"(c delta a);
theorem :: QUANTAL1:30
a1 [= b1 & a2 [= b2 implies a1 delta a2 [= b1 delta b2;
theorem :: QUANTAL1:31
a delta b delta c = a delta (b delta c);
theorem :: QUANTAL1:32
a [*] Top Q = a & Top Q [*] a = a;
theorem :: QUANTAL1:33
a delta Bottom Q = a & (Bottom Q) delta a = a;
theorem :: QUANTAL1:34
for Q being Quantale for j being UnOp of Q st j is monotone idempotent
\/-distributive ex L being complete Lattice st the carrier of L = rng j & for X
being Subset of L holds "\/"X = j."\/"(X,Q);