set A = W -SUP_category ;
set B = W -INF_category ;
set F = W UpperAdj ;
A16:
ex x being non empty set st x in W
by SETFAM_1:def 11;
deffunc H1( object of (W -SUP_category )) -> RelStr = latt W;
deffunc H2( object of (W -SUP_category ), object of (W -SUP_category ), Morphism of W,c2) -> Function of (latt c2),(latt W) = UpperAdj (@ c3);
A17:
for a being object of (W -SUP_category ) holds (W UpperAdj ) . a = H1(a)
by Def7;
A18:
for a, b being object of (W -SUP_category ) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W UpperAdj ) . f = H2(a,b,f)
by Def7;
A19:
for a, b being object of (W -SUP_category ) st H1(a) = H1(b) holds
a = b
;
A20:
now let a,
b be
object of
(W -SUP_category );
:: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g )assume A21:
<^a,b^> <> {}
;
:: thesis: for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = glet f,
g be
Morphism of
a,
b;
:: thesis: ( H2(a,b,f) = H2(a,b,g) implies f = g )A22:
(
@ f = f &
@ g = g )
by A21, YELLOW21:def 7;
then A23:
(
latt a is
complete &
latt b is
complete &
@ f is
sups-preserving &
@ g is
sups-preserving )
by A16, A21, Def5;
assume
H2(
a,
b,
f)
= H2(
a,
b,
g)
;
:: thesis: f = ghence f =
LowerAdj (UpperAdj (@ g))
by A22, A23, Th11
.=
g
by A22, A23, Th11
;
:: thesis: verum end;
A24:
now let a,
b be
object of
(W -INF_category );
:: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of (W -SUP_category ) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) ) )assume A25:
<^a,b^> <> {}
;
:: thesis: for f being Morphism of a,b ex c, d being object of (W -SUP_category ) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )let f be
Morphism of
a,
b;
:: thesis: ex c, d being object of (W -SUP_category ) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
(
latt a is
strict &
latt a is
complete & the
carrier of
(latt a) in W &
latt b is
strict &
latt b is
complete & the
carrier of
(latt b) in W )
by A16, Def4;
then reconsider c =
latt b,
d =
latt a as
object of
(W -SUP_category ) by Def5;
take c =
c;
:: thesis: ex d being object of (W -SUP_category ) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )take d =
d;
:: thesis: ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )A26:
(
latt c = c &
latt d = d )
;
A27:
f = @ f
by A25, YELLOW21:def 7;
then A28:
@ f is
infs-preserving
by A16, A25, Def4;
then A29:
(
LowerAdj (@ f) is
monotone &
LowerAdj (@ f) is
sups-preserving )
by A26;
then A30:
LowerAdj (@ f) in <^c,d^>
by A16, Def5;
reconsider g =
LowerAdj (@ f) as
Morphism of
c,
d by A16, A29, Def5;
take g =
g;
:: thesis: ( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )thus
(
b = H1(
c) &
a = H1(
d) &
<^c,d^> <> {} )
by A16, A29, Def5;
:: thesis: f = H2(c,d,g)
g = @ g
by A30, YELLOW21:def 7;
hence
f = H2(
c,
d,
g)
by A27, A28, Th10;
:: thesis: verum end;
thus
W UpperAdj is bijective
from YELLOW18:sch 12(A17, A18, A19, A20, A24); :: thesis: verum