:: Closure Operators and Subalgebras :: by Grzegorz Bancerek :: :: Received January 15, 1997 :: Copyright (c) 1997-2021 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;