let S, T be complete LATTICE; for 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 )
let g be infs-preserving Function of S,T; ( 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 )
hereby ( ( 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 ) implies g is directed-sups-preserving )
assume A1:
g is
directed-sups-preserving
;
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 Ylet X be
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 Ylet Y be
Scott TopAugmentation of
S;
for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Ylet V be
open Subset of
X;
uparrow ((LowerAdj g) .: V) is open Subset of YA2:
RelStr(# the
carrier of
X, the
InternalRel of
X #)
= RelStr(# the
carrier of
T, the
InternalRel of
T #)
by YELLOW_9:def 4;
A3:
RelStr(# the
carrier of
Y, the
InternalRel of
Y #)
= RelStr(# the
carrier of
S, the
InternalRel 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;
WAYBEL11:def 1 ( not "\/" (D,Y) in uparrow (d .: V) or not D misses uparrow (d .: V) )
assume
sup D in uparrow (d .: V)
;
not D misses 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 =
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 & not
g .: D is
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 . x
by A21, FUNCT_2:64;
reconsider x =
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
not
D misses uparrow (d .: V)
by A24, XBOOLE_0:3;
verum
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;
verum
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
; g is directed-sups-preserving
set X = the Scott TopAugmentation of T;
set Y = the Scott TopAugmentation of S;
A29:
RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
A30:
RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
then reconsider g9 = g as Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A29;
reconsider g9 = g9 as infs-preserving Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A29, A30, WAYBEL21:6;
set d = LowerAdj g;
reconsider d9 = LowerAdj g as Function of the Scott TopAugmentation of T, the Scott TopAugmentation of S by A29, A30;
let D be Subset of S; WAYBEL_0:def 37 ( D is empty or not D is directed or g preserves_sup_of D )
assume A31:
( not D is empty & D is directed )
; g preserves_sup_of D
assume
ex_sup_of D,S
; WAYBEL_0:def 31 ( ex_sup_of g .: D,T & "\/" ((g .: D),T) = g . ("\/" (D,S)) )
thus
ex_sup_of g .: D,T
by YELLOW_0:17; "\/" ((g .: D),T) = g . ("\/" (D,S))
A32:
sup (g .: D) <= g . (sup D)
by WAYBEL17:15;
reconsider D9 = D as Subset of the Scott TopAugmentation of S by A30;
reconsider D9 = D9 as non empty directed Subset of the Scott TopAugmentation of S by A30, A31, WAYBEL_0:3;
reconsider s = sup D as Element of the Scott TopAugmentation of S by A30;
set U9 = (downarrow (sup (g9 .: D9))) ` ;
A33:
(downarrow (sup (g9 .: D9))) ` is open
by WAYBEL11:12;
then
uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) `)) is open Subset of the Scott TopAugmentation of S
by A28;
then A34:
uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) `)) is upper inaccessible Subset of the Scott TopAugmentation of S
by WAYBEL11:def 4;
sup (g9 .: D9) = sup (g .: D)
by A29, YELLOW_0:17, YELLOW_0: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,(LowerAdj g)] is Galois
by Def1;
then A38:
(LowerAdj g) * g <= id S
by WAYBEL_1:18;
A39:
id T <= g * (LowerAdj g)
by A37, WAYBEL_1:18;
A40:
(id S) . (sup D) = sup D
by FUNCT_1:18;
((LowerAdj g) * g) . (sup D) = (LowerAdj g) . (g . (sup D))
by FUNCT_2:15;
then
(LowerAdj g) . (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, YELLOW_0:26;
g . (sup D) <= sup (g .: D)
proof
assume
not
g . (sup D) <= sup (g .: D)
;
contradiction
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 (downarrow (sup (g9 .: D9))) `
by A29, A35, A43, XBOOLE_0:def 5;
A46:
not
sup (g .: D) in (downarrow (sup (g9 .: D9))) `
by A35, A44, XBOOLE_0:def 5;
A47:
d9 . (g9 . s) in d9 .: ((downarrow (sup (g9 .: D9))) `)
by A45, FUNCT_2:35;
d9 .: ((downarrow (sup (g9 .: D9))) `) c= uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `))
by WAYBEL_0:16;
then A48:
s in uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `))
by A41, A47, WAYBEL_0:def 20;
uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `)) = uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) `))
by A30, WAYBEL_0:13;
then
D9 meets uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `))
by A34, A42, A48, WAYBEL11:def 1;
then consider x being
object such that A49:
x in D9
and A50:
x in uparrow (d9 .: ((downarrow (sup (g9 .: D9))) `))
by XBOOLE_0:3;
reconsider x =
x as
Element of the
Scott TopAugmentation of
S by A49;
consider u9 being
Element of the
Scott TopAugmentation of
S such that A51:
u9 <= x
and A52:
u9 in d9 .: ((downarrow (sup (g9 .: D9))) `)
by A50, WAYBEL_0:def 16;
consider u being
object such that A53:
u in the
carrier of the
Scott TopAugmentation of
T
and A54:
u in (downarrow (sup (g9 .: D9))) `
and A55:
u9 = d9 . u
by A52, FUNCT_2:64;
reconsider u =
u as
Element of the
Scott TopAugmentation of
T by A53;
reconsider a =
u as
Element of
T by A29;
(id T) . a = u
by FUNCT_1:18;
then
a <= (g * (LowerAdj g)) . a
by A39, YELLOW_2:9;
then
a <= g . ((LowerAdj g) . 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;
(downarrow (sup (g9 .: D9))) ` is
upper
by A33, WAYBEL11:def 4;
then
sup (g9 .: D9) in (downarrow (sup (g9 .: D9))) `
by A54, A58;
hence
contradiction
by A29, A46, YELLOW_0:17, YELLOW_0:26;
verum
end;
hence
"\/" ((g .: D),T) = g . ("\/" (D,S))
by A32, ORDERS_2:2; verum