:: Irreducible and Prime Elements
:: by Beata Madras
::
:: Received December 1, 1996
:: Copyright (c) 1996-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 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, CARD_1, RELAT_1, XCMPLX_0, NAT_1, FUNCT_7;
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;