The abstract of the Mizar article:

Irreducible and Prime Elements

by

Beata Madras

Received December 1, 1996

MML identifier: WAYBEL_6

[ Mizar article, MML identifier index ]

environ

 vocabulary WAYBEL_0, ORDERS_1, FUNCT_1, RELAT_1, FUNCT_4, QUANTAL1, RELAT_2,
      ORDINAL2, LATTICES, REALSET1, PRE_TOPC, YELLOW_0, BHSP_3, FUNCOP_1,
      BOOLE, LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, TARSKI, FILTER_0, SUBSET_1,
      ORDERS_2, ZFMISC_1, FINSET_1, YELLOW_1, FUNCT_3, FRAENKEL, LATTICE2,
      OPPCAT_1, WAYBEL_5, ZF_REFLE, PBOOLE, YELLOW_2, FUNCT_6, CARD_3, PRALG_1,
      FINSEQ_4, WAYBEL_6, HAHNBAN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      FINSET_1, RELAT_1, ORDINAL1, RELAT_2, REALSET1, STRUCT_0, ORDERS_1,
      PRE_TOPC, CARD_3, FRAENKEL, LATTICE3, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_6,
      PBOOLE, PRALG_1, PRALG_2, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1,
      YELLOW_2, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, BORSUK_1,
      YELLOW_7, FUNCT_7;
 constructors WAYBEL_5, WAYBEL_4, NAT_1, RELAT_2, BORSUK_1, YELLOW_4, ORDERS_3,
      WAYBEL_1, WAYBEL_2, WAYBEL_3, PRALG_2, FUNCT_7, MEMBERED;
 clusters SUBSET_1, WAYBEL_0, WAYBEL_2, WAYBEL_3, YELLOW_0, STRUCT_0, ORDERS_1,
      LATTICE3, PBOOLE, FINSET_1, WAYBEL_1, WAYBEL_5, PRALG_1, YELLOW_7,
      YELLOW_4, RELSET_1, ARYTM_3, XBOOLE_0, FRAENKEL, MEMBERED, ZFMISC_1,
      FUNCT_2, PARTFUN1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve x,y,Y,Z for set,
        L for LATTICE,
        l for Element of L,
        n,k for Nat;

:: Preliminaries

scheme NonUniqExD1 { Z() ->non empty RelStr, X() -> Subset of Z(),
                   Y() -> non empty Subset of Z(), P[set,set] }:
 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 LATTICE;
let A be non empty Subset of L;
let f be Function of A,A;
let n be Element of NAT;
 redefine func iter (f,n) -> Function of A,A;
end;


definition
let L be LATTICE;
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;

definition
let L be non empty Poset;
cluster -> filtered directed Chain of L;
end;

definition
cluster strict continuous distributive lower-bounded LATTICE;
end;

theorem :: WAYBEL_6:1
for S,T being Semilattice, f being map 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 map 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 map of S,T st T is distributive &
f is meet-preserving join-preserving one-to-one holds
S is distributive;


definition
let S,T be complete LATTICE;
cluster sups-preserving map of S,T;
end;


theorem :: WAYBEL_6:4
for S,T being complete LATTICE, f being sups-preserving map of S,T st
T is meet-continuous & f is meet-preserving one-to-one holds
S is meet-continuous;


begin :: Open sets

definition       ::def 3.1, p.68
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};


definition
let L be up-complete lower-bounded LATTICE;
cluster Open 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;
synonym g is 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;


definition
let L be upper-bounded antisymmetric with_infima non empty RelStr;
cluster irreducible 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 ::def 3.8, p.70
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   ::def 3.11, p.70
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;


definition
let L be upper-bounded antisymmetric non empty RelStr;
cluster prime 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 map 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 map 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 map 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;