:: WAYBEL34 semantic presentation

registration

let S, T be complete LATTICE;
cluster Galois Connection of S,T;
existence

proof end;

end;

theorem Th1: :: WAYBEL34:1

for S, T, S', T' being non empty RelStr st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of S',the InternalRel of S' #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of T',the InternalRel of T' #) holds
for c being Connection of S,T
for c' being Connection of S',T' st c = c' & c is Galois holds
c' is Galois

proof end;

definition

let S, T be LATTICE;
let g be Function of S,T;
assume ( S is complete & T is complete & g is infs-preserving ) ;
then A1: g has_a_lower_adjoint by WAYBEL_1:17;
func LowerAdj g -> Function of T,S means :Def1: :: WAYBEL34:def 1
[g,it] is Galois;
uniqueness

proof end;

existence by A1, WAYBEL_1:def 11;

end;

:: deftheorem Def1 defines LowerAdj WAYBEL34:def 1 :

definition

let S, T be LATTICE;
let d be Function of T,S;
assume ( S is complete & T is complete & d is sups-preserving ) ;
then A1: d has_an_upper_adjoint by WAYBEL_1:18;
func UpperAdj d -> Function of S,T means :Def2: :: WAYBEL34:def 2
[it,d] is Galois;
existence by A1, WAYBEL_1:def 12;
correctness

proof end;

end;

:: deftheorem Def2 defines UpperAdj WAYBEL34:def 2 :

Lm1: now

let S, T be LATTICE; :: thesis:
assume ( S is complete & T is complete ) ; :: thesis:
then reconsider S' = S, T' = T as complete LATTICE ;
let g be Function of S,T; :: thesis:
assume g is infs-preserving ; :: thesis:
then reconsider g' = g as infs-preserving Function of S',T' ;
[g',(LowerAdj g')] is Galois by Def1;
then ( LowerAdj g' is lower_adjoint & LowerAdj g' is monotone ) by WAYBEL_1:9, WAYBEL_1:def 12;
hence ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) by WAYBEL_1:18; :: thesis:

end;

Lm2: now

let S, T be LATTICE; :: thesis:
assume ( S is complete & T is complete ) ; :: thesis:
then reconsider S' = S, T' = T as complete LATTICE ;
let g be Function of S,T; :: thesis:
assume g is sups-preserving ; :: thesis:
then reconsider g' = g as sups-preserving Function of S',T' ;
[(UpperAdj g'),g'] is Galois by Def2;
then ( UpperAdj g' is upper_adjoint & UpperAdj g' is monotone ) by WAYBEL_1:9, WAYBEL_1:def 11;
hence ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) by WAYBEL_1:17; :: thesis:

end;

registration

let S, T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster LowerAdj g -> lower_adjoint ;
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 ;
coherence by Lm2;

end;

theorem :: WAYBEL34:2

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 end;

theorem :: WAYBEL34:3

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 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 :: WAYBEL34:def 3
f;
coherence ;

end;

:: deftheorem defines opp WAYBEL34:def 3 :

registration

let S, T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster g opp -> lower_adjoint ;
coherence

proof 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 end;

end;

theorem :: WAYBEL34:4

for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds LowerAdj g = UpperAdj (g opp )

proof end;

theorem :: WAYBEL34:5

for S, T being complete LATTICE
for d being sups-preserving Function of S,T holds LowerAdj (d opp ) = UpperAdj d

proof end;

theorem Th6: :: WAYBEL34:6

for L being non empty RelStr holds [(id L),(id L)] is Galois

proof end;

theorem Th7: :: WAYBEL34:7

for L being complete LATTICE holds
( LowerAdj (id L) = id L & UpperAdj (id L) = id L )

proof end;

theorem Th8: :: WAYBEL34:8

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 end;

theorem Th9: :: WAYBEL34:9

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 end;

theorem Th10: :: WAYBEL34:10

for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds UpperAdj (LowerAdj g) = g

proof end;

theorem Th11: :: WAYBEL34:11

for S, T being complete LATTICE
for d being sups-preserving Function of S,T holds LowerAdj (UpperAdj d) = d

proof end;

theorem Th12: :: WAYBEL34:12

for C being non empty AltCatStr
for a, b, f being set st f in the Arrows of C . a,b holds
ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )

proof end;

definition

let W be non empty set ;
defpred S₁[ LATTICE] means $1 is complete;
defpred S₂[ LATTICE, LATTICE, Function of $1,$2] means $3 is infs-preserving;
given w being Element of W such that A1: not w is empty ;
func W -INF_category -> strict lattice-wise category means :Def4: :: WAYBEL34:def 4
( ( for x being LATTICE holds
( x is object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of it
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines -INF_category WAYBEL34:def 4 :

Lm3: for W being with_non-empty_element set
for a, b being LATTICE
for 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 end;

definition

let W be non empty set ;
defpred S₁[ LATTICE] means $1 is complete;
defpred S₂[ LATTICE, LATTICE, Function of $1,$2] means $3 is sups-preserving;
given w being Element of W such that A1: not w is empty ;
func W -SUP_category -> strict lattice-wise category means :Def5: :: WAYBEL34:def 5
( ( for x being LATTICE holds
( x is object of it iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being object of it
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines -SUP_category WAYBEL34:def 5 :

Lm4: for W being with_non-empty_element set
for a, b being LATTICE
for 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 end;

registration

let W be with_non-empty_element set ;
cluster W -INF_category -> strict lattice-wise with_complete_lattices ;
coherence

proof end;

cluster W -SUP_category -> strict lattice-wise with_complete_lattices ;
coherence

proof end;

end;

theorem Th13: :: WAYBEL34:13

for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -INF_category ) iff ( L is strict & L is complete & the carrier of L in W ) )

proof end;

theorem Th14: :: WAYBEL34:14

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 end;

theorem Th15: :: WAYBEL34:15

for W being with_non-empty_element set
for L being LATTICE holds
( L is object of (W -SUP_category ) iff ( L is strict & L is complete & the carrier of L in W ) )

proof end;

theorem Th16: :: WAYBEL34:16

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 end;

theorem Th17: :: WAYBEL34:17

for W being with_non-empty_element set holds the carrier of (W -INF_category ) = the carrier of (W -SUP_category )

proof end;

definition

let W be with_non-empty_element set ;
set A = W -INF_category ;
set B = W -SUP_category ;
deffunc H₁( LATTICE) -> LATTICE = $1;
deffunc H₂( LATTICE, LATTICE, Function of $1,$2) -> Function of $2,$1 = LowerAdj $3;
defpred S₁[ LATTICE, LATTICE, Function of $1,$2] means ( $1 is complete & $2 is complete & $3 is infs-preserving );
defpred S₂[ LATTICE, LATTICE, Function of $1,$2] means ( $1 is complete & $2 is complete & $3 is sups-preserving );
A1: for a, b being LATTICE
for 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 ) & S₁[a,b,f] ) ) by Lm3;
A2: for a, b being LATTICE
for 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 ) & S₂[a,b,f] ) ) by Lm4;
A3: for a being LATTICE st a in the carrier of (W -INF_category ) holds
H₁(a) in the carrier of (W -SUP_category ) by Th17;
A4: for a, b being LATTICE
for f being Function of a,b st S₁[a,b,f] holds
( H₂(a,b,f) is Function of H₁(b),H₁(a) & S₂[H₁(b),H₁(a),H₂(a,b,f)] ) by Lm1;

A5: now

let a be LATTICE; :: thesis:
assume a in the carrier of (W -INF_category ) ; :: thesis:
then a is complete by YELLOW21:def 5;
hence H₂(a,a, id a) = id H₁(a) by Th7; :: thesis:

end;

A6: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st S₁[a,b,f] & S₁[b,c,g] holds
H₂(a,c,g * f) = H₂(a,b,f) * H₂(b,c,g) by Th8;
func W LowerAdj -> strict contravariant Functor of W -INF_category ,W -SUP_category means :Def6: :: WAYBEL34:def 6
( ( 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^> <> {} holds
for f being Morphism of a,b holds it . f = LowerAdj (@ f) ) );
existence

proof end;

uniqueness

proof end;

