let S, T be complete LATTICE; :: thesis: 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; :: thesis: ( 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 :: thesis: ( ( 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
;
:: thesis: 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;
:: thesis: 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;
:: thesis: for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Ylet V be
open Subset of
X;
:: thesis: 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 #) &
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 g' =
g as
Function of
Y,
X ;
reconsider d =
LowerAdj g as
Function of
X,
Y by A2;
uparrow (d .: V) is
inaccessible_by_directed_joins
proof
let D be non
empty directed Subset of
Y;
:: according to WAYBEL11:def 1 :: thesis: ( not "\/" D,Y in uparrow (d .: V) or not D misses uparrow (d .: V) )
assume
sup D in uparrow (d .: V)
;
:: thesis: not D misses uparrow (d .: V)
then consider y being
Element of
Y such that A3:
(
y <= sup D &
y in d .: V )
by WAYBEL_0:def 16;
consider u being
set such that A4:
(
u in the
carrier of
X &
u in V &
y = d . u )
by A3, FUNCT_2:115;
reconsider u =
u as
Element of
X by A4;
reconsider g =
g' as
Function of
Y,
X ;
[g,d] is
Galois Connection of
S,
T
by Def1;
then
[g,d] is
Galois
by A2, Th1;
then A5:
(
d * g <= id Y &
id X <= g * d )
by WAYBEL_1:19;
A6:
(
(id X) . u = u &
(g * d) . u = g . (d . u) )
by FUNCT_1:35, FUNCT_2:21;
A7:
g is
infs-preserving Function of
Y,
X
by A2, WAYBEL21:6;
then
(
u <= g . y &
g . y <= g . (sup D) )
by A3, A4, A5, A6, ORDERS_3:def 5, YELLOW_2:10;
then
(
u <= g . (sup D) &
V is
upper )
by ORDERS_2:26, WAYBEL11:def 4;
then A8:
g . (sup D) in V
by A4, WAYBEL_0:def 20;
g is
directed-sups-preserving
by A1, A2, WAYBEL21:6;
then
(
g preserves_sup_of D &
ex_sup_of D,
Y )
by WAYBEL_0:def 37, YELLOW_0:17;
then A9:
g . (sup D) = sup (g .: D)
by WAYBEL_0:def 31;
(
g .: D is
directed & not
g .: D is
empty &
V is
inaccessible_by_directed_joins )
by A7, WAYBEL11:def 4, YELLOW_2:17;
then
g .: D meets V
by A8, A9, WAYBEL11:def 1;
then consider z being
set such that A10:
(
z in g .: D &
z in V )
by XBOOLE_0:3;
consider x being
set such that A11:
(
x in the
carrier of
Y &
x in D &
z = g . x )
by A10, FUNCT_2:115;
reconsider x =
x as
Element of
Y by A11;
(
(d * g) . x = d . (g . x) &
(id Y) . x = x )
by FUNCT_1:35, FUNCT_2:21;
then
(
d . (g . x) <= x &
d . z in d .: V )
by A5, A10, FUNCT_2:43, YELLOW_2:10;
then
x in uparrow (d .: V)
by A11, WAYBEL_0:def 16;
hence
not
D misses uparrow (d .: V)
by A11, XBOOLE_0:3;
:: thesis: 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 A2, WAYBEL_0:13;
:: thesis: verum
end;
assume A12:
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
; :: thesis: g is directed-sups-preserving
consider X being Scott TopAugmentation of T, Y being Scott TopAugmentation of S;
A13:
( RelStr(# the carrier of X,the InternalRel of X #) = RelStr(# the carrier of T,the InternalRel of T #) & 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 g' = g as Function of Y,X ;
reconsider g' = g' as infs-preserving Function of Y,X by A13, WAYBEL21:6;
set d = LowerAdj g;
reconsider d' = LowerAdj g as Function of X,Y by A13;
let D be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or g preserves_sup_of D )
assume A14:
( not D is empty & D is directed )
; :: thesis: g preserves_sup_of D
assume
ex_sup_of D,S
; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: D,T & "\/" (g .: D),T = g . ("\/" D,S) )
thus
ex_sup_of g .: D,T
by YELLOW_0:17; :: thesis: "\/" (g .: D),T = g . ("\/" D,S)
A15:
sup (g .: D) <= g . (sup D)
by WAYBEL17:15;
reconsider D' = D as Subset of Y by A13;
reconsider D' = D' as non empty directed Subset of Y by A13, A14, WAYBEL_0:3;
reconsider s = sup D as Element of Y by A13;
set U' = (downarrow (sup (g' .: D'))) ` ;
A16:
(downarrow (sup (g' .: D'))) ` is open
by WAYBEL11:12;
then
uparrow ((LowerAdj g) .: ((downarrow (sup (g' .: D'))) ` )) is open Subset of Y
by A12;
then A17:
uparrow ((LowerAdj g) .: ((downarrow (sup (g' .: D'))) ` )) is upper inaccessible Subset of Y
by WAYBEL11:def 4;
A18:
ex_sup_of g .: D,T
by YELLOW_0:17;
then
sup (g' .: D') = sup (g .: D)
by A13, YELLOW_0:26;
then A19:
downarrow (sup (g' .: D')) = downarrow (sup (g .: D))
by A13, WAYBEL_0:13;
A20:
sup (g .: D) <= sup (g .: D)
;
[g,(LowerAdj g)] is Galois
by Def1;
then A21:
( (LowerAdj g) * g <= id S & id T <= g * (LowerAdj g) )
by WAYBEL_1:19;
( (id S) . (sup D) = sup D & ((LowerAdj g) * g) . (sup D) = (LowerAdj g) . (g . (sup D)) )
by FUNCT_1:35, FUNCT_2:21;
then
(LowerAdj g) . (g . (sup D)) <= sup D
by A21, YELLOW_2:10;
then A22:
d' . (g' . s) <= s
by A13, YELLOW_0:1;
ex_sup_of D,S
by YELLOW_0:17;
then A23:
s = sup D'
by A13, YELLOW_0:26;
g . (sup D) <= sup (g .: D)
proof
assume
not
g . (sup D) <= sup (g .: D)
;
:: thesis: contradiction
then
( not
g . (sup D) in downarrow (sup (g .: D)) &
sup (g .: D) in downarrow (sup (g .: D)) )
by A20, WAYBEL_0:17;
then A24:
(
g . (sup D) in (downarrow (sup (g' .: D'))) ` & not
sup (g .: D) in (downarrow (sup (g' .: D'))) ` )
by A13, A19, XBOOLE_0:def 5;
then
(
d' . (g' . s) in d' .: ((downarrow (sup (g' .: D'))) ` ) &
d' .: ((downarrow (sup (g' .: D'))) ` ) c= uparrow (d' .: ((downarrow (sup (g' .: D'))) ` )) )
by FUNCT_2:43, WAYBEL_0:16;
then
(
s in uparrow (d' .: ((downarrow (sup (g' .: D'))) ` )) &
uparrow (d' .: ((downarrow (sup (g' .: D'))) ` )) = uparrow ((LowerAdj g) .: ((downarrow (sup (g' .: D'))) ` )) )
by A13, A22, WAYBEL_0:13, WAYBEL_0:def 20;
then
D' meets uparrow (d' .: ((downarrow (sup (g' .: D'))) ` ))
by A17, A23, WAYBEL11:def 1;
then consider x being
set such that A25:
(
x in D' &
x in uparrow (d' .: ((downarrow (sup (g' .: D'))) ` )) )
by XBOOLE_0:3;
reconsider x =
x as
Element of
Y by A25;
consider u' being
Element of
Y such that A26:
(
u' <= x &
u' in d' .: ((downarrow (sup (g' .: D'))) ` ) )
by A25, WAYBEL_0:def 16;
consider u being
set such that A27:
(
u in the
carrier of
X &
u in (downarrow (sup (g' .: D'))) ` &
u' = d' . u )
by A26, FUNCT_2:115;
reconsider u =
u as
Element of
X by A27;
reconsider a =
u as
Element of
T by A13;
(id T) . a = u
by FUNCT_1:35;
then
a <= (g * (LowerAdj g)) . a
by A21, YELLOW_2:10;
then
a <= g . ((LowerAdj g) . a)
by FUNCT_2:21;
then
(
u <= g' . (d' . u) &
g' . (d' . u) <= g' . x )
by A13, A26, A27, ORDERS_3:def 5, YELLOW_0:1;
then A28:
u <= g' . x
by ORDERS_2:26;
g' . x in g' .: D'
by A25, FUNCT_2:43;
then
g' . x <= sup (g' .: D')
by YELLOW_2:24;
then
(
u <= sup (g' .: D') &
(downarrow (sup (g' .: D'))) ` is
upper )
by A16, A28, ORDERS_2:26, WAYBEL11:def 4;
then
sup (g' .: D') in (downarrow (sup (g' .: D'))) `
by A27, WAYBEL_0:def 20;
hence
contradiction
by A13, A18, A24, YELLOW_0:26;
:: thesis: verum
end;
hence
"\/" (g .: D),T = g . ("\/" D,S)
by A15, ORDERS_2:25; :: thesis: verum