let W be with_non-empty_element set ; W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj
set A1 = W -INF_category ;
set A2 = W -SUP_category ;
reconsider B1 = W -CL_category as non empty subcategory of W -INF_category by ALTCAT_4:36;
reconsider B2 = W -CL-opp_category as non empty subcategory of W -SUP_category by ALTCAT_4:36;
set F = W LowerAdj ;
A1:
ex a being non empty set st a in W
by SETFAM_1:def 10;
A2:
for a being Object of (W -INF_category) holds
( a is Object of B1 iff (W LowerAdj) . a is Object of B2 )
A5:
now for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )let a,
b be
Object of
(W -INF_category);
( <^a,b^> <> {} implies for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )assume A6:
<^a,b^> <> {}
;
for a1, b1 being Object of B1 st a1 = a & b1 = b holds
for a2, b2 being Object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )let a1,
b1 be
Object of
B1;
( a1 = a & b1 = b implies for a2, b2 being Object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )assume that A7:
a1 = a
and A8:
b1 = b
;
for a2, b2 being Object of B2 st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )let a2,
b2 be
Object of
B2;
( a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b implies for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )assume that A9:
a2 = (W LowerAdj) . a
and A10:
b2 = (W LowerAdj) . b
;
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )let f be
Morphism of
a,
b;
( ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) & ( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> ) )A11:
@ f = f
by A6, YELLOW21:def 7;
A12:
(W LowerAdj) . a = latt a
by Def6;
A13:
(W LowerAdj) . b = latt b
by Def6;
A14:
(W LowerAdj) . f = LowerAdj (@ f)
by A6, Def6;
reconsider g =
f as
infs-preserving Function of
(latt a1),
(latt b1) by A1, A6, A7, A8, A11, Def4;
A15:
UpperAdj (LowerAdj g) = g
by Th10;
then
(
f in <^a1,b1^> iff
UpperAdj (LowerAdj g) is
directed-sups-preserving )
by Th49;
hence
(
f in <^a1,b1^> implies
(W LowerAdj) . f in <^b2,a2^> )
by A7, A8, A9, A10, A11, A12, A13, A14, Th51;
( (W LowerAdj) . f in <^b2,a2^> implies f in <^a1,b1^> )assume
(W LowerAdj) . f in <^b2,a2^>
;
f in <^a1,b1^>then
ex
g being
sups-preserving Function of
(latt b2),
(latt a2) st
(
(W LowerAdj) . f = g &
UpperAdj g is
directed-sups-preserving )
by Th51;
hence
f in <^a1,b1^>
by A7, A8, A9, A10, A11, A12, A13, A14, A15, Th49;
verum end;
B1,B2 are_anti-isomorphic_under W LowerAdj
by A2, A5, YELLOW20:57;
hence
W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj
; verum