:: by Grzegorz Bancerek

::

:: Received August 8, 2001

:: Copyright (c) 2001-2019 Association of Mizar Users

::<section1>Infs-preserving and sups-preserving maps</section1>

registration

let S, T be complete LATTICE;

existence

ex b_{1} being Connection of S,T st b_{1} is Galois

end;
existence

ex b

proof end;

theorem Th1: :: WAYBEL34:1

for S, T, S9, T9 being non empty RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds

for c being Connection of S,T

for c9 being Connection of S9,T9 st c = c9 & c is Galois holds

c9 is Galois

for c being Connection of S,T

for c9 being Connection of S9,T9 st c = c9 & c is Galois holds

c9 is Galois

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

uniqueness

for b_{1}, b_{2} being Function of T,S st [g,b_{1}] is Galois & [g,b_{2}] is Galois holds

b_{1} = b_{2}

ex b_{1} being Function of T,S st [g,b_{1}] is Galois
by A3;

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

uniqueness

for b

b

proof end;

existence ex b

:: deftheorem Def1 defines LowerAdj WAYBEL34:def 1 :

for S, T being LATTICE

for g being Function of S,T st S is complete & g is infs-preserving holds

for b_{4} being Function of T,S holds

( b_{4} = LowerAdj g iff [g,b_{4}] is Galois );

for S, T being LATTICE

for g being Function of S,T st S is complete & g is infs-preserving holds

for b

( b

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;

existence

ex b_{1} being Function of S,T st [b_{1},d] is Galois
by A3;

correctness

uniqueness

for b_{1}, b_{2} being Function of S,T st [b_{1},d] is Galois & [b_{2},d] is Galois holds

b_{1} = b_{2};

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

existence

ex b

correctness

uniqueness

for b

b

proof end;

:: deftheorem Def2 defines UpperAdj WAYBEL34:def 2 :

for S, T being LATTICE

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

for b_{4} being Function of S,T holds

( b_{4} = UpperAdj d iff [b_{4},d] is Galois );

for S, T being LATTICE

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

for b

( b

Lm1: now :: thesis: for S, T being LATTICE st S is complete & T is complete holds

for g being Function of S,T st g is infs-preserving holds

( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving )

for g being Function of S,T st g is infs-preserving holds

( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving )

let S, T be LATTICE; :: thesis: ( S is complete & T is complete implies for g being Function of S,T st g is infs-preserving holds

( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) )

assume that

A1: S is complete and

A2: T is complete ; :: thesis: for g being Function of S,T st g is infs-preserving holds

( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving )

reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;

let g be Function of S,T; :: thesis: ( g is infs-preserving implies ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) )

assume g is infs-preserving ; :: thesis: ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-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 & LowerAdj g9 is monotone ) by WAYBEL_1:8;

hence ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) ; :: thesis: verum

end;
( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) )

assume that

A1: S is complete and

A2: T is complete ; :: thesis: for g being Function of S,T st g is infs-preserving holds

( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving )

reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;

let g be Function of S,T; :: thesis: ( g is infs-preserving implies ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) )

assume g is infs-preserving ; :: thesis: ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-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 & LowerAdj g9 is monotone ) by WAYBEL_1:8;

hence ( LowerAdj g is monotone & LowerAdj g is lower_adjoint & LowerAdj g is sups-preserving ) ; :: thesis: verum

Lm2: now :: thesis: for S, T being LATTICE st S is complete & T is complete holds

for g being Function of S,T st g is sups-preserving holds

( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving )

for g being Function of S,T st g is sups-preserving holds

( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving )

let S, T be LATTICE; :: thesis: ( S is complete & T is complete implies for g being Function of S,T st g is sups-preserving holds

( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) )

assume that

A1: S is complete and

A2: T is complete ; :: thesis: for g being Function of S,T st g is sups-preserving holds

( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving )

reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;

let g be Function of S,T; :: thesis: ( g is sups-preserving implies ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) )

assume g is sups-preserving ; :: thesis: ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-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 & UpperAdj g9 is monotone ) by WAYBEL_1:8;

hence ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) ; :: thesis: verum

end;
( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) )

assume that

A1: S is complete and

A2: T is complete ; :: thesis: for g being Function of S,T st g is sups-preserving holds

( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving )

reconsider S9 = S, T9 = T as complete LATTICE by A1, A2;

let g be Function of S,T; :: thesis: ( g is sups-preserving implies ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) )

