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_by_directed_joins
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
set such that A6:
u in the
carrier of
X
and A7:
u in V
and A8:
y = d . u
by A5, FUNCT_2:115;
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:19;
A11:
id X <= g * d
by A9, WAYBEL_1:19;
A12:
(id X) . u = u
by FUNCT_1:35;
A13:
(g * d) . u = g . (d . u)
by FUNCT_2:21;
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:10;
g . y <= g . (sup D)
by A4, A14, ORDERS_3:def 5;
then A16:
u <= g . (sup D)
by A15, ORDERS_2:26;
V is
upper
by WAYBEL11:def 4;
then A17:
g . (sup D) in V
by A7, A16, WAYBEL_0:def 20;
g is
directed-sups-preserving
by A1, A2, A3, WAYBEL21:6;
then A18:
g preserves_sup_of D
by WAYBEL_0:def 37;
ex_sup_of D,
Y
by YELLOW_0:17;
then A19:
g . (sup D) = sup (g .: D)
by A18, WAYBEL_0:def 31;
A20:
(
g .: D is
directed & not
g .: D is
empty )
by A14, YELLOW_2:17;
V is
inaccessible_by_directed_joins
by WAYBEL11:def 4;
then
g .: D meets V
by A17, A19, A20, WAYBEL11:def 1;
then consider z being
set such that A21:
z in g .: D
and A22:
z in V
by XBOOLE_0:3;
consider x being
set such that A23:
x in the
carrier of
Y
and A24:
x in D
and A25:
z = g . x
by A21, FUNCT_2:115;
reconsider x =
x as
Element of
Y by A23;
A26:
(d * g) . x = d . (g . x)
by FUNCT_2:21;
(id Y) . x = x
by FUNCT_1:35;
then A27:
d . (g . x) <= x
by A10, A26, YELLOW_2:10;
d . z in d .: V
by A22, FUNCT_2:43;
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
consider X being Scott TopAugmentation of T, Y being Scott TopAugmentation of S;
A29:
RelStr(# the carrier of X,the InternalRel of X #) = RelStr(# the carrier of T,the InternalRel of T #)
by YELLOW_9:def 4;
A30:
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 A29;
reconsider g9 = g9 as infs-preserving Function of Y,X by A29, A30, WAYBEL21:6;
set d = LowerAdj g;
reconsider d9 = LowerAdj g as Function of X,Y 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 Y by A30;
reconsider D9 = 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:
(downarrow (sup (g9 .: D9))) ` is open
by WAYBEL11:12;
then
uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) ` )) is open Subset of Y
by A28;
then A34:
uparrow ((LowerAdj g) .: ((downarrow (sup (g9 .: D9))) ` )) is upper inaccessible Subset of Y
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:19;
A39:
id T <= g * (LowerAdj g)
by A37, WAYBEL_1:19;
A40:
(id S) . (sup D) = sup D
by FUNCT_1:35;
((LowerAdj g) * g) . (sup D) = (LowerAdj g) . (g . (sup D))
by FUNCT_2:21;
then
(LowerAdj g) . (g . (sup D)) <= sup D
by A38, A40, YELLOW_2:10;
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:43;
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
set 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
Y by A49;
consider u9 being
Element of
Y such that A51:
u9 <= x
and A52:
u9 in d9 .: ((downarrow (sup (g9 .: D9))) ` )
by A50, WAYBEL_0:def 16;
consider u being
set such that A53:
u in the
carrier of
X
and A54:
u in (downarrow (sup (g9 .: D9))) `
and A55:
u9 = d9 . u
by A52, FUNCT_2:115;
reconsider u =
u as
Element of
X by A53;
reconsider a =
u as
Element of
T by A29;
(id T) . a = u
by FUNCT_1:35;
then
a <= (g * (LowerAdj g)) . a
by A39, YELLOW_2:10;
then
a <= g . ((LowerAdj g) . a)
by FUNCT_2:21;
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:26;
g9 . x in g9 .: D9
by A49, FUNCT_2:43;
then
g9 . x <= sup (g9 .: D9)
by YELLOW_2:24;
then A58:
u <= sup (g9 .: D9)
by A57, ORDERS_2:26;
(downarrow (sup (g9 .: D9))) ` is
upper
by A33, WAYBEL11:def 4;
then
sup (g9 .: D9) in (downarrow (sup (g9 .: D9))) `
by A54, A58, WAYBEL_0:def 20;
hence
contradiction
by A29, A46, YELLOW_0:17, YELLOW_0:26;
verum
end;
hence
"\/" (g .: D),T = g . ("\/" D,S)
by A32, ORDERS_2:25; verum