:: Categorial Background for Duality Theory
:: by Grzegorz Bancerek
::
:: Received August 1, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users


definition
let a be object ;
func a as_1-sorted -> 1-sorted equals :Def1: :: YELLOW21:def 1
a if a is 1-sorted
otherwise the 1-sorted ;
coherence
( ( a is 1-sorted implies a is 1-sorted ) & ( a is not 1-sorted implies the 1-sorted is 1-sorted ) ) ;
consistency
for b1 being 1-sorted holds verum ;
end;

:: deftheorem Def1 defines as_1-sorted YELLOW21:def 1 :
for a being object holds
( ( a is 1-sorted implies a as_1-sorted = a ) & ( a is not 1-sorted implies a as_1-sorted = the 1-sorted ) );

definition
let W be set ;
defpred S1[ object ] means ( $1 is strict Poset & the carrier of ($1 as_1-sorted) in W );
func POSETS W -> set means :Def2: :: YELLOW21:def 2
 for x being object holds
( x in it iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) );
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being object holds
( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being set st
for x being object holds
( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) )
proof end;
end;

:: deftheorem Def2 defines POSETS YELLOW21:def 2 :
for W, b2 being set holds
( b2 = POSETS W iff for x being object holds
( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) );

registration
let W be non empty set ;
cluster POSETS W -> non empty ;
coherence
not POSETS W is empty
proof end;
end;

registration
let W be with_non-empty_elements set ;
cluster POSETS W -> POSet_set-like ;
coherence
POSETS W is POSet_set-like
proof end;
end;

definition
let C be category;
attr C is carrier-underlaid means :Def3: :: YELLOW21:def 3
 for a being Object of C ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S );
end;

:: 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 ) );

definition
let C be category;
attr C is lattice-wise means :Def4: :: YELLOW21:def 4
( 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) ) );
end;

:: 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) ) ) );

definition
let C be category;
attr C is with_complete_lattices means :Def5: :: YELLOW21:def 5
( C is lattice-wise & ( for a being Object of C holds a is complete LATTICE ) );
end;

:: 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 ) ) );

registration
cluster non empty transitive V121() with_units with_complete_lattices -> lattice-wise for AltCatStr ;
coherence
for b1 being category st b1 is with_complete_lattices holds
b1 is lattice-wise ;
cluster non empty transitive V121() with_units lattice-wise -> concrete carrier-underlaid for AltCatStr ;
coherence
for b1 being category st b1 is lattice-wise holds
( b1 is concrete & b1 is carrier-underlaid )
proof end;
end;

scheme :: YELLOW21:sch 1
localCLCatEx{ F1() -> non empty set , P1[ object , object , object ] } :
ex C being strict category st
( C is lattice-wise & the carrier of C = F1() & ( for a, b being LATTICE
for f being monotone Function of a,b holds
( f in the Arrows of C . (a,b) iff ( a in F1() & b in F1() & P1[a,b,f] ) ) ) )
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]
proof end;

registration
cluster non empty transitive strict V121() with_units reflexive with_complete_lattices for AltCatStr ;
existence
ex b1 being category st
( b1 is strict & b1 is with_complete_lattices )
proof end;
end;

theorem :: YELLOW21:1
for C being carrier-underlaid category
for a being Object of C holds the_carrier_of a = the carrier of (a as_1-sorted)
proof end;

theorem Th2: :: YELLOW21:2
for C being set-id-inheriting carrier-underlaid category
for a being Object of C holds idm a = id (a as_1-sorted)
proof end;

notation
let C be lattice-wise category;
let a be Object of C;
synonym latt a for C as_1-sorted ;
end;

definition
let C be lattice-wise category;
let a be Object of C;
:: original: as_1-sorted
redefine func latt a -> LATTICE equals :: YELLOW21:def 6
a;
coherence
a as_1-sorted is LATTICE
proof end;
compatibility
for b1 being LATTICE holds
( b1 = a as_1-sorted iff b1 = a )
proof end;
end;

:: deftheorem defines latt YELLOW21:def 6 :
for C being lattice-wise category
for a being Object of C holds latt a = a;

notation
let C be with_complete_lattices category;
let a be Object of C;
synonym latt a for C as_1-sorted ;
end;

definition
let C be with_complete_lattices category;
let a be Object of C;
:: original: as_1-sorted
redefine func latt a -> complete LATTICE;
coherence
a as_1-sorted is complete LATTICE by Def5;
end;

definition
let C be lattice-wise category;
let a, b be Object of C;
assume A1: <^a,b^> <> {} ;
let f be Morphism of a,b;
func @ f -> monotone Function of (latt a),(latt b) equals :Def7: :: YELLOW21:def 7
f;
coherence
f is monotone Function of (latt a),(latt b)
proof end;
end;

:: 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: :: YELLOW21:3
for C being lattice-wise category
for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (@ g) * (@ f)
proof end;

scheme :: YELLOW21:sch 2
CLCatEx1{ F1() -> non empty set , P1[ set , set , set ] } :
ex C being strict lattice-wise category st
( the carrier of C = F1() & ( for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[ latt a, latt b,f] ) ) )
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]
proof end;