assume g is sups-preserving ; :: thesis: ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-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 & UpperAdj g9 is monotone ) by WAYBEL_1:8;

hence ( UpperAdj g is monotone & UpperAdj g is upper_adjoint & UpperAdj g is infs-preserving ) ; :: thesis: verum

registration

let S, T be complete LATTICE;

let g be infs-preserving Function of S,T;

coherence

LowerAdj g is lower_adjoint by Lm1;

end;
let g be infs-preserving Function of S,T;

coherence

LowerAdj g is lower_adjoint by Lm1;

registration

let S, T be complete LATTICE;

let d be sups-preserving Function of T,S;

coherence

UpperAdj d is upper_adjoint by Lm2;

end;
let d be sups-preserving Function of T,S;

coherence

UpperAdj d is upper_adjoint by Lm2;

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))

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))

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;

coherence

f is Function of (S opp),(T opp) ;

end;
let f be Function of the carrier of S, the carrier of T;

coherence

f is Function of (S opp),(T opp) ;

:: deftheorem defines opp WAYBEL34:def 3 :

for S, T being RelStr

for f being Function of the carrier of S, the carrier of T holds f opp = f;

for S, T being RelStr

for f being Function of the carrier of S, the carrier of T holds f opp = f;

registration

let S, T be complete LATTICE;

let g be infs-preserving Function of S,T;

coherence

g opp is lower_adjoint

end;
let g be infs-preserving Function of S,T;

coherence

g opp is lower_adjoint

proof end;

registration

let S, T be complete LATTICE;

let d be sups-preserving Function of S,T;

coherence

d opp is upper_adjoint

end;
let d be sups-preserving Function of S,T;

coherence

d opp is upper_adjoint

proof 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)

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

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

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)

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)

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

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

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 object 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 )

for a, b, f being object 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_{1}[ LATTICE] means $1 is complete ;

defpred S_{2}[ LATTICE, LATTICE, Function of $1,$2] means $3 is infs-preserving ;

given w being Element of W such that A1: not w is empty ;

ex b_{1} being strict lattice-wise category st

( ( for x being LATTICE holds

( x is Object of b_{1} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{1}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) )

for b_{1}, b_{2} being strict lattice-wise category st ( for x being LATTICE holds

( x is Object of b_{1} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{1}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) & ( for x being LATTICE holds

( x is Object of b_{2} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{2}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) holds

b_{1} = b_{2}

end;
defpred S

defpred S

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 ( ( 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 ) ) );

ex b

( ( for x being LATTICE holds

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) )

proof end;

uniqueness for b

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) & ( for x being LATTICE holds

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) holds

b

proof end;

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

for W being non empty set st not for w being Element of W holds w is empty holds

for b_{2} being strict lattice-wise category holds

( b_{2} = W -INF_category iff ( ( for x being LATTICE holds

( x is Object of b_{2} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{2}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) ) );

for W being non empty set st not for w being Element of W holds w is empty holds

for b

( b

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is infs-preserving ) ) ) );

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_{1}[ LATTICE] means $1 is complete ;

defpred S_{2}[ LATTICE, LATTICE, Function of $1,$2] means $3 is sups-preserving ;

given w being Element of W such that A1: not w is empty ;

ex b_{1} being strict lattice-wise category st

( ( for x being LATTICE holds

( x is Object of b_{1} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{1}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) )

for b_{1}, b_{2} being strict lattice-wise category st ( for x being LATTICE holds

( x is Object of b_{1} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{1}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) & ( for x being LATTICE holds

( x is Object of b_{2} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{2}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) holds

b_{1} = b_{2}

end;
defpred S

defpred S

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 ( ( 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 ) ) );

ex b

( ( for x being LATTICE holds

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) )

proof end;

uniqueness for b

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) & ( for x being LATTICE holds

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) holds

b

proof end;

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

for W being non empty set st not for w being Element of W holds w is empty holds

for b_{2} being strict lattice-wise category holds

( b_{2} = W -SUP_category iff ( ( for x being LATTICE holds

( x is Object of b_{2} iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b_{2}

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) ) );

for W being non empty set st not for w being Element of W holds w is empty holds

for b

( b

( x is Object of b

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff f is sups-preserving ) ) ) );

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 ;

coherence

W -INF_category is with_complete_lattices

W -SUP_category is with_complete_lattices

end;
coherence

W -INF_category is with_complete_lattices

proof end;

coherence W -SUP_category is with_complete_lattices

