let W be with_non-empty_element set ; ( (W LowerAdj) " = W UpperAdj & (W UpperAdj) " = W LowerAdj )
A1:
ex x being non empty set st x in W
by SETFAM_1:def 10;
set B = W -SUP_category ;
set F = W LowerAdj ;
set G = W UpperAdj ;
now for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = flet a,
b be
Object of
(W -SUP_category);
( <^a,b^> <> {} implies for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = f )assume A3:
<^a,b^> <> {}
;
for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = fthen A4:
<^((W UpperAdj) . b),((W UpperAdj) . a)^> <> {}
by FUNCTOR0:def 19;
let f be
Morphism of
a,
b;
(W LowerAdj) . ((W UpperAdj) . f) = fA5:
(W UpperAdj) . f = UpperAdj (@ f)
by A3, Def7;
A6:
@ f = f
by A3, YELLOW21:def 7;
A7:
@ ((W UpperAdj) . f) = (W UpperAdj) . f
by A4, YELLOW21:def 7;
A8:
(W UpperAdj) . a = latt a
by Def7;
A9:
(W UpperAdj) . b = latt b
by Def7;
A10:
@ f is
sups-preserving
by A1, A3, A6, Def5;
thus (W LowerAdj) . ((W UpperAdj) . f) =
LowerAdj (@ ((W UpperAdj) . f))
by A4, Def6
.=
f
by A5, A6, A7, A8, A9, A10, Th11
;
verum end;
hence
(W LowerAdj) " = W UpperAdj
by A2, YELLOW20:7; (W UpperAdj) " = W LowerAdj
set B = W -INF_category ;
set G = W LowerAdj ;
set F = W UpperAdj ;
now for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = flet a,
b be
Object of
(W -INF_category);
( <^a,b^> <> {} implies for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = f )assume A12:
<^a,b^> <> {}
;
for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = fthen A13:
<^((W LowerAdj) . b),((W LowerAdj) . a)^> <> {}
by FUNCTOR0:def 19;
let f be
Morphism of
a,
b;
(W UpperAdj) . ((W LowerAdj) . f) = fA14:
(W LowerAdj) . f = LowerAdj (@ f)
by A12, Def6;
A15:
@ f = f
by A12, YELLOW21:def 7;
A16:
@ ((W LowerAdj) . f) = (W LowerAdj) . f
by A13, YELLOW21:def 7;
A17:
(W LowerAdj) . a = latt a
by Def6;
A18:
(W LowerAdj) . b = latt b
by Def6;
A19:
@ f is
infs-preserving
by A1, A12, A15, Def4;
thus (W UpperAdj) . ((W LowerAdj) . f) =
UpperAdj (@ ((W LowerAdj) . f))
by A13, Def7
.=
f
by A14, A15, A16, A17, A18, A19, Th10
;
verum end;
hence
(W UpperAdj) " = W LowerAdj
by A11, YELLOW20:7; verum