scheme :: YELLOW21:sch 3
CLCatEx2{ F1() -> non empty set , P1[ object ], P2[ set , set , set ] } :
ex C being strict lattice-wise category st
( ( for x being LATTICE holds
( x is Object of C iff ( x is strict & P1[x] & the carrier of x in F1() ) ) ) & ( for a, b being Object of C
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P2[ latt a, latt b,f] ) ) )
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]
proof end;

scheme :: YELLOW21:sch 4
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 #)
proof end;

scheme :: YELLOW21:sch 5
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 #)
proof end;

scheme :: YELLOW21:sch 6
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 } :
ex F being strict covariant Functor of F1(),F2() st
( ( for a being Object of F1() holds F . a = F3((latt a)) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
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)
proof end;

scheme :: YELLOW21:sch 7
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 } :
ex F being strict contravariant Functor of F1(),F2() st
( ( for a being Object of F1() holds F . a = F3((latt a)) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F4((latt a),(latt b),(@ f)) ) )
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)
proof end;

scheme :: YELLOW21:sch 8
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 } :
F1(),F2() are_isomorphic
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) )
proof end;

scheme :: YELLOW21:sch 9
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 } :
F1(),F2() are_anti-isomorphic
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) )
proof end;

definition
let C be lattice-wise category;
attr C is with_all_isomorphisms means :Def8: :: YELLOW21:def 8
 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^>;
end;

:: 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^> );

registration
cluster non empty transitive strict semi-functional V121() with_units reflexive para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_all_isomorphisms for AltCatStr ;
existence
ex b1 being strict lattice-wise category st b1 is with_all_isomorphisms
proof end;
end;

theorem :: YELLOW21:4
for C being lattice-wise with_all_isomorphisms category
for a, b being Object of C
for f being Morphism of a,b st @ f is isomorphic holds
f is iso
proof end;

theorem :: YELLOW21:5
for C being lattice-wise category
for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
@ f is isomorphic
proof end;

scheme :: YELLOW21:sch 10
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 } :
F1(),F2() are_equivalent
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)
proof end;

definition
let R be Relation;
attr R is upper-bounded means :: YELLOW21:def 9
 ex x being set st
for y being set st y in field R holds
[y,x] in R;
end;

:: deftheorem 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} )
by ZFMISC_1:31, XBOOLE_1:7, XBOOLE_1:45;

registration
cluster Relation-like well-ordering -> well_founded reflexive antisymmetric connected transitive for set ;
coherence
for b1 being Relation st b1 is well-ordering holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded ) ;
end;

registration
cluster Relation-like well-ordering for set ;
existence
ex b1 being Relation st b1 is well-ordering
proof end;
end;

theorem Th6: :: YELLOW21:6
for x, y being object
for f being one-to-one Function
for R being Relation holds
( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )
proof end;