proof 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 ) )

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) )

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 ) )

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) )

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_{1}( LATTICE) -> LATTICE = $1;

deffunc H_{2}( LATTICE, LATTICE, Function of $1,$2) -> Function of $2,$1 = LowerAdj $3;

defpred S_{1}[ LATTICE, LATTICE, Function of $1,$2] means ( $1 is complete & $2 is complete & $3 is infs-preserving );

defpred S_{2}[ 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_{1}[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_{2}[a,b,f] ) )
by Lm4;

A3: for a being LATTICE st a in the carrier of (W -INF_category) holds

H_{1}(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_{1}[a,b,f] holds

( H_{2}(a,b,f) is Function of H_{1}(b),H_{1}(a) & S_{2}[H_{1}(b),H_{1}(a),H_{2}(a,b,f)] )
;

for f being Function of a,b

for g being Function of b,c st S_{1}[a,b,f] & S_{1}[b,c,g] holds

H_{2}(a,c,g * f) = H_{2}(a,b,f) * H_{2}(b,c,g)
by Th8;

ex b_{1} being strict contravariant Functor of W -INF_category ,W -SUP_category st

( ( for a being Object of (W -INF_category) holds b_{1} . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{1} . f = LowerAdj (@ f) ) )

for b_{1}, b_{2} being strict contravariant Functor of W -INF_category ,W -SUP_category st ( for a being Object of (W -INF_category) holds b_{1} . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{1} . f = LowerAdj (@ f) ) & ( for a being Object of (W -INF_category) holds b_{2} . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{2} . f = LowerAdj (@ f) ) holds

b_{1} = b_{2}
_{3}( 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_{1}(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_{2}[a,b,f] holds

( H_{3}(a,b,f) is Function of H_{1}(b),H_{1}(a) & S_{1}[H_{1}(b),H_{1}(a),H_{3}(a,b,f)] )
;

for f being Function of a,b

for g being Function of b,c st S_{2}[a,b,f] & S_{2}[b,c,g] holds

H_{3}(a,c,g * f) = H_{3}(a,b,f) * H_{3}(b,c,g)
by Th9;

ex b_{1} being strict contravariant Functor of W -SUP_category ,W -INF_category st

( ( for a being Object of (W -SUP_category) holds b_{1} . a = latt a ) & ( for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{1} . f = UpperAdj (@ f) ) )

for b_{1}, b_{2} being strict contravariant Functor of W -SUP_category ,W -INF_category st ( for a being Object of (W -SUP_category) holds b_{1} . a = latt a ) & ( for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{1} . f = UpperAdj (@ f) ) & ( for a being Object of (W -SUP_category) holds b_{2} . a = latt a ) & ( for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{2} . f = UpperAdj (@ f) ) holds

b_{1} = b_{2}

end;
set A = W -INF_category ;

set B = W -SUP_category ;

deffunc H

deffunc H

defpred S

defpred S

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

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

A3: for a being LATTICE st a in the carrier of (W -INF_category) holds

H

A4: for a, b being LATTICE

for f being Function of a,b st S

( H

A5: now :: thesis: for a being LATTICE st a in the carrier of (W -INF_category) holds

H_{2}(a,a, id a) = id H_{1}(a)

A6:
for a, b, c being LATTICEH

let a be LATTICE; :: thesis: ( a in the carrier of (W -INF_category) implies H_{2}(a,a, id a) = id H_{1}(a) )

assume a in the carrier of (W -INF_category) ; :: thesis: H_{2}(a,a, id a) = id H_{1}(a)

then a is complete by YELLOW21:def 5;

hence H_{2}(a,a, id a) = id H_{1}(a)
by Th7; :: thesis: verum

end;
assume a in the carrier of (W -INF_category) ; :: thesis: H

then a is complete by YELLOW21:def 5;

hence H

for f being Function of a,b

for g being Function of b,c st S

H

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 ( ( 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) ) );

ex b

( ( for a being Object of (W -INF_category) holds b

for f being Morphism of a,b holds b

proof end;

uniqueness for b

for f being Morphism of a,b holds b

for f being Morphism of a,b holds b

b

proof end;

deffunc HA13: for a being LATTICE st a in the carrier of (W -SUP_category) holds

H

A14: for a, b being LATTICE

for f being Function of a,b st S

( H

A15: now :: thesis: for a being LATTICE st a in the carrier of (W -SUP_category) holds

H_{3}(a,a, id a) = id H_{1}(a)

A16:
for a, b, c being LATTICEH

let a be LATTICE; :: thesis: ( a in the carrier of (W -SUP_category) implies H_{3}(a,a, id a) = id H_{1}(a) )

assume a in the carrier of (W -SUP_category) ; :: thesis: H_{3}(a,a, id a) = id H_{1}(a)

then a is complete by YELLOW21:def 5;

hence H_{3}(a,a, id a) = id H_{1}(a)
by Th7; :: thesis: verum

end;
assume a in the carrier of (W -SUP_category) ; :: thesis: H

then a is complete by YELLOW21:def 5;

hence H

for f being Function of a,b

for g being Function of b,c st S

H

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 ( ( 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) ) );

ex b

( ( for a being Object of (W -SUP_category) holds b

for f being Morphism of a,b holds b

proof end;

uniqueness for b

for f being Morphism of a,b holds b

for f being Morphism of a,b holds b

b

proof end;

:: deftheorem Def6 defines LowerAdj WAYBEL34:def 6 :

for W being with_non-empty_element set

for b_{2} being strict contravariant Functor of W -INF_category ,W -SUP_category holds

( b_{2} = W LowerAdj iff ( ( for a being Object of (W -INF_category) holds b_{2} . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{2} . f = LowerAdj (@ f) ) ) );

for W being with_non-empty_element set

for b

( b

for f being Morphism of a,b holds b

:: deftheorem Def7 defines UpperAdj WAYBEL34:def 7 :

for W being with_non-empty_element set

for b_{2} being strict contravariant Functor of W -SUP_category ,W -INF_category holds

( b_{2} = W UpperAdj iff ( ( for a being Object of (W -SUP_category) holds b_{2} . a = latt a ) & ( for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds

for f being Morphism of a,b holds b_{2} . f = UpperAdj (@ f) ) ) );

for W being with_non-empty_element set

for b

( b

for f being Morphism of a,b holds b

registration

let W be with_non-empty_element set ;

coherence

W LowerAdj is bijective

W UpperAdj is bijective

end;
coherence

W LowerAdj is bijective

proof end;

coherence W UpperAdj is bijective

proof end;

theorem Th18: :: WAYBEL34:18

for W being with_non-empty_element set holds

( (W LowerAdj) " = W UpperAdj & (W UpperAdj) " = W LowerAdj )

( (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) )

( (W LowerAdj) * (W UpperAdj) = id (W -SUP_category) & (W UpperAdj) * (W LowerAdj) = id (W -INF_category) )

proof end;

::<section2>Scott continuous maps and continuous lattices</section2>

theorem Th21: :: WAYBEL34:21

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 )

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;

end;
let f be Function of S,T;

attr f is waybelow-preserving means :: WAYBEL34:def 8

for x, y being Element of S st x << y holds

f . x << f . y;

for x, y being Element of S st x << y holds

f . x << f . y;

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

for S, T being non empty reflexive RelStr

for f being Function of S,T holds

( f is waybelow-preserving iff for x, y being Element of S st x << y holds

f . x << f . y );

for S, T being non empty reflexive RelStr

for f being Function of S,T holds

( f is waybelow-preserving iff for x, y being Element of S st x << y holds

f . x << f . y );

theorem Th22: :: WAYBEL34:22

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

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

LowerAdj g is waybelow-preserving

proof end;

theorem Th23: :: WAYBEL34:23

for S being complete LATTICE

for T being continuous complete LATTICE

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

g is directed-sups-preserving

for T being continuous complete 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;

end;
let f be Function of S,T;

attr f is relatively_open means :: WAYBEL34:def 9

for V being open Subset of S holds f .: V is open Subset of (T | (rng f));

for V being open Subset of S holds f .: V is open Subset of (T | (rng f));

:: deftheorem defines relatively_open WAYBEL34:def 9 :

for S, T being TopSpace

for f being Function of S,T holds

( f is relatively_open iff for V being open Subset of S holds f .: V is open Subset of (T | (rng f)) );

for S, T being TopSpace

for f being Function of S,T holds

( f is relatively_open iff for V being open Subset of S holds f .: V is open Subset of (T | (rng f)) );

theorem :: WAYBEL34:24

for X, Y being non empty TopSpace

for d being Function of X,Y holds

( d is relatively_open iff corestr d is open )

for d being Function of X,Y holds

( d is relatively_open iff corestr d is open )

proof end;

theorem Th25: :: WAYBEL34:25

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))

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 Th26: :: WAYBEL34:26

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

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;

coherence

Image f is complete by YELLOW_2:34;

end;
let f be sups-preserving Function of X,Y;

coherence

Image f is complete by YELLOW_2:34;

theorem :: 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 Z being Scott TopAugmentation of Image (LowerAdj g)

for d being Function of X,Y

for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds

d9 is open

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 d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds

d9 is open

proof end;

theorem Th28: :: WAYBEL34:28

for S, T being complete LATTICE

for g being infs-preserving Function of S,T st g is V7() 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 )

for g being infs-preserving Function of S,T st g is V7() 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;

coherence

Image f is complete by WAYBEL_1:54;

end;
let f be projection Function of X,X;

coherence

Image f is complete by WAYBEL_1:54;

theorem Th29: :: WAYBEL34:29

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 )

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 Th30: :: WAYBEL34:30

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 )

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:31

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 )

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 Th32: :: WAYBEL34:32

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

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:33

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 )

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:34

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

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 Th35: :: WAYBEL34:35

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 )

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 Th36: :: WAYBEL34:36

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 )

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:37

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 )

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:38

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

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:39

for L being continuous complete LATTICE

for c being closure Function of L,L st corestr c is waybelow-preserving holds

Image c is directed-sups-inheriting

for c being closure Function of L,L st corestr c is waybelow-preserving holds

Image c is directed-sups-inheriting

proof end;

::<section3>Duality of subcategories of {\it INF} and {\it SUP}</section3>

definition

let W be non empty set ;

set A = W -INF_category ;

defpred S_{1}[ set ] means verum;

defpred S_{2}[ 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_{1}[a]
;

A2: for a, b, c being Object of (W -INF_category) st S_{1}[a] & S_{1}[b] & S_{1}[c] & <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c st S_{2}[a,b,f] & S_{2}[b,c,g] holds

S_{2}[a,c,g * f]
_{1}[a] holds

S_{2}[a,a, idm a]

ex b_{1} being non empty strict subcategory of W -INF_category st

( ( for a being Object of (W -INF_category) holds a is Object of b_{1} ) & ( for a, b being Object of (W -INF_category)

for a9, b9 being Object of b_{1} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) )

uniqueness

for b_{1}, b_{2} being non empty strict subcategory of W -INF_category st ( for a being Object of (W -INF_category) holds a is Object of b_{1} ) & ( for a, b being Object of (W -INF_category)

for a9, b9 being Object of b_{1} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) & ( for a being Object of (W -INF_category) holds a is Object of b_{2} ) & ( for a, b being Object of (W -INF_category)

for a9, b9 being Object of b_{2} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) holds

b_{1} = b_{2};

end;
set A = W -INF_category ;

defpred S

defpred S

A1: ex a being Object of (W -INF_category) st S

A2: for a, b, c being Object of (W -INF_category) st S

for f being Morphism of a,b

for g being Morphism of b,c st S

S

proof end;

A8:
for a being Object of (W -INF_category) st SS

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 a9, b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) );

existence ( ( 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^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) );

ex b

( ( for a being Object of (W -INF_category) holds a is Object of b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) )

proof end;

correctness uniqueness

for b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) & ( for a being Object of (W -INF_category) holds a is Object of b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) holds

b

proof end;

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

for W being non empty set

for b_{2} being non empty strict subcategory of W -INF_category holds

( b_{2} = W -INF(SC)_category iff ( ( for a being Object of (W -INF_category) holds a is Object of b_{2} ) & ( for a, b being Object of (W -INF_category)

for a9, b9 being Object of b_{2} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) ) );

for W being non empty set

for b

( b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) ) );

definition

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 S_{1}[ set ] means verum;

defpred S_{2}[ 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_{1}[a]
;

A3: for a, b, c being Object of (W -SUP_category) st S_{1}[a] & S_{1}[b] & S_{1}[c] & <^a,b^> <> {} & <^b,c^> <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c st S_{2}[a,b,f] & S_{2}[b,c,g] holds

S_{2}[a,c,g * f]
_{1}[a] holds

S_{2}[a,a, idm a]

ex b_{1} being non empty strict subcategory of W -SUP_category st

( ( for a being Object of (W -SUP_category) holds a is Object of b_{1} ) & ( for a, b being Object of (W -SUP_category)

for a9, b9 being Object of b_{1} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) )

uniqueness

for b_{1}, b_{2} being non empty strict subcategory of W -SUP_category st ( for a being Object of (W -SUP_category) holds a is Object of b_{1} ) & ( for a, b being Object of (W -SUP_category)

for a9, b9 being Object of b_{1} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) & ( for a being Object of (W -SUP_category) holds a is Object of b_{2} ) & ( for a, b being Object of (W -SUP_category)

for a9, b9 being Object of b_{2} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) holds

b_{1} = b_{2};

end;
A1: ex w being non empty set st w in W by SETFAM_1:def 10;

set A = W -SUP_category ;

defpred S

defpred S

A2: ex a being Object of (W -SUP_category) st S

A3: for a, b, c being Object of (W -SUP_category) st S

for f being Morphism of a,b

for g being Morphism of b,c st S

S

proof end;

A12:
for a being Object of (W -SUP_category) st SS

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 a9, b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) );

