Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### Duality Based on Galois Connection. Part I

**by****Grzegorz Bancerek**- Received August 8, 2001
- MML identifier: WAYBEL34

- [ Mizar article, MML identifier index ]

environ vocabulary BHSP_3, WAYBEL_0, WAYBEL_1, PRE_TOPC, ORDERS_1, SEQM_3, FUNCT_1, RELAT_1, LATTICES, ORDINAL2, OPPCAT_1, ALTCAT_1, CAT_1, WELLORD1, YELLOW21, FILTER_0, TRIANG_1, QC_LANG1, FUNCTOR0, BOOLE, SGRAPH1, WAYBEL11, YELLOW_9, QUANTAL1, YELLOW_0, SUBSET_1, RELAT_2, WAYBEL_3, LATTICE3, GROUP_6, ALTCAT_2, FUNCOP_1, CANTOR_1, YELLOW20, YELLOW18, COMPTS_1, WAYBEL_8, FINSET_1, WAYBEL34; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, BINOP_1, FINSET_1, STRUCT_0, ORDERS_1, LATTICE3, GRCAT_1, BORSUK_1, TRIANG_1, WELLORD1, ALTCAT_1, FUNCTOR0, ALTCAT_2, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, PRE_TOPC, T_0TOPSP, WAYBEL_3, WAYBEL_8, YELLOW_7, WAYBEL11, YELLOW_9, WAYBEL18, YELLOW18, YELLOW20, YELLOW21; constructors RELAT_2, GRCAT_1, TOPS_2, T_0TOPSP, WAYBEL_1, WAYBEL_8, WAYBEL11, YELLOW_9, QUANTAL1, WAYBEL18, YELLOW18, YELLOW20, YELLOW21, BORSUK_1, MEMBERED; clusters RELSET_1, FUNCT_1, PRE_TOPC, FINSET_1, RLVECT_2, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, LATTICE5, YELLOW_2, WAYBEL_1, WAYBEL_2, TRIANG_1, WAYBEL_8, YELLOW_7, WAYBEL11, YELLOW_9, WAYBEL_3, TOPS_1, WAYBEL10, WAYBEL17, WAYBEL21, YELLOW21, ALTCAT_4, FUNCTOR0, FUNCTOR2, MEMBERED, ZFMISC_1; requirements SUBSET, BOOLE; begin ::<section1>Infs-preserving and sups-preserving maps</section1> definition let S,T be complete LATTICE; cluster Galois Connection of S,T; end; theorem :: WAYBEL34:1 for S,T, S',T' being non empty RelStr st the RelStr of S = the RelStr of S' & the RelStr of T = the RelStr of T' for c being Connection of S,T, c' being Connection of S',T' st c = c' holds c is Galois implies c' is Galois; definition let S,T be LATTICE; let g be map of S,T; assume S is complete & T is complete & g is infs-preserving; func LowerAdj g -> map of T,S means :: WAYBEL34:def 1 [g, it] is Galois; end; definition let S,T be LATTICE; let d be map of T,S; assume S is complete & T is complete & d is sups-preserving; func UpperAdj d -> map of S,T means :: WAYBEL34:def 2 [it, d] is Galois; end; definition let S,T be complete LATTICE; let g be infs-preserving map of S,T; cluster LowerAdj g -> lower_adjoint; end; definition let S,T be complete LATTICE; let d be sups-preserving map of T,S; cluster UpperAdj d -> upper_adjoint; end; theorem :: WAYBEL34:2 for S,T being complete LATTICE for g being infs-preserving map of S,T for t being Element of T holds (LowerAdj g).t = inf (g"uparrow t); theorem :: WAYBEL34:3 for S,T being complete LATTICE for d being sups-preserving map of T,S for s being Element of S holds (UpperAdj d).s = sup (d"downarrow s); definition let S,T be RelStr; let f be Function of the carrier of S, the carrier of T; func f opp -> map of S opp, T opp equals :: WAYBEL34:def 3 f; end; definition let S,T be complete LATTICE; let g be infs-preserving map of S,T; cluster g opp -> lower_adjoint; end; definition let S,T be complete LATTICE; let d be sups-preserving map of S,T; cluster d opp -> upper_adjoint; end; theorem :: WAYBEL34:4 for S,T being complete LATTICE for g being infs-preserving map of S, T holds LowerAdj g = UpperAdj (g opp); theorem :: WAYBEL34:5 for S,T being complete LATTICE for d being sups-preserving map of S, T holds LowerAdj (d opp) = UpperAdj d; theorem :: WAYBEL34:6 for L be non empty RelStr holds [id L, id L] is Galois; theorem :: WAYBEL34:7 :: 1.2. LEMMA, p. 179 :: LowerAdj and UpperAdj preserve identities for L being complete LATTICE holds LowerAdj id L = id L & UpperAdj id L = id L; theorem :: WAYBEL34:8 :: 1.2. LEMMA, p. 179 :: LowerAdj preserves contravariantly composition for L1,L2,L3 being complete LATTICE for g1 being infs-preserving map of L1,L2 for g2 being infs-preserving map of L2,L3 holds LowerAdj (g2*g1) = (LowerAdj g1)*(LowerAdj g2); theorem :: WAYBEL34:9 :: 1.2. LEMMA, p. 179 :: UpperAdj preserves contravariantly composition for L1,L2,L3 being complete LATTICE for d1 being sups-preserving map of L1,L2 for d2 being sups-preserving map of L2,L3 holds UpperAdj (d2*d1) = (UpperAdj d1)*(UpperAdj d2); theorem :: WAYBEL34:10 :: 1.3. THEOREM, p. 179 for S,T being complete LATTICE for g being infs-preserving map of S,T holds UpperAdj LowerAdj g = g; theorem :: WAYBEL34:11 :: 1.3. THEOREM, p. 179 for S,T being complete LATTICE for d being sups-preserving map of S,T holds LowerAdj UpperAdj d = d; theorem :: WAYBEL34:12 for C being non empty AltCatStr for a,b,f being set st f in (the Arrows of C).(a,b) ex o1,o2 being object of C st o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2; definition :: 1.1 DEFINITION, p. 179 let W be non empty set; given w being Element of W such that w is non empty; func W-INF_category -> lattice-wise strict category means :: WAYBEL34:def 4 (for x being LATTICE holds x is object of it iff x is strict complete & the carrier of x in W) & for a,b being object of it, f being monotone map of latt a, latt b holds f in <^a,b^> iff f is infs-preserving; end; definition :: 1.1 DEFINITION, p. 179 let W be non empty set; given w being Element of W such that w is non empty; func W-SUP_category -> lattice-wise strict category means :: WAYBEL34:def 5 (for x being LATTICE holds x is object of it iff x is strict complete & the carrier of x in W) & for a,b being object of it, f being monotone map of latt a, latt b holds f in <^a,b^> iff f is sups-preserving; end; definition let W be with_non-empty_element set; cluster W-INF_category -> with_complete_lattices; cluster W-SUP_category -> with_complete_lattices; end; theorem :: WAYBEL34:13 for W being with_non-empty_element set for L being LATTICE holds L is object of W-INF_category iff L is strict complete & the carrier of L in W; theorem :: WAYBEL34:14 for W being with_non-empty_element set for a, b being object of W-INF_category for f being set holds f in <^a,b^> iff f is infs-preserving map of latt a, latt b; theorem :: WAYBEL34:15 for W being with_non-empty_element set for L being LATTICE holds L is object of W-SUP_category iff L is strict complete & the carrier of L in W; theorem :: WAYBEL34:16 for W being with_non-empty_element set for a, b being object of W-SUP_category for f being set holds f in <^a,b^> iff f is sups-preserving map of latt a, latt b; theorem :: WAYBEL34:17 for W being with_non-empty_element set holds the carrier of W-INF_category = the carrier of W-SUP_category; definition :: 1.2 LEMMA, p. 179 let W be with_non-empty_element set; func W LowerAdj -> contravariant strict Functor of W-INF_category, W-SUP_category means :: WAYBEL34:def 6 (for a being object of W-INF_category holds it.a = latt a) & for a,b being object of W-INF_category st <^a,b^> <> {} for f being Morphism of a,b holds it.f = LowerAdj @f; func W UpperAdj -> contravariant strict Functor of W-SUP_category, W-INF_category means :: WAYBEL34:def 7 (for a being object of W-SUP_category holds it.a = latt a) & for a,b being object of W-SUP_category st <^a,b^> <> {} for f being Morphism of a,b holds it.f = UpperAdj @f; end; definition let W be with_non-empty_element set; cluster W LowerAdj -> bijective; cluster W UpperAdj -> bijective; end; theorem :: WAYBEL34:18 for W being with_non-empty_element set holds W LowerAdj" = W UpperAdj & W UpperAdj" = W LowerAdj; theorem :: WAYBEL34:19 :: 1.3 THEOREM, p. 179 for W being with_non-empty_element set holds (W LowerAdj)*(W UpperAdj) = id (W-SUP_category) & (W UpperAdj)*(W LowerAdj) = id (W-INF_category); theorem :: WAYBEL34:20 :: 1.3 THEOREM, p. 179 for W being with_non-empty_element set holds W-INF_category, W-SUP_category are_anti-isomorphic; begin ::<section2>Scott continuous maps and continuous lattices</section2> canceled 2; theorem :: WAYBEL34:23 :: 1.4. THEOREM, (1) <=> (2), p. 180 for S,T being complete LATTICE, g being infs-preserving map of S,T holds g is directed-sups-preserving iff for X being Scott TopAugmentation of T for Y being Scott TopAugmentation of S for V being open Subset of X holds uparrow ((LowerAdj g).:V) is open Subset of Y; definition let S,T be non empty reflexive RelStr; let f be map of S,T; attr f is waybelow-preserving means :: WAYBEL34:def 8 for x,y being Element of S st x << y holds f.x << f.y; end; theorem :: WAYBEL34:24 :: 1.4. THEOREM, (1) => (3), p. 180 for S,T being complete LATTICE, g being infs-preserving map of S,T holds g is directed-sups-preserving implies LowerAdj g is waybelow-preserving; theorem :: WAYBEL34:25 :: 1.4. THEOREM, (3+) => (1), p. 180 for S being complete LATTICE for T being complete continuous LATTICE for g being infs-preserving map of S,T st LowerAdj g is waybelow-preserving holds g is directed-sups-preserving; definition let S,T be TopSpace; let f be map of S,T; attr f is relatively_open means :: WAYBEL34:def 9 for V being open Subset of S holds f.:V is open Subset of T|rng f; end; theorem :: WAYBEL34:26 for X,Y being non empty TopSpace for d being map of X, Y holds d is relatively_open iff corestr d is open; theorem :: WAYBEL34:27 :: requirement of 1.5. REMARK, p. 181 for S,T being complete LATTICE, g being infs-preserving map of S,T for X being Scott TopAugmentation of T for Y being Scott TopAugmentation of S for V being open Subset of X holds (LowerAdj g).:V = (rng LowerAdj g) /\ uparrow ((LowerAdj g).:V); theorem :: WAYBEL34:28 :: 1.5. REMARK, (2) => (2'), p. 181 for S,T being complete LATTICE, g being infs-preserving map of S,T for X being Scott TopAugmentation of T for Y being Scott TopAugmentation of S st for V being open Subset of X holds uparrow ((LowerAdj g).:V) is open Subset of Y holds for d being map of X, Y st d = LowerAdj g holds d is relatively_open; definition let X,Y be complete LATTICE; let f be sups-preserving map of X,Y; cluster Image f -> complete; end; theorem :: WAYBEL34:29 :: 1.5. REMARK, (2') => (2''), p. 181 for S,T being complete LATTICE, g being infs-preserving map of S,T for X being Scott TopAugmentation of T for Y being Scott TopAugmentation of S for Z being Scott TopAugmentation of Image LowerAdj g for d being map of X, Y, d' being map of X, Z st d = LowerAdj g & d' = d holds d is relatively_open implies d' is open; theorem :: WAYBEL34:30 for T1, T2, S1, S2 being TopStruct st the TopStruct of T1 = the TopStruct of T2 & the TopStruct of S1 = the TopStruct of S2 holds S1 is SubSpace of T1 implies S2 is SubSpace of T2; theorem :: WAYBEL34:31 for T being TopStruct holds T|[#]T = the TopStruct of T; theorem :: WAYBEL34:32 :: 1.6. COROLLARY, p. 181 for S,T being complete LATTICE, g being infs-preserving map of S,T st g is one-to-one for X being Scott TopAugmentation of T for Y being Scott TopAugmentation of S for d being map of X,Y st d = LowerAdj g holds g is directed-sups-preserving iff d is open; definition let X be complete LATTICE; let f be projection map of X,X; cluster Image f -> complete; end; theorem :: WAYBEL34:33 for L being complete LATTICE, k being kernel map of L,L holds corestr k is infs-preserving & inclusion k is sups-preserving & LowerAdj corestr k = inclusion k & UpperAdj inclusion k = corestr k; theorem :: WAYBEL34:34 for L being complete LATTICE, k being kernel map of L,L holds k is directed-sups-preserving iff corestr k is directed-sups-preserving; theorem :: WAYBEL34:35 :: 1.7. COROLLARY, (1) <=> (2), p. 181 for L being complete LATTICE, k being kernel map of L,L holds k is directed-sups-preserving iff for X being Scott TopAugmentation of Image k for Y being Scott TopAugmentation of L for V being Subset of L st V is open Subset of X holds uparrow V is open Subset of Y; theorem :: WAYBEL34:36 for L being complete LATTICE for S being sups-inheriting non empty full SubRelStr of L for x,y being Element of L, a,b being Element of S st a = x & b = y holds x << y implies a << b; theorem :: WAYBEL34:37 :: 1.7. COROLLARY, (1) => (3), p. 181 for L being complete LATTICE, k being kernel map of L,L st k is directed-sups-preserving for x,y being Element of L, a,b being Element of Image k st a = x & b = y holds x << y iff a << b; theorem :: WAYBEL34:38 :: 1.7. COROLLARY, (3) => (1), p. 181 for L being complete LATTICE, k being kernel map of L,L st Image k is continuous & for x,y being Element of L, a,b being Element of Image k st a = x & b = y holds x << y iff a << b holds k is directed-sups-preserving; theorem :: WAYBEL34:39 for L being complete LATTICE, c being closure map of L,L holds corestr c is sups-preserving & inclusion c is infs-preserving & UpperAdj corestr c = inclusion c & LowerAdj inclusion c = corestr c; theorem :: WAYBEL34:40 for L being complete LATTICE, c being closure map of L,L holds Image c is directed-sups-inheriting iff inclusion c is directed-sups-preserving; theorem :: WAYBEL34:41 :: 1.8. COROLLARY, (1) <=> (2), p. 182 for L being complete LATTICE, c being closure map of L,L holds Image c is directed-sups-inheriting iff for X being Scott TopAugmentation of Image c for Y being Scott TopAugmentation of L for f being map of Y,X st f = c holds f is open; theorem :: WAYBEL34:42 :: 1.8. COROLLARY, (1) => (3), p. 182 for L being complete LATTICE, c being closure map of L,L holds Image c is directed-sups-inheriting implies corestr c is waybelow-preserving; theorem :: WAYBEL34:43 :: 1.8. COROLLARY, (3) => (1), p. 182 :: SHOULD BE: :: for L being complete LATTICE, c being closure map of L,L :: st :: Image c is continuous & corestr c is waybelow-preserving :: holds Image c is directed-sups-inheriting :: ------------------------ a bug ??? for L being continuous complete LATTICE, c being closure map of L,L st corestr c is waybelow-preserving holds Image c is directed-sups-inheriting; begin ::<section3>Duality of subcategories of {\it INF} and {\it SUP}</section3> definition :: 1.9. DEFINITION, p. 182 let W be non empty set; func W-INF(SC)_category -> strict non empty subcategory of W-INF_category means :: WAYBEL34:def 10 (for a being object of W-INF_category holds a is object of it) & (for a,b being object of W-INF_category for a',b' being object of it st a' = a & b' = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a',b'^> iff @f is directed-sups-preserving); end; definition :: 1.9. DEFINITION, p. 182 let W be with_non-empty_element set; func W-SUP(SO)_category -> strict non empty subcategory of W-SUP_category means :: WAYBEL34:def 11 (for a being object of W-SUP_category holds a is object of it) & (for a,b being object of W-SUP_category for a',b' being object of it st a' = a & b' = b & <^a,b^> <> {} for f being Morphism of a,b holds f in <^a',b'^> iff UpperAdj @f is directed-sups-preserving); end; theorem :: WAYBEL34:44 for S being non empty RelStr, T being non empty reflexive antisymmetric RelStr for t being Element of T for X being non empty Subset of S holds S --> t preserves_sup_of X & S --> t preserves_inf_of X; theorem :: WAYBEL34:45 for S being non empty RelStr for T being lower-bounded non empty reflexive antisymmetric RelStr holds S --> Bottom T is sups-preserving; theorem :: WAYBEL34:46 for S being non empty RelStr for T being upper-bounded non empty reflexive antisymmetric RelStr holds S --> Top T is infs-preserving; definition :: WAYBEL24 let S be non empty RelStr; let T be upper-bounded non empty reflexive antisymmetric RelStr; cluster S --> Top T -> directed-sups-preserving infs-preserving; end; definition let S be non empty RelStr; let T be lower-bounded non empty reflexive antisymmetric RelStr; cluster S --> Bottom T -> filtered-infs-preserving sups-preserving; end; definition let S be non empty RelStr; let T be upper-bounded non empty reflexive antisymmetric RelStr; cluster directed-sups-preserving infs-preserving map of S, T; end; definition let S be non empty RelStr; let T be lower-bounded non empty reflexive antisymmetric RelStr; cluster filtered-infs-preserving sups-preserving map of S, T; end; theorem :: WAYBEL34:47 for W being with_non-empty_element set for L being LATTICE holds L is object of W-INF(SC)_category iff L is strict complete & the carrier of L in W; theorem :: WAYBEL34:48 for W being with_non-empty_element set for a, b being object of W-INF(SC)_category for f being set holds f in <^a,b^> iff f is directed-sups-preserving infs-preserving map of latt a, latt b; theorem :: WAYBEL34:49 for W being with_non-empty_element set for L being LATTICE holds L is object of W-SUP(SO)_category iff L is strict complete & the carrier of L in W; theorem :: WAYBEL34:50 for W being with_non-empty_element set for a, b being object of W-SUP(SO)_category for f being set holds f in <^a,b^> iff ex g being sups-preserving map of latt a, latt b st g = f & UpperAdj g is directed-sups-preserving; theorem :: WAYBEL34:51 :: Remark after 1.9. DEFINITION, p. 182 for W being with_non-empty_element set holds W-INF(SC)_category = Intersect(W-INF_category, W-UPS_category); definition :: 1.9. DEFINITION, p. 182 let W be with_non-empty_element set; func W-CL_category -> strict full non empty subcategory of W-INF(SC)_category means :: WAYBEL34:def 12 for a being object of W-INF(SC)_category holds a is object of it iff latt a is continuous; end; definition let W be with_non-empty_element set; :: COS ZLE!!! To jest wniosek z rejestracji warunkowej YELLOW21:condreg 9, :: a jest potrzebna rejstracja aby zadzialalo nizej cluster W-CL_category -> with_complete_lattices; end; theorem :: WAYBEL34:52 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-CL_category iff L is strict complete continuous; theorem :: WAYBEL34:53 for W being with_non-empty_element set for a,b being object of W-CL_category for f being set holds f in <^a,b^> iff f is infs-preserving directed-sups-preserving map of latt a, latt b; definition :: 1.9. DEFINITION, p. 182 let W be with_non-empty_element set; func W-CL-opp_category -> strict full non empty subcategory of W-SUP(SO)_category means :: WAYBEL34:def 13 for a being object of W-SUP(SO)_category holds a is object of it iff latt a is continuous; end; theorem :: WAYBEL34:54 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-CL-opp_category iff L is strict complete continuous; theorem :: WAYBEL34:55 for W being with_non-empty_element set for a, b being object of W-CL-opp_category for f being set holds f in <^a,b^> iff ex g being sups-preserving map of latt a, latt b st g = f & UpperAdj g is directed-sups-preserving; :: 1.10. THEOREM, p. 182 :::::::::::::::::::::::::::::::::::::: theorem :: WAYBEL34:56 for W being with_non-empty_element set holds W-INF(SC)_category, W-SUP(SO)_category are_anti-isomorphic_under W LowerAdj; theorem :: WAYBEL34:57 for W being with_non-empty_element set holds W-SUP(SO)_category, W-INF(SC)_category are_anti-isomorphic_under W UpperAdj; theorem :: WAYBEL34:58 for W being with_non-empty_element set holds W-CL_category, W-CL-opp_category are_anti-isomorphic_under W LowerAdj; theorem :: WAYBEL34:59 for W being with_non-empty_element set holds W-CL-opp_category, W-CL_category are_anti-isomorphic_under W UpperAdj; begin ::<section4>Compact preserving maps and sup-semilattices morphisms</section4> definition let S,T be non empty reflexive RelStr; let f be map of S,T; attr f is compact-preserving means :: WAYBEL34:def 14 for s being Element of S st s is compact holds f.s is compact; end; theorem :: WAYBEL34:60 :: 1.11. PROPOSITION, (1) => (2) p.183 for S,T being complete LATTICE, d being sups-preserving map of T,S st d is waybelow-preserving holds d is compact-preserving; theorem :: WAYBEL34:61 :: 1.11. PROPOSITION, (2) => (1) p.183 for S,T being complete LATTICE, d being sups-preserving map of T,S st T is algebraic & d is compact-preserving holds d is waybelow-preserving; theorem :: WAYBEL34:62 for R,S,T being non empty RelStr, X being Subset of R for f being map of R,S for g being map of S,T st f preserves_sup_of X & g preserves_sup_of f.:X holds g*f preserves_sup_of X; definition let S,T be non empty RelStr; let f be map of S,T; attr f is finite-sups-preserving means :: WAYBEL34:def 15 for X being finite Subset of S holds f preserves_sup_of X; attr f is bottom-preserving means :: WAYBEL34:def 16 f preserves_sup_of {}S; end; theorem :: WAYBEL34:63 for R,S,T being non empty RelStr for f being map of R,S for g being map of S,T st f is finite-sups-preserving & g is finite-sups-preserving holds g*f is finite-sups-preserving; definition let S,T be non empty antisymmetric lower-bounded RelStr; let f be map of S,T; redefine attr f is bottom-preserving means :: WAYBEL34:def 17 f.Bottom S = Bottom T; end; definition let L be non empty RelStr; let S be SubRelStr of L; attr S is finite-sups-inheriting means :: WAYBEL34:def 18 for X being finite Subset of S st ex_sup_of X,L holds "\/"(X,L) in the carrier of S; attr S is bottom-inheriting means :: WAYBEL34:def 19 Bottom L in the carrier of S; end; definition let S,T be non empty RelStr; cluster sups-preserving -> bottom-preserving map of S,T; end; definition let L be lower-bounded antisymmetric non empty RelStr; cluster finite-sups-inheriting -> bottom-inheriting join-inheriting SubRelStr of L; end; definition let L be non empty RelStr; cluster sups-inheriting -> finite-sups-inheriting SubRelStr of L; end; definition let S,T be lower-bounded non empty Poset; cluster sups-preserving map of S,T; end; definition let L be lower-bounded antisymmetric non empty RelStr; cluster bottom-inheriting -> non empty lower-bounded (full SubRelStr of L); end; definition let L be lower-bounded antisymmetric non empty RelStr; cluster non empty sups-inheriting finite-sups-inheriting bottom-inheriting full SubRelStr of L; end; theorem :: WAYBEL34:64 for L being lower-bounded antisymmetric non empty RelStr for S being non empty bottom-inheriting full SubRelStr of L holds Bottom S = Bottom L; definition let L be with_suprema lower-bounded non empty Poset; cluster bottom-inheriting join-inheriting -> finite-sups-inheriting (full SubRelStr of L); end; theorem :: WAYBEL34:65 for S,T being non empty RelStr, f being map of S,T st f is finite-sups-preserving holds f is join-preserving bottom-preserving; theorem :: WAYBEL34:66 for S,T being lower-bounded with_suprema Poset, f being map of S,T st f is join-preserving bottom-preserving holds f is finite-sups-preserving; definition let S,T be non empty RelStr; cluster sups-preserving -> finite-sups-preserving map of S,T; cluster finite-sups-preserving -> join-preserving bottom-preserving map of S,T; end; definition let S be non empty RelStr; let T be lower-bounded non empty reflexive antisymmetric RelStr; cluster sups-preserving finite-sups-preserving map of S,T; end; definition :: WAYBEL13:15 let L be lower-bounded non empty Poset; cluster CompactSublatt L -> lower-bounded; end; theorem :: WAYBEL34:67 for S being RelStr, T being non empty RelStr, f being map of S,T for S' being SubRelStr of S for T' being SubRelStr of T st f.:the carrier of S' c= the carrier of T' holds f|the carrier of S' is map of S', T'; theorem :: WAYBEL34:68 for S,T being LATTICE, f being join-preserving map of S,T for S' being non empty join-inheriting full SubRelStr of S for T' being non empty join-inheriting full SubRelStr of T for g being map of S', T' st g = f|the carrier of S' holds g is join-preserving; theorem :: WAYBEL34:69 for S,T being lower-bounded LATTICE for f being finite-sups-preserving map of S,T for S' being non empty finite-sups-inheriting full SubRelStr of S for T' being non empty finite-sups-inheriting full SubRelStr of T for g being map of S', T' st g = f|the carrier of S' holds g is finite-sups-preserving; definition let L be complete LATTICE; cluster CompactSublatt L -> finite-sups-inheriting; end; theorem :: WAYBEL34:70 for S,T being complete LATTICE for d being sups-preserving map of T,S holds d is compact-preserving iff d|the carrier of CompactSublatt T is finite-sups-preserving map of CompactSublatt T, CompactSublatt S; theorem :: WAYBEL34:71 :: 1.12. COROLLARY, p. 183 for S,T being complete LATTICE st T is algebraic for g being infs-preserving map of S,T holds g is directed-sups-preserving iff (LowerAdj g)|the carrier of CompactSublatt T is finite-sups-preserving map of CompactSublatt T, CompactSublatt S;

Back to top