:: Irreducible and Prime Elements :: by Beata Madras :: :: Received December 1, 1996 :: Copyright (c) 1996-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 WAYBEL_0, SUBSET_1, XBOOLE_0, ORDERS_2, FUNCT_1, RELAT_1, TARSKI, NUMBERS, FUNCT_7, TREES_2, RELAT_2, XXREAL_0, STRUCT_0, ORDINAL2, LATTICES, ORDERS_1, ZFMISC_1, YELLOW_0, EQREL_1, REWRITE1, FUNCOP_1, LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, CARD_FIL, SETFAM_1, ARYTM_3, CARD_1, NAT_1, ORDINAL1, YELLOW_8, FINSET_1, INT_2, YELLOW_1, FUNCT_3, LATTICE2, ARYTM_0, WAYBEL_5, PBOOLE, YELLOW_2, FUNCT_6, CARD_3, WAYBEL_6; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FINSET_1, RELAT_1, RELAT_2, ORDERS_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, STRUCT_0, ORDERS_2, CARD_3, LATTICE3, FUNCT_3, FUNCT_6, PBOOLE, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1, YELLOW_2, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, YELLOW_7, FUNCT_7, ABIAN, XXREAL_0; constructors SETFAM_1, XXREAL_0, NAT_1, FUNCT_7, BORSUK_1, PRALG_2, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, RELSET_1, NUMBERS, ABIAN; registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCOP_1, FINSET_1, PBOOLE, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_5, YELLOW_7, ORDINAL1, RELSET_1, XXREAL_0, RELAT_1, XCMPLX_0, NAT_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x,y,Y,Z for set, L for LATTICE, l for Element of L; :: Preliminaries scheme :: WAYBEL_6:sch 1 NonUniqExD1 { Z() ->non empty RelStr, X() -> Subset of Z(), Y() -> non empty Subset of Z(), P[object,object] }: ex f being Function of X(),Y() st for e be Element of Z() st e in X() ex u be Element of Z() st u in Y() & u = f.e & P[e,u] provided for e be Element of Z() st e in X() ex u be Element of Z() st u in Y () & P[e,u]; definition let L be non empty 1-sorted; let C,D be non empty Subset of L; let f be Function of C,D; let c be Element of C; redefine func f.c -> Element of L; end; registration let L be non empty Poset; cluster -> filtered directed for Chain of L; end; registration cluster strict continuous distributive lower-bounded for LATTICE; end; theorem :: WAYBEL_6:1 for S,T being Semilattice, f being Function of S,T holds f is meet-preserving iff for x,y being Element of S holds f.(x "/\" y) = f.x "/\" f.y; theorem :: WAYBEL_6:2 for S,T being sup-Semilattice, f being Function of S,T holds f is join-preserving iff for x,y being Element of S holds f.(x "\/" y) = f. x "\/" f .y; theorem :: WAYBEL_6:3 for S,T being LATTICE, f being Function of S,T st T is distributive & f is meet-preserving join-preserving one-to-one holds S is distributive; registration let S,T be complete LATTICE; cluster sups-preserving for Function of S,T; end; theorem :: WAYBEL_6:4 for S,T being complete LATTICE, f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving one-to-one holds S is meet-continuous; begin :: Open sets definition let L be non empty reflexive RelStr, X be Subset of L; attr X is Open means :: WAYBEL_6:def 1 for x be Element of L st x in X ex y be Element of L st y in X & y << x; end; theorem :: WAYBEL_6:5 for L be up-complete LATTICE, X be upper Subset of L holds X is Open iff for x be Element of L st x in X holds waybelow x meets X; theorem :: WAYBEL_6:6 ::3.2, p.68 for L be up-complete LATTICE, X be upper Subset of L holds X is Open iff X = union {wayabove x where x is Element of L : x in X}; registration let L be up-complete lower-bounded LATTICE; cluster Open for Filter of L; end; theorem :: WAYBEL_6:7 for L be lower-bounded continuous LATTICE, x be Element of L holds ( wayabove x) is Open; theorem :: WAYBEL_6:8 ::3.3, p.68 for L be lower-bounded continuous LATTICE, x,y be Element of L st x << y holds ex F be Open Filter of L st y in F & F c= wayabove x; theorem :: WAYBEL_6:9 ::3.4, p.69 for L being complete LATTICE, X being Open upper Subset of L holds for x being Element of L st x in (X`) ex m being Element of L st x <= m & m is_maximal_in (X`); begin :: Irreducible elements definition ::def 3.5, p.69 let G be non empty RelStr, g be Element of G; attr g is meet-irreducible means :: WAYBEL_6:def 2 for x,y being Element of G st g = x "/\" y holds x = g or y = g; end; notation ::def 3.5, p.69 let G be non empty RelStr, g be Element of G; synonym g is irreducible for g is meet-irreducible; end; definition let G be non empty RelStr, g be Element of G; attr g is join-irreducible means :: WAYBEL_6:def 3 for x,y being Element of G st g = x "\/" y holds x = g or y = g; end; definition let L be non empty RelStr; func IRR L -> Subset of L means :: WAYBEL_6:def 4 for x be Element of L holds x in it iff x is irreducible; end; theorem :: WAYBEL_6:10 for L being upper-bounded antisymmetric with_infima non empty RelStr holds Top L is irreducible; registration let L be upper-bounded antisymmetric with_infima non empty RelStr; cluster irreducible for Element of L; end; theorem :: WAYBEL_6:11 for L being Semilattice, x being Element of L holds x is irreducible iff for A being finite non empty Subset of L st x = inf A holds x in A; theorem :: WAYBEL_6:12 for L be LATTICE,l be Element of L st (uparrow l \ {l}) is Filter of L holds l is irreducible; theorem :: WAYBEL_6:13 ::3.6, p.69 for L be LATTICE, p be Element of L, F be Filter of L st p is_maximal_in (F`) holds p is irreducible; theorem :: WAYBEL_6:14 ::3.7, p.69 for L be lower-bounded continuous LATTICE, x,y be Element of L st not y <= x holds ex p be Element of L st p is irreducible & x <= p & not y <= p; begin :: Order generating sets definition let L be non empty RelStr, X be Subset of L; attr X is order-generating means :: WAYBEL_6:def 5 for x be Element of L holds ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X); end; theorem :: WAYBEL_6:15 ::3.9 (1-2), p.70 for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for l being Element of L ex Y be Subset of X st l = "/\" (Y,L); theorem :: WAYBEL_6:16 ::3.9 (1-3), p.70 for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for Y be Subset of L st X c= Y & for Z be Subset of Y holds "/\" (Z,L) in Y holds the carrier of L = Y; theorem :: WAYBEL_6:17 ::3.9 (1-4), p.70 for L be up-complete lower-bounded LATTICE, X be Subset of L holds X is order-generating iff for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st p in X & l1 <= p & not l2 <= p; theorem :: WAYBEL_6:18 ::3.10, p.70 for L be lower-bounded continuous LATTICE, X be Subset of L st X = IRR L \ { Top L} holds X is order-generating; theorem :: WAYBEL_6:19 for L being lower-bounded continuous LATTICE, X,Y being Subset of L st X is order-generating & X c= Y holds Y is order-generating; begin :: Prime elements definition let L be non empty RelStr; let l be Element of L; attr l is prime means :: WAYBEL_6:def 6 for x,y be Element of L st x "/\" y <= l holds x <= l or y <= l; end; definition let L be non empty RelStr; func PRIME L -> Subset of L means :: WAYBEL_6:def 7 for x be Element of L holds x in it iff x is prime; end; definition let L be non empty RelStr; let l be Element of L; attr l is co-prime means :: WAYBEL_6:def 8 l~ is prime; end; theorem :: WAYBEL_6:20 for L being upper-bounded antisymmetric non empty RelStr holds Top L is prime ; theorem :: WAYBEL_6:21 for L being lower-bounded antisymmetric non empty RelStr holds Bottom L is co-prime; registration let L be upper-bounded antisymmetric non empty RelStr; cluster prime for Element of L; end; theorem :: WAYBEL_6:22 for L being Semilattice, l being Element of L holds l is prime iff for A being finite non empty Subset of L st l >= inf A ex a being Element of L st a in A & l >= a; theorem :: WAYBEL_6:23 for L being sup-Semilattice, x being Element of L holds x is co-prime iff for A being finite non empty Subset of L st x <= sup A ex a being Element of L st a in A & x <= a; theorem :: WAYBEL_6:24 for L being LATTICE, l being Element of L st l is prime holds l is irreducible; theorem :: WAYBEL_6:25 ::3.12 (1-2), p.70 for l holds l is prime iff for x being set, f being Function of L,BoolePoset {x} st (for p be Element of L holds f.p = {} iff p <= l) holds f is meet-preserving join-preserving; theorem :: WAYBEL_6:26 ::3.12 (1-3), p.70 for L being upper-bounded LATTICE, l being Element of L st l <> Top L holds l is prime iff (downarrow l)` is Filter of L; theorem :: WAYBEL_6:27 ::3.12 (1-4), p.70 for L being distributive LATTICE for l being Element of L holds l is prime iff l is irreducible; theorem :: WAYBEL_6:28 for L being distributive LATTICE holds PRIME L = IRR L; theorem :: WAYBEL_6:29 ::3.12 (1-5), p.70 for L being Boolean LATTICE for l being Element of L st l <> Top L holds l is prime iff for x be Element of L st x > l holds x = Top L; theorem :: WAYBEL_6:30 ::3.12 (1-6), p.70 for L being continuous distributive lower-bounded LATTICE for l being Element of L st l <> Top L holds l is prime iff ex F being Open Filter of L st l is_maximal_in (F`); theorem :: WAYBEL_6:31 for L being RelStr, X being Subset of L holds chi(X, the carrier of L) is Function of L, BoolePoset {{}}; theorem :: WAYBEL_6:32 for L being non empty RelStr, p,x being Element of L holds chi(( downarrow p)`,the carrier of L).x = {} iff x <= p; theorem :: WAYBEL_6:33 for L being upper-bounded LATTICE, f being Function of L, BoolePoset {{}}, p being prime Element of L st chi((downarrow p)`,the carrier of L) = f holds f is meet-preserving join-preserving; theorem :: WAYBEL_6:34 ::3.13, p.71 for L being complete LATTICE st PRIME L is order-generating holds L is distributive meet-continuous; theorem :: WAYBEL_6:35 ::3.14 (1-3), p.71 for L being lower-bounded continuous LATTICE holds L is distributive iff PRIME L is order-generating; theorem :: WAYBEL_6:36 ::3.14 (1-2), p.71 for L being lower-bounded continuous LATTICE holds L is distributive iff L is Heyting; theorem :: WAYBEL_6:37 for L being continuous complete LATTICE st for l being Element of L ex X being Subset of L st l = sup X & for x being Element of L st x in X holds x is co-prime for l being Element of L holds l = "\/"((waybelow l) /\ PRIME(L opp), L); theorem :: WAYBEL_6:38 ::3.15 (2-1), p.72 for L being complete LATTICE holds L is completely-distributive iff L is continuous & for l being Element of L ex X being Subset of L st l = sup X & for x being Element of L st x in X holds x is co-prime; theorem :: WAYBEL_6:39 ::3.15 (2-3), p.72 for L being complete LATTICE holds L is completely-distributive iff L is distributive continuous & L opp is continuous;