existence ( ( 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^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) );

ex b

( ( for a being Object of (W -SUP_category) holds a is Object of b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) )

proof end;

correctness uniqueness

for b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) & ( for a being Object of (W -SUP_category) holds a is Object of b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) holds

b

proof end;

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

for W being with_non-empty_element set

for b_{2} being non empty strict subcategory of W -SUP_category holds

( b_{2} = W -SUP(SO)_category iff ( ( for a being Object of (W -SUP_category) holds a is Object of b_{2} ) & ( for a, b being Object of (W -SUP_category)

for a9, b9 being Object of b_{2} st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) ) );

for W being with_non-empty_element set

for b

( b

for a9, b9 being Object of b

for f being Morphism of a,b holds

( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) ) );

theorem Th40: :: WAYBEL34:40

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 )

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 Th41: :: WAYBEL34:41

for S being non empty RelStr

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

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

proof end;

theorem Th42: :: WAYBEL34:42

for S being non empty RelStr

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

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 ;

coherence

( S --> (Top T) is directed-sups-preserving & S --> (Top T) is infs-preserving ) by Th40, Th42;

end;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;

coherence

( S --> (Top T) is directed-sups-preserving & S --> (Top T) is infs-preserving ) by Th40, Th42;

registration

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric lower-bounded RelStr ;

coherence

( S --> (Bottom T) is filtered-infs-preserving & S --> (Bottom T) is sups-preserving ) by Th40, Th41;

end;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;

coherence

( S --> (Bottom T) is filtered-infs-preserving & S --> (Bottom T) is sups-preserving ) by Th40, Th41;

registration

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric upper-bounded RelStr ;

ex b_{1} being Function of S,T st

( b_{1} is directed-sups-preserving & b_{1} is infs-preserving )

end;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;

cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total infs-preserving directed-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

