:: Closure Operators and Subalgebras
:: by Grzegorz Bancerek
::
:: Received January 15, 1997
:: Copyright (c) 1997-2016 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;
begin :: Preliminaries
scheme :: WAYBEL10:sch 1
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
P[a()] and
a() in the carrier of L();
scheme :: WAYBEL10:sch 2
RelstrEq {L1, L2() -> non empty RelStr, P[object], Q[set,set]}:
the RelStr of L1() = the RelStr of L2()
provided
for x being object holds x is Element of L1() iff P[x] and
for x being object holds x is Element of L2() iff P[x] and
for a,b being Element of L1() holds a <= b iff Q[a,b] and
for a,b being Element of L2() holds a <= b iff Q[a,b];
scheme :: WAYBEL10:sch 3
SubrelstrEq1 {L() -> non empty RelStr, S1, S2() -> non empty full SubRelStr
of L(), P[object]}:
the RelStr of S1() = the RelStr of S2()
provided
for x being object holds x is Element of S1() iff P[x] and
for x being object holds x is Element of S2() iff P[x];
scheme :: WAYBEL10:sch 4
SubrelstrEq2 {L() -> non empty RelStr, S1, S2() -> non empty full SubRelStr
of L(), P[object]}:
the RelStr of S1() = the RelStr of S2()
provided
for x being Element of L() holds x is Element of S1() iff P[x] and
for x being Element of L() holds x is Element of S2() iff P[x];
theorem :: WAYBEL10:1
for R,Q being Relation holds (R c= Q iff R~ c= Q~) & (R~ c= Q iff R c= Q~);
theorem :: WAYBEL10:2
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);
theorem :: WAYBEL10:3
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);
definition
let L be RelStr, S be full SubRelStr of L;
redefine func S opp -> strict full SubRelStr of L opp;
end;
registration
let X be set, L be non empty RelStr;
cluster X --> L -> non-Empty;
end;
registration
let S be RelStr, T be non empty reflexive RelStr;
cluster monotone for Function of S,T;
end;
registration
let L be non empty RelStr;
cluster projection -> monotone idempotent for Function of L,L;
end;
registration
let S,T be non empty reflexive RelStr;
let f be monotone Function of S,T;
cluster corestr f -> monotone;
end;
registration
let L be non empty reflexive RelStr;
cluster id L -> sups-preserving infs-preserving;
end;
theorem :: WAYBEL10:4
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;
registration
let L be non empty reflexive RelStr;
cluster sups-preserving infs-preserving closure kernel one-to-one for
Function
of L,L;
end;
theorem :: WAYBEL10:5
for L being non empty reflexive RelStr, c being closure Function
of L,L for x being Element of L holds c.x >= x;
theorem :: WAYBEL10:6
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;
theorem :: WAYBEL10:7
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;
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;
end;
theorem :: WAYBEL10:8
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)";
begin :: The lattice of closure operators
registration
let S be RelStr, T be non empty reflexive RelStr;
cluster MonMaps(S,T) -> non empty;
end;
theorem :: WAYBEL10:9
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;
definition
let L be non empty reflexive RelStr;
func ClOpers L -> non empty full strict SubRelStr of MonMaps(L,L) means
:: WAYBEL10:def 1
for f being Function of L,L holds f is Element of it iff f is closure;
end;
theorem :: WAYBEL10:10
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;
theorem :: WAYBEL10:11
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;
theorem :: WAYBEL10:12
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;
theorem :: WAYBEL10:13
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;
theorem :: WAYBEL10:14
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;
begin :: The lattice of closure systems
definition
let L be RelStr;
func Sub L -> strict non empty RelStr means
:: WAYBEL10:def 2
( 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;
end;
theorem :: WAYBEL10:15
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;
registration
let L be RelStr;
cluster Sub L -> reflexive antisymmetric transitive;
end;
registration
let L be RelStr;
cluster Sub L -> complete;
end;
registration
let L be complete LATTICE;
cluster infs-inheriting -> non empty for SubRelStr of L;
cluster sups-inheriting -> non empty for SubRelStr of L;
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;
end;
definition
let L be non empty RelStr;
func ClosureSystems L -> full strict non empty SubRelStr of Sub L means
:: WAYBEL10:def 3
for R being strict SubRelStr of L holds R is Element of it iff R is
infs-inheriting full;
end;
theorem :: WAYBEL10:16
for L being non empty RelStr, x being object holds x is Element of
ClosureSystems L iff x is strict closure System of L;
theorem :: WAYBEL10:17
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;
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;
end;
definition
let L be non empty Poset;
func ClImageMap L -> Function of ClOpers L, (ClosureSystems L) opp means
:: WAYBEL10:def 4
for c being closure Function of L,L holds it.c = Image c;
end;
definition
let L be non empty RelStr;
let S be SubRelStr of L;
func closure_op S -> Function of L,L means
:: WAYBEL10:def 5
for x being Element of L
holds it.x = "/\"((uparrow x) /\ the carrier of S,L);
end;
registration
let L be complete LATTICE;
let S be closure System of L;
cluster closure_op S -> closure;
end;
theorem :: WAYBEL10:18
for L being complete LATTICE for S being closure System of L
holds Image closure_op S = the RelStr of S;
theorem :: WAYBEL10:19
for L being complete LATTICE for c being closure Function of L,L
holds closure_op Image c = c;
registration
let L be complete LATTICE;
cluster ClImageMap L -> one-to-one;
end;
theorem :: WAYBEL10:20
for L being complete LATTICE holds (ClImageMap L)" is Function
of (ClosureSystems L) opp, ClOpers L;
theorem :: WAYBEL10:21
for L being complete LATTICE for S being strict closure System
of L holds (ClImageMap L)".S = closure_op S;
registration
let L be complete LATTICE;
cluster ClImageMap L -> isomorphic;
end;
theorem :: WAYBEL10:22
for L being complete LATTICE holds ClOpers L, (ClosureSystems L) opp
are_isomorphic;
begin :: Isomorphism between closure operators preserving directed sups
:: and subalgebras
theorem :: WAYBEL10:23
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);
:: Corollary 3.14, p. 24
theorem :: WAYBEL10:24
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;
theorem :: WAYBEL10:25
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;
registration
let L be complete LATTICE;
let S be directed-sups-inheriting closure System of L;
cluster closure_op S -> directed-sups-preserving;
end;
registration
let L be complete LATTICE;
let h be directed-sups-preserving closure Function of L,L;
cluster Image h -> directed-sups-inheriting;
end;
definition
let L be non empty reflexive RelStr;
func DsupClOpers L -> non empty full strict SubRelStr of ClOpers L means
:: WAYBEL10:def 6
for f being closure Function of L,L holds f is Element of it iff f is
directed-sups-preserving;
end;
theorem :: WAYBEL10:26
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;
definition
let L be non empty RelStr;
func Subalgebras L -> full strict non empty SubRelStr of ClosureSystems L
means
:: WAYBEL10:def 7
for R being strict closure System of L holds R is Element of it
iff R is directed-sups-inheriting;
end;
theorem :: WAYBEL10:27
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;
theorem :: WAYBEL10:28
for L being complete LATTICE holds Image ((ClImageMap L)|
DsupClOpers L) = (Subalgebras L) opp;
registration
let L be complete LATTICE;
cluster corestr ((ClImageMap L)|DsupClOpers L) -> isomorphic;
end;
theorem :: WAYBEL10:29
for L being complete LATTICE holds DsupClOpers L, (Subalgebras L) opp
are_isomorphic;