environ
vocabularies HIDDEN, STRUCT_0, ORDERS_2, ORDERS_1, ZFMISC_1, FUNCT_1, RELAT_1, CARD_3, XBOOLE_0, SUBSET_1, SETFAM_1, ORDERS_3, ALTCAT_1, YELLOW18, WAYBEL_0, TARSKI, REWRITE1, PBOOLE, FUNCT_2, SEQM_3, FILTER_0, CAT_1, QC_LANG1, FUNCTOR0, WELLORD1, ALTCAT_3, CAT_3, LATTICES, RELAT_2, ORDINAL1, WELLORD2, CARD_1, LATTICE3, XXREAL_0, ORDINAL2, ARYTM_3, RCOMP_1, TREES_2, WAYBEL_8, WAYBEL_3, ALTCAT_2, YELLOW21;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SETFAM_1, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, CARD_3, BINOP_1, ORDINAL1, CARD_1, WELLORD1, WELLORD2, ORDERS_1, STRUCT_0, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_3, WAYBEL_8, ALTCAT_1, ALTCAT_2, FUNCTOR0, ALTCAT_3, YELLOW18;
definitions TARSKI, RELAT_2, WELLORD1, WELLORD2, ORDERS_2, LATTICE3, ORDERS_3, ALTCAT_1, ALTCAT_3, YELLOW_0, WAYBEL_0, WAYBEL_3, YELLOW18, XBOOLE_0;
theorems ZFMISC_1, RELAT_1, FUNCT_1, WELLORD1, WELLORD2, ORDERS_2, ORDERS_1, FUNCT_2, ALTCAT_1, ALTCAT_2, ORDERS_3, ALTCAT_3, ORDINAL1, CARD_1, CARD_5, WAYBEL_0, WAYBEL13, ORDINAL3, TARSKI, RELSET_1, RELAT_2, YELLOW_0, YELLOW_2, WAYBEL_3, WAYBEL_8, YELLOW18, WAYBEL20, YELLOW16, XBOOLE_0, XBOOLE_1, PARTFUN1, SETFAM_1, XTUPLE_0;
schemes TARSKI, CARD_3, PBOOLE, CLASSES1, YELLOW18, YELLOW20, XBOOLE_0;
registrations SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, CARD_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, ALTCAT_2, FUNCTOR0, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL10, FUNCTOR2, ALTCAT_4, WAYBEL17, YELLOW_9, YELLOW18, WELLORD1, WELLORD2;
constructors HIDDEN, WELLORD1, ORDERS_3, WAYBEL_8, ALTCAT_3, YELLOW18, RELSET_1, WAYBEL20, ENUMSET1;
requirements HIDDEN, SUBSET, BOOLE;
equalities ALTCAT_1, YELLOW18, XBOOLE_0, BINOP_1, STRUCT_0;
expansions TARSKI, RELAT_2, WELLORD1, ORDERS_2, LATTICE3, ALTCAT_3, WAYBEL_3, YELLOW18, XBOOLE_0;
scheme
localCLCatEx{
F1()
-> non
empty set ,
P1[
object ,
object ,
object ] } :
provided
A1:
for
a being
Element of
F1() holds
a is
LATTICE
and A2:
for
a,
b,
c being
LATTICE st
a in F1() &
b in F1() &
c in F1() holds
for
f being
Function of
a,
b for
g being
Function of
b,
c st
P1[
a,
b,
f] &
P1[
b,
c,
g] holds
P1[
a,
c,
g * f]
and A3:
for
a being
LATTICE st
a in F1() holds
P1[
a,
a,
id a]
scheme
CLCatEx1{
F1()
-> non
empty set ,
P1[
set ,
set ,
set ] } :
provided
A1:
for
a being
Element of
F1() holds
a is
LATTICE
and A2:
for
a,
b,
c being
LATTICE st
a in F1() &
b in F1() &
c in F1() holds
for
f being
Function of
a,
b for
g being
Function of
b,
c st
P1[
a,
b,
f] &
P1[
b,
c,
g] holds
P1[
a,
c,
g * f]
and A3:
for
a being
LATTICE st
a in F1() holds
P1[
a,
a,
id a]
scheme
CLCatEx2{
F1()
-> non
empty set ,
P1[
object ],
P2[
set ,
set ,
set ] } :
provided
A1:
ex
x being
strict LATTICE st
(
P1[
x] & the
carrier of
x in F1() )
and A2:
for
a,
b,
c being
LATTICE st
P1[
a] &
P1[
b] &
P1[
c] holds
for
f being
Function of
a,
b for
g being
Function of
b,
c st
P2[
a,
b,
f] &
P2[
b,
c,
g] holds
P2[
a,
c,
g * f]
and A3:
for
a being
LATTICE st
P1[
a] holds
P2[
a,
a,
id a]
scheme
CLCatUniq1{
F1()
-> non
empty set ,
P1[
set ,
set ,
set ] } :
for
C1,
C2 being
lattice-wise category st the
carrier of
C1 = F1() & ( for
a,
b being
Object of
C1 for
f being
monotone Function of
(latt a),
(latt b) holds
(
f in <^a,b^> iff
P1[
a,
b,
f] ) ) & the
carrier of
C2 = F1() & ( for
a,
b being
Object of
C2 for
f being
monotone Function of
(latt a),
(latt b) holds
(
f in <^a,b^> iff
P1[
a,
b,
f] ) ) holds
AltCatStr(# the
carrier of
C1, the
Arrows of
C1, the
Comp of
C1 #)
= AltCatStr(# the
carrier of
C2, the
Arrows of
C2, the
Comp of
C2 #)
scheme
CLCatUniq2{
F1()
-> non
empty set ,
P1[
object ],
P2[
set ,
set ,
set ] } :
for
C1,
C2 being
lattice-wise category st ( for
x being
LATTICE holds
(
x is
Object of
C1 iff (
x is
strict &
P1[
x] & the
carrier of
x in F1() ) ) ) & ( for
a,
b being
Object of
C1 for
f being
monotone Function of
(latt a),
(latt b) holds
(
f in <^a,b^> iff
P2[
a,
b,
f] ) ) & ( for
x being
LATTICE holds
(
x is
Object of
C2 iff (
x is
strict &
P1[
x] & the
carrier of
x in F1() ) ) ) & ( for
a,
b being
Object of
C2 for
f being
monotone Function of
(latt a),
(latt b) holds
(
f in <^a,b^> iff
P2[
a,
b,
f] ) ) holds
AltCatStr(# the
carrier of
C1, the
Arrows of
C1, the
Comp of
C1 #)
= AltCatStr(# the
carrier of
C2, the
Arrows of
C2, the
Comp of
C2 #)
scheme
CLCovariantFunctorEx{
P1[
set ,
set ,
set ],
P2[
set ,
set ,
set ],
F1()
-> lattice-wise category,
F2()
-> lattice-wise category,
F3(
set )
-> LATTICE,
F4(
set ,
set ,
set )
-> Function } :
provided
A1:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F1()
. (
a,
b) iff (
a in the
carrier of
F1() &
b in the
carrier of
F1() &
P1[
a,
b,
f] ) )
and A2:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F2()
. (
a,
b) iff (
a in the
carrier of
F2() &
b in the
carrier of
F2() &
P2[
a,
b,
f] ) )
and A3:
for
a being
LATTICE st
a in the
carrier of
F1() holds
F3(
a)
in the
carrier of
F2()
and A4:
for
a,
b being
LATTICE for
f being
Function of
a,
b st
P1[
a,
b,
f] holds
(
F4(
a,
b,
f) is
Function of
F3(
a),
F3(
b) &
P2[
F3(
a),
F3(
b),
F4(
a,
b,
f)] )
and A5:
for
a being
LATTICE st
a in the
carrier of
F1() holds
F4(
a,
a,
(id a))
= id F3(
a)
and A6:
for
a,
b,
c being
LATTICE for
f being
Function of
a,
b for
g being
Function of
b,
c st
P1[
a,
b,
f] &
P1[
b,
c,
g] holds
F4(
a,
c,
(g * f))
= F4(
b,
c,
g)
* F4(
a,
b,
f)
scheme
CLContravariantFunctorEx{
P1[
set ,
set ,
set ],
P2[
set ,
set ,
set ],
F1()
-> lattice-wise category,
F2()
-> lattice-wise category,
F3(
set )
-> LATTICE,
F4(
set ,
set ,
set )
-> Function } :
provided
A1:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F1()
. (
a,
b) iff (
a in the
carrier of
F1() &
b in the
carrier of
F1() &
P1[
a,
b,
f] ) )
and A2:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F2()
. (
a,
b) iff (
a in the
carrier of
F2() &
b in the
carrier of
F2() &
P2[
a,
b,
f] ) )
and A3:
for
a being
LATTICE st
a in the
carrier of
F1() holds
F3(
a)
in the
carrier of
F2()
and A4:
for
a,
b being
LATTICE for
f being
Function of
a,
b st
P1[
a,
b,
f] holds
(
F4(
a,
b,
f) is
Function of
F3(
b),
F3(
a) &
P2[
F3(
b),
F3(
a),
F4(
a,
b,
f)] )
and A5:
for
a being
LATTICE st
a in the
carrier of
F1() holds
F4(
a,
a,
(id a))
= id F3(
a)
and A6:
for
a,
b,
c being
LATTICE for
f being
Function of
a,
b for
g being
Function of
b,
c st
P1[
a,
b,
f] &
P1[
b,
c,
g] holds
F4(
a,
c,
(g * f))
= F4(
a,
b,
f)
* F4(
b,
c,
g)
scheme
CLCatIsomorphism{
P1[
set ,
set ,
set ],
P2[
set ,
set ,
set ],
F1()
-> lattice-wise category,
F2()
-> lattice-wise category,
F3(
set )
-> LATTICE,
F4(
set ,
set ,
set )
-> Function } :
provided
A1:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F1()
. (
a,
b) iff (
a in the
carrier of
F1() &
b in the
carrier of
F1() &
P1[
a,
b,
f] ) )
and A2:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F2()
. (
a,
b) iff (
a in the
carrier of
F2() &
b in the
carrier of
F2() &
P2[
a,
b,
f] ) )
and A3:
ex
F being
covariant Functor of
F1(),
F2() st
( ( for
a being
Object of
F1() holds
F . a = F3(
a) ) & ( for
a,
b being
Object of
F1() st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b holds
F . f = F4(
a,
b,
f) ) )
and A4:
for
a,
b being
LATTICE st
a in the
carrier of
F1() &
b in the
carrier of
F1() &
F3(
a)
= F3(
b) holds
a = b
and A5:
for
a,
b being
LATTICE for
f,
g being
Function of
a,
b st
P1[
a,
b,
f] &
P1[
a,
b,
g] &
F4(
a,
b,
f)
= F4(
a,
b,
g) holds
f = g
and A6:
for
a,
b being
LATTICE for
f being
Function of
a,
b st
P2[
a,
b,
f] holds
ex
c,
d being
LATTICE ex
g being
Function of
c,
d st
(
c in the
carrier of
F1() &
d in the
carrier of
F1() &
P1[
c,
d,
g] &
a = F3(
c) &
b = F3(
d) &
f = F4(
c,
d,
g) )
scheme
CLCatAntiIsomorphism{
P1[
set ,
set ,
set ],
P2[
set ,
set ,
set ],
F1()
-> lattice-wise category,
F2()
-> lattice-wise category,
F3(
set )
-> LATTICE,
F4(
set ,
set ,
set )
-> Function } :
provided
A1:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F1()
. (
a,
b) iff (
a in the
carrier of
F1() &
b in the
carrier of
F1() &
P1[
a,
b,
f] ) )
and A2:
for
a,
b being
LATTICE for
f being
Function of
a,
b holds
(
f in the
Arrows of
F2()
. (
a,
b) iff (
a in the
carrier of
F2() &
b in the
carrier of
F2() &
P2[
a,
b,
f] ) )
and A3:
ex
F being
contravariant Functor of
F1(),
F2() st
( ( for
a being
Object of
F1() holds
F . a = F3(
a) ) & ( for
a,
b being
Object of
F1() st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b holds
F . f = F4(
a,
b,
f) ) )
and A4:
for
a,
b being
LATTICE st
a in the
carrier of
F1() &
b in the
carrier of
F1() &
F3(
a)
= F3(
b) holds
a = b
and A5:
for
a,
b being
LATTICE for
f,
g being
Function of
a,
b st
F4(
a,
b,
f)
= F4(
a,
b,
g) holds
f = g
and A6:
for
a,
b being
LATTICE for
f being
Function of
a,
b st
P2[
a,
b,
f] holds
ex
c,
d being
LATTICE ex
g being
Function of
c,
d st
(
c in the
carrier of
F1() &
d in the
carrier of
F1() &
P1[
c,
d,
g] &
b = F3(
c) &
a = F3(
d) &
f = F4(
c,
d,
g) )
scheme
CLCatEquivalence{
P1[
set ,
set ,
set ],
P2[
set ,
set ,
set ],
F1()
-> lattice-wise category,
F2()
-> lattice-wise category,
F3(
set )
-> LATTICE,
F4(
set )
-> LATTICE,
F5(
set ,
set ,
set )
-> Function,
F6(
set ,
set ,
set )
-> Function,
F7(
set )
-> Function,
F8(
set )
-> Function } :
provided
A1:
for
a,
b being
Object of
F1()
for
f being
monotone Function of
(latt a),
(latt b) holds
(
f in <^a,b^> iff
P1[
latt a,
latt b,
f] )
and A2:
for
a,
b being
Object of
F2()
for
f being
monotone Function of
(latt a),
(latt b) holds
(
f in <^a,b^> iff
P2[
latt a,
latt b,
f] )
and A3:
ex
F being
covariant Functor of
F1(),
F2() st
( ( for
a being
Object of
F1() holds
F . a = F3(
a) ) & ( for
a,
b being
Object of
F1() st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b holds
F . f = F5(
a,
b,
f) ) )
and A4:
ex
G being
covariant Functor of
F2(),
F1() st
( ( for
a being
Object of
F2() holds
G . a = F4(
a) ) & ( for
a,
b being
Object of
F2() st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b holds
G . f = F6(
a,
b,
f) ) )
and A5:
for
a being
LATTICE st
a in the
carrier of
F1() holds
ex
f being
monotone Function of
F4(
F3(
a)),
a st
(
f = F7(
a) &
f is
isomorphic &
P1[
F4(
F3(
a)),
a,
f] &
P1[
a,
F4(
F3(
a)),
f " ] )
and A6:
for
a being
LATTICE st
a in the
carrier of
F2() holds
ex
f being
monotone Function of
a,
F3(
F4(
a)) st
(
f = F8(
a) &
f is
isomorphic &
P2[
a,
F3(
F4(
a)),
f] &
P2[
F3(
F4(
a)),
a,
f " ] )
and A7:
for
a,
b being
Object of
F1() st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b holds
F7(
b)
* F6(
F3(
a),
F3(
b),
F5(
a,
b,
f))
= (@ f) * F7(
a)
and A8:
for
a,
b being
Object of
F2() st
<^a,b^> <> {} holds
for
f being
Morphism of
a,
b holds
F5(
F4(
a),
F4(
b),
F6(
a,
b,
f))
* F8(
a)
= F8(
b)
* (@ f)
Lm1:
for x, X being set holds
( x in X iff X = (X \ {x}) \/ {x} )
by ZFMISC_1:31, XBOOLE_1:7, XBOOLE_1:45;
definition
defpred S1[
LATTICE,
LATTICE,
Function of $1,$2]
means $3 is
directed-sups-preserving ;
defpred S2[
LATTICE]
means $1 is
complete ;
let W be non
empty set ;
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 directed-sups-preserving ) ) )
correctness
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 directed-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 directed-sups-preserving ) ) holds
b1 = b2;
end;