deffunc H₃( LATTICE, LATTICE, Function of $1,$2) -> Function of $2,$1 = UpperAdj $3;
A13: for a being LATTICE st a in the carrier of (W -SUP_category ) holds
H₁(a) in the carrier of (W -INF_category ) by Th17;
A14: for a, b being LATTICE
for f being Function of a,b st S₂[a,b,f] holds
( H₃(a,b,f) is Function of H₁(b),H₁(a) & S₁[H₁(b),H₁(a),H₃(a,b,f)] ) by Lm2;

A15: now

let a be LATTICE; :: thesis:
assume a in the carrier of (W -SUP_category ) ; :: thesis:
then a is complete by YELLOW21:def 5;
hence H₃(a,a, id a) = id H₁(a) by Th7; :: thesis:

end;

A16: for a, b, c being LATTICE
for f being Function of a,b
for g being Function of b,c st S₂[a,b,f] & S₂[b,c,g] holds
H₃(a,c,g * f) = H₃(a,b,f) * H₃(b,c,g) by Th9;
func W UpperAdj -> strict contravariant Functor of W -SUP_category ,W -INF_category means :Def7: :: WAYBEL34:def 7
( ( 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^> <> {} holds
for f being Morphism of a,b holds it . f = UpperAdj (@ f) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines LowerAdj WAYBEL34:def 6 :

:: deftheorem Def7 defines UpperAdj WAYBEL34:def 7 :

registration

let W be with_non-empty_element set ;
cluster W LowerAdj -> strict contravariant bijective ;
coherence

proof end;

cluster W UpperAdj -> strict contravariant bijective ;
coherence

proof end;

end;

theorem Th18: :: WAYBEL34:18

for W being with_non-empty_element set holds
( (W LowerAdj ) " = W UpperAdj & (W UpperAdj ) " = W LowerAdj )

proof end;

theorem :: WAYBEL34:19

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 end;

theorem :: WAYBEL34:20

for W being with_non-empty_element set holds W -INF_category ,W -SUP_category are_anti-isomorphic

proof end;

theorem :: WAYBEL34:21

canceled;

theorem :: WAYBEL34:22

canceled;

theorem Th23: :: WAYBEL34:23

for S, T being 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 )

proof end;

definition

let S, T be non empty reflexive RelStr ;
let f be Function of S,T;
attr f is waybelow-preserving means :Def8: :: WAYBEL34:def 8
for x, y being Element of S st x << y holds
f . x << f . y;

end;

:: deftheorem Def8 defines waybelow-preserving WAYBEL34:def 8 :

theorem Th24: :: WAYBEL34:24

for S, T being complete LATTICE
for g being infs-preserving Function of S,T st g is directed-sups-preserving holds
LowerAdj g is waybelow-preserving

proof end;

theorem Th25: :: WAYBEL34:25

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 end;

definition

let S, T be TopSpace;
let f be Function of S,T;
attr f is relatively_open means :Def9: :: WAYBEL34:def 9
for V being open Subset of S holds f .: V is open Subset of (T | (rng f));

end;

:: deftheorem Def9 defines relatively_open WAYBEL34:def 9 :

theorem :: WAYBEL34:26

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 end;

theorem Th27: :: WAYBEL34:27

for S, T being complete LATTICE
for 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 end;

theorem Th28: :: WAYBEL34:28

for S, T being complete LATTICE
for 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 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:36;

end;

theorem :: WAYBEL34:29

for S, T being complete LATTICE
for 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
for d' being Function of X,Z st d = LowerAdj g & d' = d & d is relatively_open holds
d' is open

proof end;

theorem Th30: :: WAYBEL34:30

for T1, T2, S1, S2 being TopStruct st TopStruct(# the carrier of T1,the topology of T1 #) = TopStruct(# the carrier of T2,the topology of T2 #) & TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of S2,the topology of S2 #) & S1 is SubSpace of T1 holds
S2 is SubSpace of T2

proof end;

theorem Th31: :: WAYBEL34:31

for T being TopStruct holds T | ([#] T) = TopStruct(# the carrier of T,the topology of T #)

proof end;

theorem Th32: :: WAYBEL34:32

for S, T being complete LATTICE
for g being infs-preserving Function of S,T st g is one-to-one holds
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 end;

registration

let X be complete LATTICE;
let f be projection Function of X,X;
cluster Image f -> complete ;
coherence by WAYBEL_1:57;

end;

theorem Th33: :: WAYBEL34:33

for L being complete LATTICE
for 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 end;

theorem Th34: :: WAYBEL34:34

for L being complete LATTICE
for k being kernel Function of L,L holds
( k is directed-sups-preserving iff corestr k is directed-sups-preserving )

proof end;

theorem :: WAYBEL34:35

for L being complete LATTICE
for 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 end;

theorem Th36: :: WAYBEL34:36

for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L
for x, y being Element of L
for a, b being Element of S st a = x & b = y & x << y holds
a << b

proof end;

theorem :: WAYBEL34:37

for L being complete LATTICE
for k being kernel Function of L,L st k is directed-sups-preserving holds
for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b )

proof end;

theorem :: WAYBEL34:38

for L being complete LATTICE
for k being kernel Function of L,L st Image k is continuous & ( for x, y being Element of L
for 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 end;

theorem Th39: :: WAYBEL34:39

for L being complete LATTICE
for 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 end;

theorem Th40: :: WAYBEL34:40

for L being complete LATTICE
for c being closure Function of L,L holds
( Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving )

proof end;

theorem :: WAYBEL34:41

for L being complete LATTICE
for 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 end;

theorem :: WAYBEL34:42

for L being complete LATTICE
for c being closure Function of L,L st Image c is directed-sups-inheriting holds
corestr c is waybelow-preserving

proof end;

theorem :: WAYBEL34:43

for L being complete continuous LATTICE
for c being closure Function of L,L st corestr c is waybelow-preserving holds
Image c is directed-sups-inheriting

proof end;

definition

let W be non empty set ;
set A = W -INF_category ;
defpred S₁[ set ] means verum;
defpred S₂[ object of (W -INF_category ), object of (W -INF_category ), Morphism of $1,$2] means @ $3 is directed-sups-preserving;
A1: ex a being object of (W -INF_category ) st S₁[a] ;
A2: for a, b, c being object of (W -INF_category ) st S₁[a] & S₁[b] & S₁[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S₂[a,b,f] & S₂[b,c,g] holds
S₂[a,c,g * f]

proof end;

A5: for a being object of (W -INF_category ) st S₁[a] holds
S₂[a,a, idm a]

proof end;

func W -INF(SC)_category -> non empty strict subcategory of W -INF_category means :Def10: :: WAYBEL34:def 10
( ( for a being object of (W -INF_category ) holds a is object of it ) & ( for a, b being object of (W -INF_category )
for a', b' being object of it st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a',b'^> iff @ f is directed-sups-preserving ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def10 defines -INF(SC)_category WAYBEL34:def 10 :

definition

let W be with_non-empty_element set ;
A1: ex w being non empty set st w in W by SETFAM_1:def 11;
set A = W -SUP_category ;
defpred S₁[ set ] means verum;
defpred S₂[ object of (W -SUP_category ), object of (W -SUP_category ), Morphism of $1,$2] means UpperAdj (@ $3) is directed-sups-preserving;
A2: ex a being object of (W -SUP_category ) st S₁[a] ;
A3: for a, b, c being object of (W -SUP_category ) st S₁[a] & S₁[b] & S₁[c] & <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c st S₂[a,b,f] & S₂[b,c,g] holds
S₂[a,c,g * f]

proof end;

A6: for a being object of (W -SUP_category ) st S₁[a] holds
S₂[a,a, idm a]

proof end;

func W -SUP(SO)_category -> non empty strict subcategory of W -SUP_category means :Def11: :: WAYBEL34:def 11
( ( for a being object of (W -SUP_category ) holds a is object of it ) & ( for a, b being object of (W -SUP_category )
for a', b' being object of it st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a',b'^> iff UpperAdj (@ f) is directed-sups-preserving ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def11 defines -SUP(SO)_category WAYBEL34:def 11 :

theorem Th44: :: WAYBEL34:44

for S being non empty RelStr
for 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 end;

theorem Th45: :: WAYBEL34:45

for S being non empty RelStr
for T being non empty reflexive antisymmetric lower-bounded RelStr holds S --> (Bottom T) is sups-preserving

proof end;

theorem Th46: :: WAYBEL34:46

for S being non empty RelStr
for T being non empty reflexive antisymmetric upper-bounded RelStr holds S --> (Top T) is infs-preserving

proof end;

registration

let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster S --> (Top T) -> infs-preserving directed-sups-preserving ;
coherence

proof end;

end;

registration

let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster S --> (Bottom T) -> sups-preserving filtered-infs-preserving ;
coherence

proof end;

end;

registration

let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster infs-preserving directed-sups-preserving Relation of the carrier of S,the carrier of T;
existence

proof end;

end;

registration

let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster sups-preserving filtered-infs-preserving Relation of the carrier of S,the carrier of T;
existence

proof end;

end;

theorem Th47: :: WAYBEL34:47

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 & L is complete & the carrier of L in W ) )

proof end;

theorem Th48: :: WAYBEL34:48

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 infs-preserving directed-sups-preserving Function of (latt a),(latt b) )

proof end;

theorem :: WAYBEL34:49

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 & L is complete & the carrier of L in W ) )

proof end;

theorem Th50: :: WAYBEL34:50

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 end;

theorem :: WAYBEL34:51

for W being with_non-empty_element set holds W -INF(SC)_category = Intersect (W -INF_category ),(W -UPS_category )

proof end;

definition

let W be with_non-empty_element set ;
defpred S₁[ 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 11;
consider r being upper-bounded well-ordering Order of a;
set b = RelStr(# a,r #);
func W -CL_category -> non empty strict full subcategory of W -INF(SC)_category means :Def12: :: WAYBEL34:def 12
for a being object of (W -INF(SC)_category ) holds
( a is object of it iff latt a is continuous );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def12 defines -CL_category WAYBEL34:def 12 :

registration

let W be with_non-empty_element set ;
cluster W -CL_category -> non empty strict full with_complete_lattices ;
coherence ;

end;

theorem Th52: :: WAYBEL34:52

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 & L is complete & L is continuous ) )

proof end;

theorem Th53: :: WAYBEL34:53

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 end;

definition

let W be with_non-empty_element set ;
defpred S₁[ 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 11;
consider r being upper-bounded well-ordering Order of a;
set b = RelStr(# a,r #);
func W -CL-opp_category -> non empty strict full subcategory of W -SUP(SO)_category means :Def13: :: WAYBEL34:def 13
for a being object of (W -SUP(SO)_category ) holds
( a is object of it iff latt a is continuous );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def13 defines -CL-opp_category WAYBEL34:def 13 :

theorem Th54: :: WAYBEL34:54

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 & L is complete & L is continuous ) )

proof end;

theorem Th55: :: WAYBEL34:55

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 end;

theorem Th56: :: WAYBEL34:56

for W being with_non-empty_element set holds W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj

proof end;

theorem :: WAYBEL34:57

for W being with_non-empty_element set holds W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj

proof end;

theorem Th58: :: WAYBEL34:58

for W being with_non-empty_element set holds W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj

proof end;

theorem :: WAYBEL34:59

for W being with_non-empty_element set holds W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj

proof end;

definition

let S, T be non empty reflexive RelStr ;
let f be Function of S,T;
attr f is compact-preserving means :: WAYBEL34:def 14
for s being Element of S st s is compact holds
f . s is compact;

end;

:: deftheorem defines compact-preserving WAYBEL34:def 14 :

theorem Th60: :: WAYBEL34:60

for S, T being complete LATTICE
for d being sups-preserving Function of T,S st d is waybelow-preserving holds
d is compact-preserving

proof end;

theorem Th61: :: WAYBEL34:61

for S, T being complete LATTICE
for d being sups-preserving Function of T,S st T is algebraic & d is compact-preserving holds
d is waybelow-preserving

proof end;

theorem Th62: :: WAYBEL34:62

for R, S, T being non empty RelStr
for 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 end;

definition

let S, T be non empty RelStr ;
let f be Function of S,T;
attr f is finite-sups-preserving means :: WAYBEL34:def 15
for X being finite Subset of S holds f preserves_sup_of X;
attr f is bottom-preserving means :Def16: :: WAYBEL34:def 16
f preserves_sup_of {} S;

end;

:: deftheorem defines finite-sups-preserving WAYBEL34:def 15 :

:: deftheorem Def16 defines bottom-preserving WAYBEL34:def 16 :

theorem :: WAYBEL34:63

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 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: :: WAYBEL34:def 17
f . (Bottom S) = Bottom T;
compatibility

proof end;

end;

:: deftheorem Def17 defines bottom-preserving WAYBEL34:def 17 :

definition

let L be non empty RelStr ;
let S be SubRelStr of L;
attr S is finite-sups-inheriting means :Def18: :: WAYBEL34:def 18
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: :: WAYBEL34:def 19
Bottom L in the carrier of S;

end;

:: deftheorem Def18 defines finite-sups-inheriting WAYBEL34:def 18 :

:: deftheorem Def19 defines bottom-inheriting WAYBEL34:def 19 :

registration

let S, T be non empty RelStr ;
cluster sups-preserving -> bottom-preserving Relation of the carrier of S,the carrier of T;
coherence

proof end;

end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;
cluster finite-sups-inheriting -> join-inheriting bottom-inheriting SubRelStr of L;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
cluster sups-inheriting -> finite-sups-inheriting SubRelStr of L;
coherence

proof end;

end;

registration

let S, T be non empty lower-bounded Poset;
cluster sups-preserving bottom-preserving Relation of the carrier of S,the carrier of T;
existence

proof end;

end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;
cluster full bottom-inheriting -> non empty lower-bounded full SubRelStr of L;
coherence

proof end;

end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;
cluster non empty lower-bounded full join-inheriting sups-inheriting finite-sups-inheriting bottom-inheriting SubRelStr of L;
existence

proof end;

end;

theorem Th64: :: WAYBEL34:64

for L being non empty antisymmetric lower-bounded RelStr
for S being non empty full bottom-inheriting SubRelStr of L holds Bottom S = Bottom L

proof end;

registration

let L be non empty lower-bounded with_suprema Poset;
cluster full join-inheriting bottom-inheriting -> non empty lower-bounded full join-inheriting finite-sups-inheriting bottom-inheriting SubRelStr of L;
coherence

proof end;

end;

theorem Th65: :: WAYBEL34:65

for S, T being non empty RelStr
for f being Function of S,T st f is finite-sups-preserving holds
( f is join-preserving & f is bottom-preserving )

proof end;

theorem Th66: :: WAYBEL34:66

for S, T being lower-bounded with_suprema Poset
for f being Function of S,T st f is join-preserving & f is bottom-preserving holds
f is finite-sups-preserving

proof end;

registration

let S, T be non empty RelStr ;
cluster sups-preserving -> finite-sups-preserving Relation of the carrier of S,the carrier of T;
coherence

proof end;

cluster finite-sups-preserving -> join-preserving bottom-preserving Relation of the carrier of S,the carrier of T;
coherence by Th65;

end;

registration

let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster sups-preserving join-preserving finite-sups-preserving bottom-preserving Relation of the carrier of S,the carrier of T;
existence

proof end;

end;

registration

let L be non empty lower-bounded Poset;
cluster CompactSublatt L -> lower-bounded ;
coherence

proof end;

end;

theorem Th67: :: WAYBEL34:67

for S being RelStr
for T being non empty RelStr
for f being Function of S,T
for S' being SubRelStr of S
for T' being SubRelStr of T st f .: the carrier of S' c= the carrier of T' holds
f | the carrier of S' is Function of S',T'

proof end;

theorem Th68: :: WAYBEL34:68

for S, T being LATTICE
for f being join-preserving Function of S,T
for S' being non empty full join-inheriting SubRelStr of S
for T' being non empty full join-inheriting SubRelStr of T
for g being Function of S',T' st g = f | the carrier of S' holds
g is join-preserving

proof end;

theorem Th69: :: WAYBEL34:69

for S, T being lower-bounded LATTICE
for f being finite-sups-preserving Function of S,T
for S' being non empty full finite-sups-inheriting SubRelStr of S
for T' being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S',T' st g = f | the carrier of S' holds
g is finite-sups-preserving

proof end;

registration

let L be complete LATTICE;
cluster CompactSublatt L -> lower-bounded finite-sups-inheriting bottom-inheriting ;
coherence

proof end;

end;

theorem Th70: :: WAYBEL34:70

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 end;

theorem :: WAYBEL34:71

for S, T being complete LATTICE st T is algebraic holds
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 end;