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 10;
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 for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = glet a,
b be
Object of
(W -INF_category);
( <^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^> <> {}
;
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;
( H2(a,b,f) = H2(a,b,g) implies f = g )A7:
@ f = f
by A6, YELLOW21:def 7;
A8:
@ g = g
by A6, YELLOW21:def 7;
A9:
latt a is
complete
;
A10:
latt b is
complete
;
A11:
@ f is
infs-preserving
by A1, A6, A7, Def4;
A12:
@ g is
infs-preserving
by A1, A6, A8, Def4;
assume
H2(
a,
b,
f)
= H2(
a,
b,
g)
;
f = ghence f =
UpperAdj (LowerAdj (@ g))
by A7, A9, A10, A11, Th10
.=
g
by A8, A9, A10, A12, Th10
;
verum end;
A13:
now for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
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 a,
b be
Object of
(W -SUP_category);
( <^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 A14:
<^a,b^> <> {}
;
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;
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) )A15:
(
latt a is
strict &
latt a is
complete )
by A1, Def5;
A16:
the
carrier of
(latt a) in W
by A1, Def5;
A17:
(
latt b is
strict &
latt b is
complete )
by A1, Def5;
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 A15, A16, A17, Def4;
take c =
c;
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;
ex g being Morphism of c,d st
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )A18:
latt c = c
;
A19:
latt d = d
;
A20:
f = @ f
by A14, YELLOW21:def 7;
then A21:
@ f is
sups-preserving
by A1, A14, Def5;
then A22:
(
UpperAdj (@ f) is
monotone &
UpperAdj (@ f) is
infs-preserving )
by A18, A19;
A23:
UpperAdj (@ f) in <^c,d^>
by A1, A21, Def4;
reconsider g =
UpperAdj (@ f) as
Morphism of
c,
d by A1, A21, Def4;
take g =
g;
( b = H1(c) & a = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )thus
(
b = H1(
c) &
a = H1(
d) &
<^c,d^> <> {} )
by A1, A22, Def4;
f = H2(c,d,g)
g = @ g
by A23, YELLOW21:def 7;
hence
f = H2(
c,
d,
g)
by A20, A21, Th11;
verum end;
thus
W LowerAdj is bijective
from YELLOW18:sch 12(A2, A3, A4, A5, A13); verum