environ
vocabularies HIDDEN, REWRITE1, WAYBEL_0, WAYBEL_1, FUNCT_1, XBOOLE_0, ORDERS_2, SEQM_3, SUBSET_1, XXREAL_0, RELAT_1, LATTICES, EQREL_1, ORDINAL2, STRUCT_0, ARYTM_0, ALTCAT_1, CAT_1, ZFMISC_1, YELLOW21, FILTER_0, WELLORD1, ORDERS_1, SETFAM_1, QC_LANG1, TARSKI, FUNCTOR0, FUNCT_2, WAYBEL11, YELLOW_9, RCOMP_1, CARD_FIL, YELLOW_0, RELAT_2, WAYBEL_3, LATTICE3, PRE_TOPC, GROUP_6, ALTCAT_2, FUNCOP_1, YELLOW20, YELLOW18, WAYBEL_8, FINSET_1, WAYBEL34;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, ORDERS_1, DOMAIN_1, FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, WELLORD1, ALTCAT_1, FUNCTOR0, ALTCAT_2, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, PRE_TOPC, T_0TOPSP, WAYBEL_3, WAYBEL_8, YELLOW_7, WAYBEL11, YELLOW_9, WAYBEL18, YELLOW18, YELLOW20, YELLOW21;
definitions TARSKI, PRE_TOPC, T_0TOPSP, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL11, FUNCTOR0, YELLOW21, XBOOLE_0;
theorems ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, ORDERS_2, ORDERS_3, TSEP_1, TARSKI, FUNCOP_1, ALTCAT_1, ALTCAT_2, ALTCAT_4, FUNCTOR0, FUNCTOR1, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_3, WAYBEL_6, YELLOW_7, WAYBEL_8, YELLOW_3, WAYBEL_9, YELLOW_9, WAYBEL11, WAYBEL15, WAYBEL17, WAYBEL18, WAYBEL20, WAYBEL21, YELLOW18, YELLOW20, YELLOW21, XBOOLE_0, XBOOLE_1, SETFAM_1, PARTFUN1;
schemes FINSET_1, YELLOW18, YELLOW20, YELLOW21;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0, ALTCAT_2, FUNCTOR0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_7, WAYBEL_8, WAYBEL10, WAYBEL11, FUNCTOR2, ALTCAT_4, LATTICE5, WAYBEL17, YELLOW_9, WAYBEL21, YELLOW18, YELLOW21, RELAT_1;
constructors HIDDEN, WELLORD1, BORSUK_1, T_0TOPSP, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL18, YELLOW18, YELLOW20, YELLOW21, WAYBEL20;
requirements HIDDEN, SUBSET, BOOLE;
equalities SUBSET_1, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW21, BINOP_1, STRUCT_0, RELAT_1;
expansions TARSKI, PRE_TOPC, T_0TOPSP, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL11, XBOOLE_0;
definition
let S,
T be
LATTICE;
let g be
Function of
S,
T;
assume that A1:
S is
complete
and A2:
g is
infs-preserving
;
A3:
g is
upper_adjoint
by A1, A2, WAYBEL_1:16;
uniqueness
for b1, b2 being Function of T,S st [g,b1] is Galois & [g,b2] is Galois holds
b1 = b2
existence
ex b1 being Function of T,S st [g,b1] is Galois
by A3;
end;
definition
let S,
T be
LATTICE;
let d be
Function of
T,
S;
assume that A1:
T is
complete
and A2:
d is
sups-preserving
;
A3:
d is
lower_adjoint
by A1, A2, WAYBEL_1:17;
existence
ex b1 being Function of S,T st [b1,d] is Galois
by A3;
correctness
uniqueness
for b1, b2 being Function of S,T st [b1,d] is Galois & [b2,d] is Galois holds
b1 = b2;
end;
definition
let W be non
empty set ;
defpred S1[
LATTICE]
means $1 is
complete ;
defpred S2[
LATTICE,
LATTICE,
Function of $1,$2]
means $3 is
infs-preserving ;
given w being
Element of
W such that A1:
not
w is
empty
;
existence
ex b1 being strict lattice-wise category st
( ( for x being LATTICE holds
( x is Object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) )
uniqueness
for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is Object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) & ( for x being LATTICE holds
( x is Object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is infs-preserving ) ) holds
b1 = b2
end;
Lm3:
for W being with_non-empty_element set
for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -INF_category) . (a,b) iff ( a in the carrier of (W -INF_category) & b in the carrier of (W -INF_category) & a is complete & b is complete & f is infs-preserving ) )
definition
let W be non
empty set ;
defpred S1[
LATTICE]
means $1 is
complete ;
defpred S2[
LATTICE,
LATTICE,
Function of $1,$2]
means $3 is
sups-preserving ;
given w being
Element of
W such that A1:
not
w is
empty
;
existence
ex b1 being strict lattice-wise category st
( ( for x being LATTICE holds
( x is Object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) )
uniqueness
for b1, b2 being strict lattice-wise category st ( for x being LATTICE holds
( x is Object of b1 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) & ( for x being LATTICE holds
( x is Object of b2 iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is sups-preserving ) ) holds
b1 = b2
end;
Lm4:
for W being with_non-empty_element set
for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category) . (a,b) iff ( a in the carrier of (W -SUP_category) & b in the carrier of (W -SUP_category) & a is complete & b is complete & f is sups-preserving ) )
definition
let W be
with_non-empty_element set ;
set A =
W -INF_category ;
set B =
W -SUP_category ;
deffunc H1(
LATTICE)
-> LATTICE = $1;
deffunc H2(
LATTICE,
LATTICE,
Function of $1,$2)
-> Function of $2,$1 =
LowerAdj $3;
defpred S1[
LATTICE,
LATTICE,
Function of $1,$2]
means ( $1 is
complete & $2 is
complete & $3 is
infs-preserving );
defpred S2[
LATTICE,
LATTICE,
Function of $1,$2]
means ( $1 is
complete & $2 is
complete & $3 is
sups-preserving );
A1:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
(W -INF_category) . (
a,
b) iff (
a in the
carrier of
(W -INF_category) &
b in the
carrier of
(W -INF_category) &
S1[
a,
b,
f] ) )
by Lm3;
A2:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
(W -SUP_category) . (
a,
b) iff (
a in the
carrier of
(W -SUP_category) &
b in the
carrier of
(W -SUP_category) &
S2[
a,
b,
f] ) )
by Lm4;
A3:
for
a being
LATTICE st
a in the
carrier of
(W -INF_category) holds
H1(
a)
in the
carrier of
(W -SUP_category)
by Th17;
A4:
for
a,
b being
LATTICE for
f being
Function of
a,
b st
S1[
a,
b,
f] holds
(
H2(
a,
b,
f) is
Function of
H1(
b),
H1(
a) &
S2[
H1(
b),
H1(
a),
H2(
a,
b,
f)] )
;
A6:
for
a,
b,
c being
LATTICE for
f being
Function of
a,
b for
g being
Function of
b,
c st
S1[
a,
b,
f] &
S1[
b,
c,
g] holds
H2(
a,
c,
g * f)
= H2(
a,
b,
f)
* H2(
b,
c,
g)
by Th8;
existence
ex b1 being strict contravariant Functor of W -INF_category ,W -SUP_category st
( ( for a being Object of (W -INF_category) holds b1 . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = LowerAdj (@ f) ) )
uniqueness
for b1, b2 being strict contravariant Functor of W -INF_category ,W -SUP_category st ( for a being Object of (W -INF_category) holds b1 . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = LowerAdj (@ f) ) & ( for a being Object of (W -INF_category) holds b2 . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = LowerAdj (@ f) ) holds
b1 = b2
deffunc H3(
LATTICE,
LATTICE,
Function of $1,$2)
-> Function of $2,$1 =
UpperAdj $3;
A13:
for
a being
LATTICE st
a in the
carrier of
(W -SUP_category) holds
H1(
a)
in the
carrier of
(W -INF_category)
by Th17;
A14:
for
a,
b being
LATTICE for
f being
Function of
a,
b st
S2[
a,
b,
f] holds
(
H3(
a,
b,
f) is
Function of
H1(
b),
H1(
a) &
S1[
H1(
b),
H1(
a),
H3(
a,
b,
f)] )
;
A16:
for
a,
b,
c being
LATTICE for
f being
Function of
a,
b for
g being
Function of
b,
c st
S2[
a,
b,
f] &
S2[
b,
c,
g] holds
H3(
a,
c,
g * f)
= H3(
a,
b,
f)
* H3(
b,
c,
g)
by Th9;
existence
ex b1 being strict contravariant Functor of W -SUP_category ,W -INF_category st
( ( for a being Object of (W -SUP_category) holds b1 . a = latt a ) & ( for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = UpperAdj (@ f) ) )
uniqueness
for b1, b2 being strict contravariant Functor of W -SUP_category ,W -INF_category st ( for a being Object of (W -SUP_category) holds b1 . a = latt a ) & ( for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b1 . f = UpperAdj (@ f) ) & ( for a being Object of (W -SUP_category) holds b2 . a = latt a ) & ( for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b2 . f = UpperAdj (@ f) ) holds
b1 = b2
end;
definition
let W be non
empty set ;
set A =
W -INF_category ;
defpred S1[
set ]
means verum;
defpred S2[
Object of
(W -INF_category),
Object of
(W -INF_category),
Morphism of $1,$2]
means @ $3 is
directed-sups-preserving ;
A1:
ex
a being
Object of
(W -INF_category) st
S1[
a]
;
A2:
for
a,
b,
c being
Object of
(W -INF_category) st
S1[
a] &
S1[
b] &
S1[
c] &
<^a,b^> <> {} &
<^b,c^> <> {} holds
for
f being
Morphism of
a,
b for
g being
Morphism of
b,
c st
S2[
a,
b,
f] &
S2[
b,
c,
g] holds
S2[
a,
c,
g * f]
A8:
for
a being
Object of
(W -INF_category) st
S1[
a] holds
S2[
a,
a,
idm a]
existence
ex b1 being non empty strict subcategory of W -INF_category st
( ( for a being Object of (W -INF_category) holds a is Object of b1 ) & ( for a, b being Object of (W -INF_category)
for a9, b9 being Object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) )
correctness
uniqueness
for b1, b2 being non empty strict subcategory of W -INF_category st ( for a being Object of (W -INF_category) holds a is Object of b1 ) & ( for a, b being Object of (W -INF_category)
for a9, b9 being Object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) & ( for a being Object of (W -INF_category) holds a is Object of b2 ) & ( for a, b being Object of (W -INF_category)
for a9, b9 being Object of b2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) holds
b1 = b2;
end;
definition
let W be
with_non-empty_element set ;
A1:
ex
w being non
empty set st
w in W
by SETFAM_1:def 10;
set A =
W -SUP_category ;
defpred S1[
set ]
means verum;
defpred S2[
Object of
(W -SUP_category),
Object of
(W -SUP_category),
Morphism of $1,$2]
means UpperAdj (@ $3) is
directed-sups-preserving ;
A2:
ex
a being
Object of
(W -SUP_category) st
S1[
a]
;
A3:
for
a,
b,
c being
Object of
(W -SUP_category) st
S1[
a] &
S1[
b] &
S1[
c] &
<^a,b^> <> {} &
<^b,c^> <> {} holds
for
f being
Morphism of
a,
b for
g being
Morphism of
b,
c st
S2[
a,
b,
f] &
S2[
b,
c,
g] holds
S2[
a,
c,
g * f]
A12:
for
a being
Object of
(W -SUP_category) st
S1[
a] holds
S2[
a,
a,
idm a]
existence
ex b1 being non empty strict subcategory of W -SUP_category st
( ( for a being Object of (W -SUP_category) holds a is Object of b1 ) & ( for a, b being Object of (W -SUP_category)
for a9, b9 being Object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) )
correctness
uniqueness
for b1, b2 being non empty strict subcategory of W -SUP_category st ( for a being Object of (W -SUP_category) holds a is Object of b1 ) & ( for a, b being Object of (W -SUP_category)
for a9, b9 being Object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) & ( for a being Object of (W -SUP_category) holds a is Object of b2 ) & ( for a, b being Object of (W -SUP_category)
for a9, b9 being Object of b2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) holds
b1 = b2;
end;