:: Duality Based on Galois Connection. Part I
:: by Grzegorz Bancerek
::
:: Received August 8, 2001
:: Copyright (c) 2001-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 REWRITE1, WAYBEL_0, WAYBEL_1, FUNCT_1, XBOOLE_0, ORDERS_2,
SEQM_3, SUBSET_1, XXREAL_0, RELAT_1, LATTICES, EQREL_1, ORDINAL2,
STRUCT_0, ARYTM_0, ALTCAT_1, CAT_1, ZFMISC_1, YELLOW21, FILTER_0,
WELLORD1, ORDERS_1, SETFAM_1, QC_LANG1, TARSKI, FUNCTOR0, FUNCT_2,
WAYBEL11, YELLOW_9, RCOMP_1, CARD_FIL, YELLOW_0, RELAT_2, WAYBEL_3,
LATTICE3, PRE_TOPC, GROUP_6, ALTCAT_2, FUNCOP_1, YELLOW20, YELLOW18,
WAYBEL_8, FINSET_1, WAYBEL34;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, ORDERS_1, DOMAIN_1,
FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, WELLORD1, ALTCAT_1, FUNCTOR0,
ALTCAT_2, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, PRE_TOPC, T_0TOPSP,
WAYBEL_3, WAYBEL_8, YELLOW_7, WAYBEL11, YELLOW_9, WAYBEL18, YELLOW18,
YELLOW20, YELLOW21;
constructors WELLORD1, BORSUK_1, T_0TOPSP, WAYBEL_8, WAYBEL11, YELLOW_9,
WAYBEL18, YELLOW18, YELLOW20, YELLOW21, WAYBEL20;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELSET_1, FUNCT_2, FINSET_1,
STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0, ALTCAT_2, FUNCTOR0,
WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_7, WAYBEL_8,
WAYBEL10, WAYBEL11, FUNCTOR2, ALTCAT_4, LATTICE5, WAYBEL17, YELLOW_9,
WAYBEL21, YELLOW18, YELLOW21, RELAT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, PRE_TOPC, T_0TOPSP, LATTICE3, YELLOW_0, WAYBEL_0,
WAYBEL_1, WAYBEL_3, WAYBEL11, FUNCTOR0, YELLOW21, XBOOLE_0;
equalities SUBSET_1, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW21,
BINOP_1, STRUCT_0, RELAT_1;
expansions TARSKI, PRE_TOPC, T_0TOPSP, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3,
WAYBEL11, XBOOLE_0;
theorems ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, ORDERS_2, ORDERS_3,
TSEP_1, TARSKI, FUNCOP_1, ALTCAT_1, ALTCAT_2, ALTCAT_4, FUNCTOR0,
FUNCTOR1, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL_6,
YELLOW_7, WAYBEL_8, YELLOW_3, WAYBEL_9, YELLOW_9, WAYBEL11, WAYBEL15,
WAYBEL17, WAYBEL18, WAYBEL20, WAYBEL21, YELLOW18, YELLOW20, YELLOW21,
XBOOLE_0, XBOOLE_1, SETFAM_1, PARTFUN1;
schemes FINSET_1, YELLOW18, YELLOW20, YELLOW21;
begin
::Infs-preserving and sups-preserving maps
registration
let S,T be complete LATTICE;
cluster Galois for Connection of S,T;
existence
proof set g = the infs-preserving Function of S,T;
g is upper_adjoint by WAYBEL_1:16;
then ex d being Function of T,S st [g,d] is Galois;
hence thesis;
end;
end;
theorem Th1:
for S,T, S9,T9 being non empty RelStr
st the RelStr of S = the RelStr of S9 & the RelStr of T = the RelStr of T9
for c being Connection of S,T, c9 being Connection of S9,T9 st c = c9
holds c is Galois implies c9 is Galois
proof
let S,T, S9,T9 being non empty RelStr such that
A1: the RelStr of S = the RelStr of S9 and
A2: the RelStr of T = the RelStr of T9;
let c be Connection of S,T, c9 be Connection of S9,T9 such that
A3: c = c9;
given g being Function of S,T, d being Function of T,S such that
A4: c = [g,d] and
A5: g is monotone and
A6: d is monotone and
A7: for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s;
reconsider g9 = g as Function of S9, T9 by A1,A2;
reconsider d9 = d as Function of T9, S9 by A1,A2;
take g9,d9;
thus c9 = [g9,d9] by A3,A4;
thus g9 is monotone & d9 is monotone by A1,A2,A5,A6,WAYBEL_9:1;
let t9 be Element of T9, s9 be Element of S9;
reconsider t = t9 as Element of T by A2;
reconsider s = s9 as Element of S by A1;
A8: t9 <= g9.s9 iff t <= g.s by A2,YELLOW_0:1;
d9.t9 <= s9 iff d.t <= s by A1,YELLOW_0:1;
hence thesis by A7,A8;
end;
definition
let S,T be LATTICE;
let g be Function of S,T;
assume that
A1: S is complete and
A2: g is infs-preserving;
A3: g is upper_adjoint by A1,A2,WAYBEL_1:16;
func LowerAdj g -> Function of T,S means
: Def1:
[g, it] is Galois;
uniqueness
proof
let d1,d2 be Function of T,S such that
A4: [g, d1] is Galois and
A5: [g, d2] is Galois;
now
let t be Element of T;
reconsider t9 = t as Element of T;
A6: d1.t9 is_minimum_of g"(uparrow t) by A4,WAYBEL_1:10;
A7: d2.t9 is_minimum_of g"(uparrow t ) by A5,WAYBEL_1:10;
d1.t = "/\"(g"(uparrow t), S) by A6;
hence d1.t = d2.t by A7;
end;
hence thesis by FUNCT_2:63;
end;
existence by A3;
end;
definition
let S,T be LATTICE;
let d be Function of T,S;
assume that
A1: T is complete and
A2: d is sups-preserving;
A3: d is lower_adjoint by A1,A2,WAYBEL_1:17;
func UpperAdj d -> Function of S,T means
: Def2:
[it, d] is Galois;
existence by A3;
correctness
proof
let g1,g2 be Function of S,T such that
A4: [g1, d] is Galois and
A5: [g2, d] is Galois;
now
let t be Element of S;
reconsider t9 = t as Element of S;
A6: g1.t9 is_maximum_of d"(downarrow t) by A4,WAYBEL_1:11;
A7: g2.t9 is_maximum_of d"(downarrow t) by A5,WAYBEL_1:11;
g1.t = "\/"(d"(downarrow t), T) by A6;
hence g1.t = g2.t by A7;
end;
hence thesis by FUNCT_2:63;
end;
end;
Lm1: now
let S,T be LATTICE;
assume that
A1: S is complete and
A2: T is complete;
reconsider S9 = S, T9 = T as complete LATTICE by A1,A2;
let g be Function of S,T;
assume g is infs-preserving;
then reconsider g9 = g as infs-preserving Function of S9, T9;
[g9, LowerAdj g9] is Galois by Def1;
then LowerAdj g9 is lower_adjoint monotone by WAYBEL_1:8;
hence LowerAdj g is monotone lower_adjoint sups-preserving;
end;
Lm2: now
let S,T be LATTICE;
assume that
A1: S is complete and
A2: T is complete;
reconsider S9 = S, T9 = T as complete LATTICE by A1,A2;
let g be Function of S,T;
assume g is sups-preserving;
then reconsider g9 = g as sups-preserving Function of S9, T9;
[UpperAdj g9, g9] is Galois by Def2;
then UpperAdj g9 is upper_adjoint monotone by WAYBEL_1:8;
hence UpperAdj g is monotone upper_adjoint infs-preserving;
end;
registration
let S,T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster LowerAdj g -> lower_adjoint; :: sups-preserving
coherence by Lm1;
end;
registration
let S,T be complete LATTICE;
let d be sups-preserving Function of T,S;
cluster UpperAdj d -> upper_adjoint; :: infs-preserving
coherence by Lm2;
end;
theorem
for S,T being complete LATTICE for g being infs-preserving Function of S,T
for t being Element of T holds (LowerAdj g).t = inf (g"uparrow t)
proof
let S,T be complete LATTICE;
let g be infs-preserving Function of S,T;
let t be Element of T;
[g, LowerAdj g] is Galois by Def1;
then (LowerAdj g).t is_minimum_of g"(uparrow t) by WAYBEL_1:10;
hence thesis;
end;
theorem
for S,T being complete LATTICE for d being sups-preserving Function of T,S
for s being Element of S holds (UpperAdj d).s = sup (d"downarrow s)
proof
let S,T be complete LATTICE;
let d be sups-preserving Function of T,S;
let s be Element of S;
[UpperAdj d, d] is Galois by Def2;
then (UpperAdj d).s is_maximum_of d"(downarrow s) by WAYBEL_1:11;
hence thesis;
end;
definition
let S,T be RelStr;
let f be Function of the carrier of S, the carrier of T;
func f opp -> Function of S opp, T opp equals
f;
coherence;
end;
registration
let S,T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster g opp -> lower_adjoint;
coherence
proof
[g, LowerAdj g] is Galois by Def1;
then [(LowerAdj g) opp, g opp] is Galois by YELLOW_7:44;
hence thesis;
end;
end;
registration
let S,T be complete LATTICE;
let d be sups-preserving Function of S,T;
cluster d opp -> upper_adjoint;
coherence
proof
[UpperAdj d, d] is Galois by Def2;
then [d opp, (UpperAdj d) opp] is Galois by YELLOW_7:44;
hence thesis;
end;
end;
theorem
for S,T being complete LATTICE for g being infs-preserving Function of S, T
holds LowerAdj g = UpperAdj (g opp)
proof
let S,T be complete LATTICE;
let g be infs-preserving Function of S, T;
[g, LowerAdj g] is Galois by Def1;
then [(LowerAdj g) opp, g opp] is Galois by YELLOW_7:44;
hence thesis by Def2;
end;
theorem
for S,T being complete LATTICE for d being sups-preserving Function of S, T
holds LowerAdj (d opp) = UpperAdj d
proof
let S,T be complete LATTICE;
let d be sups-preserving Function of S, T;
[UpperAdj d, d] is Galois by Def2;
then [d opp, (UpperAdj d) opp] is Galois by YELLOW_7:44;
hence thesis by Def1;
end;
theorem Th6:
for L be non empty RelStr holds [id L, id L] is Galois
proof
let L be non empty RelStr;
take g = id L, d = id L;
thus [id L, id L] = [g,d] & g is monotone & d is monotone;
let t,s be Element of L;
g.s = s by FUNCT_1:18;
hence thesis by FUNCT_1:18;
end;
theorem Th7: :: 1.2. LEMMA, p. 179
:: LowerAdj and UpperAdj preserve identities
for L being complete LATTICE holds
LowerAdj id L = id L & UpperAdj id L = id L
proof
let L be complete LATTICE;
[id L, id L] is Galois by Th6;
hence thesis by Def1,Def2;
end;
theorem Th8: :: 1.2. LEMMA, p. 179
:: LowerAdj preserves contravariantly composition
for L1,L2,L3 being complete LATTICE
for g1 being infs-preserving Function of L1,L2
for g2 being infs-preserving Function of L2,L3 holds
LowerAdj (g2*g1) = (LowerAdj g1)*(LowerAdj g2)
proof
let L1,L2,L3 be complete LATTICE;
let g1 be infs-preserving Function of L1,L2;
let g2 be infs-preserving Function of L2,L3;
A1: [g1, LowerAdj g1] is Galois by Def1;
[g2, LowerAdj g2] is Galois by Def1;
then
A2: [g2*g1, (LowerAdj g1)*(LowerAdj g2)] is Galois by A1,WAYBEL15:5;
g2*g1 is infs-preserving by WAYBEL20:25;
hence thesis by A2,Def1;
end;
theorem Th9: :: 1.2. LEMMA, p. 179
:: UpperAdj preserves contravariantly composition
for L1,L2,L3 being complete LATTICE
for d1 being sups-preserving Function of L1,L2
for d2 being sups-preserving Function of L2,L3 holds
UpperAdj (d2*d1) = (UpperAdj d1)*(UpperAdj d2)
proof
let L1,L2,L3 be complete LATTICE;
let d1 be sups-preserving Function of L1,L2;
let d2 be sups-preserving Function of L2,L3;
A1: [UpperAdj d1, d1] is Galois by Def2;
[UpperAdj d2, d2] is Galois by Def2;
then
A2: [(UpperAdj d1)*(UpperAdj d2), d2*d1] is Galois by A1,WAYBEL15:5;
d2*d1 is sups-preserving by WAYBEL20:27;
hence thesis by A2,Def2;
end;
theorem Th10: :: 1.3. THEOREM, p. 179
for S,T being complete LATTICE for g being infs-preserving Function of S,T
holds UpperAdj LowerAdj g = g
proof
let S,T be complete LATTICE;
let g be infs-preserving Function of S,T;
[g, LowerAdj g] is Galois by Def1;
hence thesis by Def2;
end;
theorem Th11: :: 1.3. THEOREM, p. 179
for S,T being complete LATTICE for d being sups-preserving Function of S,T
holds LowerAdj UpperAdj d = d
proof
let S,T be complete LATTICE;
let d be sups-preserving Function of S,T;
[UpperAdj d, d] is Galois by Def2;
hence thesis by Def1;
end;
theorem Th12:
for C being non empty AltCatStr
for a,b,f being object st f in (the Arrows of C).(a,b)
ex o1,o2 being Object of C
st o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2
proof
let C be non empty AltCatStr;
let a,b,f be object;
assume
A1: f in (the Arrows of C).(a,b);
then [a,b] in dom the Arrows of C by FUNCT_1:def 2;
then [a,b] in [:the carrier of C, the carrier of C:];
then reconsider o1 = a, o2 = b as Object of C by ZFMISC_1:87;
take o1, o2;
thus thesis by A1,ALTCAT_1:def 1;
end;
definition :: 1.1 DEFINITION, p. 179
let W be non empty set;
defpred L[LATTICE] means $1 is complete;
defpred P[LATTICE,LATTICE,Function of $1,$2] means $3 is infs-preserving;
given w being Element of W such that
A1: w is non empty;
func W-INF_category -> lattice-wise strict category means
:
Def4: (for x being LATTICE holds
x is Object of it iff x is strict complete & the carrier of x in W) &
for a,b being Object of it, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff f is infs-preserving;
existence
proof
reconsider w as non empty set by A1;
set r = the upper-bounded well-ordering Order of w;
RelStr(#w,r#) is complete;
then
A2: ex x being strict LATTICE st L[x] & the carrier of x in W;
A3: for a,b,c being LATTICE st L[a] & L[b] & L[c]
for f being Function of a,b, g being Function
of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] by WAYBEL20:25;
A4: for a being LATTICE st L[a] holds P[a,a,id a];
thus
ex C being lattice-wise strict category st (for x being LATTICE holds
x is Object of C iff x is strict & L[x] & the carrier of x in W) &
for a,b being Object of C, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff P[latt a, latt b, f] from YELLOW21:sch 3(A2,A3,
A4);
end;
uniqueness
proof
let C1, C2 be lattice-wise strict category such that
A5: for x being LATTICE holds
x is Object of C1 iff x is strict & L[x] & the carrier of x in W and
A6: for a,b being Object of C1, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff f is infs-preserving and
A7: for x being LATTICE holds
x is Object of C2 iff x is strict & L[x] & the carrier of x in W and
A8: for a,b being Object of C2, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff f is infs-preserving;
defpred Q[set, set, set] means
ex L1,L2 being LATTICE, f being Function of L1,L2
st $1 = L1 & $2 = L2 & $3 = f & f is infs-preserving;
A9: now
let a,b be Object of C1;
let f be monotone Function of latt a, latt b;
f in <^a,b^> iff f is infs-preserving by A6;
hence f in <^a,b^> iff Q[a,b,f];
end;
A10: now
let a,b be Object of C2;
let f be monotone Function of latt a, latt b;
f in <^a,b^> iff f is infs-preserving by A8;
hence f in <^a,b^> iff Q[a,b,f];
end;
for C1, C2 being lattice-wise category st (for x being LATTICE holds
x is Object of C1 iff x is strict & L[x] & the carrier of x in W) &
(for a,b being Object of C1, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff Q[a, b, f]) & (for x being LATTICE holds
x is Object of C2 iff x is strict & L[x] & the carrier of x in W) &
(for a,b being Object of C2, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff Q[a, b, f])
holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW21:sch 5;
hence thesis by A5,A7,A9,A10;
end;
end;
Lm3: for W being with_non-empty_element set
for a,b being LATTICE, f being Function of a,b
holds f in (the Arrows of W-INF_category).(a,b) iff
a in the carrier of W-INF_category & b in the carrier of W-INF_category &
a is complete & b is complete & f is infs-preserving
proof
let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
let a,b be LATTICE, f be Function of a,b;
set A = W-INF_category;
hereby
assume f in (the Arrows of A).(a,b);
then consider o1, o2 being Object of A such that
A2: o1 = a and
A3: o2 = b and
A4: f in <^o1,o2^> and f is Morphism of o1, o2 by Th12;
reconsider g = f as Morphism of o1,o2 by A4;
thus a in the carrier of A & b in the carrier of A by A2,A3;
thus a is complete & b is complete by A1,A2,A3,Def4;
@g = f by A4,YELLOW21:def 7;
hence f is infs-preserving by A1,A2,A3,A4,Def4;
end;
assume that
A5: a in the carrier of W-INF_category and
A6: b in the carrier of W-INF_category;
reconsider x = a, y = b as Object of A by A5,A6;
A7: latt x = a;
A8: latt y = b;
assume that
a is complete and b is complete and
A9: f is infs-preserving;
f in <^x,y^> by A1,A7,A8,A9,Def4;
hence thesis by ALTCAT_1:def 1;
end;
definition :: 1.1 DEFINITION, p. 179
let W be non empty set;
defpred L[LATTICE] means $1 is complete;
defpred P[LATTICE,LATTICE,Function of $1,$2] means $3 is sups-preserving;
given w being Element of W such that
A1: w is non empty;
func W-SUP_category -> lattice-wise strict category means
:
Def5: (for x being LATTICE holds
x is Object of it iff x is strict complete & the carrier of x in W) &
for a,b being Object of it, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff f is sups-preserving;
existence
proof
reconsider w as non empty set by A1;
set r = the upper-bounded well-ordering Order of w;
RelStr(#w,r#) is complete;
then
A2: ex x being strict LATTICE st L[x] & the carrier of x in W;
A3: for a,b,c being LATTICE st L[a] & L[b] & L[c]
for f being Function of a,b, g being Function
of b,c st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] by WAYBEL20:27;
A4: for a being LATTICE st L[a] holds P[a,a,id a];
thus
ex C being lattice-wise strict category st (for x being LATTICE holds
x is Object of C iff x is strict & L[x] & the carrier of x in W) &
for a,b being Object of C, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff P[latt a, latt b, f] from YELLOW21:sch 3
(A2,A3,A4);
end;
uniqueness
proof
let C1, C2 be lattice-wise strict category such that
A5: for x being LATTICE holds
x is Object of C1 iff x is strict & L[x] & the carrier of x in W and
A6: for a,b being Object of C1, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff f is sups-preserving and
A7: for x being LATTICE holds
x is Object of C2 iff x is strict & L[x] & the carrier of x in W and
A8: for a,b being Object of C2, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff f is sups-preserving;
defpred Q[set, set, set] means
ex L1,L2 being LATTICE, f being Function of L1,L2
st $1 = L1 & $2 = L2 & $3 = f & f is sups-preserving;
A9: now
let a,b be Object of C1;
let f be monotone Function of latt a, latt b;
f in <^a,b^> iff f is sups-preserving by A6;
hence f in <^a,b^> iff Q[a,b,f];
end;
A10: now
let a,b be Object of C2;
let f be monotone Function of latt a, latt b;
f in <^a,b^> iff f is sups-preserving by A8;
hence f in <^a,b^> iff Q[a,b,f];
end;
for C1, C2 being lattice-wise category st (for x being LATTICE holds
x is Object of C1 iff x is strict & L[x] & the carrier of x in W) &
(for a,b being Object of C1, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff Q[a, b, f]) & (for x being LATTICE holds
x is Object of C2 iff x is strict & L[x] & the carrier of x in W) &
(for a,b being Object of C2, f being monotone Function of latt a, latt b
holds f in <^a,b^> iff Q[a, b, f])
holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW21:sch 5;
hence thesis by A5,A7,A9,A10;
end;
end;
Lm4: for W being with_non-empty_element set
for a,b being LATTICE, f being Function of a,b
holds f in (the Arrows of W-SUP_category).(a,b) iff
a in the carrier of W-SUP_category & b in the carrier of W-SUP_category &
a is complete & b is complete & f is sups-preserving
proof
let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
let a,b be LATTICE, f be Function of a,b;
set A = W-SUP_category;
hereby
assume f in (the Arrows of A).(a,b);
then consider o1, o2 being Object of A such that
A2: o1 = a and
A3: o2 = b and
A4: f in <^o1,o2^> and f is Morphism of o1, o2 by Th12;
reconsider g = f as Morphism of o1,o2 by A4;
thus a in the carrier of A & b in the carrier of A by A2,A3;
thus a is complete & b is complete by A1,A2,A3,Def5;
@g = f by A4,YELLOW21:def 7;
hence f is sups-preserving by A1,A2,A3,A4,Def5;
end;
assume that
A5: a in the carrier of W-SUP_category and
A6: b in the carrier of W-SUP_category;
reconsider x = a, y = b as Object of A by A5,A6;
A7: latt x = a;
A8: latt y = b;
assume that
a is complete and b is complete and
A9: f is sups-preserving;
f in <^x,y^> by A1,A7,A8,A9,Def5;
hence thesis by ALTCAT_1:def 1;
end;
registration
let W be with_non-empty_element set;
cluster W-INF_category -> with_complete_lattices;
coherence
proof
thus W-INF_category is lattice-wise;
let a be Object of W-INF_category;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
a = latt a;
hence thesis by A1,Def4;
end;
cluster W-SUP_category -> with_complete_lattices;
coherence
proof
thus W-SUP_category is lattice-wise;
let a be Object of W-SUP_category;
A2: ex x being non empty set st x in W by SETFAM_1:def 10;
a = latt a;
hence thesis by A2,Def5;
end;
end;
theorem Th13:
for W being with_non-empty_element set for L being LATTICE holds
L is Object of W-INF_category iff
L is strict complete & the carrier of L in W
proof
let W be with_non-empty_element set;
ex a being non empty set st a in W by SETFAM_1:def 10;
hence thesis by Def4;
end;
theorem Th14:
for W being with_non-empty_element set
for a, b being Object of W-INF_category for f being set
holds f in <^a,b^> iff f is infs-preserving Function of latt a, latt b
proof
let W be with_non-empty_element set;
let a,b be Object of W-INF_category, f be set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
hereby
assume
A2: f in <^a,b^>;
then reconsider g = f as Morphism of a,b;
f = @g by A2,YELLOW21:def 7;
hence f is infs-preserving Function of latt a, latt b by A1,A2,Def4;
end;
thus thesis by A1,Def4;
end;
theorem Th15:
for W being with_non-empty_element set for L being LATTICE holds
L is Object of W-SUP_category iff
L is strict complete & the carrier of L in W
proof
let W be with_non-empty_element set;
ex a being non empty set st a in W by SETFAM_1:def 10;
hence thesis by Def5;
end;
theorem Th16:
for W being with_non-empty_element set
for a, b being Object of W-SUP_category for f being set
holds f in <^a,b^> iff f is sups-preserving Function of latt a, latt b
proof
let W be with_non-empty_element set;
let a,b be Object of W-SUP_category, f be set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
hereby
assume
A2: f in <^a,b^>;
then reconsider g = f as Morphism of a,b;
f = @g by A2,YELLOW21:def 7;
hence f is sups-preserving Function of latt a, latt b by A1,A2,Def5;
end;
thus thesis by A1,Def5;
end;
theorem Th17:
for W being with_non-empty_element set holds
the carrier of W-INF_category = the carrier of W-SUP_category
proof
let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
thus the carrier of W-INF_category c= the carrier of W-SUP_category
proof
let x be object;
assume
A2: x in the carrier of W-INF_category;
then reconsider x as LATTICE by YELLOW21:def 4;
A3: x is strict complete by A1,A2,Def4;
the carrier of x in W by A1,A2,Def4;
then x is Object of W-SUP_category by A3,Def5;
hence thesis;
end;
let x be object;
assume
A4: x in the carrier of W-SUP_category;
then reconsider x as LATTICE by YELLOW21:def 4;
A5: x is strict complete by A1,A4,Def5;
the carrier of x in W by A1,A4,Def5;
then x is Object of W-INF_category by A5,Def4;
hence thesis;
end;
definition :: 1.2 LEMMA, p. 179
let W be with_non-empty_element set;
set A = W-INF_category, B = W-SUP_category;
deffunc O(LATTICE) = $1;
deffunc F(LATTICE,LATTICE, Function of $1,$2) = LowerAdj $3;
defpred P[LATTICE,LATTICE, Function of $1,$2] means
$1 is complete & $2 is complete & $3 is infs-preserving;
defpred Q[LATTICE,LATTICE, Function of $1,$2] means
$1 is complete & $2 is complete & $3 is sups-preserving;
A1: for a,b being LATTICE, f being Function of a,b
holds f in (the Arrows of A).(a,b) iff
a in the carrier of A & b in the carrier of A & P[a,b,f] by Lm3;
A2: for a,b being LATTICE, f being Function of a,b
holds f in (the Arrows of B).(a,b) iff
a in the carrier of B & b in the carrier of B & Q[a,b,f] by Lm4;
A3: for a being LATTICE st a in the carrier of A
holds O(a) in the carrier of B by Th17;
A4: for a,b being LATTICE, f being Function of a,b st P[a,b,f]
holds F(a,b,f) is Function of O(b),O(a) & Q[O(b), O(a), F(a,b,f)];
A5: now
let a be LATTICE;
assume a in the carrier of A;
then a is complete by YELLOW21:def 5;
hence F(a,a,id a) = id O(a) by Th7;
end;
A6: for a,b,c being LATTICE, f being Function of a,b, g being Function of b,c
st P[a,b,f] & P[b,c,g] holds F(a,c,g*f) = F(a,b,f)*F(b,c,g) by Th8;
func W LowerAdj ->
contravariant strict Functor of W-INF_category, W-SUP_category means
:
Def6: (for a being Object of W-INF_category holds it.a = latt a) &
for a,b being Object of W-INF_category st <^a,b^> <> {}
for f being Morphism of a,b holds it.f = LowerAdj @f;
existence
proof
thus ex F being contravariant strict
Functor of W-INF_category, W-SUP_category st
(for a being Object of W-INF_category holds F.a = O(latt a)) &
for a,b being Object of W-INF_category st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(latt a, latt b, @f)
from YELLOW21:sch 7(A1,A2,A3,A4,A5,A6);
end;
uniqueness
proof
let F,G be contravariant strict Functor of A, B such that
A7: for a being Object of W-INF_category holds F.a = latt a and
A8: for a,b being Object of W-INF_category st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = LowerAdj @f and
A9: for a being Object of W-INF_category holds G.a = latt a and
A10: for a,b being Object of W-INF_category st <^a,b^> <> {}
for f being Morphism of a,b holds G.f = LowerAdj @f;
A11: now
let a be Object of A;
thus F.a = latt a by A7
.= G.a by A9;
end;
now
let a,b be Object of A such that
A12: <^a,b^> <> {};
let f be Morphism of a,b;
thus F.f = LowerAdj @f by A8,A12
.= G.f by A10,A12;
end;
hence thesis by A11,YELLOW18:2;
end;
deffunc G(LATTICE,LATTICE, Function of $1,$2) = UpperAdj $3;
A13: for a being LATTICE st a in the carrier of B
holds O(a) in the carrier of A by Th17;
A14: for a,b being LATTICE, f being Function of a,b st Q[a,b,f]
holds G(a,b,f) is Function of O(b), O(a) & P[O(b), O(a), G(a,b,f)];
A15: now
let a be LATTICE;
assume a in the carrier of B;
then a is complete by YELLOW21:def 5;
hence G(a,a,id a) = id O(a) by Th7;
end;
A16: for a,b,c being LATTICE, f being Function of a,b, g being Function of b,c
st Q[a,b,f] & Q[b,c,g] holds G(a,c,g*f) = G(a,b,f)*G(b,c,g) by Th9;
func W UpperAdj ->
contravariant strict Functor of W-SUP_category, W-INF_category means
:
Def7: (for a being Object of W-SUP_category holds it.a = latt a) &
for a,b being Object of W-SUP_category st <^a,b^> <> {}
for f being Morphism of a,b holds it.f = UpperAdj @f;
existence
proof
thus ex F being contravariant strict Functor of B,A st
(for a being Object of B holds F.a = O(latt a)) &
for a,b being Object of B st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = G(latt a, latt b, @f)
from YELLOW21:sch 7(A2,A1,A13,A14,A15,A16);
end;
uniqueness
proof
let F,G be contravariant strict Functor of B,A such that
A17: for a being Object of B holds F.a = latt a and
A18: for a,b being Object of B st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = UpperAdj @f and
A19: for a being Object of B holds G.a = latt a and
A20: for a,b being Object of B st <^a,b^> <> {}
for f being Morphism of a,b holds G.f = UpperAdj @f;
A21: now
let a be Object of B;
thus F.a = latt a by A17
.= G.a by A19;
end;
now
let a,b be Object of B such that
A22: <^a,b^> <> {};
let f be Morphism of a,b;
thus F.f = UpperAdj @f by A18,A22
.= G.f by A20,A22;
end;
hence thesis by A21,YELLOW18:2;
end;
end;
registration
let W be with_non-empty_element set;
cluster W LowerAdj -> bijective;
coherence
proof
set A = W-INF_category, B = W-SUP_category;
set F = W LowerAdj;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
deffunc O(Object of A) = latt $1;
deffunc F(Object of A,Object of A,Morphism of $1,$2) = LowerAdj @$3;
A2: for a being Object of A holds F.a = O(a) by Def6;
A3: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f) by Def6;
A4: for a,b be Object of A st O(a) = O(b) holds a = b;
A5: now
let a,b be Object of A such that
A6: <^a,b^> <> {};
let f,g be Morphism of a,b;
A7: @f = f by A6,YELLOW21:def 7;
A8: @g = g by A6,YELLOW21:def 7;
A9: latt a is complete;
A10: latt b is complete;
A11: @f is infs-preserving by A1,A6,A7,Def4;
A12: @g is infs-preserving by A1,A6,A8,Def4;
assume F(a,b,f) = F(a,b,g);
hence f = UpperAdj LowerAdj @g by A7,A9,A10,A11,Th10
.= g by A8,A9,A10,A12,Th10;
end;
A13: now
let a,b be Object of B such that
A14: <^a,b^> <> {};
let f be Morphism of a,b;
A15: latt a is strict complete by A1,Def5;
A16: the carrier of latt a in W by A1,Def5;
A17: latt b is strict complete by A1,Def5;
the carrier of latt b in W by A1,Def5;
then reconsider c = latt b, d = latt a as Object of A by A15,A16,A17,Def4
;
take c,d;
A18: latt c = c;
A19: latt d = d;
A20: f = @f by A14,YELLOW21:def 7;
then
A21: @f is sups-preserving by A1,A14,Def5;
then
A22: UpperAdj @f is monotone infs-preserving by A18,A19;
A23: UpperAdj @f in <^c,d^> by A1,A21,Def4;
reconsider g = UpperAdj @f as Morphism of c,d by A1,A21,Def4;
take g;
thus b = O(c) & a = O(d) & <^c,d^> <> {} by A1,A22,Def4;
g = @g by A23,YELLOW21:def 7;
hence f = F(c,d,g) by A20,A21,Th11;
end;
thus thesis from YELLOW18:sch 12(A2,A3,A4,A5,A13);
end;
cluster W UpperAdj -> bijective;
coherence
proof
set A = W-SUP_category, B = W-INF_category;
set F = W UpperAdj;
A24: ex x being non empty set st x in W by SETFAM_1:def 10;
deffunc O(Object of A) = latt $1;
deffunc F(Object of A, Object of A, Morphism of $1,$2) = UpperAdj @$3;
A25: for a being Object of A holds F.a = O(a) by Def7;
A26: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f) by Def7;
A27: for a,b be Object of A st O(a) = O(b) holds a = b;
A28: now
let a,b be Object of A such that
A29: <^a,b^> <> {};
let f,g be Morphism of a,b;
A30: @f = f by A29,YELLOW21:def 7;
A31: @g = g by A29,YELLOW21:def 7;
A32: latt a is complete;
A33: latt b is complete;
A34: @f is sups-preserving by A24,A29,A30,Def5;
A35: @g is sups-preserving by A24,A29,A31,Def5;
assume F(a,b,f) = F(a,b,g);
hence f = LowerAdj UpperAdj @g by A30,A32,A33,A34,Th11
.= g by A31,A32,A33,A35,Th11;
end;
A36: now
let a,b be Object of B such that
A37: <^a,b^> <> {};
let f be Morphism of a,b;
A38: latt a is strict complete by A24,Def4;
A39: the carrier of latt a in W by A24,Def4;
A40: latt b is strict complete by A24,Def4;
the carrier of latt b in W by A24,Def4;
then reconsider c = latt b, d = latt a as Object of A by A38,A39,A40,Def5
;
take c,d;
A41: latt c = c;
A42: latt d = d;
A43: f = @f by A37,YELLOW21:def 7;
then
A44: @f is infs-preserving by A24,A37,Def4;
then
A45: LowerAdj @f is monotone sups-preserving by A41,A42;
A46: LowerAdj @f in <^c,d^> by A24,A44,Def5;
reconsider g = LowerAdj @f as Morphism of c,d by A24,A44,Def5;
take g;
thus b = O(c) & a = O(d) & <^c,d^> <> {} by A24,A45,Def5;
g = @g by A46,YELLOW21:def 7;
hence f = F(c,d,g) by A43,A44,Th10;
end;
thus thesis from YELLOW18:sch 12(A25,A26,A27,A28,A36);
end;
end;
theorem Th18:
for W being with_non-empty_element set
holds W LowerAdj" = W UpperAdj & W UpperAdj" = W LowerAdj
proof
let W be with_non-empty_element set;
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
set B = W-SUP_category;
set F = W LowerAdj, G = W UpperAdj;
A2: now
let a be Object of B;
thus F.(G.a) = latt (G.a) by Def6
.= latt a by Def7
.= a;
end;
now
let a,b be Object of B;
assume
A3: <^a,b^> <> {};
then
A4: <^G.b, G.a^> <> {} by FUNCTOR0:def 19;
let f be Morphism of a,b;
A5: G.f = UpperAdj @f by A3,Def7;
A6: @f = f by A3,YELLOW21:def 7;
A7: @(G.f) = G.f by A4,YELLOW21:def 7;
A8: G.a = latt a by Def7;
A9: G.b = latt b by Def7;
A10: @f is sups-preserving by A1,A3,A6,Def5;
thus F.(G.f) = LowerAdj @(G.f) by A4,Def6
.= f by A5,A6,A7,A8,A9,A10,Th11;
end;
hence F" = G by A2,YELLOW20:7;
set B = W-INF_category;
set G = W LowerAdj, F = W UpperAdj;
A11: now
let a be Object of B;
thus F.(G.a) = latt (G.a) by Def7
.= latt a by Def6
.= a;
end;
now
let a,b be Object of B;
assume
A12: <^a,b^> <> {};
then
A13: <^G.b, G.a^> <> {} by FUNCTOR0:def 19;
let f be Morphism of a,b;
A14: G.f = LowerAdj @f by A12,Def6;
A15: @f = f by A12,YELLOW21:def 7;
A16: @(G.f) = G.f by A13,YELLOW21:def 7;
A17: G.a = latt a by Def6;
A18: G.b = latt b by Def6;
A19: @f is infs-preserving by A1,A12,A15,Def4;
thus F.(G.f) = UpperAdj @(G.f) by A13,Def7
.= f by A14,A15,A16,A17,A18,A19,Th10;
end;
hence thesis by A11,YELLOW20:7;
end;
theorem :: 1.3 THEOREM, p. 179
for W being with_non-empty_element set holds
(W LowerAdj)*(W UpperAdj) = id (W-SUP_category) &
(W UpperAdj)*(W LowerAdj) = id (W-INF_category)
proof
let W be with_non-empty_element set;
A1: W LowerAdj" = W UpperAdj by Th18;
W UpperAdj" = W LowerAdj by Th18;
hence thesis by A1,FUNCTOR1:18;
end;
theorem :: 1.3 THEOREM, p. 179
for W being with_non-empty_element set holds
W-INF_category, W-SUP_category are_anti-isomorphic
proof
let W be with_non-empty_element set;
take W LowerAdj;
thus thesis;
end;
begin
::Scott continuous maps and continuous lattices
theorem Th21: :: 1.4. THEOREM, (1) <=> (2), p. 180
for S,T being complete LATTICE, g being infs-preserving Function of S,T
holds g is directed-sups-preserving iff
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S for V being open Subset of X holds
uparrow ((LowerAdj g).:V) is open Subset of Y
proof
let S,T be complete LATTICE, g be infs-preserving Function of S,T;
hereby
assume
A1: g is directed-sups-preserving;
let X be Scott TopAugmentation of T;
let Y be Scott TopAugmentation of S;
let V be open Subset of X;
A2: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A3: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
then reconsider g9 = g as Function of Y,X by A2;
reconsider d = LowerAdj g as Function of X,Y by A2,A3;
uparrow (d.:V) is inaccessible
proof
let D be non empty directed Subset of Y;
assume sup D in uparrow (d.:V);
then consider y being Element of Y such that
A4: y <= sup D and
A5: y in d.:V by WAYBEL_0:def 16;
consider u being object such that
A6: u in the carrier of X and
A7: u in V and
A8: y = d.u by A5,FUNCT_2:64;
reconsider u as Element of X by A6;
reconsider g = g9 as Function of Y,X;
[g, d] is Galois Connection of S,T by Def1;
then
A9: [g, d] is Galois by A2,A3,Th1;
then
A10: d*g <= id Y by WAYBEL_1:18;
A11: id X <= g*d by A9,WAYBEL_1:18;
A12: (id X).u = u by FUNCT_1:18;
A13: (g*d).u = g.(d.u) by FUNCT_2:15;
A14: g is infs-preserving Function of Y,X by A2,A3,WAYBEL21:6;
A15: u <= g.y by A8,A11,A12,A13,YELLOW_2:9;
g.y <= g.sup D by A4,A14,ORDERS_3:def 5;
then
A16: u <= g.sup D by A15,ORDERS_2:3;
V is upper by WAYBEL11:def 4;
then
A17: g.sup D in V by A7,A16;
g is directed-sups-preserving by A1,A2,A3,WAYBEL21:6;
then
A18: g preserves_sup_of D;
ex_sup_of D, Y by YELLOW_0:17;
then
A19: g.sup D = sup (g.:D) by A18;
A20: g.:D is directed non empty by A14,YELLOW_2:15;
V is inaccessible by WAYBEL11:def 4;
then g.:D meets V by A17,A19,A20;
then consider z being object such that
A21: z in g.:D and
A22: z in V by XBOOLE_0:3;
consider x being object such that
A23: x in the carrier of Y and
A24: x in D and
A25: z = g qua Function.x by A21,FUNCT_2:64;
reconsider x as Element of Y by A23;
A26: (d*g).x = d.(g.x) by FUNCT_2:15;
(id Y).x = x by FUNCT_1:18;
then
A27: d.(g.x) <= x by A10,A26,YELLOW_2:9;
d.z in d.:V by A22,FUNCT_2:35;
then x in uparrow (d.:V) by A25,A27,WAYBEL_0:def 16;
hence thesis by A24,XBOOLE_0:3;
end;
then uparrow (d.:V) is open Subset of Y by WAYBEL11:def 4;
hence uparrow ((LowerAdj g).:V) is open Subset of Y by A3,WAYBEL_0:13;
end;
assume
A28: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S for V being open Subset of X holds
uparrow ((LowerAdj g).:V) is open Subset of Y;
set X = the Scott TopAugmentation of T,Y = the Scott TopAugmentation of S;
A29: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A30: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
then reconsider g9 = g as Function of Y,X by A29;
reconsider g9 as infs-preserving Function of Y,X by A29,A30,WAYBEL21:6;
set d = LowerAdj g;
reconsider d9 = d as Function of X,Y by A29,A30;
let D be Subset of S such that
A31: D is non empty directed;
assume ex_sup_of D, S;
thus ex_sup_of g.:D,T by YELLOW_0:17;
A32: sup (g.:D) <= g.sup D by WAYBEL17:15;
reconsider D9 = D as Subset of Y by A30;
reconsider D9 as non empty directed Subset of Y by A30,A31,WAYBEL_0:3;
reconsider s = sup D as Element of Y by A30;
set U9 = (downarrow sup (g9.:D9))`;
A33: U9 is open by WAYBEL11:12;
then uparrow (d.:U9) is open Subset of Y by A28;
then
A34: uparrow (d.:U9) is upper inaccessible Subset of Y by WAYBEL11:def 4;
sup (g9.:D9) = sup (g.:D) by A29,YELLOW_0:17,26;
then
A35: downarrow sup (g9.:D9) = downarrow sup (g.:D) by A29,WAYBEL_0:13;
A36: sup (g.:D) <= sup (g.:D);
A37: [g,d] is Galois by Def1;
then
A38: d*g <= id S by WAYBEL_1:18;
A39: id T <= g*d by A37,WAYBEL_1:18;
A40: (id S).sup D = sup D by FUNCT_1:18;
(d*g).sup D = d.(g.sup D) by FUNCT_2:15;
then d.(g.sup D) <= sup D by A38,A40,YELLOW_2:9;
then
A41: d9.(g9.s) <= s by A30,YELLOW_0:1;
A42: s = sup D9 by A30,YELLOW_0:17,26;
g.sup D <= sup (g.:D)
proof
assume not thesis;
then
A43: not g.sup D in downarrow sup (g.:D) by WAYBEL_0:17;
A44: sup (g.:D) in downarrow sup (g.:D) by A36,WAYBEL_0:17;
A45: g.sup D in U9 by A29,A35,A43,XBOOLE_0:def 5;
A46: not sup (g.:D) in U9 by A35,A44,XBOOLE_0:def 5;
A47: d9.(g9.s) in d9.:U9 by A45,FUNCT_2:35;
d9.:U9 c= uparrow (d9.:U9) by WAYBEL_0:16;
then
A48: s in uparrow (d9.:U9) by A41,A47,WAYBEL_0:def 20;
uparrow (d9.:U9) = uparrow (d.:U9) by A30,WAYBEL_0:13;
then D9 meets uparrow (d9.:U9) by A34,A42,A48,WAYBEL11:def 1;
then consider x being object such that
A49: x in D9 and
A50: x in uparrow (d9.:U9) by XBOOLE_0:3;
reconsider x as Element of Y by A49;
consider u9 being Element of Y such that
A51: u9 <= x and
A52: u9 in d9.:U9 by A50,WAYBEL_0:def 16;
consider u being object such that
A53: u in the carrier of X and
A54: u in U9 and
A55: u9 = d9.u by A52,FUNCT_2:64;
reconsider u as Element of X by A53;
reconsider a = u as Element of T by A29;
(id T).a = u by FUNCT_1:18;
then a <= (g*d).a by A39,YELLOW_2:9;
then a <= g.(d.a) by FUNCT_2:15;
then
A56: u <= g9.(d9.u) by A29,YELLOW_0:1;
g9.(d9.u) <= g9.x by A51,A55,ORDERS_3:def 5;
then
A57: u <= g9.x by A56,ORDERS_2:3;
g9.x in g9.:D9 by A49,FUNCT_2:35;
then g9.x <= sup (g9.:D9) by YELLOW_2:22;
then
A58: u <= sup (g9.:D9) by A57,ORDERS_2:3;
U9 is upper by A33,WAYBEL11:def 4;
then sup (g9.:D9) in U9 by A54,A58;
hence thesis by A29,A46,YELLOW_0:17,26;
end;
hence thesis by A32,ORDERS_2:2;
end;
definition
let S,T be non empty reflexive RelStr;
let f be Function of S,T;
attr f is waybelow-preserving means
for x,y being Element of S st x << y holds f.x << f.y;
end;
theorem Th22: :: 1.4. THEOREM, (1) => (3), p. 180
for S,T being complete LATTICE, g being infs-preserving Function of S,T holds
g is directed-sups-preserving implies LowerAdj g is waybelow-preserving
proof
let S,T be complete LATTICE, g be infs-preserving Function of S,T such that
A1: g is directed-sups-preserving;
set d = (LowerAdj g);
A2: [g,d] is Galois by Def1;
let t,t9 be Element of T such that
A3: t << t9;
let D be non empty directed Subset of S;
assume d.t9 <= sup D;
then
A4: t9 <= g.sup D by A2,WAYBEL_1:8;
A5: g preserves_sup_of D by A1;
ex_sup_of D,S by YELLOW_0:17;
then
A6: g.sup D = sup (g.:D) by A5;
g.:D is directed non empty by YELLOW_2:15;
then consider x being Element of T such that
A7: x in g.:D and
A8: t <= x by A3,A4,A6;
consider s being object such that
A9: s in the carrier of S and
A10: s in D and
A11: x = g.s by A7,FUNCT_2:64;
reconsider s as Element of S by A9;
take s;
thus thesis by A2,A8,A10,A11,WAYBEL_1:8;
end;
theorem Th23: :: 1.4. THEOREM, (3+) => (1), p. 180
for S being complete LATTICE for T being complete continuous LATTICE
for g being infs-preserving Function of S,T
st LowerAdj g is waybelow-preserving holds g is directed-sups-preserving
proof
let S be complete LATTICE;
let T be complete continuous LATTICE;
let g be infs-preserving Function of S,T such that
A1: for t,t9 being Element of T st t << t9
holds (LowerAdj g).t << (LowerAdj g).t9;
let D be Subset of S;
assume
A2: D is non empty directed;
assume ex_sup_of D,S;
thus ex_sup_of g.:D, T by YELLOW_0:17;
A3: sup (g.:D) <= g.sup D by WAYBEL17:15;
A4: g.sup D = sup waybelow (g.sup D) by WAYBEL_3:def 5;
waybelow (g.sup D) is_<=_than sup (g.:D)
proof
let t be Element of T;
assume t in waybelow (g.sup D);
then t << g.sup D by WAYBEL_3:7;
then
A5: (LowerAdj g).t << (LowerAdj g).(g.sup D) by A1;
A6: [g, LowerAdj g] is Galois by Def1;
then
A7: (LowerAdj g)*g <= id S by WAYBEL_1:18;
(id S).sup D = sup D by FUNCT_1:18;
then ((LowerAdj g)*g).sup D <= sup D by A7,YELLOW_2:9;
then (LowerAdj g).(g.sup D) <= sup D by FUNCT_2:15;
then consider x being Element of S such that
A8: x in D and
A9: (LowerAdj g).t <= x by A2,A5;
A10: g.x in g.:D by A8,FUNCT_2:35;
A11: t <= g.x by A6,A9,WAYBEL_1:8;
g.x <= sup (g.:D) by A10,YELLOW_2:22;
hence thesis by A11,ORDERS_2:3;
end;
then g.sup D <= sup (g.:D) by A4,YELLOW_0:32;
hence thesis by A3,ORDERS_2:2;
end;
definition
let S,T be TopSpace;
let f be Function of S,T;
attr f is relatively_open means
for V being open Subset of S holds f.:V is open Subset of T|rng f;
end;
theorem
for X,Y being non empty TopSpace for d being Function of X, Y holds
d is relatively_open iff corestr d is open
proof
let X,Y be non empty TopSpace;
let d be Function of X, Y;
A1: corestr d = d by WAYBEL18:def 7;
A2: Image d = Y|rng d by WAYBEL18:def 6;
thus d is relatively_open implies corestr d is open
by A1,A2;
assume
A3: for V being Subset of X st V is open holds (corestr d).:V is open;
let V be open Subset of X;
thus thesis by A1,A2,A3;
end;
theorem Th25: :: requirement of 1.5. REMARK, p. 181
for S,T being complete LATTICE, g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S for V being open Subset of X holds
(LowerAdj g).:V = (rng LowerAdj g) /\ uparrow ((LowerAdj g).:V)
proof
let S,T be complete LATTICE, g be infs-preserving Function of S,T;
let X be Scott TopAugmentation of T;
let Y be Scott TopAugmentation of S;
A1: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A2: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
then reconsider d = LowerAdj g as Function of X, Y by A1;
let V be open Subset of X;
reconsider A = uparrow ((LowerAdj g).:V) as Subset of Y by A2;
d.:V = A /\ rng d
proof
A3: d.:V c= A by WAYBEL_0:16;
d.:V c= rng d by RELAT_1:111;
hence d.:V c= A /\ rng d by A3,XBOOLE_1:19;
let t be object;
assume
A4: t in A /\ rng d;
then
A5: t in A by XBOOLE_0:def 4;
A6: t in rng d by A4,XBOOLE_0:def 4;
reconsider t as Element of S by A5;
consider x being Element of S such that
A7: x <= t and
A8: x in (LowerAdj g).:V by A5,WAYBEL_0:def 16;
consider u being object such that
A9: u in the carrier of T and
A10: u in V and
A11: x = (LowerAdj g).u by A8,FUNCT_2:64;
dom d = the carrier of T by FUNCT_2:def 1;
then consider v being object such that
A12: v in the carrier of T and
A13: t = d.v by A6,FUNCT_1:def 3;
reconsider u,v as Element of T by A9,A12;
A14: (LowerAdj g).(u "\/" v) = x "\/" t by A11,A13,WAYBEL_6:2
.= t by A7,YELLOW_0:24;
reconsider V9 = V as Subset of T by A1;
V is upper by WAYBEL11:def 4;
then
A15: V9 is upper by A1,WAYBEL_0:25;
u <= u "\/" v by YELLOW_0:22;
then u "\/" v in V9 by A10,A15;
hence thesis by A14,FUNCT_2:35;
end;
hence thesis;
end;
theorem Th26: :: 1.5. REMARK, (2) => (2'), p. 181
for S,T being complete LATTICE, g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S st for V being open Subset of X holds
uparrow ((LowerAdj g).:V) is open Subset of Y holds
for d being Function of X, Y st d = LowerAdj g holds d is relatively_open
proof
let S,T be complete LATTICE, g be infs-preserving Function of S,T;
let X be Scott TopAugmentation of T;
let Y be Scott TopAugmentation of S such that
A1: for V being open Subset of X holds
uparrow ((LowerAdj g).:V) is open Subset of Y;
let d be Function of X, Y such that
A2: d = LowerAdj g;
let V be open Subset of X;
reconsider A = uparrow ((LowerAdj g).:V) as open Subset of Y by A1;
d.:V = A /\ rng d by A2,Th25;
then
A3: d.:V = [#](Y|rng d) /\ A by PRE_TOPC:def 5;
A4: A in the topology of Y by PRE_TOPC:def 2;
reconsider B = d.:V as Subset of Y|rng d by A3,XBOOLE_1:17;
B in the topology of Y|rng d by A3,A4,PRE_TOPC:def 4;
hence thesis by PRE_TOPC:def 2;
end;
registration
let X,Y be complete LATTICE;
let f be sups-preserving Function of X,Y;
cluster Image f -> complete;
coherence by YELLOW_2:34;
end;
theorem :: 1.5. REMARK, (2') => (2''), p. 181
for S,T being complete LATTICE, g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image LowerAdj g
for d being Function of X, Y, d9 being Function
of X, Z st d = LowerAdj g & d9 = d
holds d is relatively_open implies d9 is open
proof
let S,T be complete LATTICE, g be infs-preserving Function of S,T;
let X be Scott TopAugmentation of T;
let Y be Scott TopAugmentation of S;
let Z be Scott TopAugmentation of Image LowerAdj g;
let d be Function of X, Y, d9 be Function of X, Z such that
A1: d = LowerAdj g and
A2: d9 = d and
A3: for V being open Subset of X holds d.:V is open Subset of Y|rng d;
let V be Subset of X;
assume V is open;
then reconsider A = d.:V as open Subset of Y|rng d by A3;
A4: Image LowerAdj g = subrelstr rng LowerAdj g by YELLOW_2:def 2;
then
A5: the carrier of Image LowerAdj g = rng d by A1,YELLOW_0:def 15;
A6: [#](Y|rng d) = rng d by PRE_TOPC:def 5;
A7: the RelStr of Z = Image LowerAdj g by YELLOW_9:def 4;
A8: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
reconsider B = A as Subset of Z by A1,A4,A6,A7,YELLOW_0:def 15;
A in the topology of Y|rng d by PRE_TOPC:def 2;
then consider C being Subset of Y such that
A9: C in the topology of Y and
A10: A = C /\ [#](Y|rng d) by PRE_TOPC:def 4;
C is open by A9;
then
A11: C is upper inaccessible by WAYBEL11:def 4;
A12: B is upper
proof
let x,y be Element of Z;
reconsider x9 = x, y9 = y as Element of Image LowerAdj g by A7;
reconsider a = x9, b = y9 as Element of S by YELLOW_0:58;
reconsider a9 = a, b9 = b as Element of Y by A8;
assume that
A13: x in B and
A14: x <= y;
A15: x9 <= y9 by A7,A14,YELLOW_0:1;
A16: a in C by A10,A13,XBOOLE_0:def 4;
a <= b by A15,YELLOW_0:59;
then a9 <= b9 by A8,YELLOW_0:1;
then b9 in C by A11,A16;
hence thesis by A5,A6,A10,XBOOLE_0:def 4;
end;
B is inaccessible
proof
let D be directed non empty Subset of Z such that
A17: sup D in B;
reconsider D9 = D as non empty Subset of Image LowerAdj g by A7;
reconsider E = D9 as non empty Subset of S by A5,A8,XBOOLE_1:1;
reconsider E9 = E as non empty Subset of Y by A8;
D9 is directed by A7,WAYBEL_0:3;
then E is directed by YELLOW_2:7;
then
A18: E9 is directed by A8,WAYBEL_0:3;
A19: ex_sup_of D9,S by YELLOW_0:17;
Image LowerAdj g is sups-inheriting by YELLOW_2:32;
then "\/"(D9,S) in the carrier of Image LowerAdj g by A19;
then sup E = sup D9 by YELLOW_0:68
.= sup D by A7,YELLOW_0:17,26;
then sup E9 = sup D by A8,YELLOW_0:17,26;
then sup E9 in C by A10,A17,XBOOLE_0:def 4;
then C meets E by A11,A18;
hence thesis by A5,A6,A10,XBOOLE_1:77;
end;
hence thesis by A2,A12,WAYBEL11:def 4;
end;
theorem Th28: :: 1.6. COROLLARY, p. 181
for S,T being complete LATTICE, g being infs-preserving Function of S,T
st g is one-to-one for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
g is directed-sups-preserving iff d is open
proof
let S,T be complete LATTICE, g be infs-preserving Function of S,T such that
A1: g is one-to-one;
let X be Scott TopAugmentation of T;
let Y be Scott TopAugmentation of S;
[g, LowerAdj g] is Galois by Def1;
then LowerAdj g is onto by A1,WAYBEL_1:27;
then
A2: rng LowerAdj g = the carrier of S by FUNCT_2:def 3;
A3: the RelStr of Y = the RelStr of S by YELLOW_9:def 4;
A4: the RelStr of X = the RelStr of T by YELLOW_9:def 4;
A5: [#]Y = the carrier of Y;
let d be Function of X,Y such that
A6: d = LowerAdj g;
A7: Y|rng d = the TopStruct of Y by A2,A3,A5,A6,TSEP_1:93;
thus g is directed-sups-preserving implies d is open
proof
assume g is directed-sups-preserving;
then for V being open Subset of X holds
uparrow ((LowerAdj g).:V) is open Subset of Y by Th21;
then
A8: d is relatively_open by A6,Th26;
let V be Subset of X;
assume V is open;
then d.:V is open Subset of Y|rng d by A8;
hence d.:V in the topology of Y by A7,PRE_TOPC:def 2;
end;
assume
A9: for V being Subset of X st V is open holds d.:V is open;
now
let X9 be Scott TopAugmentation of T;
let Y9 be Scott TopAugmentation of S;
let V9 be open Subset of X9;
A10: the RelStr of X9 = the RelStr of T by YELLOW_9:def 4;
A11: the RelStr of Y9 = the RelStr of S by YELLOW_9:def 4;
reconsider V = V9 as Subset of X by A4,A10;
reconsider V as open Subset of X by A4,A10,YELLOW_9:50;
reconsider d9 = d as Function of X9,Y9 by A3,A4,A10,A11;
d.:V is open by A9;
then
A12: d9.:V9 is open Subset of Y9 by A3,A11,YELLOW_9:50;
then d9.:V9 is upper by WAYBEL11:def 4;
then
A13: uparrow (d9.:V9) c= d9.:V9 by WAYBEL_0:24;
d9.:V9 c= uparrow (d9.:V9) by WAYBEL_0:16;
then uparrow (d9.:V9) = d9.:V9 by A13;
hence uparrow ((LowerAdj g).:V9) is open Subset of Y9
by A6,A11,A12,WAYBEL_0:13;
end;
hence thesis by Th21;
end;
registration
let X be complete LATTICE;
let f be projection Function of X,X;
cluster Image f -> complete;
coherence by WAYBEL_1:54;
end;
theorem Th29:
for L being complete LATTICE, k being kernel Function of L,L holds
corestr k is infs-preserving & inclusion k is sups-preserving &
LowerAdj corestr k = inclusion k & UpperAdj inclusion k = corestr k
proof
let L be complete LATTICE, k be kernel Function of L,L;
A1: [corestr k, inclusion k] is Galois by WAYBEL_1:39;
then
A2: inclusion k is lower_adjoint;
A3: corestr k is upper_adjoint by A1;
hence corestr k is infs-preserving & inclusion k is sups-preserving by A2;
thus thesis by A1,A2,A3,Def1,Def2;
end;
theorem Th30:
for L being complete LATTICE, k being kernel Function of L,L holds
k is directed-sups-preserving iff corestr k is directed-sups-preserving
proof
let L be complete LATTICE, k be kernel Function of L,L;
set ck = corestr k;
[ck, inclusion k] is Galois by WAYBEL_1:39;
then
A1: inclusion k is lower_adjoint;
A2: k = (inclusion k)*ck by WAYBEL_1:32;
hereby
assume
A3: k is directed-sups-preserving;
thus corestr k is directed-sups-preserving
proof
let D be Subset of L;
assume D is non empty directed;
then
A4: k preserves_sup_of D by A3;
assume ex_sup_of D, L;
then
A5: sup (k.:D) = k.sup D by A4
.= (inclusion k).(ck.sup D) by A2,FUNCT_2:15
.= ck.sup D by FUNCT_1:18;
thus ex_sup_of ck.:D, Image k by YELLOW_0:17;
A6: ex_sup_of (inclusion k).:(ck.:D), L by YELLOW_0:17;
A7: Image k is sups-inheriting by WAYBEL_1:53;
ex_sup_of ck.:D, L by YELLOW_0:17;
then
A8: "\/"((ck.:D), L) in the carrier of Image k by A7;
ck.:D = (inclusion k).:(ck.:D) by WAYBEL15:12;
hence sup (ck.:D) = sup ((inclusion k).:(ck.:D)) by A6,A8,YELLOW_0:64
.= ck.sup D by A2,A5,RELAT_1:126;
end;
end;
thus thesis by A1,A2,WAYBEL15:11;
end;
theorem :: 1.7. COROLLARY, (1) <=> (2), p. 181
for L being complete LATTICE, k being kernel Function of L,L holds
k is directed-sups-preserving iff
for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X
holds uparrow V is open Subset of Y
proof
let L be complete LATTICE, k be kernel Function of L,L;
A1: [corestr k, inclusion k] is Galois by WAYBEL_1:39;
then
A2: corestr k is upper_adjoint;
then
A3: inclusion k = LowerAdj corestr k by A1,Def1;
hereby
assume
A4: k is directed-sups-preserving;
let X be Scott TopAugmentation of Image k;
let Y be Scott TopAugmentation of L;
A5: the RelStr of X = Image k by YELLOW_9:def 4;
let V be Subset of L;
assume V is open Subset of X;
then reconsider A = V as open Subset of X;
reconsider B = A as Subset of Image k by A5;
A6: corestr k is directed-sups-preserving by A4,Th30;
(inclusion k).:B = V by WAYBEL15:12;
hence uparrow V is open Subset of Y by A2,A3,A6,Th21;
end;
assume
A7: for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X
holds uparrow V is open Subset of Y;
now
set g = corestr k;
let X be Scott TopAugmentation of Image k;
let Y be Scott TopAugmentation of L;
let V be open Subset of X;
the RelStr of X = Image k by YELLOW_9:def 4;
then reconsider B = V as Subset of Image k;
the carrier of Image k c= the carrier of L by YELLOW_0:def 13;
then reconsider A = B as Subset of L by XBOOLE_1:1;
uparrow A is open Subset of Y by A7;
hence uparrow ((LowerAdj g).:V) is open Subset of Y by A3,WAYBEL15:12;
end;
then corestr k is directed-sups-preserving by A2,Th21;
hence thesis by Th30;
end;
theorem Th32:
for L being complete LATTICE
for S being sups-inheriting non empty full SubRelStr of L
for x,y being Element of L, a,b being Element of S st a = x & b = y
holds x << y implies a << b
proof
let L be complete LATTICE;
let S be sups-inheriting non empty full SubRelStr of L;
let x,y be Element of L, a,b be Element of S such that
A1: a = x and
A2: b = y and
A3: for D being non empty directed Subset of L st y <= sup D
ex d being Element of L st d in D & x <= d;
let D be non empty directed Subset of S such that
A4: b <= sup D;
reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A5: ex_sup_of D, L by YELLOW_0:17;
then "\/"(D,L) in the carrier of S by YELLOW_0:def 19;
then sup E = sup D by A5,YELLOW_0:64;
then y <= sup E by A2,A4,YELLOW_0:59;
then consider e being Element of L such that
A6: e in E and
A7: x <= e by A3;
reconsider d = e as Element of S by A6;
take d;
thus thesis by A1,A6,A7,YELLOW_0:60;
end;
theorem :: 1.7. COROLLARY, (1) => (3), p. 181
for L being complete LATTICE, k being kernel Function of L,L
st k is directed-sups-preserving
for x,y being Element of L, a,b being Element of Image k st a = x & b = y
holds x << y iff a << b
proof
let L be complete LATTICE, k be kernel Function of L,L;
set g = corestr k;
assume k is directed-sups-preserving;
then corestr k is directed-sups-preserving infs-preserving by Th29,Th30;
then
A1: LowerAdj g is waybelow-preserving by Th22;
let x,y be Element of L, a,b be Element of Image k;
A2: Image k is sups-inheriting by WAYBEL_1:53;
A3: inclusion k = LowerAdj g by Th29;
then
A4: (LowerAdj g).a = a by FUNCT_1:18;
(LowerAdj g).b = b by A3,FUNCT_1:18;
hence thesis by A1,A2,A4,Th32;
end;
theorem :: 1.7. COROLLARY, (3) => (1), p. 181
for L being complete LATTICE, k being kernel Function of L,L
st Image k is continuous &
for x,y being Element of L, a,b being Element of Image k st a = x & b = y
holds x << y iff a << b holds k is directed-sups-preserving
proof
let L be complete LATTICE, k be kernel Function of L,L such that
A1: Image k is continuous and
A2: for x,y being Element of L, a,b being Element of Image k st a = x & b = y
holds x << y iff a << b;
set g = corestr k;
A3: corestr k is infs-preserving by Th29;
LowerAdj g is waybelow-preserving
proof
let t,t9 be Element of Image k;
A4: LowerAdj g = inclusion k by Th29;
then
A5: (LowerAdj g).t = t by FUNCT_1:18;
(LowerAdj g).t9 = t9 by A4,FUNCT_1:18;
hence thesis by A2,A5;
end;
then corestr k is directed-sups-preserving by A1,A3,Th23;
hence thesis by Th30;
end;
theorem Th35:
for L being complete LATTICE, c being closure Function of L,L holds
corestr c is sups-preserving & inclusion c is infs-preserving &
UpperAdj corestr c = inclusion c & LowerAdj inclusion c = corestr c
proof
let L be complete LATTICE, c be closure Function of L,L;
A1: [inclusion c, corestr c] is Galois by WAYBEL_1:36;
then
A2: inclusion c is upper_adjoint;
A3: corestr c is lower_adjoint by A1;
hence corestr c is sups-preserving & inclusion c is infs-preserving by A2;
thus thesis by A1,A2,A3,Def1,Def2;
end;
theorem Th36:
for L being complete LATTICE, c being closure Function of L,L holds
Image c is directed-sups-inheriting iff
inclusion c is directed-sups-preserving
proof
let L be complete LATTICE, c be closure Function of L,L;
set ic = inclusion c;
thus Image c is directed-sups-inheriting implies
inclusion c is directed-sups-preserving
proof
assume
A1: Image c is directed-sups-inheriting;
let D be Subset of Image c;
assume
A2: D is non empty directed;
then reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A3: ic.:D = E by WAYBEL15:12;
assume ex_sup_of D, Image c;
thus ex_sup_of ic.:D, L by YELLOW_0:17;
hence sup (ic.:D) = sup D by A1,A2,A3,WAYBEL_0:7
.= ic.sup D by FUNCT_1:18;
end;
assume
A4: inclusion c is directed-sups-preserving;
let X be directed Subset of Image c;
assume
A5: X <> {};
assume ex_sup_of X,L;
A6: ic preserves_sup_of X by A4,A5;
ex_sup_of X, Image c by YELLOW_0:17;
then sup (ic.:X) = ic.sup X by A6
.= sup X by FUNCT_1:18;
then sup (ic.:X) in the carrier of Image c;
hence thesis by WAYBEL15:12;
end;
theorem :: 1.8. COROLLARY, (1) <=> (2), p. 182
for L being complete LATTICE, c being closure Function of L,L holds
Image c is directed-sups-inheriting iff
for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds f is open
proof
let L be complete LATTICE, c be closure Function of L,L;
A1: LowerAdj inclusion c = corestr c by Th35;
A2: corestr c = c by WAYBEL_1:30;
A3: inclusion c is infs-preserving Function of Image c, L by Th35;
A4: Image c is directed-sups-inheriting iff inclusion c is
directed-sups-preserving by Th36;
hence Image c is directed-sups-inheriting implies
for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds f is open by A1,A2,A3,Th28;
assume
A5: for X being Scott TopAugmentation of Image c
for Y being Scott TopAugmentation of L
for f being Function of Y,X st f = c holds f is open;
set X = the Scott TopAugmentation of Image c,Y = the Scott TopAugmentation of L
;
A6: the RelStr of X = the RelStr of Image c by YELLOW_9:def 4;
the RelStr of Y = the RelStr of L by YELLOW_9:def 4;
then reconsider f = c as Function of Y,X by A2,A6;
f is open by A5;
hence thesis by A1,A2,A3,A4,Th28;
end;
theorem :: 1.8. COROLLARY, (1) => (3), p. 182
for L being complete LATTICE, c being closure Function of L,L holds
Image c is directed-sups-inheriting implies corestr c is waybelow-preserving
proof
let L be complete LATTICE, c be closure Function of L,L;
assume Image c is directed-sups-inheriting;
then inclusion c is directed-sups-preserving infs-preserving by Th35,Th36;
then LowerAdj inclusion c is waybelow-preserving by Th22;
hence thesis by Th35;
end;
theorem :: 1.8. COROLLARY, (3) => (1), p. 182
:: SHOULD BE:
:: for L being complete LATTICE, c being closure map of L,L
:: st
:: Image c is continuous & corestr c is waybelow-preserving
:: holds Image c is directed-sups-inheriting
:: ------------------------ a bug ???
for L being continuous complete LATTICE, c being closure Function of L,L st
corestr c is waybelow-preserving holds Image c is directed-sups-inheriting
proof
let L be continuous complete LATTICE, c be closure Function of L,L;
assume
A1: corestr c is waybelow-preserving;
A2: LowerAdj inclusion c = corestr c by Th35;
inclusion c is infs-preserving by Th35;
then inclusion c is directed-sups-preserving by A1,A2,Th23;
hence thesis by Th36;
end;
begin
::Duality of subcategories of {\it INF} and {\it SUP}
definition :: 1.9. DEFINITION, p. 182
let W be non empty set;
set A = W-INF_category;
defpred P[set] means not contradiction;
defpred Q[Object of A, Object of A, Morphism of $1,$2] means
@$3 is directed-sups-preserving;
A1: ex a being Object of A st P[a];
A2: for a,b,c being Object of A
st P[a] & P[b] & P[c] & <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
st Q[a,b,f] & Q[b,c,g] holds Q[a,c,g*f]
proof
let a,b,c be Object of A such that
A3: <^a,b^> <> {} and
A4: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
A5: <^a,c^> <> {} by A3,A4,ALTCAT_1:def 2;
A6: @f = f by A3,YELLOW21:def 7;
A7: @g = g by A4,YELLOW21:def 7;
@(g*f) = g*f by A5,YELLOW21:def 7;
then @(g*f) = (@g)*(@f) by A3,A4,A5,A6,A7,ALTCAT_1:def 12;
hence thesis by WAYBEL20:28;
end;
A8: for a being Object of A st P[a] holds Q[a,a,idm a]
proof
let a be Object of A;
idm a = id latt a by YELLOW21:2;
hence thesis by YELLOW21:def 7;
end;
func W-INF(SC)_category -> strict non empty subcategory of W-INF_category
means
:
Def10: (for a being Object of W-INF_category holds a is Object of it) &
for a,b being Object of W-INF_category
for a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds
f in <^a9,b9^> iff @f is directed-sups-preserving;
existence
proof
ex B being strict non empty subcategory of A st
(for a being Object of A holds a is Object of B iff P[a]) &
for a,b being Object of A, a9,b9 being Object of B
st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f]
from YELLOW18:sch 7(A1,A2,A8);
hence thesis;
end;
correctness
proof
let B1,B2 being strict non empty subcategory of A;
assume for a being Object of W-INF_category holds a is Object of B1;
then
A9: for a being Object of W-INF_category holds a is Object of B1 iff P [a];
assume
A10: for a,b being Object of W-INF_category
for a9,b9 being Object of B1 st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
assume for a being Object of W-INF_category holds a is Object of B2;
then
A11: for
a being Object of W-INF_category holds a is Object of B2 iff P [ a];
assume
A12: for a,b being Object of W-INF_category
for a9,b9 being Object of B2 st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
the AltCatStr of B1 = the AltCatStr of B2
from YELLOW20:sch 1(A9,A10,A11,A12);
hence thesis;
end;
end;
definition :: 1.9. DEFINITION, p. 182
let W be with_non-empty_element set;
A1: ex w being non empty set st w in W by SETFAM_1:def 10;
set A = W-SUP_category;
defpred P[set] means not contradiction;
defpred Q[Object of A, Object of A, Morphism of $1,$2] means
UpperAdj @$3 is directed-sups-preserving;
A2: ex a being Object of A st P[a];
A3: for a,b,c being Object of A
st P[a] & P[b] & P[c] & <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c st Q[a,b,f] & Q[b,c,g]
holds Q[a,c,g*f]
proof
let a,b,c be Object of A such that
A4: <^a,b^> <> {} and
A5: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
A6: <^a,c^> <> {} by A4,A5,ALTCAT_1:def 2;
A7: @f = f by A4,YELLOW21:def 7;
A8: @g = g by A5,YELLOW21:def 7;
A9: @(g*f) = g*f by A6,YELLOW21:def 7;
A10: @g is sups-preserving Function of latt b, latt c by A1,A5,A8,Def5;
A11: @f is sups-preserving Function of latt a, latt b by A1,A4,A7,Def5;
@(g*f) = (@g)*(@f) by A4,A5,A6,A7,A8,A9,ALTCAT_1:def 12;
then UpperAdj @(g*f) = (UpperAdj @f)*(UpperAdj @g) by A10,A11,Th9;
hence thesis by WAYBEL20:28;
end;
A12: for a being Object of A st P[a] holds Q[a,a,idm a]
proof
let a be Object of A;
A13: idm a = id latt a by YELLOW21:2;
UpperAdj id latt a = id latt a by Th7;
hence thesis by A13,YELLOW21:def 7;
end;
func W-SUP(SO)_category -> strict non empty subcategory of W-SUP_category
means
:
Def11: (for a being Object of W-SUP_category holds a is Object of it) &
for a,b being Object of W-SUP_category
for a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds
f in <^a9,b9^> iff UpperAdj @f is directed-sups-preserving;
existence
proof
ex B being strict non empty subcategory of A st
(for a being Object of A holds a is Object of B iff P[a]) &
for a,b being Object of A, a9,b9 being Object of B
st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f]
from YELLOW18:sch 7(A2,A3,A12);
hence thesis;
end;
correctness
proof
let B1,B2 being strict non empty subcategory of A;
assume for a being Object of W-SUP_category holds a is Object of B1;
then
A14: for
a being Object of W-SUP_category holds a is Object of B1 iff P [ a];
assume
A15: for a,b being Object of W-SUP_category
for a9,b9 being Object of B1 st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
assume for a being Object of W-SUP_category holds a is Object of B2;
then
A16: for
a being Object of W-SUP_category holds a is Object of B2 iff P [ a];
assume
A17: for a,b being Object of W-SUP_category
for a9,b9 being Object of B2 st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f];
the AltCatStr of B1 = the AltCatStr of B2
from YELLOW20:sch 1(A14,A15,A16,A17);
hence thesis;
end;
end;
theorem Th40:
for S being non empty RelStr, T being non empty reflexive antisymmetric RelStr
for t being Element of T for X being non empty Subset of S
holds S --> t preserves_sup_of X & S --> t preserves_inf_of X
proof
let S be non empty RelStr;
let T be non empty reflexive antisymmetric RelStr;
let t be Element of T;
let X be non empty Subset of S;
set f = S --> t;
A1: f.:X = {t}
proof
thus f.:X c= {t} by FUNCOP_1:81;
set x = the Element of X;
f.x = t by FUNCOP_1:7;
then t in f.:X by FUNCT_2:35;
hence thesis by ZFMISC_1:31;
end;
A2: f.sup X = t by FUNCOP_1:7;
A3: f.inf X = t by FUNCOP_1:7;
A4: inf {t} = t by YELLOW_0:39;
A5: sup {t} = t by YELLOW_0:39;
A6: ex_sup_of {t}, T by YELLOW_0:38;
ex_inf_of {t}, T by YELLOW_0:38;
hence thesis by A1,A2,A3,A4,A5,A6;
end;
theorem Th41:
for S being non empty RelStr
for T being lower-bounded non empty reflexive antisymmetric RelStr
holds S --> Bottom T is sups-preserving
proof
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
let X be Subset of S such that ex_sup_of X,S;
set f = (the carrier of S) --> Bottom T;
A1: f.sup X = Bottom T by FUNCOP_1:7;
(S --> Bottom T).:X c= {Bottom T} by FUNCOP_1:81;
then (S --> Bottom T).:X = {Bottom T} or (S --> Bottom T).:
X = {} by ZFMISC_1:33;
hence thesis by A1,YELLOW_0:38,39,42;
end;
theorem Th42:
for S being non empty RelStr
for T being upper-bounded non empty reflexive antisymmetric RelStr
holds S --> Top T is infs-preserving
proof
let S be non empty RelStr;
let T be upper-bounded non empty reflexive antisymmetric RelStr;
let X be Subset of S such that ex_inf_of X,S;
set t = Top T, f = (the carrier of S) --> t;
A1: f.inf X = t by FUNCOP_1:7;
(S --> t).:X c= {t} by FUNCOP_1:81;
then (S --> t).:X = {t} or (S --> t).:X = {} by ZFMISC_1:33;
hence thesis by A1,YELLOW_0:38,39,43;
end;
registration :: WAYBEL24
let S be non empty RelStr;
let T be upper-bounded non empty reflexive antisymmetric RelStr;
cluster S --> Top T -> directed-sups-preserving infs-preserving;
coherence
by Th40,Th42;
end;
registration
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster S --> Bottom T -> filtered-infs-preserving sups-preserving;
coherence
by Th40,Th41;
end;
registration
let S be non empty RelStr;
let T be upper-bounded non empty reflexive antisymmetric RelStr;
cluster directed-sups-preserving infs-preserving for Function of S, T;
existence
proof
take S --> Top T;
thus thesis;
end;
end;
registration
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster filtered-infs-preserving sups-preserving for Function of S, T;
existence
proof
take S --> Bottom T;
thus thesis;
end;
end;
theorem Th43:
for W being with_non-empty_element set for L being LATTICE holds
L is Object of W-INF(SC)_category iff
L is strict complete & the carrier of L in W
proof
let W be with_non-empty_element set;
let L be LATTICE;
the carrier of W-INF(SC)_category c= the carrier of W-INF_category
by ALTCAT_2:def 11;
then L in the carrier of W-INF(SC)_category implies
L is Object of W-INF_category;
then L is Object of W-INF(SC)_category iff L is Object of W-INF_category
by Def10;
hence thesis by Th13;
end;
theorem Th44:
for W being with_non-empty_element set
for a, b being Object of W-INF(SC)_category for f being set
holds f in <^a,b^> iff
f is directed-sups-preserving infs-preserving Function of latt a, latt b
proof
let W be with_non-empty_element set;
let a,b be Object of W-INF(SC)_category, f be set;
the carrier of W-INF(SC)_category c= the carrier of W-INF_category by
ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as Object of W-INF_category;
hereby
assume
A1: f in <^a,b^>;
A2: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
then reconsider g = f as Morphism of a1,b1 by A1;
f = @g by A1,A2,YELLOW21:def 7;
hence f is directed-sups-preserving infs-preserving Function
of latt a, latt b by A1,A2,Def10,Th14;
end;
assume f is directed-sups-preserving infs-preserving Function
of latt a, latt b;
then reconsider f as
directed-sups-preserving infs-preserving Function of latt a, latt b;
A3: f in <^a1,b1^> by Th14;
reconsider g = f as Morphism of a1,b1 by Th14;
f = @g by A3,YELLOW21:def 7;
hence thesis by A3,Def10;
end;
theorem
for W being with_non-empty_element set for L being LATTICE holds
L is Object of W-SUP(SO)_category iff
L is strict complete & the carrier of L in W
proof
let W be with_non-empty_element set;
let L be LATTICE;
the carrier of W-SUP(SO)_category c= the carrier of W-SUP_category
by ALTCAT_2:def 11;
then L in the carrier of W-SUP(SO)_category implies
L is Object of W-SUP_category;
then L is Object of W-SUP(SO)_category iff L is Object of W-SUP_category
by Def11;
hence thesis by Th15;
end;
theorem Th46:
for W being with_non-empty_element set
for a, b being Object of W-SUP(SO)_category for f being set
holds f in <^a,b^> iff
ex g being sups-preserving Function of latt a, latt b st g = f &
UpperAdj g is directed-sups-preserving
proof
let W be with_non-empty_element set;
let a,b be Object of W-SUP(SO)_category, f be set;
the carrier of W-SUP(SO)_category c= the carrier of W-SUP_category by
ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as Object of W-SUP_category;
hereby
assume
A1: f in <^a,b^>;
A2: <^a,b^> c= <^a1,b1^> by ALTCAT_2:31;
then reconsider g = f as Morphism of a1,b1 by A1;
A3: f = @g by A1,A2,YELLOW21:def 7;
A4: UpperAdj @g is directed-sups-preserving by A1,A2,Def11;
f is sups-preserving Function of latt a1, latt b1 by A1,A2,Th16;
hence ex g being sups-preserving Function of latt a, latt b st g = f &
UpperAdj g is directed-sups-preserving by A3,A4;
end;
given g being sups-preserving Function of latt a, latt b such that
A5: g = f and
A6: UpperAdj g is directed-sups-preserving;
A7: f in <^a1,b1^> by A5,Th16;
reconsider g = f as Morphism of a1,b1 by A5,Th16;
f = @g by A7,YELLOW21:def 7;
hence thesis by A5,A6,A7,Def11;
end;
theorem :: Remark after 1.9. DEFINITION, p. 182
for W being with_non-empty_element set
holds W-INF(SC)_category = Intersect(W-INF_category, W-UPS_category)
proof
let W be with_non-empty_element set;
consider w being non empty set such that
A1: w in W by SETFAM_1:def 10;
set r = the upper-bounded well-ordering Order of w;
A2: now
let a be Object of W-INF_category, b be Object of W-UPS_category;
idm a = id latt a by YELLOW21:2;
hence a = b implies idm a = idm b by YELLOW21:2;
end;
set B = Intersect(W-INF_category, W-UPS_category);
A3: W-INF_category, W-UPS_category have_the_same_composition by YELLOW20:12;
then
A4: the carrier of B = (the carrier of W-INF_category) /\
(the carrier of W-UPS_category) by YELLOW20:def 3;
A5: RelStr(#w,r#) is Object of W-INF_category by A1,Th13;
RelStr(#w,r#) is Object of W-UPS_category by A1,YELLOW21:14;
then Intersect(W-INF_category, W-UPS_category) is non empty by A4,A5,
XBOOLE_0:def 4;
then reconsider I = Intersect(W-INF_category, W-UPS_category) as
non empty subcategory of W-INF_category by A2,YELLOW20:12,25;
set A = W-INF(SC)_category;
deffunc B(set,set) = (the Arrows of A).($1,$2);
A6: for C1, C2 being para-functional semi-functional category
st the carrier of C1 = the carrier of A &
(for a,b being Object of C1 holds <^a,b^> = B(a,b)) &
the carrier of C2 = the carrier of A &
(for a,b being Object of C2 holds <^a,b^> = B(a,b))
holds the AltCatStr of C1 = the AltCatStr of C2 from YELLOW18:sch 19;
A7: the carrier of I = the carrier of A
proof
thus the carrier of I c= the carrier of A
proof
let x be object;
assume x in the carrier of I;
then reconsider x as Object of I;
reconsider L = x as LATTICE by YELLOW21:def 4;
A8: x in the carrier of W-UPS_category by A4,XBOOLE_0:def 4;
then
A9: L is strict complete by A1,YELLOW21:def 10;
the carrier of L in W by A1,A8,YELLOW21:def 10;
then L is Object of A by A9,Th43;
hence thesis;
end;
let x be object;
assume x in the carrier of A;
then reconsider x as Object of A;
reconsider L = x as LATTICE by YELLOW21:def 4;
A10: L is complete strict by Th43;
A11: the carrier of L in W by Th43;
then
A12: x is Object of W-INF_category by A10,Th13;
x is Object of W-UPS_category by A10,A11,YELLOW21:def 10;
hence thesis by A4,A12,XBOOLE_0:def 4;
end;
A13: for a,b being Object of A holds <^a,b^> = B(a,b) by ALTCAT_1:def 1;
now
let a,b be Object of I;
reconsider a9 = a, b9 = b as Object of A by A7;
reconsider a1 = a, b1 = b as Object of W-INF_category by A4,XBOOLE_0:def 4;
reconsider a2 = a, b2 = b as Object of W-UPS_category by A4,XBOOLE_0:def 4;
A14: dom the Arrows of W-INF_category = [:the carrier of W-INF_category, the
carrier of W-INF_category:] by PARTFUN1:def 2;
dom the Arrows of W-UPS_category = [:the carrier of W-UPS_category, the
carrier of W-UPS_category:] by PARTFUN1:def 2;
then
A15: (dom the Arrows of W-INF_category) /\ (dom the Arrows of W
-UPS_category) = [:(the carrier of W-INF_category)/\ the carrier of W
-UPS_category, (the carrier of W-INF_category)/\ the carrier of W-UPS_category
:] by A14,ZFMISC_1:100;
A16: <^a,b^> = (the Arrows of I).(a,b) by ALTCAT_1:def 1
.= Intersect(the Arrows of W-INF_category, the Arrows of W-UPS_category)
. [a,b] by A3,YELLOW20:def 3
.= ((the Arrows of W-INF_category).(a,b)) /\
((the Arrows of W-UPS_category). [a,b]) by A4,A15,YELLOW20:def 2
.= <^a1,b1^> /\ ((the Arrows of W-UPS_category).(a,b)) by ALTCAT_1:def 1
.= <^a1,b1^> /\ <^a2,b2^> by ALTCAT_1:def 1;
now
let f be object;
f in <^a,b^> iff f in <^a1,b1^> & f in <^a2,b2^> by A16,XBOOLE_0:def 4;
then f in <^a,b^> iff f is directed-sups-preserving Function of latt a2,
latt b2 & f is infs-preserving Function of latt a1, latt b1
by Th14,YELLOW21:15;
then f in <^a,b^> iff f in <^a9,b9^> by Th44;
hence f in <^a,b^> iff f in B(a,b) by ALTCAT_1:def 1;
end;
hence <^a,b^> = B(a,b) by TARSKI:2;
end;
hence thesis by A6,A7,A13;
end;
definition :: 1.9. DEFINITION, p. 182
let W be with_non-empty_element set;
defpred P[Object of W-INF(SC)_category] means latt $1 is continuous;
consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
set r = the upper-bounded well-ordering Order of a;
set b = RelStr(#a,r#);
func W-CL_category -> strict full non empty subcategory of W-INF(SC)_category
means
: Def12:
for a being Object of W-INF(SC)_category holds
a is Object of it iff latt a is continuous;
existence
proof
b is Object of W-INF_category by A1,Def4;
then reconsider b as Object of W-INF(SC)_category by Def10;
b = latt b;
then
A2: ex b being Object of W-INF(SC)_category st P[b];
thus
ex B being strict full non empty subcategory of W-INF(SC)_category st
for a being Object of W-INF(SC)_category holds a is Object of B iff P[a]
from YELLOW20:sch 2(A2);
end;
correctness
proof
let B1,B2 be strict full non empty subcategory of W-INF(SC)_category
such that
A3: for a being Object of W-INF(SC)_category holds a is Object of B1 iff P[a]
and
A4: for
a being Object of W-INF(SC)_category holds a is Object of B2 iff P[a];
the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3(A3,
A4);
hence thesis;
end;
end;
registration
let W be with_non-empty_element set;
cluster W-CL_category -> with_complete_lattices;
coherence;
end;
theorem Th48:
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W
holds L is Object of W-CL_category iff L is strict complete continuous
proof
let W be with_non-empty_element set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: the carrier of W-INF(SC)_category c= the carrier of W-INF_category
by ALTCAT_2:def 11;
A3: the carrier of W-CL_category c= the carrier of W-INF(SC)_category
by ALTCAT_2:def 11;
let L be LATTICE;
assume
A4: the carrier of L in W;
hereby
assume
A5: L is Object of W-CL_category;
then L in the carrier of W-CL_category;
then reconsider a = L as Object of W-INF(SC)_category by A3;
A6: a in the carrier of W-INF(SC)_category;
latt a is continuous by A5,Def12;
hence L is strict complete continuous by A1,A2,A6,Def4;
end;
assume
A7: L is strict complete continuous;
then L is Object of W-INF_category by A4,Def4;
then reconsider a = L as Object of W-INF(SC)_category by Def10;
latt a = L;
hence thesis by A7,Def12;
end;
theorem Th49:
for W being with_non-empty_element set for a,b being Object of W-CL_category
for f being set holds f in <^a,b^> iff
f is infs-preserving directed-sups-preserving Function of latt a, latt b
proof
let W be with_non-empty_element set;
let a,b be Object of W-CL_category, f be set;
the carrier of W-CL_category c= the carrier of W-INF(SC)_category by
ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as Object of W-INF(SC)_category;
<^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence thesis by Th44;
end;
definition :: 1.9. DEFINITION, p. 182
let W be with_non-empty_element set;
defpred P[Object of W-SUP(SO)_category] means latt $1 is continuous;
consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
set r = the upper-bounded well-ordering Order of a;
set b = RelStr(#a,r#);
func W-CL-opp_category ->
strict full non empty subcategory of W-SUP(SO)_category means
:
Def13: for a being Object of W-SUP(SO)_category holds
a is Object of it iff latt a is continuous;
existence
proof
b is Object of W-SUP_category by A1,Def5;
then reconsider b as Object of W-SUP(SO)_category by Def11;
b = latt b;
then
A2: ex b being Object of W-SUP(SO)_category st P[b];
thus
ex B being strict full non empty subcategory of W-SUP(SO)_category st
for a being Object of W-SUP(SO)_category holds a is Object of B iff P[a]
from YELLOW20:sch 2(A2);
end;
correctness
proof
let B1,B2 be strict full non empty subcategory of W-SUP(SO)_category
such that
A3: for a being Object of W-SUP(SO)_category holds a is Object of B1 iff P[a]
and
A4: for
a being Object of W-SUP(SO)_category holds a is Object of B2 iff P[a];
the AltCatStr of B1 = the AltCatStr of B2 from YELLOW20:sch 3(A3,
A4);
hence thesis;
end;
end;
theorem Th50:
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W
holds L is Object of W-CL-opp_category iff L is strict complete continuous
proof
let W be with_non-empty_element set;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: the carrier of W-SUP(SO)_category c= the carrier of W-SUP_category
by ALTCAT_2:def 11;
A3: the carrier of W-CL-opp_category c= the carrier of W-SUP(SO)_category
by ALTCAT_2:def 11;
let L be LATTICE;
assume
A4: the carrier of L in W;
hereby
assume
A5: L is Object of W-CL-opp_category;
then L in the carrier of W-CL-opp_category;
then reconsider a = L as Object of W-SUP(SO)_category by A3;
A6: a in the carrier of W-SUP(SO)_category;
latt a is continuous by A5,Def13;
hence L is strict complete continuous by A1,A2,A6,Def5;
end;
assume
A7: L is strict complete continuous;
then L is Object of W-SUP_category by A4,Def5;
then reconsider a = L as Object of W-SUP(SO)_category by Def11;
latt a = L;
hence thesis by A7,Def13;
end;
theorem Th51:
for W being with_non-empty_element set
for a, b being Object of W-CL-opp_category for f being set
holds f in <^a,b^> iff
ex g being sups-preserving Function of latt a, latt b st g = f &
UpperAdj g is directed-sups-preserving
proof
let W be with_non-empty_element set;
let a,b be Object of W-CL-opp_category, f be set;
the carrier of W-CL-opp_category c= the carrier of W-SUP(SO)_category
by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as Object of W-SUP(SO)_category;
<^a,b^> = <^a1,b1^> by ALTCAT_2:28;
hence thesis by Th46;
end;
:: 1.10. THEOREM, p. 182
theorem Th52:
for W being with_non-empty_element set holds
W-INF(SC)_category, W-SUP(SO)_category are_anti-isomorphic_under W LowerAdj
proof
let W be with_non-empty_element set;
set A1 = W-INF_category;
set B1 = W-INF(SC)_category, B2 = W-SUP(SO)_category;
set F = W LowerAdj;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: for a being Object of A1 holds
a is Object of B1 iff F.a is Object of B2 by Def10,Def11;
A3: now
let a,b be Object of A1 such that
A4: <^a,b^> <> {};
let a1,b1 be Object of B1 such that
A5: a1 = a and
A6: b1 = b;
let a2,b2 be Object of B2 such that
A7: a2 = F.a and
A8: b2 = F.b;
let f be Morphism of a,b;
A9: <^F.b,F.a^> <> {} by A4,FUNCTOR0:def 19;
A10: @f = f by A4,YELLOW21:def 7;
A11: @(F.f) = F.f by A9,YELLOW21:def 7;
A12: F.a = latt a by Def6;
A13: F.b = latt b by Def6;
A14: F.f = LowerAdj @f by A4,Def6;
reconsider g = f as infs-preserving Function
of latt a1, latt b1 by A1,A4,A5,A6,A10,Def4;
UpperAdj LowerAdj g = g by Th10;
then f in <^a1,b1^> iff UpperAdj LowerAdj g is directed-sups-preserving
by A4,A5,A6,A10,Def10;
hence f in <^a1,b1^> iff F.f in <^b2,a2^> by A5,A6,A7,A8,A9,A10,A11,A12,A13
,A14,Def11;
end;
thus thesis by A2,A3,YELLOW20:57;
end;
theorem
for W being with_non-empty_element set holds
W-SUP(SO)_category, W-INF(SC)_category are_anti-isomorphic_under W UpperAdj
proof
let W be with_non-empty_element set;
W-SUP(SO)_category, W-INF(SC)_category
are_anti-isomorphic_under (W LowerAdj)" by Th52,YELLOW20:51;
hence thesis by Th18;
end;
theorem Th54:
for W being with_non-empty_element set holds
W-CL_category, W-CL-opp_category are_anti-isomorphic_under W LowerAdj
proof
let W be with_non-empty_element set;
set A1 = W-INF_category, A2 = W-SUP_category;
reconsider B1 = W-CL_category as non empty subcategory of A1 by ALTCAT_4:36;
reconsider B2 = W-CL-opp_category as non empty subcategory of A2
by ALTCAT_4:36;
set F = W LowerAdj;
A1: ex a being non empty set st a in W by SETFAM_1:def 10;
A2: for a being Object of A1 holds a is Object of B1 iff F.a is Object of B2
proof
let a be Object of A1;
A3: F.a = latt a by Def6;
A4: the carrier of latt a in W by A1,Def4;
then a is Object of B1 iff latt a is strict complete continuous by Th48;
hence thesis by A3,A4,Th50;
end;
A5: now
let a,b be Object of A1 such that
A6: <^a,b^> <> {};
let a1,b1 be Object of B1 such that
A7: a1 = a and
A8: b1 = b;
let a2,b2 be Object of B2 such that
A9: a2 = F.a and
A10: b2 = F.b;
let f be Morphism of a,b;
A11: @f = f by A6,YELLOW21:def 7;
A12: F.a = latt a by Def6;
A13: F.b = latt b by Def6;
A14: F.f = LowerAdj @f by A6,Def6;
reconsider g = f as infs-preserving Function
of latt a1, latt b1 by A1,A6,A7,A8,A11,Def4;
A15: UpperAdj LowerAdj g = g by Th10;
then f in <^a1,b1^> iff UpperAdj LowerAdj g is directed-sups-preserving
by Th49;
hence f in <^a1,b1^> implies F.f in <^b2,a2^> by A7,A8,A9,A10,A11,A12,A13
,A14,Th51;
assume F.f in <^b2,a2^>;
then ex g being sups-preserving Function of latt b2, latt a2 st F.f = g &
UpperAdj g is directed-sups-preserving by Th51;
hence f in <^a1,b1^> by A7,A8,A9,A10,A11,A12,A13,A14,A15,Th49;
end;
B1,B2 are_anti-isomorphic_under F by A2,A5,YELLOW20:57;
hence thesis;
end;
theorem
for W being with_non-empty_element set holds
W-CL-opp_category, W-CL_category are_anti-isomorphic_under W UpperAdj
proof
let W be with_non-empty_element set;
set A1 = W-INF_category, A2 = W-SUP_category;
reconsider B1 = W-CL_category as non empty subcategory of A1 by ALTCAT_4:36;
reconsider B2 = W-CL-opp_category as non empty subcategory of A2
by ALTCAT_4:36;
B2, B1 are_anti-isomorphic_under (W LowerAdj)" by Th54,YELLOW20:51;
hence thesis by Th18;
end;
begin
::Compact preserving maps and sup-semilattices morphisms
definition
let S,T be non empty reflexive RelStr;
let f be Function of S,T;
attr f is compact-preserving means
for s being Element of S st s is compact holds f.s is compact;
end;
theorem Th56: :: 1.11. PROPOSITION, (1) => (2) p.183
for S,T being complete LATTICE, d being sups-preserving Function of T,S
st d is waybelow-preserving holds d is compact-preserving
proof
let S,T be complete LATTICE, d be sups-preserving Function of T,S such that
A1: for t,t9 being Element of T st t << t9 holds d.t << d.t9;
let t be Element of T;
assume t << t;
hence d.t << d.t by A1;
end;
theorem Th57: :: 1.11. PROPOSITION, (2) => (1) p.183
for S,T being complete LATTICE, d being sups-preserving Function of T,S
st T is algebraic & d is compact-preserving holds d is waybelow-preserving
proof
let S,T be complete LATTICE, d be sups-preserving Function of T,S such that
A1: T is algebraic and
A2: for t being Element of T st t is compact holds d.t is compact;
let t,t9 be Element of T;
assume t << t9;
then consider k being Element of T such that
A3: k in the carrier of CompactSublatt T and
A4: t <= k and
A5: k <= t9 by A1,WAYBEL_8:7;
k is compact by A3,WAYBEL_8:def 1;
then d.k is compact by A2;
then
A6: d.k << d.k;
A7: d.t <= d.k by A4,WAYBEL_1:def 2;
d.k <= d.t9 by A5,WAYBEL_1:def 2;
hence thesis by A6,A7,WAYBEL_3:2;
end;
theorem Th58:
for R,S,T being non empty RelStr, X being Subset of R
for f being Function of R,S for g being Function of S,T
st f preserves_sup_of X & g preserves_sup_of f.:X
holds g*f preserves_sup_of X
proof
let R,S,T be non empty RelStr, X be Subset of R;
let f be Function of R,S;
let g be Function of S,T such that
A1: ex_sup_of X, R implies ex_sup_of f.:X, S & sup (f.:X) = f.sup X and
A2: ex_sup_of f.:X, S implies
ex_sup_of g.:(f.:X), T & sup (g.:(f.:X)) = g.sup (f.:X);
A3: g.:(f.:X) = (g*f).:X by RELAT_1:126;
assume ex_sup_of X, R;
hence thesis by A1,A2,A3,FUNCT_2:15;
end;
definition
let S,T be non empty RelStr;
let f be Function of S,T;
attr f is finite-sups-preserving means
for X being finite Subset of S holds f preserves_sup_of X;
attr f is bottom-preserving means
f preserves_sup_of {}S;
end;
theorem
for R,S,T being non empty RelStr
for f being Function of R,S for g being Function of S,T
st f is finite-sups-preserving & g is finite-sups-preserving
holds g*f is finite-sups-preserving
proof
let R,S,T be non empty RelStr;
let f be Function of R,S;
let g be Function of S,T such that
A1: for X being finite Subset of R holds f preserves_sup_of X and
A2: for X being finite Subset of S holds g preserves_sup_of X;
let X be finite Subset of R;
g preserves_sup_of f.:X by A2;
hence thesis by A1,Th58;
end;
definition
let S,T be non empty antisymmetric lower-bounded RelStr;
let f be Function of S,T;
redefine attr f is bottom-preserving means
: Def17:
f.Bottom S = Bottom T;
compatibility
proof
thus f is bottom-preserving implies f.Bottom S = Bottom T
proof
assume f preserves_sup_of {}S;
then ex_sup_of {}S, S implies sup (f.:{}S) = f.sup {}S;
hence thesis by YELLOW_0:42;
end;
assume that
A1: f.Bottom S = Bottom T and ex_sup_of {}S, S;
thus ex_sup_of f.:{}S, T by YELLOW_0:42;
thus thesis by A1;
end;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
attr S is finite-sups-inheriting means
for X being finite Subset of S st ex_sup_of X,L
holds "\/"(X,L) in the carrier of S;
attr S is bottom-inheriting means
: Def19:
Bottom L in the carrier of S;
end;
registration
let S,T be non empty RelStr;
cluster sups-preserving -> bottom-preserving for Function of S,T;
coherence;
end;
registration
let L be lower-bounded antisymmetric non empty RelStr;
cluster finite-sups-inheriting ->
bottom-inheriting join-inheriting for SubRelStr of L;
coherence
proof
let S be SubRelStr of L;
assume
A1: S is finite-sups-inheriting;
then ex_sup_of {}, L implies "\/" ({}S, L) in the carrier of S;
hence Bottom L in the carrier of S by YELLOW_0:42;
let x,y be Element of L;
assume that
A2: x in the carrier of S and
A3: y in the carrier of S;
reconsider X = {x,y} as finite Subset of S by A2,A3,ZFMISC_1:32;
ex_sup_of X,L implies "\/"(X,L) in the carrier of S by A1;
hence thesis;
end;
end;
registration
let L be non empty RelStr;
cluster sups-inheriting -> finite-sups-inheriting for SubRelStr of L;
coherence;
end;
registration
let S,T be lower-bounded non empty Poset;
cluster sups-preserving for Function of S,T;
existence
proof set f = the sups-preserving Function of S,T;
take f;
thus thesis;
end;
end;
registration
let L be lower-bounded antisymmetric non empty RelStr;
cluster bottom-inheriting -> non empty lower-bounded for
full SubRelStr of L;
coherence
proof
let S be full SubRelStr of L;
assume
A1: Bottom L in the carrier of S;
hence
A2: S is non empty;
reconsider x = Bottom L as Element of S by A1;
take x;
let y be Element of S;
assume
A3: y in the carrier of S;
reconsider a = y as Element of L by A2,YELLOW_0:58;
Bottom L <= a by YELLOW_0:44;
hence thesis by A3,YELLOW_0:60;
end;
end;
registration
let L be lower-bounded antisymmetric non empty RelStr;
cluster non empty sups-inheriting finite-sups-inheriting bottom-inheriting
full for SubRelStr of L;
existence
proof set S = the non empty sups-inheriting full SubRelStr of L;
take S;
thus thesis;
end;
end;
theorem Th60:
for L being lower-bounded antisymmetric non empty RelStr
for S being non empty bottom-inheriting full SubRelStr of L
holds Bottom S = Bottom L
proof
let L be lower-bounded antisymmetric non empty RelStr;
let S be non empty bottom-inheriting full SubRelStr of L;
reconsider s = Bottom L as Element of S by Def19;
reconsider l = Bottom S as Element of L by YELLOW_0:58;
A1: Bottom L <= l by YELLOW_0:44;
A2: Bottom S <= s by YELLOW_0:44;
Bottom S >= s by A1,YELLOW_0:60;
hence thesis by A2,ORDERS_2:2;
end;
registration
let L be with_suprema lower-bounded non empty Poset;
cluster bottom-inheriting join-inheriting -> finite-sups-inheriting
for full SubRelStr of L;
coherence
proof
let S be full SubRelStr of L;
assume S is bottom-inheriting join-inheriting;
then reconsider S9 = S as join-inheriting bottom-inheriting full SubRelStr
of L;
let X be finite Subset of S;
reconsider X9 = X as Subset of S9;
A1: X is finite;
defpred P[set] means for Y being finite Subset of S9 st Y = $1
holds ex_sup_of Y,L & "\/"(Y, L) = sup Y;
A2: Bottom L = "\/"({}, L);
Bottom S9 = "\/"({}, S9);
then
A3: P[{}] by A2,Th60,YELLOW_0:42;
A4: for x,B being set st x in X & B c= X & P[B] holds P[B \/ {x}]
proof
let x,B be set such that x in X and B c= X and
A5: for Y being finite Subset of S9 st Y = B
holds ex_sup_of Y,L & "\/"(Y, L) = sup Y;
let Y be finite Subset of S9 such that
A6: Y = B \/ {x};
A7: B c= Y by A6,XBOOLE_1:7;
A8: {x} c= Y by A6,XBOOLE_1:7;
reconsider Z = B as finite Subset of S9 by A7,XBOOLE_1:1;
A9: ex_sup_of Z,L by A5;
A10: "\/"(Z, L) = sup Z by A5;
x in Y by A8,ZFMISC_1:31;
then reconsider x as Element of S9;
reconsider a = x as Element of L by YELLOW_0:58;
A11: ex_sup_of {a}, L by YELLOW_0:38;
hence ex_sup_of Y,L by A6,A9,YELLOW_2:3;
A12: Z = {} or Z <> {} & S9 is with_suprema;
A13: ex_sup_of {x}, S9 by YELLOW_0:54;
A14: ex_sup_of Z, S9 by A12,YELLOW_0:42,54;
thus "\/"(Y, L) = "\/"(Z, L) "\/" sup {a} by A6,A9,A11,YELLOW_2:3
.= "\/"(Z, L) "\/" a by YELLOW_0:39
.= (sup Z) "\/" x by A10,YELLOW_0:70
.= (sup Z) "\/" sup {x} by YELLOW_0:39
.= sup Y by A6,A13,A14,YELLOW_2:3;
end;
P[X] from FINSET_1:sch 2(A1,A3,A4);
then "\/"(X, L) = sup X9;
hence thesis;
end;
end;
theorem
for S,T being non empty RelStr, f being Function of S,T
st f is finite-sups-preserving holds f is join-preserving bottom-preserving;
theorem Th62:
for S,T being lower-bounded with_suprema Poset, f being Function of S,T
st f is join-preserving bottom-preserving holds f is finite-sups-preserving
proof
let S,T be lower-bounded with_suprema Poset, f be Function of S,T;
assume
A1: f is join-preserving bottom-preserving;
let X be finite Subset of S;
A2: X is finite;
defpred P[set] means
for Y being finite Subset of S st Y = $1 holds f preserves_sup_of Y;
f preserves_sup_of {}S by A1;
then
A3: P[{}];
A4: for x,B being set st x in X & B c= X & P[B] holds P[B \/ {x}]
proof
let x,B be set such that x in X and B c= X and
A5: for Y being finite Subset of S st Y = B holds f preserves_sup_of Y;
let Y be finite Subset of S such that
A6: Y = B \/ {x};
A7: B c= Y by A6,XBOOLE_1:7;
A8: {x} c= Y by A6,XBOOLE_1:7;
reconsider Z = B as finite Subset of S by A7,XBOOLE_1:1;
A9: x in Y by A8,ZFMISC_1:31;
then reconsider x as Element of S;
A10: f preserves_sup_of Z by A5;
f.:Z = {} or f.:Z <> {} & f.:Z is finite;
then
A11: ex_sup_of f.:Z,T by YELLOW_0:42,54;
A12: ex_sup_of {f.x},T by YELLOW_0:54;
Z = {} or Z <> {};
then
A13: ex_sup_of Z,S by YELLOW_0:42,54;
A14: f preserves_sup_of {sup Z, x} by A1;
A15: sup {x} = x by YELLOW_0:39;
A16: ex_sup_of {x}, S by YELLOW_0:38;
A17: ex_sup_of Y,S by A9,YELLOW_0:54;
assume ex_sup_of Y,S;
thus ex_sup_of f.:Y,T by A9,YELLOW_0:54;
dom f = the carrier of S by FUNCT_2:def 1;
then Im(f,x) = {f.x} by FUNCT_1:59;
then
A18: f.:Y = (f.:Z) \/ {f.x} by A6,RELAT_1:120;
sup {f.x} = f.x by YELLOW_0:39;
hence sup (f.:Y) = (sup (f.:Z)) "\/" (f.x) by A11,A12,A18,YELLOW_2:3
.= (f.(sup Z)) "\/" (f.x) by A10,A13
.= f.((sup Z) "\/" x) by A14,YELLOW_3:9
.= f.sup Y by A6,A13,A15,A16,A17,YELLOW_0:36;
end;
P[X] from FINSET_1:sch 2(A2,A3,A4);
hence thesis;
end;
registration
let S,T be non empty RelStr;
cluster sups-preserving -> finite-sups-preserving for Function of S,T;
coherence;
cluster finite-sups-preserving ->
join-preserving bottom-preserving for Function of S,T;
coherence;
end;
registration
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster sups-preserving finite-sups-preserving for Function of S,T;
existence
proof set f = the sups-preserving Function of S,T;
take f;
thus thesis;
end;
end;
registration :: WAYBEL13:15
let L be lower-bounded non empty Poset;
cluster CompactSublatt L -> lower-bounded;
coherence
proof Bottom L is compact by WAYBEL_3:15;
then reconsider c = Bottom L as Element of CompactSublatt L by
WAYBEL_8:def 1;
take c;
let b be Element of CompactSublatt L such that
b in the carrier of CompactSublatt L;
reconsider x = b as Element of L by YELLOW_0:58;
Bottom L <= x by YELLOW_0:44;
hence c <= b by YELLOW_0:60;
end;
end;
theorem Th63:
for S being RelStr, T being non empty RelStr, f being Function of S,T
for S9 being SubRelStr of S for T9 being SubRelStr of T
st f.:the carrier of S9 c= the carrier of T9
holds f|the carrier of S9 is Function of S9, T9
proof
let S be RelStr, T be non empty RelStr, f be Function of S,T;
let S9 be SubRelStr of S, T9 be SubRelStr of T such that
A1: f.:the carrier of S9 c= the carrier of T9;
set g = f|the carrier of S9;
A2: dom f = the carrier of S by FUNCT_2:def 1;
the carrier of S9 c= the carrier of S by YELLOW_0:def 13;
then
A3: dom g = the carrier of S9 by A2,RELAT_1:62;
rng g = f.:the carrier of S9 by RELAT_1:115;
hence thesis by A1,A3,FUNCT_2:2;
end;
theorem Th64:
for S,T being LATTICE, f being join-preserving Function of S,T
for S9 being non empty join-inheriting full SubRelStr of S
for T9 being non empty join-inheriting full SubRelStr of T
for g being Function of S9, T9 st g = f|the carrier of S9
holds g is join-preserving
proof
let S,T be LATTICE, f be join-preserving Function of S,T;
let S9 be non empty join-inheriting full SubRelStr of S;
let T9 be non empty join-inheriting full SubRelStr of T;
let g be Function of S9, T9 such that
A1: g = f|the carrier of S9;
now
let x,y be Element of S9;
reconsider a = x, b = y as Element of S by YELLOW_0:58;
x"\/"y = a"\/"b by YELLOW_0:70;
then
A2: g.(x"\/"y) = f.(a"\/"b) by A1,FUNCT_1:49;
A3: g.x = f.a by A1,FUNCT_1:49;
A4: g.y = f.b by A1,FUNCT_1:49;
thus g.(x"\/"y) = (f.a)"\/"(f.b) by A2,WAYBEL_6:2
.= (g.x)"\/"(g.y) by A3,A4,YELLOW_0:70;
end;
hence thesis by WAYBEL_6:2;
end;
theorem Th65:
for S,T being lower-bounded LATTICE
for f being finite-sups-preserving Function of S,T
for S9 being non empty finite-sups-inheriting full SubRelStr of S
for T9 being non empty finite-sups-inheriting full SubRelStr of T
for g being Function of S9, T9 st g = f|the carrier of S9
holds g is finite-sups-preserving
proof
let S,T be lower-bounded LATTICE;
let f be finite-sups-preserving Function of S,T;
let S9 be non empty finite-sups-inheriting full SubRelStr of S;
let T9 be non empty finite-sups-inheriting full SubRelStr of T;
let g be Function of S9, T9 such that
A1: g = f|the carrier of S9;
Bottom S9 = Bottom S by Th60;
then g.Bottom S9 = f.Bottom S by A1,FUNCT_1:49
.= Bottom T by Def17
.=
Bottom T9 by Th60;
then g is bottom-preserving;
hence thesis by A1,Th62,Th64;
end;
registration
let L be complete LATTICE;
cluster CompactSublatt L -> finite-sups-inheriting;
coherence
proof
Bottom L in the carrier of CompactSublatt L by WAYBEL_8:3;
then CompactSublatt L is bottom-inheriting join-inheriting non empty
full SubRelStr of L by Def19;
hence thesis;
end;
end;
theorem Th66:
for S,T being complete LATTICE
for d being sups-preserving Function of T,S holds d is compact-preserving
iff d|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
proof
let S,T be complete LATTICE, d be sups-preserving Function of T,S;
thus
d is compact-preserving implies d|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
proof
assume
A1: for x being Element of T st x is compact holds d.x is compact;
d.:the carrier of CompactSublatt T c= the carrier of CompactSublatt S
proof
let y be object;
assume y in d.: the carrier of CompactSublatt T;
then consider x being object such that
A2: x in the carrier of T and
A3: x in the carrier of CompactSublatt T and
A4: y = d.x by FUNCT_2:64;
reconsider x as Element of T by A2;
x is compact by A3,WAYBEL_8:def 1;
then d.x is compact by A1;
hence thesis by A4,WAYBEL_8:def 1;
end;
hence thesis by Th63,Th65;
end;
assume
A5: d|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S;
let x be Element of T;
assume x is compact;
then
A6: x in the carrier of CompactSublatt T by WAYBEL_8:def 1;
then d.x = (d|the carrier of CompactSublatt T).x by FUNCT_1:49;
then d.x in the carrier of CompactSublatt S by A5,A6,FUNCT_2:5;
hence thesis by WAYBEL_8:def 1;
end;
theorem :: 1.12. COROLLARY, p. 183
for S,T being complete LATTICE st T is algebraic
for g being infs-preserving Function of S,T holds
g is directed-sups-preserving iff
(LowerAdj g)|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
proof
let S,T be complete LATTICE such that
A1: T is algebraic;
let g be infs-preserving Function of S,T;
hereby
assume g is directed-sups-preserving;
then LowerAdj g is waybelow-preserving by Th22;
then LowerAdj g is compact-preserving by Th56;
hence (LowerAdj g)|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S
by Th66;
end;
assume (LowerAdj g)|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S;
then LowerAdj g is compact-preserving by Th66;
then LowerAdj g is waybelow-preserving by A1,Th57;
hence thesis by A1,Th23;
end;