:: Closure Operators and Subalgebras
:: by Grzegorz Bancerek
::
:: Received January 15, 1997
:: Copyright (c) 1997-2026 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 XBOOLE_0, ORDERS_2, CAT_1, STRUCT_0, YELLOW_0, SUBSET_1, TARSKI,
XXREAL_0, RELAT_1, ARYTM_0, WELLORD1, FUNCOP_1, WAYBEL_3, RELAT_2,
SEQM_3, FUNCT_1, WAYBEL_1, BINOP_1, WAYBEL_0, ORDINAL2, GROUP_6,
YELLOW_1, FUNCT_2, NEWTON, CARD_3, RLVECT_2, REWRITE1, UNIALG_2,
ZFMISC_1, LATTICE3, LATTICES, EQREL_1, WAYBEL10;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, CARD_3, FUNCOP_1, STRUCT_0, TMAP_1, QUANTAL1, PRALG_1, WELLORD1,
ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2,
WAYBEL_1, WAYBEL_3, YELLOW_7;
constructors TOLER_1, BORSUK_1, PRALG_1, QUANTAL1, ORDERS_3, WAYBEL_1,
WAYBEL_3, TMAP_1;
registrations FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, RELSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RELAT_1, QUANTAL1, ORDERS_2, ORDERS_3, LATTICE3,
YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_3;
equalities XBOOLE_0, LATTICE3, YELLOW_2, STRUCT_0;
expansions TARSKI, XBOOLE_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0;
theorems FUNCT_1, FUNCT_2, YELLOW_0, YELLOW_1, WAYBEL_1, FUNCOP_1, RELSET_1,
SYSREL, ORDERS_2, YELLOW_2, WAYBEL_0, ZFMISC_1, TARSKI, YELLOW_7,
RELAT_1, XBOOLE_0, XBOOLE_1, ORDERS_1, TMAP_1;
schemes YELLOW_0, FUNCT_2, XBOOLE_0;
begin :: Preliminaries
scheme
SubrelstrEx {L() -> non empty RelStr, P[object], a() -> set}:
ex S being non
empty full strict SubRelStr of L() st for x being Element of L() holds x is
Element of S iff P[x]
provided
A1: P[a()] and
A2: a() in the carrier of L()
proof
consider A being set such that
A3: for x being object holds x in A iff x in the carrier of L() & P[x] from
XBOOLE_0:sch 1;
A c= the carrier of L()
by A3;
then reconsider A as non empty Subset of L() by A1,A2,A3;
set S = subrelstr A;
take S;
let x be Element of L();
A4: the carrier of S = A by YELLOW_0:def 15;
hence x is Element of S implies P[x] by A3;
assume P[x];
hence thesis by A3,A4;
end;
scheme
RelstrEq {L1, L2() -> non empty RelStr, P[object], Q[set,set]}:
the RelStr of L1() = the RelStr of L2()
provided
A1: for x being object holds x is Element of L1() iff P[x] and
A2: for x being object holds x is Element of L2() iff P[x] and
A3: for a,b being Element of L1() holds a <= b iff Q[a,b] and
A4: for a,b being Element of L2() holds a <= b iff Q[a,b]
proof
set S1 = L1(), S2 = L2();
A5: the carrier of L1() = the carrier of L2()
proof
hereby
let x be object;
assume x in the carrier of S1;
then reconsider y = x as Element of S1;
P[y] by A1;
then x is Element of S2 by A2;
hence x in the carrier of S2;
end;
let x be object;
assume x in the carrier of S2;
then reconsider y = x as Element of S2;
P[y] by A2;
then x is Element of S1 by A1;
hence thesis;
end;
the InternalRel of L1() = the InternalRel of L2()
proof
let x,y be object;
hereby
assume
A6: [x,y] in the InternalRel of S1;
then reconsider x1 = x, y1 = y as Element of S1 by ZFMISC_1:87;
reconsider x2 = x1, y2 = y1 as Element of S2 by A5;
x1 <= y1 by A6;
then Q[x1,y1] by A3;
then x2 <= y2 by A4;
hence [x,y] in the InternalRel of S2;
end;
assume
A7: [x,y] in the InternalRel of S2;
then reconsider x2 = x, y2 = y as Element of S2 by ZFMISC_1:87;
reconsider x1 = x2, y1 = y2 as Element of S1 by A5;
x2 <= y2 by A7;
then Q[x2,y2] by A4;
then x1 <= y1 by A3;
hence thesis;
end;
hence thesis by A5;
end;
scheme
SubrelstrEq1 {L() -> non empty RelStr, S1, S2() -> non empty full SubRelStr
of L(), P[object]}:
the RelStr of S1() = the RelStr of S2()
provided
A1: for x being object holds x is Element of S1() iff P[x] and
A2: for x being object holds x is Element of S2() iff P[x]
proof
A3: for x being object holds x is Element of S2() iff P[x] by A2;
defpred Q[set,set] means [$1,$2] in the InternalRel of L();
A4: now
let a,b be Element of S1();
reconsider x = a, y = b as Element of L() by YELLOW_0:58;
x <= y iff [x,y] in the InternalRel of L();
hence a <= b iff Q[a,b] by YELLOW_0:59,60;
end;
A5: now
let a,b be Element of S2();
reconsider x = a, y = b as Element of L() by YELLOW_0:58;
x <= y iff [x,y] in the InternalRel of L();
hence a <= b iff Q[a,b] by YELLOW_0:59,60;
end;
A6: for x being object holds x is Element of S1() iff P[x] by A1;
thus thesis from RelstrEq(A6,A3,A4,A5);
end;
scheme
SubrelstrEq2 {L() -> non empty RelStr, S1, S2() -> non empty full SubRelStr
of L(), P[object]}:
the RelStr of S1() = the RelStr of S2()
provided
A1: for x being Element of L() holds x is Element of S1() iff P[x] and
A2: for x being Element of L() holds x is Element of S2() iff P[x]
proof
defpred p[object] means P[$1] & $1 is Element of L();
A3: now
let x be object;
x is Element of S2() implies x is Element of L() by YELLOW_0:58;
hence x is Element of S2() iff p[x] by A2;
end;
A4: now
let x be object;
x is Element of S1() implies x is Element of L() by YELLOW_0:58;
hence x is Element of S1() iff p[x] by A1;
end;
thus thesis from SubrelstrEq1(A4,A3);
end;
theorem Th1:
for R,Q being Relation holds (R c= Q iff R~ c= Q~) & (R~ c= Q iff R c= Q~)
proof
let R,Q be Relation;
A1: Q~~ = Q;
R~~ = R;
hence thesis by A1,SYSREL:11;
end;
theorem Th2:
for L,S being RelStr holds (S is SubRelStr of L iff S opp is
SubRelStr of L opp) & (S opp is SubRelStr of L iff S is SubRelStr of L opp)
proof
let L,S be RelStr;
thus S is SubRelStr of L implies S opp is SubRelStr of L opp
proof
assume that
A1: the carrier of S c= the carrier of L and
A2: the InternalRel of S c= the InternalRel of L;
thus the carrier of S opp c= the carrier of L opp & the InternalRel of S
opp c= the InternalRel of L opp by A1,A2,Th1;
end;
thus S opp is SubRelStr of L opp implies S is SubRelStr of L
proof
assume that
A3: the carrier of S opp c= the carrier of L opp and
A4: the InternalRel of S opp c= the InternalRel of L opp;
thus the carrier of S c= the carrier of L & the InternalRel of S c= the
InternalRel of L by A3,A4,Th1;
end;
thus S opp is SubRelStr of L implies S is SubRelStr of L opp
proof
assume that
A5: the carrier of S opp c= the carrier of L and
A6: the InternalRel of S opp c= the InternalRel of L;
thus the carrier of S c= the carrier of L opp & the InternalRel of S c=
the InternalRel of L opp by A5,A6,Th1;
end;
assume that
A7: the carrier of S c= the carrier of L opp and
A8: the InternalRel of S c= the InternalRel of L opp;
thus the carrier of S opp c= the carrier of L & the InternalRel of S opp c=
the InternalRel of L by A7,A8,Th1;
end;
theorem Th3:
for L,S being RelStr holds (S is full SubRelStr of L iff S opp is
full SubRelStr of L opp) & (S opp is full SubRelStr of L iff S is full
SubRelStr of L opp)
proof
let L,S be RelStr;
A1: ((the InternalRel of L)|_2 the carrier of S)~ = (the InternalRel of L)~
|_2 the carrier of S by ORDERS_1:83;
hereby
assume
A2: S is full SubRelStr of L;
then the InternalRel of S = (the InternalRel of L)|_2 the carrier of S by
YELLOW_0:def 14;
hence S opp is full SubRelStr of L opp by A1,A2,Th2,YELLOW_0:def 14;
end;
A3: ((the InternalRel of L)~|_2 the carrier of S)~ = (the InternalRel of L)~
~|_2 the carrier of S by ORDERS_1:83;
hereby
assume
A4: S opp is full SubRelStr of L opp;
then the InternalRel of S opp = (the InternalRel of L opp)|_2 the carrier
of S by YELLOW_0:def 14;
hence S is full SubRelStr of L by A3,A4,Th2,YELLOW_0:def 14;
end;
hereby
assume
A5: S opp is full SubRelStr of L;
then
the InternalRel of S opp = (the InternalRel of L)|_2 the carrier of S
by YELLOW_0:def 14;
hence S is full SubRelStr of L opp by A1,A5,Th2,YELLOW_0:def 14;
end;
assume
A6: S is full SubRelStr of L opp;
then the InternalRel of S = (the InternalRel of L opp)|_2 the carrier of S
by YELLOW_0:def 14;
hence thesis by A1,A6,Th2,YELLOW_0:def 14;
end;
definition
let L be RelStr, S be full SubRelStr of L;
redefine func S opp -> strict full SubRelStr of L opp; :: redefines opp (YELLOW_7, synonym) → ~ (LATTICE3, definition)
coherence by Th3;
end;
registration
let X be set, L be non empty RelStr;
cluster X --> L -> non-Empty;
coherence
proof
let R be 1-sorted;
assume R in rng (X --> L);
hence thesis by TARSKI:def 1;
end;
end;
registration
let S be RelStr, T be non empty reflexive RelStr;
cluster monotone for Function of S,T;
existence
proof
set c = the Element of T;
take f = S --> c;
let x,y be Element of S;
assume [x,y] in the InternalRel of S;
then
A1: x in the carrier of S by ZFMISC_1:87;
let a,b be Element of T;
assume that
A2: a = f.x and
A3: b = f.y;
a = c by A1,A2,FUNCOP_1:7;
hence a <= b by A1,A3,FUNCOP_1:7;
end;
end;
registration
let L be non empty RelStr;
cluster projection -> monotone idempotent for Function of L,L;
coherence by WAYBEL_1:def 13;
end;
registration
let S,T be non empty reflexive RelStr;
let f be monotone Function of S,T;
cluster corestr f -> monotone;
coherence
proof
let x,y be Element of S;
A1: f.y = (corestr f).y by WAYBEL_1:30;
assume x <= y;
then
A2: f.x <= f.y by WAYBEL_1:def 2;
f.x = (corestr f).x by WAYBEL_1:30;
hence thesis by A2,A1,YELLOW_0:60;
end;
end;
registration
let L be non empty reflexive RelStr;
cluster id L -> sups-preserving infs-preserving;
coherence
proof
thus id L is sups-preserving
proof
let X be Subset of L;
assume ex_sup_of X,L;
hence thesis by FUNCT_1:92;
end;
let X be Subset of L;
assume ex_inf_of X,L;
hence thesis by FUNCT_1:92;
end;
end;
theorem
for L being RelStr, S being Subset of L holds id S is Function of
subrelstr S, L & for f being Function of subrelstr S, L st f = id S holds f is
monotone
proof
let L be RelStr, S be Subset of L;
A1: the carrier of subrelstr S = S by YELLOW_0:def 15;
A2: rng id S = S by RELAT_1:45;
dom id S = S by RELAT_1:45;
hence id S is Function of subrelstr S, L by A1,A2,FUNCT_2:2;
let f be Function of subrelstr S, L;
assume
A3: f = id S;
let x,y be Element of subrelstr S;
assume
A4: [x,y] in the InternalRel of subrelstr S;
let a,b be Element of L;
assume that
A5: a = f.x and
A6: b = f.y;
x in S by A1,A4,ZFMISC_1:87;
then
A7: a = x by A3,A5,FUNCT_1:17;
y in S by A1,A4,ZFMISC_1:87;
then
A8: b = y by A3,A6,FUNCT_1:17;
the InternalRel of subrelstr S c= the InternalRel of L by YELLOW_0:def 13;
hence [a,b] in the InternalRel of L by A4,A7,A8;
end;
registration
let L be non empty reflexive RelStr;
cluster sups-preserving infs-preserving closure kernel one-to-one for
Function
of L,L;
existence
proof
take id L;
thus thesis;
end;
end;
theorem Th5:
for L being non empty reflexive RelStr, c being closure Function
of L,L for x being Element of L holds c.x >= x
proof
let L be non empty reflexive RelStr, c be closure Function of L,L;
let x be Element of L;
c >= id L by WAYBEL_1:def 14;
then c.x >= (id L).x by YELLOW_2:9;
hence thesis;
end;
theorem Th6:
for S,T being RelStr, R being SubRelStr of S for f being Function
of the carrier of S, the carrier of T holds f|R = f|the carrier of R & for x
being set st x in the carrier of R holds (f|R).x = f.x
proof
let S,T be RelStr, R be SubRelStr of S;
let f be Function of the carrier of S, the carrier of T;
the carrier of R c= the carrier of S by YELLOW_0:def 13;
hence f|R = f|the carrier of R by TMAP_1:def 3;
hence thesis by FUNCT_1:49;
end;
theorem Th7:
for S,T being RelStr, f being Function of S,T st f is one-to-one
for R being SubRelStr of S holds f|R is one-to-one
proof
let S,T be RelStr, f be Function of S,T such that
A1: f is one-to-one;
let R be SubRelStr of S;
f|R = f|the carrier of R by Th6;
hence thesis by A1,FUNCT_1:52;
end;
registration
let S,T be non empty reflexive RelStr;
let f be monotone Function of S,T;
let R be SubRelStr of S;
cluster f|R -> monotone;
coherence
proof
let x,y be Element of R;
A1: the carrier of R c= the carrier of S by YELLOW_0:def 13;
assume
A2: x <= y;
then
A3: [x,y] in the InternalRel of R;
then
A4: x in the carrier of R by ZFMISC_1:87;
y in the carrier of R by A3,ZFMISC_1:87;
then reconsider a = x, b = y as Element of S by A1;
A5: a <= b by A2,YELLOW_0:59;
A6: f.b = (f|R).y by A4,Th6;
f.a = (f|R).x by A4,Th6;
hence thesis by A5,A6,WAYBEL_1:def 2;
end;
end;
theorem Th8:
for S,T being non empty RelStr, R being non empty SubRelStr of S
for f being Function of S,T, g being Function of T,S st f is one-to-one & g = f
" holds g|Image (f|R) is Function of Image (f|R), R & g|Image (f|R) = (f|R)"
proof
let S,T be non empty RelStr, R be non empty SubRelStr of S;
let f be Function of S,T, g be Function of T,S;
assume that
A1: f is one-to-one and
A2: g = f";
set h = g|Image (f|R);
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: dom h = the carrier of Image (f|R) by FUNCT_2:def 1;
A5: the carrier of R c= the carrier of S by YELLOW_0:def 13;
rng h c= the carrier of R
proof
let y be object;
assume y in rng h;
then consider x being object such that
A6: x in dom h and
A7: y = h.x by FUNCT_1:def 3;
reconsider x as Element of Image (f|R) by A6;
consider a being Element of R such that
A8: (f|R).a = x by YELLOW_2:10;
A9: f.a = x by A8,Th6;
A10: a in the carrier of R;
y = g.x by A7,Th6;
hence thesis by A1,A2,A5,A3,A10,A9,FUNCT_1:32;
end;
hence h is Function of Image (f|R), R by A4,RELSET_1:4;
A11: rng (f|R) = the carrier of Image (f|R) by YELLOW_0:def 15;
A12: f|R is one-to-one by A1,Th7;
A13: now
let x be object;
A14: dom (f|R) = the carrier of R by FUNCT_2:def 1;
assume
A15: x in the carrier of Image (f|R);
then consider y being object such that
A16: y in dom (f|R) and
A17: x = (f|R).y by A11,FUNCT_1:def 3;
A18: y = (f|R)".x by A12,A16,A17,FUNCT_1:32;
x = f.y by A16,A17,Th6;
then y = g.x by A1,A2,A5,A3,A16,A14,FUNCT_1:32;
hence h.x = (f|R)".x by A15,A18,Th6;
end;
dom ((f|R)") = rng (f|R) by A12,FUNCT_1:33;
hence thesis by A4,A11,A13,FUNCT_1:2;
end;
begin :: The lattice of closure operators
registration
let S be RelStr, T be non empty reflexive RelStr;
cluster MonMaps(S,T) -> non empty;
coherence
proof
set f = the monotone Function of S,T;
f in Funcs (the carrier of S, the carrier of T) by FUNCT_2:8;
hence thesis by YELLOW_1:def 6;
end;
end;
theorem Th9:
for S being RelStr, T being non empty reflexive RelStr, x being
set holds x is Element of MonMaps(S,T) iff x is monotone Function of S,T
proof
let S be RelStr, T be non empty reflexive RelStr;
let x be set;
hereby
assume x is Element of MonMaps(S,T);
then reconsider f = x as Element of MonMaps(S,T);
f is Element of T|^the carrier of S by YELLOW_0:58;
then f in the carrier of T|^the carrier of S;
then f in Funcs(the carrier of S, the carrier of T) by YELLOW_1:28;
then reconsider f as Function of S,T by FUNCT_2:66;
f in the carrier of MonMaps(S,T);
hence x is monotone Function of S,T by YELLOW_1:def 6;
end;
assume x is monotone Function of S,T;
then reconsider f = x as monotone Function of S,T;
f in Funcs(the carrier of S, the carrier of T) by FUNCT_2:8;
hence thesis by YELLOW_1:def 6;
end;
definition
let L be non empty reflexive RelStr;
func ClOpers L -> non empty full strict SubRelStr of MonMaps(L,L) means
:
Def1: for f being Function of L,L holds f is Element of it iff f is closure;
existence
proof
defpred P[set] means $1 is closure Function of L,L;
set h = the closure Function of L,L;
h in Funcs (the carrier of L, the carrier of L) by FUNCT_2:9;
then
A1: h in the carrier of MonMaps(L,L) by YELLOW_1:def 6;
A2: P[h];
consider S being non empty full strict SubRelStr of MonMaps(L,L) such that
A3: for f being Element of MonMaps(L,L) holds f is Element of S iff P[
f] from SubrelstrEx(A2,A1);
take S;
let f be Function of L,L;
hereby
assume
A4: f is Element of S;
then f is Element of MonMaps(L,L) by YELLOW_0:58;
hence f is closure by A3,A4;
end;
assume
A5: f is closure;
f in Funcs (the carrier of L, the carrier of L) by FUNCT_2:9;
then f in the carrier of MonMaps(L,L) by A5,YELLOW_1:def 6;
hence thesis by A3,A5;
end;
correctness
proof
let S1,S2 be non empty full strict SubRelStr of MonMaps(L,L) such that
A6: for f being Function of L,L holds f is Element of S1 iff f is closure and
A7: for f being Function of L,L holds f is Element of S2 iff f is closure;
the carrier of S1 = the carrier of S2
proof
hereby
let x be object;
assume x in the carrier of S1;
then reconsider y = x as Element of S1;
y is Element of MonMaps(L,L) by YELLOW_0:58;
then reconsider y as Function of L,L by Th9;
y is closure by A6;
then y is Element of S2 by A7;
hence x in the carrier of S2;
end;
let x be object;
assume x in the carrier of S2;
then reconsider y = x as Element of S2;
y is Element of MonMaps(L,L) by YELLOW_0:58;
then reconsider y as Function of L,L by Th9;
y is closure by A7;
then y is Element of S1 by A6;
hence thesis;
end;
hence thesis by YELLOW_0:57;
end;
end;
theorem Th10:
for L being non empty reflexive RelStr, x being set holds x is
Element of ClOpers L iff x is closure Function of L,L
by YELLOW_0:58,Def1,Th9;
theorem Th11:
for X being set, L being non empty RelStr for f,g being Function
of X, the carrier of L for x,y being Element of L|^X st x = f & y = g holds x
<= y iff f <= g
proof
let X be set, L be non empty RelStr;
let f,g be Function of X, the carrier of L;
let x,y be Element of L|^X such that
A1: x = f and
A2: y = g;
set J = X --> L;
A3: L|^X = product J by YELLOW_1:def 5;
A4: the carrier of product J = product Carrier J by YELLOW_1:def 4;
then
A5: x <= y iff ex f,g being Function st f = x & g = y &
for i be object st i in
X ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i
& xi <= yi by A3,YELLOW_1:def 4;
hereby
assume
A6: x <= y;
thus f <= g
proof
let i be set;
assume
A7: i in X;
then
A8: J.i = L by FUNCOP_1:7;
ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i &
yi = g.i & xi <= yi by A1,A2,A5,A6,A7;
hence thesis by A8;
end;
end;
assume
A9: for j being set st j in X ex a, b being Element of L st a = f.j & b
= g.j & a <= b;
now
reconsider f9 = f, g9 = g as Function;
take f9, g9;
thus f9 = x & g9 = y by A1,A2;
let i be object;
assume
A10: i in X;
then
A11: J.i = L by FUNCOP_1:7;
ex a, b being Element of L st a = f.i & b = g.i & a <= b by A9,A10;
hence ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f9.i &
yi = g9.i & xi <= yi by A11;
end;
hence thesis by A4,A3,YELLOW_1:def 4;
end;
theorem Th12:
for L being complete LATTICE for c1,c2 being Function of L,L for
x,y being Element of ClOpers L st x = c1 & y = c2 holds x <= y iff c1 <= c2
proof
let L be complete LATTICE;
let c1,c2 be Function of L,L, x,y be Element of ClOpers L such that
A1: x = c1 and
A2: y = c2;
reconsider x9 = x, y9 = y as Element of MonMaps(L,L) by YELLOW_0:58;
reconsider x99 = x9, y99 = y9 as Element of L|^the carrier of L by
YELLOW_0:58;
x99 <= y99 iff x9 <= y9 by YELLOW_0:59,60;
hence thesis by A1,A2,Th11,YELLOW_0:59,60;
end;
theorem Th13:
for L being reflexive RelStr, S1, S2 being full SubRelStr of L
st the carrier of S1 c= the carrier of S2 holds S1 is SubRelStr of S2
proof
let L be reflexive RelStr, S1,S2 be full SubRelStr of L;
assume
A1: the carrier of S1 c= the carrier of S2;
hence the carrier of S1 c= the carrier of S2;
let x,y be object;
assume
A2: [x,y] in the InternalRel of S1;
then
A3: x in the carrier of S1 by ZFMISC_1:87;
reconsider x,y as Element of S1 by A2,ZFMISC_1:87;
the carrier of S1 c= the carrier of L by YELLOW_0:def 13;
then reconsider a = x, b = y as Element of L by A3;
reconsider x9 = x, y9 = y as Element of S2 by A1,A3;
x <= y by A2;
then a <= b by YELLOW_0:59;
then x9 <= y9 by A1,A3,YELLOW_0:60;
hence thesis;
end;
theorem Th14:
for L being complete LATTICE for c1,c2 being closure Function of
L,L holds c1 <= c2 iff Image c2 is SubRelStr of Image c1
proof
let L be complete LATTICE;
let c1,c2 be closure Function of L,L;
hereby
assume
A1: c1 <= c2;
the carrier of Image c2 c= the carrier of Image c1
proof
let x be object;
assume x in the carrier of Image c2;
then consider y being Element of L such that
A2: c2.y = x by YELLOW_2:10;
A3: c2.(c2.y) = c2.y by YELLOW_2:18;
A4: c1.(c2.y) <= c2.(c2.y) by A1,YELLOW_2:9;
c2.y <= c1.(c2.y) by Th5;
then c1.(c2.y) = x by A2,A4,A3,ORDERS_2:2;
then x in rng c1 by FUNCT_2:4;
hence thesis by YELLOW_0:def 15;
end;
hence Image c2 is SubRelStr of Image c1 by Th13;
end;
assume that
A5: the carrier of Image c2 c= the carrier of Image c1 and
the InternalRel of Image c2 c= the InternalRel of Image c1;
now
let x be Element of L;
c2.x in rng c2 by FUNCT_2:4;
then c2.x in the carrier of Image c2 by YELLOW_0:def 15;
then ex a being Element of L st c1.a = c2.x by A5,YELLOW_2:10;
then
A6: c1.(c2.x) = c2.x by YELLOW_2:18;
x <= c2.x by Th5;
hence c1.x <= c2.x by A6,WAYBEL_1:def 2;
end;
hence thesis by YELLOW_2:9;
end;
begin :: The lattice of closure systems
definition
let L be RelStr;
func Sub L -> strict non empty RelStr means
: Def2:
( for x being object holds
x is Element of it iff x is strict SubRelStr of L) & for a,b being Element of
it holds a <= b iff ex R being RelStr st b = R & a is SubRelStr of R;
existence
proof
set X = {RelStr(#A,B#) where A is Subset of L, B is Relation of A,A: B c=
the InternalRel of L};
A1: the InternalRel of subrelstr {}L c= the InternalRel of L by YELLOW_0:def 13
;
the carrier of subrelstr {}L = {}L by YELLOW_0:def 15;
then subrelstr {}L in X by A1;
then reconsider X as non empty set;
defpred P[set,set] means ex R being RelStr st $2 = R & $1 is SubRelStr of
R;
consider S being strict non empty RelStr such that
A2: the carrier of S = X and
A3: for a,b being Element of S holds a <= b iff P[a,b] from YELLOW_0:
sch 1;
take S;
hereby
let x be object;
hereby
assume x is Element of S;
then x in X by A2;
then
ex A being Subset of L, B being Relation of A,A st x = RelStr(#A,B
#) & B c= the InternalRel of L;
hence x is strict SubRelStr of L by YELLOW_0:def 13;
end;
assume x is strict SubRelStr of L;
then reconsider R = x as strict SubRelStr of L;
A4: the InternalRel of R c= the InternalRel of L by YELLOW_0:def 13;
the carrier of R c= the carrier of L by YELLOW_0:def 13;
then R in X by A4;
hence x is Element of S by A2;
end;
thus thesis by A3;
end;
correctness
proof
defpred Q[set,set] means ex R being RelStr st $2 = R & $1 is SubRelStr of
R;
defpred P[object] means $1 is strict SubRelStr of L;
let S1,S2 be non empty strict RelStr such that
A5: for x being object holds x is Element of S1 iff P[x] and
A6: for a,b being Element of S1 holds a <= b iff Q[a,b] and
A7: for x being object holds x is Element of S2 iff P[x] and
A8: for a,b being Element of S2 holds a <= b iff Q[a,b];
the RelStr of S1 = the RelStr of S2 from RelstrEq(A5,A7,A6,A8 );
hence thesis;
end;
end;
theorem Th15:
for L,R being RelStr for x,y being Element of Sub L st y = R
holds x <= y iff x is SubRelStr of R
proof
let L,R be RelStr;
let x,y be Element of Sub L;
x <= y iff ex R being RelStr st y = R & x is SubRelStr of R by Def2;
hence thesis;
end;
registration
let L be RelStr;
cluster Sub L -> reflexive antisymmetric transitive;
coherence
proof
set R = Sub L;
thus R is reflexive
proof
let x be Element of R;
reconsider A = x as strict SubRelStr of L by Def2;
A is SubRelStr of A by YELLOW_0:def 13;
hence thesis by Th15;
end;
thus R is antisymmetric
proof
let x,y be Element of R;
reconsider A = x, B = y as strict SubRelStr of L by Def2;
assume that
A1: x <= y and
A2: y <= x;
A3: B is SubRelStr of A by A2,Th15;
then
A4: the carrier of B c= the carrier of A by YELLOW_0:def 13;
A5: A is SubRelStr of B by A1,Th15;
then the carrier of A c= the carrier of B by YELLOW_0:def 13;
then
A6: the carrier of A = the carrier of B by A4;
A7: the InternalRel of B c= the InternalRel of A by A3,YELLOW_0:def 13;
the InternalRel of A c= the InternalRel of B by A5,YELLOW_0:def 13;
hence thesis by A7,A6,XBOOLE_0:def 10;
end;
thus R is transitive
proof
let x,y,z be Element of R;
reconsider A = x, B = y, C = z as strict SubRelStr of L by Def2;
assume that
A8: x <= y and
A9: y <= z;
A10: B is SubRelStr of C by A9,Th15;
then
A11: the carrier of B c= the carrier of C by YELLOW_0:def 13;
A12: the InternalRel of B c= the InternalRel of C by A10,YELLOW_0:def 13;
A13: A is SubRelStr of B by A8,Th15;
then the InternalRel of A c= the InternalRel of B by YELLOW_0:def 13;
then
A14: the InternalRel of A c= the InternalRel of C by A12;
the carrier of A c= the carrier of B by A13,YELLOW_0:def 13;
then the carrier of A c= the carrier of C by A11;
then A is SubRelStr of C by A14,YELLOW_0:def 13;
hence thesis by Th15;
end;
end;
end;
registration
let L be RelStr;
cluster Sub L -> complete;
coherence
proof
now
let X be Subset of Sub L;
now
defpred Q[object] means
ex R being RelStr st R in X & $1 in the InternalRel of R;
defpred P[object] means
ex R being RelStr st R in X & $1 in the carrier of R;
consider Y being set such that
A1: for x being object holds x in Y iff x in the carrier of L & P[x]
from XBOOLE_0:sch 1;
consider S being set such that
A2: for x being object holds x in S iff x in the InternalRel of L & Q
[x] from XBOOLE_0:sch 1;
A3: S c= [:Y,Y:]
proof
let x be object;
assume x in S;
then consider R being RelStr such that
A4: R in X and
A5: x in the InternalRel of R by A2;
the carrier of R c= Y
proof
let x be object;
R is SubRelStr of L by A4,Def2;
then
A6: the carrier of R c= the carrier of L by YELLOW_0:def 13;
assume x in the carrier of R;
hence thesis by A1,A4,A6;
end;
then
A7: [:the carrier of R, the carrier of R:] c= [:Y,Y:] by ZFMISC_1:96;
x in [:the carrier of R, the carrier of R:] by A5;
hence thesis by A7;
end;
A8: S c= the InternalRel of L
by A2;
reconsider S as Relation of Y by A3;
Y c= the carrier of L
by A1;
then reconsider A = RelStr(#Y, S#) as SubRelStr of L by A8,
YELLOW_0:def 13;
reconsider a = A as Element of Sub L by Def2;
take a;
thus X is_<=_than a
proof
let b be Element of Sub L;
reconsider R = b as strict SubRelStr of L by Def2;
assume
A9: b in X;
A10: the InternalRel of R c= S
proof
let x,y be object;
A11: the InternalRel of R c= the InternalRel of L by YELLOW_0:def 13;
assume [x,y] in the InternalRel of R;
hence thesis by A2,A9,A11;
end;
the carrier of R c= Y
proof
let x be object;
A12: the carrier of R c= the carrier of L by YELLOW_0:def 13;
assume x in the carrier of R;
hence thesis by A1,A9,A12;
end;
then R is SubRelStr of A by A10,YELLOW_0:def 13;
hence b <= a by Th15;
end;
let b be Element of Sub L;
reconsider B = b as strict SubRelStr of L by Def2;
assume
A13: X is_<=_than b;
A14: S c= the InternalRel of B
proof
let x,y be object;
assume [x,y] in S;
then consider R being RelStr such that
A15: R in X and
A16: [x,y] in the InternalRel of R by A2;
reconsider c = R as Element of Sub L by A15;
c <= b by A13,A15;
then R is SubRelStr of B by Th15;
then the InternalRel of R c= the InternalRel of B by YELLOW_0:def 13;
hence thesis by A16;
end;
Y c= the carrier of B
proof
let x be object;
assume x in Y;
then consider R being RelStr such that
A17: R in X and
A18: x in the carrier of R by A1;
reconsider c = R as Element of Sub L by A17;
c <= b by A13,A17;
then R is SubRelStr of B by Th15;
then the carrier of R c= the carrier of B by YELLOW_0:def 13;
hence thesis by A18;
end;
then a is SubRelStr of B by A14,YELLOW_0:def 13;
hence a <= b by Th15;
end;
hence ex_sup_of X, Sub L by YELLOW_0:15;
end;
hence thesis by YELLOW_0:53;
end;
end;
registration
let L be complete LATTICE;
cluster infs-inheriting -> non empty for SubRelStr of L;
coherence
proof
let S be SubRelStr of L such that
A1: S is infs-inheriting;
ex_inf_of {}S,L by YELLOW_0:17;
hence thesis by A1;
end;
cluster sups-inheriting -> non empty for SubRelStr of L;
coherence
proof
let S be SubRelStr of L such that
A2: S is sups-inheriting;
ex_sup_of {}S,L by YELLOW_0:17;
hence thesis by A2;
end;
end;
definition
let L be RelStr;
mode System of L is full SubRelStr of L;
end;
notation
let L be non empty RelStr;
let S be System of L;
synonym S is closure for S is infs-inheriting;
end;
registration
let L be non empty RelStr;
cluster subrelstr [#]L -> infs-inheriting sups-inheriting;
coherence
proof
set SL = subrelstr [#]L;
A1: the carrier of SL = the carrier of L by YELLOW_0:def 15;
thus SL is infs-inheriting
by A1;
let X be Subset of SL;
thus thesis by A1;
end;
end;
definition
let L be non empty RelStr;
func ClosureSystems L -> full strict non empty SubRelStr of Sub L means
:
Def3: for R being strict SubRelStr of L holds R is Element of it iff R is
infs-inheriting full;
existence
proof
defpred P[set] means $1 is infs-inheriting full SubRelStr of L;
set SL = subrelstr [#]L;
SL is Element of Sub L by Def2;
then
A1: SL in the carrier of Sub L;
A2: P[SL];
consider S being non empty full strict SubRelStr of Sub L such that
A3: for x being Element of Sub L holds x is Element of S iff P[x] from
SubrelstrEx(A2,A1);
take S;
let R be strict SubRelStr of L;
R is Element of Sub L by Def2;
hence thesis by A3;
end;
correctness
proof
defpred P[object] means $1 is infs-inheriting full strict SubRelStr of L;
let S1,S2 be full strict non empty SubRelStr of Sub L such that
A4: for R being strict SubRelStr of L holds R is Element of S1 iff R
is infs-inheriting full and
A5: for R being strict SubRelStr of L holds R is Element of S2 iff R
is infs-inheriting full;
A6: now
let x be object;
x is Element of S2 implies x is Element of Sub L by YELLOW_0:58;
then x is Element of S2 implies x is strict SubRelStr of L by Def2;
hence x is Element of S2 iff P[x] by A5;
end;
A7: now
let x be object;
x is Element of S1 implies x is Element of Sub L by YELLOW_0:58;
then x is Element of S1 implies x is strict SubRelStr of L by Def2;
hence x is Element of S1 iff P[x] by A4;
end;
the RelStr of S1 = the RelStr of S2 from SubrelstrEq1(A7,A6);
hence thesis;
end;
end;
theorem Th16:
for L being non empty RelStr, x being object holds x is Element of
ClosureSystems L iff x is strict closure System of L
proof
let L be non empty RelStr, x be object;
x is Element of ClosureSystems L implies x is Element of Sub L by YELLOW_0:58
;
then x is Element of ClosureSystems L implies x is strict SubRelStr of L by
Def2;
hence thesis by Def3;
end;
theorem Th17:
for L being non empty RelStr, R being RelStr for x,y being
Element of ClosureSystems L st y = R holds x <= y iff x is SubRelStr of R
proof
let L be non empty RelStr, R be RelStr;
let x,y be Element of ClosureSystems L;
reconsider a = x, b = y as Element of Sub L by YELLOW_0:58;
x <= y iff a <= b by YELLOW_0:59,60;
hence thesis by Th15;
end;
begin :: Isomorphism between closure operators and closure systems
registration
let L be non empty Poset;
let h be closure Function of L,L;
cluster Image h -> infs-inheriting;
coherence by WAYBEL_1:53;
end;
definition
let L be non empty Poset;
func ClImageMap L -> Function of ClOpers L, (ClosureSystems L) opp means
:
Def4: for c being closure Function of L,L holds it.c = Image c;
existence
proof
defpred P[set,set] means ex c being closure Function of L,L st c = $1 & $2
= Image c;
A1: now
let x be Element of ClOpers L;
reconsider c = x as closure Function of L,L by Th10;
reconsider a = Image c as Element of ClosureSystems L by Th16;
take b = a~;
thus P[x, b];
end;
consider f being Function of ClOpers L, (ClosureSystems L) opp such that
A2: for x being Element of ClOpers L holds P[x,f.x] from FUNCT_2:sch
3(A1);
take f;
let c be closure Function of L,L;
c is Element of ClOpers L by Th10;
then
ex c1 being closure Function of L,L st c1 = c & f.c = Image c1 by A2;
hence thesis;
end;
correctness
proof
let f1,f2 be Function of ClOpers L, (ClosureSystems L) opp such that
A3: for c being closure Function of L,L holds f1.c = Image c and
A4: for c being closure Function of L,L holds f2.c = Image c;
now
let x be Element of ClOpers L;
reconsider c = x as closure Function of L,L by Th10;
thus f1.x = Image c by A3
.= f2.x by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
func closure_op S -> Function of L,L means
: Def5:
for x being Element of L
holds it.x = "/\"((uparrow x) /\ the carrier of S,L);
existence
proof
deffunc F(Element of L) = "/\"((uparrow $1) /\ the carrier of S,L);
thus ex f being Function of L,L st for x being Element of L holds f.x = F(
x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let f1,f2 be Function of L,L such that
A1: for x being Element of L holds f1.x = "/\" ((uparrow x) /\ the
carrier of S,L) and
A2: for x being Element of L holds f2.x = "/\" ((uparrow x) /\ the
carrier of S,L);
now
let x be Element of L;
thus f1.x = "/\"((uparrow x) /\ the carrier of S,L) by A1
.= f2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
let L be complete LATTICE;
let S be closure System of L;
cluster closure_op S -> closure;
coherence
proof
set c = closure_op S;
reconsider cc = c*c as Function of L,L;
A1: now
let x be Element of L;
thus
(id L).x = x;
(uparrow x) /\ the carrier of S c= uparrow x by XBOOLE_1:17;
then
A2: x is_<=_than (uparrow x) /\ the carrier of S by YELLOW_2:2;
c.x = "/\" ((uparrow x) /\ the carrier of S,L) by Def5;
hence (id L).x <= c.x by A2,YELLOW_0:33;
end;
now
let x be Element of L;
set y = c.x;
set X = (uparrow x) /\ the carrier of S;
reconsider X as Subset of S by XBOOLE_1:17;
A3: c.y = "/\"((uparrow y) /\ the carrier of S,L) by Def5;
y <= y;
then
A4: y in uparrow y by WAYBEL_0:18;
ex_inf_of X,L by YELLOW_0:17;
then
A5: "/\"(X,L) in the carrier of S by YELLOW_0:def 18;
y = "/\"((uparrow x) /\ the carrier of S,L) by Def5;
then y in (uparrow y) /\ the carrier of S by A5,A4,XBOOLE_0:def 4;
then
A6: c.y <= y by A3,YELLOW_2:22;
A7: c.y >= (id L).y by A1;
thus cc.x = c.y by FUNCT_2:15
.= c.x by A6,A7,ORDERS_2:2;
end;
hence c*c = c by FUNCT_2:63;
hereby
let x,y be Element of L;
A8: ex_inf_of (uparrow x) /\ the carrier of S, L by YELLOW_0:17;
A9: ex_inf_of (uparrow y) /\ the carrier of S, L by YELLOW_0:17;
assume x <= y;
then
A10: (uparrow y) /\ the carrier of S c= (uparrow x) /\ the carrier of S
by WAYBEL_0:22,XBOOLE_1:26;
A11: c.y = "/\"((uparrow y) /\ the carrier of S,L) by Def5;
c.x = "/\"((uparrow x) /\ the carrier of S,L) by Def5;
hence c.x <= c.y by A10,A8,A9,A11,YELLOW_0:35;
end;
let x be set;
assume x in the carrier of L;
then reconsider x as Element of L;
(id L).x <= c.x by A1;
hence thesis;
end;
end;
theorem Th18:
for L being complete LATTICE for S being closure System of L
holds Image closure_op S = the RelStr of S
proof
let L be complete LATTICE;
let S be infs-inheriting full non empty SubRelStr of L;
the carrier of Image closure_op S = the carrier of S
proof
hereby
let x be object;
assume x in the carrier of Image closure_op S;
then reconsider a = x as Element of Image closure_op S;
consider b being Element of L such that
A1: a = (closure_op S).b by YELLOW_2:10;
set X = (uparrow b) /\ the carrier of S;
reconsider X as Subset of S by XBOOLE_1:17;
A2: ex_inf_of X,L by YELLOW_0:17;
a = "/\"(X,L) by A1,Def5;
hence x in the carrier of S by A2,YELLOW_0:def 18;
end;
set c = closure_op S;
let x be object;
assume x in the carrier of S;
then reconsider a = x as Element of S;
reconsider a as Element of L by YELLOW_0:58;
set X = (uparrow a) /\ the carrier of S;
A3: (id L).a = a;
a <= a;
then a in uparrow a by WAYBEL_0:18;
then
A4: a in X by XBOOLE_0:def 4;
c.a = "/\"(X,L) by Def5;
then
A5: c.a <= a by A4,YELLOW_2:22;
id L <= c by WAYBEL_1:def 14;
then a <= c.a by A3,YELLOW_2:9;
then
A6: a = c.a by A5,ORDERS_2:2;
dom c = the carrier of L by FUNCT_2:def 1;
then a in rng closure_op S by A6,FUNCT_1:def 3;
hence thesis by YELLOW_0:def 15;
end;
hence thesis by YELLOW_0:57;
end;
theorem Th19:
for L being complete LATTICE for c being closure Function of L,L
holds closure_op Image c = c
proof
let L be complete LATTICE, c be closure Function of L,L;
now
let x be Element of L;
A1: id L <= c by WAYBEL_1:def 14;
x = (id L).x;
then x <= c.x by A1,YELLOW_2:9;
then
A2: c.x in uparrow x by WAYBEL_0:18;
dom c = the carrier of L by FUNCT_2:def 1;
then c.x in rng c by FUNCT_1:def 3;
then c.x in (uparrow x) /\ rng c by A2,XBOOLE_0:def 4;
then
A3: c.x >= "/\"((uparrow x) /\ rng c, L) by YELLOW_2:22;
c.x is_<=_than (uparrow x) /\ rng c
proof
let z be Element of L;
assume
A4: z in (uparrow x) /\ rng c;
then z in rng c by XBOOLE_0:def 4;
then consider a being object such that
A5: a in dom c and
A6: z = c.a by FUNCT_1:def 3;
reconsider a as Element of L by A5;
z in uparrow x by A4,XBOOLE_0:def 4;
then x <= c.a by A6,WAYBEL_0:18;
then c.x <= c.(c.a) by WAYBEL_1:def 2;
hence thesis by A6,YELLOW_2:18;
end;
then
A7: c.x <= "/\"((uparrow x) /\ rng c, L) by YELLOW_0:33;
rng c = the carrier of Image c by YELLOW_0:def 15;
hence (closure_op Image c).x = "/\"((uparrow x) /\ rng c, L) by Def5
.= c.x by A3,A7,ORDERS_2:2;
end;
hence thesis by FUNCT_2:63;
end;
registration
let L be complete LATTICE;
cluster ClImageMap L -> one-to-one;
coherence
proof
let x,y be Element of ClOpers L;
reconsider a = x, b = y as closure Function of L,L by Th10;
set f = ClImageMap L;
assume f.x = f.y;
then Image a = f.y by Def4
.= Image b by Def4;
hence x = closure_op Image b by Th19
.= y by Th19;
end;
end;
theorem Th20:
for L being complete LATTICE holds (ClImageMap L)" is Function
of (ClosureSystems L) opp, ClOpers L
proof
let L be complete LATTICE;
set f = ClImageMap L;
A1: rng (f") = dom f by FUNCT_1:33;
A2: dom f = the carrier of ClOpers L by FUNCT_2:def 1;
the carrier of (ClosureSystems L) opp c= rng f
proof
let x be object;
assume x in the carrier of (ClosureSystems L) opp;
then reconsider x as Element of (ClosureSystems L) opp;
reconsider x as infs-inheriting full strict SubRelStr of L by Th16;
A3: closure_op x is Element of ClOpers L by Th10;
f.closure_op x = Image closure_op x by Def4
.= x by Th18;
hence thesis by A2,A3,FUNCT_1:def 3;
end;
then
A4: the carrier of (ClosureSystems L) opp = rng f;
dom (f") = rng f by FUNCT_1:33;
hence thesis by A1,A4,FUNCT_2:def 1,RELSET_1:4;
end;
theorem Th21:
for L being complete LATTICE for S being strict closure System
of L holds (ClImageMap L)".S = closure_op S
proof
let L be complete LATTICE;
let S be infs-inheriting full strict SubRelStr of L;
A1: closure_op S is Element of ClOpers L by Th10;
(ClImageMap L).closure_op S = Image closure_op S by Def4
.= S by Th18;
hence thesis by A1,FUNCT_2:26;
end;
registration
let L be complete LATTICE;
cluster ClImageMap L -> isomorphic;
correctness
proof
set f = ClImageMap L;
set S = ClOpers L, T = (ClosureSystems L) opp;
reconsider g = f" as Function of T,S by Th20;
per cases;
case
S is non empty & T is non empty;
thus f is one-to-one;
thus f is monotone
proof
let x,y be Element of S;
reconsider c = x, d = y as closure Function of L,L by Th10;
A1: f.y = Image d by Def4;
assume x <= y;
then c <= d by Th12;
then
A2: Image d is SubRelStr of Image c by Th14;
f.x = Image c by Def4;
then ~(f.x) >= ~(f.y) by A2,A1,Th17;
hence f.x <= f.y by YELLOW_7:1;
end;
take g;
thus g = f";
thus g is monotone
proof
let x,y be Element of T;
reconsider A = ~x, B = ~y as infs-inheriting full strict SubRelStr of
L by Th16;
A3: B = Image closure_op B by Th18;
A4: g.A = closure_op A by Th21;
assume x <= y;
then ~y <= ~x by YELLOW_7:1;
then
A5: B is SubRelStr of A by Th17;
A6: g.B = closure_op B by Th21;
A = Image closure_op A by Th18;
then closure_op A <= closure_op B by A5,A3,Th14;
hence g.x <= g.y by A4,A6,Th12;
end;
end;
case
S is empty or T is empty;
hence thesis;
end;
end;
end;
theorem
for L being complete LATTICE holds ClOpers L, (ClosureSystems L) opp
are_isomorphic
proof
let L be complete LATTICE;
take ClImageMap L;
thus thesis;
end;
begin :: Isomorphism between closure operators preserving directed sups
:: and subalgebras
theorem Th23:
for L being RelStr, S being full SubRelStr of L for X being
Subset of S holds (X is directed Subset of L implies X is directed) & (X is
filtered Subset of L implies X is filtered)
proof
let L be RelStr, S be full SubRelStr of L;
let X be Subset of S;
hereby
assume
A1: X is directed Subset of L;
thus X is directed
proof
A2: the carrier of S c= the carrier of L by YELLOW_0:def 13;
let x,y be Element of S;
assume that
A3: x in X and
A4: y in X;
x in the carrier of S by A3;
then reconsider x9 = x, y9 = y as Element of L by A2;
consider z being Element of L such that
A5: z in X and
A6: z >= x9 and
A7: z >= y9 by A1,A3,A4,WAYBEL_0:def 1;
reconsider z as Element of S by A5;
take z;
thus thesis by A5,A6,A7,YELLOW_0:60;
end;
end;
assume
A8: X is filtered Subset of L;
A9: the carrier of S c= the carrier of L by YELLOW_0:def 13;
let x,y be Element of S;
assume that
A10: x in X and
A11: y in X;
x in the carrier of S by A10;
then reconsider x9 = x, y9 = y as Element of L by A9;
consider z being Element of L such that
A12: z in X and
A13: z <= x9 and
A14: z <= y9 by A8,A10,A11,WAYBEL_0:def 2;
reconsider z as Element of S by A12;
take z;
thus thesis by A12,A13,A14,YELLOW_0:60;
end;
:: Corollary 3.14, p. 24
theorem Th24:
for L being complete LATTICE for S being closure System of L
holds closure_op S is directed-sups-preserving iff S is
directed-sups-inheriting
proof
let L be complete LATTICE;
let S be closure System of L;
set c = closure_op S;
A1: Image c = the RelStr of S by Th18;
hereby
set Lk = {k where k is Element of L: c.k <= k};
set k = the Element of L;
A2: Lk c= the carrier of L
proof
let x be object;
assume x in Lk;
then ex k being Element of L st x = k & c.k <= k;
hence thesis;
end;
c.(c.k) = c.k by YELLOW_2:18;
then
A3: c.k in Lk;
assume closure_op S is directed-sups-preserving;
then
A4: Image c is directed-sups-inheriting by A3,A2,WAYBEL_1:52;
thus S is directed-sups-inheriting
proof
let X be directed Subset of S such that
A5: X <> {} and
A6: ex_sup_of X,L;
reconsider Y = X as Subset of Image c by A1;
Y is directed by A1,WAYBEL_0:3;
hence thesis by A1,A4,A5,A6;
end;
end;
assume
A7: for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/"(X,L) in the carrier of S;
let X be Subset of L such that
A8: X is non empty directed;
rng c = the carrier of S by A1,YELLOW_0:def 15;
then reconsider Y = c.:X as Subset of S by RELAT_1:111;
assume ex_sup_of X,L;
thus ex_sup_of c.:X,L by YELLOW_0:17;
c.:X is_<=_than c.sup X
proof
let x be Element of L;
assume x in c.:X;
then consider a being object such that
A9: a in the carrier of L and
A10: a in X and
A11: x = c.a by FUNCT_2:64;
reconsider a as Element of L by A9;
a <= sup X by A10,YELLOW_2:22;
hence thesis by A11,WAYBEL_1:def 2;
end;
then
A12: sup (c.:X) <= c.sup X by YELLOW_0:32;
X is_<=_than sup (c.:X)
proof
let x be Element of L;
assume x in X;
then c.x in c.:X by FUNCT_2:35;
then
A13: c.x <= sup (c.:X) by YELLOW_2:22;
x <= c.x by Th5;
hence thesis by A13,ORDERS_2:3;
end;
then
A14: sup X <= sup (c.:X) by YELLOW_0:32;
set x = the Element of X;
x in X by A8;
then
A15: c.x in c.:X by FUNCT_2:35;
Y is directed by A8,Th23,YELLOW_2:15;
then sup (c.:X) in the carrier of S by A7,A15,YELLOW_0:17;
then ex a being Element of L st c.a = sup (c.:X) by A1,YELLOW_2:10;
then c.sup (c.:X) = sup (c.:X) by YELLOW_2:18;
then c.sup X <= sup (c.:X) by A14,WAYBEL_1:def 2;
hence thesis by A12,ORDERS_2:2;
end;
theorem
for L being complete LATTICE for h being closure Function of L,L holds
h is directed-sups-preserving iff Image h is directed-sups-inheriting
proof
let L be complete LATTICE;
let h be closure Function of L,L;
closure_op Image h = h by Th19;
hence thesis by Th24;
end;
registration
let L be complete LATTICE;
let S be directed-sups-inheriting closure System of L;
cluster closure_op S -> directed-sups-preserving;
coherence by Th24;
end;
registration
let L be complete LATTICE;
let h be directed-sups-preserving closure Function of L,L;
cluster Image h -> directed-sups-inheriting;
coherence
proof
h = closure_op Image h by Th19;
hence thesis by Th24;
end;
end;
definition
let L be non empty reflexive RelStr;
func DsupClOpers L -> non empty full strict SubRelStr of ClOpers L means
:
Def6: for f being closure Function of L,L holds f is Element of it iff f is
directed-sups-preserving;
existence
proof
defpred P[set] means $1 is directed-sups-preserving Function of L,L;
set h = the directed-sups-preserving closure Function of L,L;
h is Element of ClOpers L by Def1;
then
A1: h in the carrier of ClOpers L;
A2: P[h];
consider S being non empty full strict SubRelStr of ClOpers L such that
A3: for f being Element of ClOpers L holds f is Element of S iff P[f]
from SubrelstrEx(A2,A1);
take S;
let f be closure Function of L,L;
hereby
assume
A4: f is Element of S;
then f is Element of ClOpers L by YELLOW_0:58;
hence f is directed-sups-preserving by A3,A4;
end;
assume
A5: f is directed-sups-preserving;
f is Element of ClOpers L by Def1;
hence thesis by A3,A5;
end;
correctness
proof
defpred P[object] means
$1 is directed-sups-preserving closure Function of L,L;
let S1,S2 be non empty full strict SubRelStr of ClOpers L such that
A6: for f being closure Function of L,L holds f is Element of S1 iff
f is directed-sups-preserving and
A7: for f being closure Function of L,L holds f is Element of S2 iff
f is directed-sups-preserving;
A8: now
let f be object;
f is Element of S2 implies f is Element of ClOpers L by YELLOW_0:58;
then f is Element of S2 implies f is closure Function of L,L by Th10;
hence f is Element of S2 iff P[f] by A7;
end;
A9: now
let f be object;
f is Element of S1 implies f is Element of ClOpers L by YELLOW_0:58;
then f is Element of S1 implies f is closure Function of L,L by Th10;
hence f is Element of S1 iff P[f] by A6;
end;
the RelStr of S1 = the RelStr of S2 from SubrelstrEq1(A9,A8);
hence thesis;
end;
end;
theorem Th26:
for L being non empty reflexive RelStr, x being set holds x is
Element of DsupClOpers L iff x is directed-sups-preserving closure Function of
L,L
proof
let L be non empty reflexive RelStr, x be set;
x is Element of ClOpers L iff x is closure Function of L,L by Th10;
hence thesis by Def6,YELLOW_0:58;
end;
definition
let L be non empty RelStr;
func Subalgebras L -> full strict non empty SubRelStr of ClosureSystems L
means
: Def7:
for R being strict closure System of L holds R is Element of it
iff R is directed-sups-inheriting;
existence
proof
defpred P[set] means $1 is directed-sups-inheriting SubRelStr of L;
set SL = subrelstr [#]L;
SL is Element of ClosureSystems L by Def3;
then
A1: SL in the carrier of ClosureSystems L;
A2: P[SL];
consider S being non empty full strict SubRelStr of ClosureSystems L such
that
A3: for x being Element of ClosureSystems L holds x is Element of S
iff P[x] from SubrelstrEx(A2,A1);
take S;
let R be strict closure System of L;
R is Element of ClosureSystems L by Def3;
hence thesis by A3;
end;
correctness
proof
defpred P[object] means
$1 is directed-sups-inheriting strict closure System of L;
let S1,S2 be full strict non empty SubRelStr of ClosureSystems L such that
A4: for R being strict closure System of L holds R is Element of S1
iff R is directed-sups-inheriting and
A5: for R being strict closure System of L holds R is Element of S2
iff R is directed-sups-inheriting;
A6: now
let x be object;
x is Element of S2 implies x is Element of ClosureSystems L by
YELLOW_0:58;
then x is Element of S2 implies x is strict closure System of L by Th16;
hence x is Element of S2 iff P[x] by A5;
end;
A7: now
let x be object;
x is Element of S1 implies x is Element of ClosureSystems L by
YELLOW_0:58;
then x is Element of S1 implies x is strict closure System of L by Th16;
hence x is Element of S1 iff P[x] by A4;
end;
the RelStr of S1 = the RelStr of S2 from SubrelstrEq1(A7,A6);
hence thesis;
end;
end;
theorem Th27:
for L being non empty RelStr, x being object holds x is Element of
Subalgebras L iff x is strict directed-sups-inheriting closure System of L
proof
let L be non empty RelStr, x be object;
x is Element of ClosureSystems L iff x is strict closure System of L by Th16;
hence thesis by Def7,YELLOW_0:58;
end;
theorem Th28:
for L being complete LATTICE holds Image ((ClImageMap L)|
DsupClOpers L) = (Subalgebras L) opp
proof
let L be complete LATTICE;
defpred P[object] means
$1 is directed-sups-inheriting closure strict System of L;
A1: now
let a be object;
hereby
assume a is Element of Image ((ClImageMap L)|DsupClOpers L);
then consider x being Element of DsupClOpers L such that
A2: ((ClImageMap L)|DsupClOpers L).x = a by YELLOW_2:10;
reconsider x as directed-sups-preserving closure Function of L,L by Th26;
a = (ClImageMap L).x by A2,Th6
.= Image x by Def4;
hence P[a];
end;
assume P[a];
then reconsider
S = a as directed-sups-inheriting closure strict System of L;
reconsider x = closure_op S as Element of DsupClOpers L by Th26;
S = Image closure_op S by Th18
.= (ClImageMap L).closure_op S by Def4
.= ((ClImageMap L)|DsupClOpers L).x by Th6;
then S in rng ((ClImageMap L)|DsupClOpers L) by FUNCT_2:4;
hence a is Element of Image ((ClImageMap L)|DsupClOpers L) by
YELLOW_0:def 15;
end;
A3: for a be object
holds a is Element of (Subalgebras L) opp iff P[a] by Th27;
the RelStr of Image ((ClImageMap L)|DsupClOpers L) = the RelStr of (
Subalgebras L) opp from SubrelstrEq1(A1,A3);
hence thesis;
end;
registration
let L be complete LATTICE;
cluster corestr ((ClImageMap L)|DsupClOpers L) -> isomorphic;
coherence
proof
set f = ClImageMap L, R = DsupClOpers L, g = corestr (f|R);
per cases;
case
DsupClOpers L is non empty & Image (f|R) is non empty;
f|R is one-to-one by Th7;
hence g is one-to-one monotone by WAYBEL_1:30;
consider f9 being Function of (ClosureSystems L) opp,ClOpers L such that
A1: f9 = f" and
f9 is monotone by WAYBEL_0:def 38;
reconsider h = f9|Image (f|R) as Function of Image (f|R), R by A1,Th8;
take h;
thus h = (f|R)" by A1,Th8
.= g" by WAYBEL_1:30;
let x,y be Element of Image (f|R);
reconsider a = x, b = y as Element of (ClosureSystems L) opp by
YELLOW_0:58;
reconsider A = ~a, B = ~b as strict closure System of L by Th16;
reconsider i = closure_op A, j = closure_op B as Element of ClOpers L by
Th10;
f9.y = j by A1,Th21;
then
A2: h.y = j by Th6;
assume x <= y;
then a <= b by YELLOW_0:59;
then ~a >= ~b by YELLOW_7:1;
then
A3: B is SubRelStr of A by Th17;
A4: B = Image closure_op B by Th18;
A = Image closure_op A by Th18;
then closure_op A <= closure_op B by A3,A4,Th14;
then
A5: i <= j by Th12;
f9.x = i by A1,Th21;
then h.x = i by Th6;
hence h.x <= h.y by A2,A5,YELLOW_0:60;
end;
case
DsupClOpers L is empty or Image (f|R) is empty;
hence thesis;
end;
end;
end;
theorem
for L being complete LATTICE holds DsupClOpers L, (Subalgebras L) opp
are_isomorphic
proof
let L be complete LATTICE;
set f = (ClImageMap L)|DsupClOpers L;
reconsider g=corestr f as Function of DsupClOpers L, (Subalgebras L) opp by
Th28;
take g;
Image f = (Subalgebras L) opp by Th28;
hence thesis;
end;