registration
let f be one-to-one Function;
let R be reflexive Relation;
cluster (f * R) * (f ") -> reflexive ;
coherence
(f * R) * (f ") is reflexive
proof end;
end;

registration
let f be one-to-one Function;
let R be antisymmetric Relation;
cluster (f * R) * (f ") -> antisymmetric ;
coherence
(f * R) * (f ") is antisymmetric
proof end;
end;

registration
let f be one-to-one Function;
let R be transitive Relation;
cluster (f * R) * (f ") -> transitive ;
coherence
(f * R) * (f ") is transitive
proof end;
end;

theorem Th7: :: YELLOW21:7
for X being set
for A being Ordinal st X,A are_equipotent holds
ex R being Order of X st
( R well_orders X & order_type_of R = A )
proof end;

registration
let X be non empty set ;
cluster Relation-like X -defined X -valued well-ordering reflexive antisymmetric transitive V24(X) quasi_total upper-bounded for Element of bool [:X,X:];
existence
ex b1 being Order of X st
( b1 is upper-bounded & b1 is well-ordering )
proof end;
end;

theorem Th8: :: YELLOW21:8
for P being non empty reflexive RelStr holds
( P is upper-bounded iff the InternalRel of P is upper-bounded )
proof end;

theorem Th9: :: YELLOW21:9
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
( P is connected & P is complete & P is continuous )
proof end;

theorem Th10: :: YELLOW21:10
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
for x, y being Element of P st y < x holds
ex z being Element of P st
( z is compact & y <= z & z <= x )
proof end;

theorem Th11: :: YELLOW21:11
for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
P is algebraic
proof end;

registration
let X be non empty set ;
let R be well-ordering upper-bounded Order of X;
cluster RelStr(# X,R #) -> algebraic complete connected continuous ;
coherence
( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic )
proof end;
end;

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: :: YELLOW21:def 10
( ( 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 ) ) )
proof end;
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;
proof end;
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 ) ) ) );

registration
let W be with_non-empty_element set ;
cluster W -UPS_category -> strict lattice-wise with_complete_lattices with_all_isomorphisms ;
coherence
( W -UPS_category is with_complete_lattices & W -UPS_category is with_all_isomorphisms )
proof end;
end;

theorem Th12: :: YELLOW21:12
for W being with_non-empty_element set holds the carrier of (W -UPS_category) c= POSETS W
proof end;

theorem Th13: :: YELLOW21:13
for W being with_non-empty_element set
for x being set holds
( x is Object of (W -UPS_category) iff ( x is complete LATTICE & x in POSETS W ) )
proof end;

theorem Th14: :: YELLOW21:14
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is Object of (W -UPS_category) iff ( L is strict & L is complete ) )
proof end;

theorem Th15: :: YELLOW21:15
for W being with_non-empty_element set
for a, b being Object of (W -UPS_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof end;

registration
let W be with_non-empty_element set ;
let a, b be Object of (W -UPS_category);
cluster <^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof end;
end;

registration
let A be set-id-inheriting category;
cluster non empty transitive id-inheriting -> non empty set-id-inheriting for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is set-id-inheriting
proof end;
end;

registration
let A be para-functional category;
cluster non empty transitive id-inheriting -> non empty para-functional for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is para-functional
proof end;
end;

registration
let A be semi-functional category;
cluster non empty transitive -> non empty transitive semi-functional for SubCatStr of A;
coherence
for b1 being non empty transitive SubCatStr of A holds b1 is semi-functional
proof end;
end;

registration
let A be carrier-underlaid category;
cluster non empty transitive id-inheriting -> non empty carrier-underlaid for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is carrier-underlaid
proof end;
end;

registration
let A be lattice-wise category;
cluster non empty transitive id-inheriting -> non empty lattice-wise for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is lattice-wise
proof end;
end;

registration
let A be lattice-wise with_all_isomorphisms category;
cluster non empty transitive full id-inheriting -> non empty with_all_isomorphisms for SubCatStr of A;
coherence
for b1 being non empty subcategory of A st b1 is full holds
b1 is with_all_isomorphisms
proof end;
end;

registration
let A be with_complete_lattices category;
cluster non empty transitive id-inheriting -> non empty with_complete_lattices for SubCatStr of A;
coherence
for b1 being non empty subcategory of A holds b1 is with_complete_lattices
proof end;
end;

definition
let W be with_non-empty_element set ;
defpred S1[ Object of (W -UPS_category)] means latt $1 is continuous ;
consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
set r = the well-ordering upper-bounded Order of a;
set b = RelStr(# a, the well-ordering upper-bounded Order of a #);
func W -CONT_category -> non empty strict full subcategory of W -UPS_category means :Def11: :: YELLOW21:def 11
 for a being Object of (W -UPS_category) holds
( a is Object of it iff latt a is continuous );
existence
ex b1 being non empty strict full subcategory of W -UPS_category st
for a being Object of (W -UPS_category) holds
( a is Object of b1 iff latt a is continuous )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -UPS_category st ( for a being Object of (W -UPS_category) holds
( a is Object of b1 iff latt a is continuous ) ) & ( for a being Object of (W -UPS_category) holds
( a is Object of b2 iff latt a is continuous ) ) holds
b1 = b2;
proof end;
end;

:: 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 ) );

definition
let W be with_non-empty_element set ;
defpred S1[ Object of (W -CONT_category)] means latt $1 is algebraic ;
consider a being non empty set such that
A1: a in W by SETFAM_1:def 10;
set r = the well-ordering upper-bounded Order of a;
set b = RelStr(# a, the well-ordering upper-bounded Order of a #);
func W -ALG_category -> non empty strict full subcategory of W -CONT_category means :Def12: :: YELLOW21:def 12
 for a being Object of (W -CONT_category) holds
( a is Object of it iff latt a is algebraic );
existence
ex b1 being non empty strict full subcategory of W -CONT_category st
for a being Object of (W -CONT_category) holds
( a is Object of b1 iff latt a is algebraic )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full subcategory of W -CONT_category st ( for a being Object of (W -CONT_category) holds
( a is Object of b1 iff latt a is algebraic ) ) & ( for a being Object of (W -CONT_category) holds
( a is Object of b2 iff latt a is algebraic ) ) holds
b1 = b2;
proof end;
end;

:: 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 Th16: :: YELLOW21:16
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is Object of (W -CONT_category) iff ( L is strict & L is complete & L is continuous ) )
proof end;

theorem :: YELLOW21:17
for W being with_non-empty_element set
for L being LATTICE st the carrier of L in W holds
( L is Object of (W -ALG_category) iff ( L is strict & L is complete & L is algebraic ) )
proof end;

theorem Th18: :: YELLOW21:18
for W being with_non-empty_element set
for a, b being Object of (W -CONT_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof end;

theorem Th19: :: YELLOW21:19
for W being with_non-empty_element set
for a, b being Object of (W -ALG_category)
for f being set holds
( f in <^a,b^> iff f is directed-sups-preserving Function of (latt a),(latt b) )
proof end;

registration
let W be with_non-empty_element set ;
let a, b be Object of (W -CONT_category);
cluster <^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof end;
end;

registration
let W be with_non-empty_element set ;
let a, b be Object of (W -ALG_category);
cluster <^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof end;
end;