:: Categorial Background for Duality Theory
:: by Grzegorz Bancerek
::
:: 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 () 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 () 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 () in W ) ) ) & ( for x being object holds ( x in b2 iff ( x is strict Poset & the carrier of () 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 () 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 () 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 ; coherence 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 coherence for b1 being category st b1 is with_complete_lattices holds b1 is lattice-wise ; 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 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 () 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 () 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 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 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 } : 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 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 ; registration 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 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 ; 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; 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 ; coherence proof end; end; theorem Th12: :: YELLOW21:12 for W being with_non-empty_element set holds the carrier of () 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 () 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 () 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 () 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 (); cluster <^a,b^> -> non empty ; coherence not <^a,b^> is empty proof end; end; registration let A be set-id-inheriting category; 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; coherence for b1 being non empty subcategory of A holds b1 is para-functional proof end; end; registration let A be semi-functional category; 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; coherence for b1 being non empty subcategory of A holds b1 is carrier-underlaid proof end; end; registration let A be lattice-wise category; 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; 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; 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 ()] 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 () 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 () 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 () holds
( a is Object of b1 iff latt a is continuous ) ) & ( for a being Object of () 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 () holds
( a is Object of b2 iff latt a is continuous ) );

definition
let W be with_non-empty_element set ;
defpred S1[ Object of ()] 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 () 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 () 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 () holds
( a is Object of b1 iff latt a is algebraic ) ) & ( for a being Object of () 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 () 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 () 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 () 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 ()
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 ()
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 ();
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 ();
cluster <^a,b^> -> non empty ;
coherence
not <^a,b^> is empty
proof end;
end;