let W be with_non-empty_element set ; :: thesis: W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj
set A1 = W -INF_category ;
set B1 = W -INF(SC)_category ;
set B2 = W -SUP(SO)_category ;
set F = W LowerAdj ;
A1:
ex a being non empty set st a in W
by SETFAM_1:def 11;
A2:
W LowerAdj is bijective
;
A3:
for a being object of (W -INF_category ) holds
( a is object of (W -INF(SC)_category ) iff (W LowerAdj ) . a is object of (W -SUP(SO)_category ) )
by Def10, Def11;
A4:
now let a,
b be
object of
(W -INF_category );
:: thesis: ( <^a,b^> <> {} implies for a1, b1 being object of (W -INF(SC)_category ) st a1 = a & b1 = b holds
for a2, b2 being object of (W -SUP(SO)_category ) st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj ) . f in <^b2,a2^> ) )assume A5:
<^a,b^> <> {}
;
:: thesis: for a1, b1 being object of (W -INF(SC)_category ) st a1 = a & b1 = b holds
for a2, b2 being object of (W -SUP(SO)_category ) st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj ) . f in <^b2,a2^> )let a1,
b1 be
object of
(W -INF(SC)_category );
:: thesis: ( a1 = a & b1 = b implies for a2, b2 being object of (W -SUP(SO)_category ) st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj ) . f in <^b2,a2^> ) )assume A6:
(
a1 = a &
b1 = b )
;
:: thesis: for a2, b2 being object of (W -SUP(SO)_category ) st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj ) . f in <^b2,a2^> )let a2,
b2 be
object of
(W -SUP(SO)_category );
:: thesis: ( a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b implies for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj ) . f in <^b2,a2^> ) )assume A7:
(
a2 = (W LowerAdj ) . a &
b2 = (W LowerAdj ) . b )
;
:: thesis: for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj ) . f in <^b2,a2^> )let f be
Morphism of
a,
b;
:: thesis: ( f in <^a1,b1^> iff (W LowerAdj ) . f in <^b2,a2^> )A8:
<^((W LowerAdj ) . b),((W LowerAdj ) . a)^> <> {}
by A5, FUNCTOR0:def 20;
then A9:
(
@ f = f &
@ ((W LowerAdj ) . f) = (W LowerAdj ) . f &
latt a1 = a1 &
latt b1 = b1 &
latt a = a &
latt b = b &
latt a2 = a2 &
latt b2 = b2 )
by A5, YELLOW21:def 7;
then A10:
(
(W LowerAdj ) . a = latt a &
(W LowerAdj ) . b = latt b &
(W LowerAdj ) . f = LowerAdj (@ f) &
@ f is
infs-preserving )
by A1, A5, Def4, Def6;
reconsider g =
f as
infs-preserving Function of
(latt a1),
(latt b1) by A1, A5, A6, A9, Def4;
UpperAdj (LowerAdj g) = g
by Th10;
then
(
f in <^a1,b1^> iff
UpperAdj (LowerAdj g) is
directed-sups-preserving )
by A5, A6, A9, Def10;
hence
(
f in <^a1,b1^> iff
(W LowerAdj ) . f in <^b2,a2^> )
by A6, A7, A8, A9, A10, Def11;
:: thesis: verum end;
thus
W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj
from YELLOW20:sch 5(A2, A3, A4); :: thesis: verum