set A = W -INF_category ;
set B = W -SUP_category ;
set F = W LowerAdj ;
A1:
ex x being non empty set st x in W
by SETFAM_1:def 11;
deffunc H1( object of (W -INF_category )) -> RelStr = latt W;
deffunc H2( object of (W -INF_category ), object of (W -INF_category ), Morphism of W,c2) -> Function of (latt c2),(latt W) = LowerAdj (@ c3);
A2:
for a being object of (W -INF_category ) holds (W LowerAdj ) . a = H1(a)
by Def6;
A3:
for a, b being object of (W -INF_category ) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W LowerAdj ) . f = H2(a,b,f)
by Def6;
A4:
for a, b being object of (W -INF_category ) st H1(a) = H1(b) holds
a = b
;
A5:
now let a,
b be
object of
(W -INF_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 A6:
<^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 )A7:
(
@ f = f &
@ g = g )
by A6, YELLOW21:def 7;
then A8:
(
latt a is
complete &
latt b is
complete &
@ f is
infs-preserving &
@ g is
infs-preserving )
by A1, A6, Def4;
assume
H2(
a,
b,
f)
= H2(
a,
b,
g)
;
:: thesis: f = ghence f =
UpperAdj (LowerAdj (@ g))
by A7, A8, Th10
.=
g
by A7, A8, Th10
;
:: thesis: verum end;
A9:
now let a,
b be
object of
(W -SUP_category );
:: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of (W -INF_category ) ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) ) )assume A10:
<^a,b^> <> {}
;
:: thesis: for f being Morphism of a,b ex c, d being object of (W -INF_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 -INF_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 A1, Def5;
then reconsider c =
latt b,
d =
latt a as
object of
(W -INF_category ) by Def4;
take c =
c;
:: thesis: ex d being object of (W -INF_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) )A11:
(
latt c = c &
latt d = d )
;
A12:
f = @ f
by A10, YELLOW21:def 7;
then A13:
@ f is
sups-preserving
by A1, A10, Def5;
then A14:
(
UpperAdj (@ f) is
monotone &
UpperAdj (@ f) is
infs-preserving )
by A11;
then A15:
UpperAdj (@ f) in <^c,d^>
by A1, Def4;
reconsider g =
UpperAdj (@ f) as
Morphism of
c,
d by A1, A14, Def4;
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 A1, A14, Def4;
:: thesis: f = H2(c,d,g)
g = @ g
by A15, YELLOW21:def 7;
hence
f = H2(
c,
d,
g)
by A12, A13, Th11;
:: thesis: verum end;
thus
W LowerAdj is bijective
from YELLOW18:sch 12(A2, A3, A4, A5, A9); :: thesis: verum