:: Duality Based on Galois Connection. Part I
:: by Grzegorz Bancerek
::
:: Received August 8, 2001
:: Copyright (c) 2001-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REWRITE1, WAYBEL_0, WAYBEL_1, FUNCT_1, XBOOLE_0, ORDERS_2,
SEQM_3, SUBSET_1, XXREAL_0, RELAT_1, LATTICES, EQREL_1, ORDINAL2,
STRUCT_0, ARYTM_0, ALTCAT_1, CAT_1, ZFMISC_1, YELLOW21, FILTER_0,
WELLORD1, ORDERS_1, SETFAM_1, QC_LANG1, TARSKI, FUNCTOR0, FUNCT_2,
WAYBEL11, YELLOW_9, RCOMP_1, CARD_FIL, YELLOW_0, RELAT_2, WAYBEL_3,
LATTICE3, PRE_TOPC, GROUP_6, ALTCAT_2, FUNCOP_1, YELLOW20, YELLOW18,
WAYBEL_8, FINSET_1, WAYBEL34;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, ORDERS_1, DOMAIN_1,
FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, 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 WELLORD1, BORSUK_1, T_0TOPSP, WAYBEL_8, WAYBEL11, YELLOW_9,
WAYBEL18, YELLOW18, YELLOW20, YELLOW21, WAYBEL20;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELSET_1, FUNCT_2, FINSET_1,
STRUCT_0, PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0, ALTCAT_2, FUNCTOR0,
WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_7, WAYBEL_8,
WAYBEL10, WAYBEL11, FUNCTOR2, ALTCAT_4, LATTICE5, WAYBEL17, YELLOW_9,
WAYBEL21, YELLOW18, YELLOW21, RELAT_1;
requirements SUBSET, BOOLE;
begin
::Infs-preserving and sups-preserving maps
registration
let S,T be complete LATTICE;
cluster Galois for Connection of S,T;
end;
theorem :: WAYBEL34:1
for S,T, S9,T9 being non empty RelStr
st the RelStr of S = the RelStr of S9 & the RelStr of T = the RelStr of T9
for c being Connection of S,T, c9 being Connection of S9,T9 st c = c9
holds c is Galois implies c9 is Galois;
definition
let S,T be LATTICE;
let g be Function of S,T;
assume that
S is complete and
g is infs-preserving;
func LowerAdj g -> Function of T,S means
:: WAYBEL34:def 1
[g, it] is Galois;
end;
definition
let S,T be LATTICE;
let d be Function of T,S;
assume that
T is complete and
d is sups-preserving;
func UpperAdj d -> Function of S,T means
:: WAYBEL34:def 2
[it, d] is Galois;
end;
registration
let S,T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster LowerAdj g -> lower_adjoint;
end;
registration
let S,T be complete LATTICE;
let d be sups-preserving Function of T,S;
cluster UpperAdj d -> upper_adjoint;
end;
theorem :: WAYBEL34:2
for S,T being complete LATTICE for g being infs-preserving Function 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 Function 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 -> Function of S opp, T opp equals
:: WAYBEL34:def 3
f;
end;
registration
let S,T be complete LATTICE;
let g be infs-preserving Function of S,T;
cluster g opp -> lower_adjoint;
end;
registration
let S,T be complete LATTICE;
let d be sups-preserving Function of S,T;
cluster d opp -> upper_adjoint;
end;
theorem :: WAYBEL34:4
for S,T being complete LATTICE for g being infs-preserving Function of S, T
holds LowerAdj g = UpperAdj (g opp);
theorem :: WAYBEL34:5
for S,T being complete LATTICE for d being sups-preserving Function 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 Function of L1,L2
for g2 being infs-preserving Function 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 Function of L1,L2
for d2 being sups-preserving Function 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 Function 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 Function of S,T
holds LowerAdj UpperAdj d = d;
theorem :: WAYBEL34:12
for C being non empty AltCatStr
for a,b,f being object 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 Function 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 Function of latt a, latt b
holds f in <^a,b^> iff f is sups-preserving;
end;
registration
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 Function 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 Function 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;
registration
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
::Scott continuous maps and continuous lattices
theorem :: WAYBEL34:21 :: 1.4. THEOREM, (1) <=> (2), p. 180
for S,T being complete LATTICE, g being infs-preserving Function 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 Function 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:22 :: 1.4. THEOREM, (1) => (3), p. 180
for S,T being complete LATTICE, g being infs-preserving Function of S,T holds
g is directed-sups-preserving implies LowerAdj g is waybelow-preserving;
theorem :: WAYBEL34:23 :: 1.4. THEOREM, (3+) => (1), p. 180
for S being complete LATTICE for T being complete continuous LATTICE
for g being infs-preserving Function of S,T
st LowerAdj g is waybelow-preserving holds g is directed-sups-preserving;
definition
let S,T be TopSpace;
let f be Function 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:24
for X,Y being non empty TopSpace for d being Function of X, Y holds
d is relatively_open iff corestr d is open;
theorem :: WAYBEL34:25 :: requirement of 1.5. REMARK, p. 181
for S,T being complete LATTICE, g being infs-preserving Function 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:26 :: 1.5. REMARK, (2) => (2'), p. 181
for S,T being complete LATTICE, g being infs-preserving Function 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 Function of X, Y st d = LowerAdj g holds d is relatively_open;
registration
let X,Y be complete LATTICE;
let f be sups-preserving Function of X,Y;
cluster Image f -> complete;
end;
theorem :: WAYBEL34:27 :: 1.5. REMARK, (2') => (2''), p. 181
for S,T being complete LATTICE, g being infs-preserving Function 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 Function of X, Y, d9 being Function
of X, Z st d = LowerAdj g & d9 = d
holds d is relatively_open implies d9 is open;
theorem :: WAYBEL34:28 :: 1.6. COROLLARY, p. 181
for S,T being complete LATTICE, g being infs-preserving Function 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 Function of X,Y st d = LowerAdj g holds
g is directed-sups-preserving iff d is open;
registration
let X be complete LATTICE;
let f be projection Function of X,X;
cluster Image f -> complete;
end;
theorem :: WAYBEL34:29
for L being complete LATTICE, k being kernel Function 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:30
for L being complete LATTICE, k being kernel Function of L,L holds
k is directed-sups-preserving iff corestr k is directed-sups-preserving;
theorem :: WAYBEL34:31 :: 1.7. COROLLARY, (1) <=> (2), p. 181
for L being complete LATTICE, k being kernel Function 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:32
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:33 :: 1.7. COROLLARY, (1) => (3), p. 181
for L being complete LATTICE, k being kernel Function 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:34 :: 1.7. COROLLARY, (3) => (1), p. 181
for L being complete LATTICE, k being kernel Function 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:35
for L being complete LATTICE, c being closure Function 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:36
for L being complete LATTICE, c being closure Function of L,L holds
Image c is directed-sups-inheriting iff
inclusion c is directed-sups-preserving;
theorem :: WAYBEL34:37 :: 1.8. COROLLARY, (1) <=> (2), p. 182
for L being complete LATTICE, c being closure Function 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 Function of Y,X st f = c holds f is open;
theorem :: WAYBEL34:38 :: 1.8. COROLLARY, (1) => (3), p. 182
for L being complete LATTICE, c being closure Function of L,L holds
Image c is directed-sups-inheriting implies corestr c is waybelow-preserving;
theorem :: WAYBEL34:39 :: 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 Function of L,L st
corestr c is waybelow-preserving holds Image c is directed-sups-inheriting;
begin
::Duality of subcategories of {\it INF} and {\it SUP}
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 a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds
f in <^a9,b9^> 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 a9,b9 being Object of it st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds
f in <^a9,b9^> iff UpperAdj @f is directed-sups-preserving;
end;
theorem :: WAYBEL34:40
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:41
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:42
for S being non empty RelStr
for T being upper-bounded non empty reflexive antisymmetric RelStr
holds S --> Top T is infs-preserving;
registration :: 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;
registration
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;
registration
let S be non empty RelStr;
let T be upper-bounded non empty reflexive antisymmetric RelStr;
cluster directed-sups-preserving infs-preserving for Function of S, T;
end;
registration
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster filtered-infs-preserving sups-preserving for Function of S, T;
end;
theorem :: WAYBEL34:43
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:44
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 Function of latt a, latt b;
theorem :: WAYBEL34:45
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:46
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 Function of latt a, latt b st g = f &
UpperAdj g is directed-sups-preserving;
theorem :: WAYBEL34:47 :: 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;
registration
let W be with_non-empty_element set;
cluster W-CL_category -> with_complete_lattices;
end;
theorem :: WAYBEL34:48
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:49
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 Function 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:50
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:51
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 Function of latt a, latt b st g = f &
UpperAdj g is directed-sups-preserving;
:: 1.10. THEOREM, p. 182
theorem :: WAYBEL34:52
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:53
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:54
for W being with_non-empty_element set holds
W-CL_category, W-CL-opp_category are_anti-isomorphic_under W LowerAdj;
theorem :: WAYBEL34:55
for W being with_non-empty_element set holds
W-CL-opp_category, W-CL_category are_anti-isomorphic_under W UpperAdj;
begin
::Compact preserving maps and sup-semilattices morphisms
definition
let S,T be non empty reflexive RelStr;
let f be Function 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:56 :: 1.11. PROPOSITION, (1) => (2) p.183
for S,T being complete LATTICE, d being sups-preserving Function of T,S
st d is waybelow-preserving holds d is compact-preserving;
theorem :: WAYBEL34:57 :: 1.11. PROPOSITION, (2) => (1) p.183
for S,T being complete LATTICE, d being sups-preserving Function of T,S
st T is algebraic & d is compact-preserving holds d is waybelow-preserving;
theorem :: WAYBEL34:58
for R,S,T being non empty RelStr, X being Subset of R
for f being Function of R,S for g being Function 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 Function 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:59
for R,S,T being non empty RelStr
for f being Function of R,S for g being Function 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 Function 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;
registration
let S,T be non empty RelStr;
cluster sups-preserving -> bottom-preserving for Function of S,T;
end;
registration
let L be lower-bounded antisymmetric non empty RelStr;
cluster finite-sups-inheriting ->
bottom-inheriting join-inheriting for SubRelStr of L;
end;
registration
let L be non empty RelStr;
cluster sups-inheriting -> finite-sups-inheriting for SubRelStr of L;
end;
registration
let S,T be lower-bounded non empty Poset;
cluster sups-preserving for Function of S,T;
end;
registration
let L be lower-bounded antisymmetric non empty RelStr;
cluster bottom-inheriting -> non empty lower-bounded for
full SubRelStr of L;
end;
registration
let L be lower-bounded antisymmetric non empty RelStr;
cluster non empty sups-inheriting finite-sups-inheriting bottom-inheriting
full for SubRelStr of L;
end;
theorem :: WAYBEL34:60
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;
registration
let L be with_suprema lower-bounded non empty Poset;
cluster bottom-inheriting join-inheriting -> finite-sups-inheriting
for full SubRelStr of L;
end;
theorem :: WAYBEL34:61
for S,T being non empty RelStr, f being Function of S,T
st f is finite-sups-preserving holds f is join-preserving bottom-preserving;
theorem :: WAYBEL34:62
for S,T being lower-bounded with_suprema Poset, f being Function of S,T
st f is join-preserving bottom-preserving holds f is finite-sups-preserving;
registration
let S,T be non empty RelStr;
cluster sups-preserving -> finite-sups-preserving for Function of S,T;
cluster finite-sups-preserving ->
join-preserving bottom-preserving for Function of S,T;
end;
registration
let S be non empty RelStr;
let T be lower-bounded non empty reflexive antisymmetric RelStr;
cluster sups-preserving finite-sups-preserving for Function of S,T;
end;
registration :: WAYBEL13:15
let L be lower-bounded non empty Poset;
cluster CompactSublatt L -> lower-bounded;
end;
theorem :: WAYBEL34:63
for S being RelStr, T being non empty RelStr, f being Function of S,T
for S9 being SubRelStr of S for T9 being SubRelStr of T
st f.:the carrier of S9 c= the carrier of T9
holds f|the carrier of S9 is Function of S9, T9;
theorem :: WAYBEL34:64
for S,T being LATTICE, f being join-preserving Function of S,T
for S9 being non empty join-inheriting full SubRelStr of S
for T9 being non empty join-inheriting full SubRelStr of T
for g being Function of S9, T9 st g = f|the carrier of S9
holds g is join-preserving;
theorem :: WAYBEL34:65
for S,T being lower-bounded LATTICE
for f being finite-sups-preserving Function of S,T
for S9 being non empty finite-sups-inheriting full SubRelStr of S
for T9 being non empty finite-sups-inheriting full SubRelStr of T
for g being Function of S9, T9 st g = f|the carrier of S9
holds g is finite-sups-preserving;
registration
let L be complete LATTICE;
cluster CompactSublatt L -> finite-sups-inheriting;
end;
theorem :: WAYBEL34:66
for S,T being complete LATTICE
for d being sups-preserving Function of T,S holds d is compact-preserving
iff d|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S;
theorem :: WAYBEL34:67 :: 1.12. COROLLARY, p. 183
for S,T being complete LATTICE st T is algebraic
for g being infs-preserving Function of S,T holds
g is directed-sups-preserving iff
(LowerAdj g)|the carrier of CompactSublatt T is
finite-sups-preserving Function of CompactSublatt T, CompactSublatt S;