( b

proof end;

registration

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric lower-bounded RelStr ;

ex b_{1} being Function of S,T st

( b_{1} is filtered-infs-preserving & b_{1} is sups-preserving )

end;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;

cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving filtered-infs-preserving for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

( b

proof end;

theorem Th43: :: WAYBEL34:43

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 ) )

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 Th44: :: WAYBEL34:44

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) )

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:45

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 ) )

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 Th46: :: WAYBEL34:46

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 ) )

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:47

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_{1}[ 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 well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

ex b_{1} being non empty strict full subcategory of W -INF(SC)_category st

for a being Object of (W -INF(SC)_category) holds

( a is Object of b_{1} iff latt a is continuous )

uniqueness

for b_{1}, b_{2} being non empty strict full subcategory of W -INF(SC)_category st ( for a being Object of (W -INF(SC)_category) holds

( a is Object of b_{1} iff latt a is continuous ) ) & ( for a being Object of (W -INF(SC)_category) holds

( a is Object of b_{2} iff latt a is continuous ) ) holds

b_{1} = b_{2};

end;
defpred S

consider a being non empty set such that

A1: a in W by SETFAM_1:def 10;

set r = the well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

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 for a being Object of (W -INF(SC)_category) holds

( a is Object of it iff latt a is continuous );

ex b

for a being Object of (W -INF(SC)_category) holds

( a is Object of b

proof end;

correctness uniqueness

for b

( a is Object of b

( a is Object of b

b

proof end;

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

for W being with_non-empty_element set

for b_{2} being non empty strict full subcategory of W -INF(SC)_category holds

( b_{2} = W -CL_category iff for a being Object of (W -INF(SC)_category) holds

( a is Object of b_{2} iff latt a is continuous ) );

for W being with_non-empty_element set

for b

( b

( a is Object of b

registration
end;

theorem Th48: :: WAYBEL34:48

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 ) )

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 Th49: :: WAYBEL34:49

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) )

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_{1}[ 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 well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

ex b_{1} being non empty strict full subcategory of W -SUP(SO)_category st

for a being Object of (W -SUP(SO)_category) holds

( a is Object of b_{1} iff latt a is continuous )

uniqueness

for b_{1}, b_{2} being non empty strict full subcategory of W -SUP(SO)_category st ( for a being Object of (W -SUP(SO)_category) holds

( a is Object of b_{1} iff latt a is continuous ) ) & ( for a being Object of (W -SUP(SO)_category) holds

( a is Object of b_{2} iff latt a is continuous ) ) holds

b_{1} = b_{2};

end;
defpred S

consider a being non empty set such that

A1: a in W by SETFAM_1:def 10;

set r = the well-ordering upper-bounded Order of a;

set b = RelStr(# a, the well-ordering upper-bounded Order of a #);

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 for a being Object of (W -SUP(SO)_category) holds

( a is Object of it iff latt a is continuous );

ex b

for a being Object of (W -SUP(SO)_category) holds

( a is Object of b

proof end;

correctness uniqueness

for b

( a is Object of b

( a is Object of b

b

proof end;

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

for W being with_non-empty_element set

for b_{2} being non empty strict full subcategory of W -SUP(SO)_category holds

( b_{2} = W -CL-opp_category iff for a being Object of (W -SUP(SO)_category) holds

( a is Object of b_{2} iff latt a is continuous ) );

for W being with_non-empty_element set

for b

( b

( a is Object of b

theorem Th50: :: WAYBEL34:50

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 ) )

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 Th51: :: WAYBEL34:51

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 ) )

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;

:: 1.10. THEOREM, p. 182

theorem Th52: :: WAYBEL34:52

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:53

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 Th54: :: WAYBEL34:54

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:55

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

proof end;

::<section4>Compact preserving maps and sup-semilattices morphisms</section4>

definition

let S, T be non empty reflexive RelStr ;

let f be Function of S,T;

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

for s being Element of S st s is compact holds

f . s is compact ;

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

for S, T being non empty reflexive RelStr

for f being Function of S,T holds

( f is compact-preserving iff for s being Element of S st s is compact holds

f . s is compact );

for S, T being non empty reflexive RelStr

for f being Function of S,T holds

( f is compact-preserving iff for s being Element of S st s is compact holds

f . s is compact );

theorem Th56: :: WAYBEL34:56

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

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

d is compact-preserving

proof end;

theorem Th57: :: WAYBEL34:57

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

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 Th58: :: WAYBEL34:58

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

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;

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

for X being finite Subset of S holds f preserves_sup_of X;

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

for S, T being non empty RelStr

for f being Function of S,T holds

( f is finite-sups-preserving iff for X being finite Subset of S holds f preserves_sup_of X );

for S, T being non empty RelStr

for f being Function of S,T holds

( f is finite-sups-preserving iff for X being finite Subset of S holds f preserves_sup_of X );

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

for S, T being non empty RelStr

for f being Function of S,T holds

( f is bottom-preserving iff f preserves_sup_of {} S );

for S, T being non empty RelStr

for f being Function of S,T holds

( f is bottom-preserving iff f preserves_sup_of {} S );

theorem :: WAYBEL34:59

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

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;

compatibility

( f is bottom-preserving iff f . (Bottom S) = Bottom T )

end;
let f be Function of S,T;

compatibility

( f is bottom-preserving iff f . (Bottom S) = Bottom T )

proof end;

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

for S, T being non empty antisymmetric lower-bounded RelStr

for f being Function of S,T holds

( f is bottom-preserving iff f . (Bottom S) = Bottom T );

for S, T being non empty antisymmetric lower-bounded RelStr

for f being Function of S,T holds

( f is bottom-preserving iff f . (Bottom S) = Bottom T );

definition

let L be non empty RelStr ;

let S be SubRelStr of L;

end;
let S be SubRelStr of L;

attr S is finite-sups-inheriting means :: WAYBEL34:def 18

for X being finite Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S;

for X being finite Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S;

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

for L being non empty RelStr

for S being SubRelStr of L holds

( S is finite-sups-inheriting iff for X being finite Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S );

for L being non empty RelStr

for S being SubRelStr of L holds

( S is finite-sups-inheriting iff for X being finite Subset of S st ex_sup_of X,L holds

"\/" (X,L) in the carrier of S );

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

for L being non empty RelStr

for S being SubRelStr of L holds

( S is bottom-inheriting iff Bottom L in the carrier of S );

for L being non empty RelStr

for S being SubRelStr of L holds

( S is bottom-inheriting iff Bottom L in the carrier of S );

registration

let S, T be non empty RelStr ;

for b_{1} being Function of S,T st b_{1} is sups-preserving holds

b_{1} is bottom-preserving
;

end;
cluster Function-like quasi_total sups-preserving -> bottom-preserving for Element of bool [: the carrier of S, the carrier of T:];

coherence for b

b

registration

let L be non empty antisymmetric lower-bounded RelStr ;

coherence

for b_{1} being SubRelStr of L st b_{1} is finite-sups-inheriting holds

( b_{1} is bottom-inheriting & b_{1} is join-inheriting )

end;
coherence

for b

( b

proof end;

registration

let L be non empty RelStr ;

coherence

for b_{1} being SubRelStr of L st b_{1} is sups-inheriting holds

b_{1} is finite-sups-inheriting
;

end;
coherence

for b

b

registration

let S, T be non empty lower-bounded Poset;

ex b_{1} being Function of S,T st b_{1} is sups-preserving

end;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

proof end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;

coherence

for b_{1} being full SubRelStr of L st b_{1} is bottom-inheriting holds

( not b_{1} is empty & b_{1} is lower-bounded )

end;
coherence

for b

( not b

proof end;

registration

let L be non empty antisymmetric lower-bounded RelStr ;

existence

ex b_{1} being SubRelStr of L st

( not b_{1} is empty & b_{1} is sups-inheriting & b_{1} is finite-sups-inheriting & b_{1} is bottom-inheriting & b_{1} is full )

end;
existence

ex b

( not b

proof end;

theorem Th60: :: WAYBEL34:60

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

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;

coherence

for b_{1} being full SubRelStr of L st b_{1} is bottom-inheriting & b_{1} is join-inheriting holds

b_{1} is finite-sups-inheriting

end;
coherence

for b

b

proof end;

theorem :: WAYBEL34:61

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

for f being Function of S,T st f is finite-sups-preserving holds

( f is join-preserving & f is bottom-preserving ) ;

theorem Th62: :: WAYBEL34:62

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

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 ;

for b_{1} being Function of S,T st b_{1} is sups-preserving holds

b_{1} is finite-sups-preserving
;

for b_{1} being Function of S,T st b_{1} is finite-sups-preserving holds

( b_{1} is join-preserving & b_{1} is bottom-preserving )
;

end;
cluster Function-like quasi_total sups-preserving -> finite-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];

coherence for b

b

cluster Function-like quasi_total finite-sups-preserving -> join-preserving bottom-preserving for Element of bool [: the carrier of S, the carrier of T:];

coherence for b

( b

registration

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric lower-bounded RelStr ;

ex b_{1} being Function of S,T st

( b_{1} is sups-preserving & b_{1} is finite-sups-preserving )

end;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;

cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V22( the carrier of S) quasi_total sups-preserving finite-sups-preserving for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

( b

proof end;

registration
end;

theorem Th63: :: WAYBEL34:63

for S being RelStr

for T being non empty RelStr

for 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

for T being non empty RelStr

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

theorem Th64: :: WAYBEL34:64

for S, T being LATTICE

for f being join-preserving Function of S,T

for S9 being non empty full join-inheriting SubRelStr of S

for T9 being non empty full join-inheriting SubRelStr of T

for g being Function of S9,T9 st g = f | the carrier of S9 holds

g is join-preserving

for f being join-preserving Function of S,T

for S9 being non empty full join-inheriting SubRelStr of S

for T9 being non empty full join-inheriting SubRelStr of T

for g being Function of S9,T9 st g = f | the carrier of S9 holds

g is join-preserving

proof end;

theorem Th65: :: WAYBEL34:65

for S, T being lower-bounded LATTICE

for f being finite-sups-preserving Function of S,T

for S9 being non empty full finite-sups-inheriting SubRelStr of S

for T9 being non empty full finite-sups-inheriting SubRelStr of T

for g being Function of S9,T9 st g = f | the carrier of S9 holds

g is finite-sups-preserving

for f being finite-sups-preserving Function of S,T

for S9 being non empty full finite-sups-inheriting SubRelStr of S

for T9 being non empty full finite-sups-inheriting SubRelStr of T

for g being Function of S9,T9 st g = f | the carrier of S9 holds

g is finite-sups-preserving

proof end;

registration
end;

theorem Th66: :: WAYBEL34:66

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) )

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:67

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) )

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;