begin
:: deftheorem Def1 defines as_1-sorted YELLOW21:def 1 :
for a being set holds
( ( a is 1-sorted implies a as_1-sorted = a ) & ( a is not 1-sorted implies a as_1-sorted = 1-sorted(# a #) ) );
:: deftheorem Def2 defines POSETS YELLOW21:def 2 :
for W being set
for b2 being set holds
( b2 = POSETS W iff for x being set holds
( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) );
:: deftheorem Def3 defines carrier-underlaid YELLOW21:def 3 :
for C being category holds
( C is carrier-underlaid iff for a being object of C ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S ) );
:: deftheorem Def4 defines lattice-wise YELLOW21:def 4 :
for C being category holds
( C is lattice-wise iff ( C is semi-functional & C is set-id-inheriting & ( for a being object of C holds a is LATTICE ) & ( for a, b being object of C
for A, B being LATTICE st A = a & B = b holds
<^a,b^> c= MonFuncs (A,B) ) ) );
:: deftheorem Def5 defines with_complete_lattices YELLOW21:def 5 :
for C being category holds
( C is with_complete_lattices iff ( C is lattice-wise & ( for a being object of C holds a is complete LATTICE ) ) );
scheme
localCLCatEx{
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]
theorem
theorem Th2:
:: deftheorem defines latt YELLOW21:def 6 :
for C being lattice-wise category
for a being object of C holds latt a = a;
:: deftheorem Def7 defines @ YELLOW21:def 7 :
for C being lattice-wise category
for a, b being object of C st <^a,b^> <> {} holds
for f being Morphism of a,b holds @ f = f;
theorem Th3:
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[
set ],
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[
set ],
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) )
begin
:: deftheorem Def8 defines with_all_isomorphisms YELLOW21:def 8 :
for C being lattice-wise category holds
( C is with_all_isomorphisms iff for a, b being object of C
for f being Function of (latt a),(latt b) st f is isomorphic holds
f in <^a,b^> );
theorem
theorem
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)
begin
:: deftheorem Def9 defines upper-bounded YELLOW21:def 9 :
for R being Relation holds
( R is upper-bounded iff ex x being set st
for y being set st y in field R holds
[y,x] in R );
Lm1:
for x, X being set holds
( x in X iff X = (X \ {x}) \/ {x} )
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
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
;
func W -UPS_category -> strict lattice-wise category means :
Def10:
( ( for
x being
LATTICE holds
(
x is
object of
it iff (
x is
strict &
x is
complete & the
carrier of
x in W ) ) ) & ( for
a,
b being
object of
it for
f being
monotone Function of
(latt a),
(latt b) holds
(
f in <^a,b^> iff
f is
directed-sups-preserving ) ) );
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;
:: deftheorem Def10 defines -UPS_category YELLOW21:def 10 :
for W being non empty set st not for w being Element of W holds w is empty holds
for b2 being strict lattice-wise category holds
( b2 = W -UPS_category iff ( ( 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 ) ) ) );
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: deftheorem Def11 defines -CONT_category YELLOW21:def 11 :
for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -UPS_category holds
( b2 = W -CONT_category iff for a being object of (W -UPS_category) holds
( a is object of b2 iff latt a is continuous ) );
:: deftheorem Def12 defines -ALG_category YELLOW21:def 12 :
for W being with_non-empty_element set
for b2 being non empty strict full subcategory of W -CONT_category holds
( b2 = W -ALG_category iff for a being object of (W -CONT_category) holds
( a is object of b2 iff latt a is algebraic ) );
theorem
canceled;
theorem Th17:
theorem
theorem Th19:
theorem Th20: