:: Categorial Background for Duality Theory :: by Grzegorz Bancerek :: :: Received August 1, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin definition let a be set ; funca as_1-sorted -> 1-sorted equals :Def1: :: YELLOW21:def 1 a if a is 1-sorted otherwise 1-sorted(# a #); coherence ( ( a is 1-sorted implies a is 1-sorted ) & ( a is not 1-sorted implies 1-sorted(# a #) is 1-sorted ) ) ; consistency for b1 being 1-sorted holds verum ; end; :: 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 #) ) ); definition let W be set ; defpred S1[ set ] 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 set 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 set holds ( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being set holds ( x in b2 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) holds b1 = b2 proofend; existence ex b1 being set st for x being set holds ( x in b1 iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) proofend; end; :: 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 ) ) ); registration let W be non empty set ; cluster POSETS W -> non empty ; coherence not POSETS W is empty proofend; end; registration let W be with_non-empty_elements set ; cluster POSETS W -> POSet_set-like ; coherence POSETS W is POSet_set-like proofend; end; definition let C be category; attrC 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; attrC 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; attrC 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 V110() 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 by Def5; cluster non empty transitive V110() 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 ) proofend; end; scheme :: YELLOW21:sch 1 localCLCatEx{ F1() -> non empty set , P1[ set , set , set ] } : 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] proofend; registration cluster non empty transitive strict V110() with_units reflexive with_complete_lattices for AltCatStr ; existence ex b1 being category st ( b1 is strict & b1 is with_complete_lattices ) proofend; 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) proofend; 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) proofend; 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 proofend; compatibility for b1 being LATTICE holds ( b1 = a as_1-sorted iff b1 = a ) proofend; 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) proofend; 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) proofend; 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] proofend; scheme :: YELLOW21:sch 3 CLCatEx2{ F1() -> non empty set , P1[ set ], 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] proofend; 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 #) proofend; scheme :: YELLOW21:sch 5 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 #) proofend; 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) proofend; 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) proofend; 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) ) proofend; 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) ) proofend; begin definition let C be lattice-wise category; attrC 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 V110() 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 proofend; 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 proofend; 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 proofend; 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) proofend; begin definition let R be Relation; attrR is upper-bounded means :Def9: :: YELLOW21:def 9 ex x being set st for y being set st y in field R holds [y,x] in R; end; :: 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} ) proofend; 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 proofend; end; theorem Th6: :: YELLOW21:6 for x, y being set 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 ) ) proofend; registration let f be one-to-one Function; let R be reflexive Relation; cluster(f * R) * (f ") -> reflexive ; coherence (f * R) * (f ") is reflexive proofend; 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 proofend; 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 proofend; 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 ) proofend; registration let X be non empty set ; cluster Relation-like X -defined X -valued well-ordering V16(X) quasi_total reflexive antisymmetric transitive upper-bounded for Element of bool [:X,X:]; existence ex b1 being Order of X st ( b1 is upper-bounded & b1 is well-ordering ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; theorem Th11: :: YELLOW21:11 for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds P is algebraic proofend; 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 ) proofend; 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 ; funcW -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 ) ) ) proofend; 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; proofend; 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 ; clusterW -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 ) proofend; end; theorem Th12: :: YELLOW21:12 for W being with_non-empty_element set holds the carrier of (W -UPS_category) c= POSETS W proofend; 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 ) ) proofend; 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 ) ) proofend; 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) ) proofend; 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 proofend; end; begin 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 #); funcW -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 ) proofend; 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; proofend; 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 #); funcW -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 ) proofend; 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; proofend; 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 ) ) proofend; 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 ) ) proofend; 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) ) proofend; 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) ) proofend; 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 proofend; 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 proofend; end;