:: Ideals :: by Grzegorz Bancerek :: :: Received October 24, 1994 :: Copyright (c) 1994-2017 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, SUBSET_1, BINOP_1, REALSET1, RELAT_1, ZFMISC_1, FUNCT_1, LATTICE2, LATTICES, STRUCT_0, EQREL_1, PBOOLE, LATTICE4, FILTER_0, CARD_FIL, CAT_1, TARSKI, INT_2, YELLOW11, LATTICE5, NAT_LAT, XBOOLEAN, XXREAL_2, FILTER_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, DOMAIN_1, BINOP_1, REALSET1, LATTICES, NAT_LAT, FILTER_0, LATTICE2, MCART_1, LATTICE4; constructors BINOP_1, REALSET1, FILTER_0, LATTICE2, NAT_LAT, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, LATTICES, FILTER_0, LATTICE2, NAT_LAT; requirements SUBSET, BOOLE; begin :: Some Properties of the Restriction of Binary Operations theorem :: FILTER_2:1 for D being non empty set, S being non empty Subset of D, f being BinOp of D, g being BinOp of S st g = f||S holds (f is commutative implies g is commutative) & (f is idempotent implies g is idempotent) & (f is associative implies g is associative); theorem :: FILTER_2:2 for D being non empty set, S being non empty Subset of D, f being BinOp of D, g being BinOp of S for d being Element of D, d9 being Element of S st g = f||S & d9 = d holds (d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g) & (d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g) & (d is_a_unity_wrt f implies d9 is_a_unity_wrt g); theorem :: FILTER_2:3 for D being non empty set, S being non empty Subset of D, f1,f2 being BinOp of D, g1,g2 being BinOp of S st g1 = f1||S & g2 = f2||S holds (f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2) & (f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2); theorem :: FILTER_2:4 for D being non empty set, S being non empty Subset of D, f1,f2 being BinOp of D, g1,g2 being BinOp of S st g1 = f1||S & g2 = f2||S holds f1 is_distributive_wrt f2 implies g1 is_distributive_wrt g2; theorem :: FILTER_2:5 for D being non empty set, S being non empty Subset of D, f1,f2 being BinOp of D, g1,g2 being BinOp of S st g1 = f1||S & g2 = f2||S holds f1 absorbs f2 implies g1 absorbs g2; begin :: Closed Subsets of a Lattice definition let D be non empty set, X1,X2 be Subset of D; redefine pred X1 = X2 means :: FILTER_2:def 1 for x being Element of D holds x in X1 iff x in X2; end; reserve L for Lattice, p,q,r for Element of L, p9,q9,r9 for Element of L.:, x, y for set; theorem :: FILTER_2:6 for L1,L2 being LattStr st the LattStr of L1 = the LattStr of L2 holds L1.: = L2.:; theorem :: FILTER_2:7 L .: .: = the LattStr of L; theorem :: FILTER_2:8 for L1,L2 being non empty LattStr st the LattStr of L1 = the LattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1 = b2 holds a1"\/"b1 = a2"\/"b2 & a1"/\"b1 = a2"/\"b2 & (a1 [= b1 iff a2 [= b2); theorem :: FILTER_2:9 for L1,L2 being 0_Lattice st the LattStr of L1 = the LattStr of L2 holds Bottom L1 = Bottom L2; theorem :: FILTER_2:10 for L1,L2 being 1_Lattice st the LattStr of L1 = the LattStr of L2 holds Top L1 = Top L2; theorem :: FILTER_2:11 for L1,L2 being C_Lattice st the LattStr of L1 = the LattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2; theorem :: FILTER_2:12 for L1,L2 being B_Lattice st the LattStr of L1 = the LattStr of L2 for a being Element of L1, b being Element of L2 st a = b holds a` = b`; theorem :: FILTER_2:13 for X being Subset of L st for p,q holds p in X & q in X iff p"/\"q in X holds X is ClosedSubset of L; theorem :: FILTER_2:14 for X being Subset of L st for p,q holds p in X & q in X iff p "\/"q in X holds X is ClosedSubset of L; definition let L; mode Ideal of L is non empty initial join-closed Subset of L; end; theorem :: FILTER_2:15 for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2 for x st x is Filter of L1 holds x is Filter of L2; theorem :: FILTER_2:16 for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2 for x st x is Ideal of L1 holds x is Ideal of L2; definition let L,p; func p.: -> Element of L.: equals :: FILTER_2:def 2 p; end; definition let L; let p be Element of L.:; func .:p -> Element of L equals :: FILTER_2:def 3 p; end; theorem :: FILTER_2:17 .:(p.:) = p & ( .:p9).: = p9; theorem :: FILTER_2:18 p"/\"q = p.:"\/"q.: & p"\/"q = p.:"/\"q.: & p9"/\"q9 = .:p9"\/".: q9 & p9"\/"q9 = .:p9 "/\".:q9; theorem :: FILTER_2:19 (p [= q iff q.: [= p.:) & (p9 [= q9 iff .:q9 [= .:p9); definition let L; let X be Subset of L; func X.: -> Subset of L.: equals :: FILTER_2:def 4 X; end; definition let L; let X be Subset of L.:; func .:X -> Subset of L equals :: FILTER_2:def 5 X; end; registration let L; let D be non empty Subset of L; cluster D.: -> non empty; end; registration let L; let D be non empty Subset of L.:; cluster .:D -> non empty; end; registration let L; let S be meet-closed Subset of L; cluster S.: -> join-closed for Subset of L.:; end; registration let L; let S be join-closed Subset of L; cluster S.: -> meet-closed for Subset of L.:; end; registration let L; let S be meet-closed Subset of L.:; cluster .:S -> join-closed for Subset of L; end; registration let L; let S be join-closed Subset of L.:; cluster .:S -> meet-closed for Subset of L; end; registration let L; let F be final Subset of L; cluster F.: -> initial for Subset of L.:; end; registration let L; let F be initial Subset of L; cluster F.: -> final for Subset of L.:; end; registration let L; let F be final Subset of L.:; cluster .:F -> initial for Subset of L; end; registration let L; let F be initial Subset of L.:; cluster F.: -> final for Subset of L; end; theorem :: FILTER_2:20 x is Ideal of L iff x is Filter of L.:; theorem :: FILTER_2:21 for D being non empty Subset of L holds D is Ideal of L iff (for p,q st p in D & q in D holds p "\/" q in D) & for p,q st p in D & q [= p holds q in D; reserve I,J for Ideal of L, F for Filter of L; theorem :: FILTER_2:22 p in I implies p"/\"q in I & q"/\"p in I; theorem :: FILTER_2:23 ex p st p in I; theorem :: FILTER_2:24 L is lower-bounded implies Bottom L in I; theorem :: FILTER_2:25 L is lower-bounded implies {Bottom L} is Ideal of L; theorem :: FILTER_2:26 {p} is Ideal of L implies L is lower-bounded; begin :: Ideals Generated by Subsets of a Lattice theorem :: FILTER_2:27 the carrier of L is Ideal of L; definition let L; func (.L.> -> Ideal of L equals :: FILTER_2:def 6 the carrier of L; end; definition let L,p; func (.p.> -> Ideal of L equals :: FILTER_2:def 7 { q : q [= p }; end; theorem :: FILTER_2:28 q in (.p.> iff q [= p; theorem :: FILTER_2:29 (.p.> = <.p.:.) & (.p.:.> = <.p.); theorem :: FILTER_2:30 p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.>; theorem :: FILTER_2:31 L is upper-bounded implies (.L.> = (.Top L.>; definition let L,I; attr I is max-ideal means :: FILTER_2:def 8 I <> the carrier of L & for J st I c= J & J <> the carrier of L holds I = J; end; theorem :: FILTER_2:32 I is max-ideal iff I.: is being_ultrafilter; theorem :: FILTER_2:33 L is upper-bounded implies for I st I <> the carrier of L ex J st I c= J & J is max-ideal; theorem :: FILTER_2:34 (ex r st p "\/" r <> p) implies (.p.> <> the carrier of L; theorem :: FILTER_2:35 L is upper-bounded & p <> Top L implies ex I st p in I & I is max-ideal; reserve D for non empty Subset of L, D9 for non empty Subset of L.:; definition let L,D; func (.D.> -> Ideal of L means :: FILTER_2:def 9 D c= it & for I st D c= I holds it c= I; end; theorem :: FILTER_2:36 <.D.:.) = (.D.> & <.D.) = (.D.:.> & <..:D9.) = (.D9.> & <.D9.) = (..: D9.>; theorem :: FILTER_2:37 (.I.> = I; reserve D1,D2 for non empty Subset of L, D19,D29 for non empty Subset of L.:; theorem :: FILTER_2:38 (D1 c= D2 implies (.D1.> c= (.D2.>) & (.(.D.>.> c= (.D.>; theorem :: FILTER_2:39 p in D implies (.p.> c= (.D.>; theorem :: FILTER_2:40 D = {p} implies (.D.> = (.p.>; theorem :: FILTER_2:41 L is upper-bounded & Top L in D implies (.D.> = (.L.> & (.D.> = the carrier of L; theorem :: FILTER_2:42 L is upper-bounded & Top L in I implies I = (.L.> & I = the carrier of L; definition let L,I; attr I is prime means :: FILTER_2:def 10 p "/\" q in I iff p in I or q in I; end; theorem :: FILTER_2:43 I is prime iff I.: is prime; definition let L,D1,D2; func D1 "\/" D2 -> Subset of L equals :: FILTER_2:def 11 { p"\/"q : p in D1 & q in D2 }; end; registration let L,D1,D2; cluster D1 "\/" D2 -> non empty; end; theorem :: FILTER_2:44 D1 "\/" D2 = D1.: "/\" D2.: & D1.: "\/" D2.: = D1 "/\" D2 & D19 "\/" D29 = .:D19 "/\" .:D29 & .:D19 "\/" .:D29 = D19 "/\" D29; theorem :: FILTER_2:45 p in D1 & q in D2 implies p"\/"q in D1 "\/" D2 & q"\/"p in D1 "\/" D2; theorem :: FILTER_2:46 x in D1 "\/" D2 implies ex p,q st x = p"\/"q & p in D1 & q in D2; theorem :: FILTER_2:47 D1 "\/" D2 = D2 "\/" D1; registration let L be D_Lattice; let I1,I2 be Ideal of L; cluster I1 "\/" I2 -> initial join-closed; end; theorem :: FILTER_2:48 (.D1 \/ D2.> = (.(.D1.> \/ D2.> & (.D1 \/ D2.> = (.D1 \/ (.D2.>.>; theorem :: FILTER_2:49 (.I \/ J.> = { r : ex p,q st r [= p"\/"q & p in I & q in J }; theorem :: FILTER_2:50 I c= I "\/" J & J c= I "\/" J; theorem :: FILTER_2:51 (.I \/ J.> = (.I "\/" J.>; reserve B for B_Lattice, IB,JB for Ideal of B, a,b for Element of B; theorem :: FILTER_2:52 L is C_Lattice iff L.: is C_Lattice; theorem :: FILTER_2:53 L is B_Lattice iff L.: is B_Lattice; registration let B be B_Lattice; cluster B.: -> Boolean Lattice-like; end; reserve a9 for Element of (B qua Lattice).:; theorem :: FILTER_2:54 a.:` = a` & ( .:a9)` = a9`; theorem :: FILTER_2:55 (.IB \/ JB.> = IB "\/" JB; theorem :: FILTER_2:56 IB is max-ideal iff IB <> the carrier of B & for a holds a in IB or a` in IB; theorem :: FILTER_2:57 IB <> (.B.> & IB is prime iff IB is max-ideal; theorem :: FILTER_2:58 IB is max-ideal implies for a holds a in IB iff not a` in IB; theorem :: FILTER_2:59 a <> b implies ex IB st IB is max-ideal & (a in IB & not b in IB or not a in IB & b in IB); reserve P for non empty ClosedSubset of L, o1,o2 for BinOp of P; theorem :: FILTER_2:60 (the L_join of L)||P is BinOp of P & (the L_meet of L)||P is BinOp of P; theorem :: FILTER_2:61 o1 = (the L_join of L)||P & o2 = (the L_meet of L)||P implies o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1; definition let L,p,q; assume p [= q; func [#p,q#] -> non empty ClosedSubset of L equals :: FILTER_2:def 12 {r: p [= r & r [= q}; end; theorem :: FILTER_2:62 p [= q implies (r in [#p,q#] iff p [= r & r [= q); theorem :: FILTER_2:63 p [= q implies p in [#p,q#] & q in [#p,q#]; theorem :: FILTER_2:64 [#p,p#] = {p}; theorem :: FILTER_2:65 L is upper-bounded implies <.p.) = [#p,Top L#]; theorem :: FILTER_2:66 L is lower-bounded implies (.p.> = [#Bottom L,p#]; theorem :: FILTER_2:67 for L1,L2 being Lattice for F1 being Filter of L1, F2 being Filter of L2 st the LattStr of L1 = the LattStr of L2 & F1 = F2 holds latt F1 = latt F2 ; begin :: Sublattices notation let L; synonym Sublattice of L for SubLattice of L; end; definition let L; redefine mode Sublattice of L means :: FILTER_2:def 13 ex P,o1,o2 st o1 = (the L_join of L)||P & o2 = (the L_meet of L)||P & the LattStr of it = LattStr (#P, o1, o2 #); end; theorem :: FILTER_2:68 for K being Sublattice of L, a being Element of K holds a is Element of L; definition let L,P; func latt (L,P) -> Sublattice of L means :: FILTER_2:def 14 ex o1,o2 st o1 = (the L_join of L)||P & o2 = (the L_meet of L)||P & it = LattStr (#P, o1, o2#); end; registration let L,P; cluster latt (L,P) -> strict; end; definition let L; let l be Sublattice of L; redefine func l.: -> strict Sublattice of L.:; end; theorem :: FILTER_2:69 latt F = latt (L,F); theorem :: FILTER_2:70 latt (L,P) = (latt (L.:,P.:)).:; theorem :: FILTER_2:71 latt (L,(.L.>) = the LattStr of L & latt (L,<.L.)) = the LattStr of L; theorem :: FILTER_2:72 the carrier of latt (L,P) = P & the L_join of latt (L,P) = (the L_join of L)||P & the L_meet of latt (L,P) = (the L_meet of L)||P; theorem :: FILTER_2:73 for p,q for p9,q9 being Element of latt (L,P) st p = p9 & q = q9 holds p"\/"q = p9"\/"q9 & p"/\"q = p9"/\"q9; theorem :: FILTER_2:74 for p,q for p9,q9 being Element of latt (L,P) st p = p9 & q = q9 holds p [= q iff p9 [= q9; theorem :: FILTER_2:75 L is lower-bounded implies latt (L,I) is lower-bounded; theorem :: FILTER_2:76 L is modular implies latt (L,P) is modular; theorem :: FILTER_2:77 L is distributive implies latt (L,P) is distributive; theorem :: FILTER_2:78 L is implicative & p [= q implies latt (L,[#p,q#]) is implicative; registration let L,p; cluster latt (L,(.p.>) -> upper-bounded; end; theorem :: FILTER_2:79 Top latt (L,(.p.>) = p; theorem :: FILTER_2:80 L is lower-bounded implies latt (L,(.p.>) is lower-bounded & Bottom latt (L,(.p.>) = Bottom L; theorem :: FILTER_2:81 L is lower-bounded implies latt (L,(.p.>) is bounded; theorem :: FILTER_2:82 p [= q implies latt (L,[#p,q#]) is bounded & Top latt (L,[#p,q#] ) = q & Bottom latt (L,[#p,q#]) = p; theorem :: FILTER_2:83 L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice; theorem :: FILTER_2:84 L is C_Lattice & L is modular & p [= q implies latt (L,[#p,q#]) is C_Lattice; theorem :: FILTER_2:85 L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice; theorem :: FILTER_2:86 for S being non empty Subset of L holds S is Ideal of L iff for p,q being Element of L holds p in S & q in S iff p "\/" q in S;