Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Closure Operators and Subalgebras

**by****Grzegorz Bancerek**- Received January 15, 1997
- MML identifier: WAYBEL10

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, CAT_1, YELLOW_0, RELAT_1, WELLORD1, BOOLE, OPPCAT_1, FUNCOP_1, WAYBEL_3, RELAT_2, SEQM_3, PRE_TOPC, FUNCT_1, WAYBEL_1, BINOP_1, GROUP_6, WAYBEL_0, ORDINAL2, YELLOW_1, FUNCT_2, GROUP_1, CARD_3, RLVECT_2, BHSP_3, UNIALG_2, LATTICE3, LATTICES, SUBSET_1, QUANTAL1, WAYBEL10; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, CARD_3, STRUCT_0, QUANTAL1, PRE_TOPC, PRALG_1, PRE_CIRC, BORSUK_1, WELLORD1, ORDERS_1, LATTICE3, GRCAT_1, ORDERS_3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, YELLOW_7; constructors PRE_CIRC, TOLER_1, BORSUK_1, QUANTAL1, GRCAT_1, ORDERS_3, WAYBEL_1, WAYBEL_3; clusters STRUCT_0, RELSET_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_3, SUBSET_1, FUNCT_2, PARTFUN1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries scheme SubrelstrEx {L() -> non empty RelStr, P[set], 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 RelstrEq {L1, L2() -> non empty RelStr, P[set], Q[set,set]}: the RelStr of L1() = the RelStr of L2() provided for x being set holds x is Element of L1() iff P[x] and for x being set 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 SubrelstrEq1 {L() -> non empty RelStr, S1, S2() -> non empty full SubRelStr of L(), P[set]}: the RelStr of S1() = the RelStr of S2() provided for x being set holds x is Element of S1() iff P[x] and for x being set holds x is Element of S2() iff P[x]; scheme SubrelstrEq2 {L() -> non empty RelStr, S1, S2() -> non empty full SubRelStr of L(), P[set]}: 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~); canceled; theorem :: WAYBEL10:3 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:4 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; definition let X be set, L be non empty RelStr; cluster X --> L -> non-Empty; end; definition let S be RelStr, T be non empty reflexive RelStr; cluster monotone map of S,T; end; definition let L be non empty RelStr; cluster projection -> monotone idempotent map of L,L; end; definition let S,T be non empty reflexive RelStr; let f be monotone map of S,T; cluster corestr f -> monotone; end; definition let L be 1-sorted; cluster id L -> one-to-one; end; definition let L be non empty reflexive RelStr; cluster id L -> sups-preserving infs-preserving; end; theorem :: WAYBEL10:5 for L being RelStr, S being Subset of L holds id S is map of subrelstr S, L & for f being map of subrelstr S, L st f = id S holds f is monotone; definition let L be non empty reflexive RelStr; cluster sups-preserving infs-preserving closure kernel one-to-one map of L,L; end; theorem :: WAYBEL10:6 for L being non empty reflexive RelStr, c being closure map of L,L for x being Element of L holds c.x >= x; definition let S,T be 1-sorted; let f be Function of the carrier of S, the carrier of T; let R be 1-sorted such that the carrier of R c= the carrier of S; func f|R -> map of R,T equals :: WAYBEL10:def 1 f|the carrier of R; end; theorem :: WAYBEL10:7 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:8 for S,T being RelStr, f being map of S,T st f is one-to-one for R being SubRelStr of S holds f|R is one-to-one; definition let S,T be non empty reflexive RelStr; let f be monotone map of S,T; let R be SubRelStr of S; cluster f|R -> monotone; end; theorem :: WAYBEL10:9 for S,T being non empty RelStr, R being non empty SubRelStr of S for f being map of S,T, g being map of T,S st f is one-to-one & g = f" holds g|Image (f|R) is map of Image (f|R), R & g|Image (f|R) = (f|R)"; begin :: The lattice of closure operators definition let S be RelStr, T be non empty reflexive RelStr; cluster MonMaps(S,T) -> non empty; end; theorem :: WAYBEL10:10 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 map 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 2 for f being map of L,L holds f is Element of it iff f is closure; end; theorem :: WAYBEL10:11 for L being non empty reflexive RelStr, x being set holds x is Element of ClOpers L iff x is closure map of L,L; theorem :: WAYBEL10:12 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:13 for L being complete LATTICE for c1,c2 being map of L,L for x,y being Element of ClOpers L st x = c1 & y = c2 holds x <= y iff c1 <= c2; theorem :: WAYBEL10:14 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:15 for L being complete LATTICE for c1,c2 being closure map 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 3 (for x being set 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:16 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; definition let L be RelStr; cluster Sub L -> reflexive antisymmetric transitive; end; definition let L be RelStr; cluster Sub L -> complete; end; definition let L be complete LATTICE; cluster infs-inheriting -> non empty SubRelStr of L; cluster sups-inheriting -> non empty SubRelStr of L; end; definition let L be RelStr; mode System of L is full SubRelStr of L; end; definition let L be non empty RelStr; let S be System of L; redefine attr S is infs-inheriting; synonym S is closure; end; definition 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 4 for R being strict SubRelStr of L holds R is Element of it iff R is infs-inheriting full; end; theorem :: WAYBEL10:17 for L being non empty RelStr, x being set holds x is Element of ClosureSystems L iff x is strict closure System of L; theorem :: WAYBEL10:18 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 definition let L be non empty Poset; let h be closure map of L,L; cluster Image h -> infs-inheriting; end; definition let L be non empty Poset; func ClImageMap L -> map of ClOpers L, (ClosureSystems L) opp means :: WAYBEL10:def 5 for c being closure map 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 -> map of L,L means :: WAYBEL10:def 6 for x being Element of L holds it.x = "/\"((uparrow x) /\ the carrier of S,L); end; definition let L be complete LATTICE; let S be closure System of L; cluster closure_op S -> closure; end; theorem :: WAYBEL10:19 for L being complete LATTICE for S being closure System of L holds Image closure_op S = the RelStr of S; theorem :: WAYBEL10:20 for L being complete LATTICE for c being closure map of L,L holds closure_op Image c = c; definition let L be complete LATTICE; cluster ClImageMap L -> one-to-one; end; theorem :: WAYBEL10:21 for L being complete LATTICE holds (ClImageMap L)" is map of (ClosureSystems L) opp, ClOpers L; theorem :: WAYBEL10:22 for L being complete LATTICE for S being strict closure System of L holds (ClImageMap L)".S = closure_op S; definition let L be complete LATTICE; cluster ClImageMap L -> isomorphic; end; theorem :: WAYBEL10:23 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:24 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:25 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:26 for L being complete LATTICE for h being closure map of L,L holds h is directed-sups-preserving iff Image h is directed-sups-inheriting; definition let L be complete LATTICE; let S be directed-sups-inheriting closure System of L; cluster closure_op S -> directed-sups-preserving; end; definition let L be complete LATTICE; let h be directed-sups-preserving closure map 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 7 for f being closure map of L,L holds f is Element of it iff f is directed-sups-preserving; end; theorem :: WAYBEL10:27 for L being non empty reflexive RelStr, x being set holds x is Element of DsupClOpers L iff x is directed-sups-preserving closure map of L,L; definition let L be non empty RelStr; func Subalgebras L -> full strict non empty SubRelStr of ClosureSystems L means :: WAYBEL10:def 8 for R being strict closure System of L holds R is Element of it iff R is directed-sups-inheriting; end; theorem :: WAYBEL10:28 for L being non empty RelStr, x being set holds x is Element of Subalgebras L iff x is strict directed-sups-inheriting closure System of L; theorem :: WAYBEL10:29 for L being complete LATTICE holds Image ((ClImageMap L)|DsupClOpers L) = (Subalgebras L) opp; definition let L be complete LATTICE; cluster corestr ((ClImageMap L)|DsupClOpers L) -> isomorphic; end; theorem :: WAYBEL10:30 for L being complete LATTICE holds DsupClOpers L, (Subalgebras L) opp are_isomorphic;

Back to top