:: Prime Ideals and Filters
:: by Grzegorz Bancerek
::
:: Received December 1, 1996
:: Copyright (c) 1996-2026 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 REWRITE1, WAYBEL_0, TARSKI, EQREL_1, XXREAL_0, LATTICES,
YELLOW_0, STRUCT_0, YELLOW_1, ZFMISC_1, ORDERS_2, WELLORD2, XXREAL_2,
RELAT_2, XBOOLE_0, SUBSET_1, CARD_FIL, XBOOLEAN, FINSET_1, SETFAM_1,
ORDINAL2, LATTICE3, INT_2, ARYTM_0, RELAT_1, WAYBEL_6, METRIC_1,
ORDINAL1, PRE_TOPC, RCOMP_1, WAYBEL_3, FUNCT_1, CANTOR_1, RLVECT_3,
MSSUBFAM, WAYBEL_4, CAT_1, MCART_1, WAYBEL_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1,
FUNCT_1, FINSET_1, FUNCT_2, DOMAIN_1, ORDERS_1, STRUCT_0, PRE_TOPC,
TOPS_2, CANTOR_1, ORDINAL1, ORDERS_2, LATTICE3, ALG_1, YELLOW_0,
WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, YELLOW_7, WAYBEL_6,
WAYBEL_4;
constructors SETFAM_1, DOMAIN_1, TOPS_2, TEX_2, CANTOR_1, WAYBEL_1, YELLOW_3,
YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6;
registrations XBOOLE_0, SUBSET_1, FINSET_1, STRUCT_0, PRE_TOPC, LATTICE3,
YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3,
WAYBEL_4, YELLOW_7, WAYBEL_6, RELAT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, YELLOW_0, WAYBEL_0, PRE_TOPC, TOPS_2, WAYBEL_3, WAYBEL_6,
XBOOLE_0, STRUCT_0;
equalities YELLOW_0, WAYBEL_0, WAYBEL_3, SUBSET_1, STRUCT_0;
expansions TARSKI, YELLOW_0, WAYBEL_0, PRE_TOPC, TOPS_2, WAYBEL_3, WAYBEL_6,
XBOOLE_0, SUBSET_1, STRUCT_0;
theorems TARSKI, ZFMISC_1, SUBSET_1, CANTOR_1, TOPS_2, SETFAM_1, ORDERS_2,
YELLOW_0, WAYBEL_0, ORDERS_1, YELLOW_2, WAYBEL_1, YELLOW_1, WAYBEL_3,
FINSET_1, FUNCT_1, LATTICE3, WAYBEL_6, YELLOW_7, WAYBEL_5, WAYBEL_4,
YELLOW_3, MCART_1, FUNCT_5, YELLOW_5, ORDINAL1, XBOOLE_0, XBOOLE_1,
STRUCT_0;
schemes FUNCT_1, FINSET_1;
begin
theorem Th1:
for L being complete LATTICE, X,Y being set st X c= Y holds "\/"(
X,L) <= "\/"(Y,L) & "/\"(X,L) >= "/\"(Y,L)
proof
let L be complete LATTICE, X,Y be set;
A1: ex_inf_of X,L & ex_inf_of Y,L by YELLOW_0:17;
ex_sup_of X,L & ex_sup_of Y,L by YELLOW_0:17;
hence thesis by A1,YELLOW_0:34,35;
end;
theorem Th2:
for X being set holds the carrier of BoolePoset X = bool X
proof
let X be set;
set L = BoolePoset X;
L = InclPoset bool X by YELLOW_1:4;
then L = RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
hence thesis;
end;
theorem
for L being bounded antisymmetric non empty RelStr holds L is
trivial iff Top L = Bottom L
proof
let L be bounded antisymmetric non empty RelStr;
thus L is trivial implies Top L = Bottom L;
assume
A1: Top L = Bottom L;
let x,y be Element of L;
reconsider x, y as Element of L;
x >= Bottom L & x <= Bottom L by A1,YELLOW_0:44,45;
then
A2: x = Bottom L by ORDERS_2:2;
y >= Bottom L & y <= Bottom L by A1,YELLOW_0:44,45;
hence thesis by A2,ORDERS_2:2;
end;
registration
let X be set;
cluster BoolePoset X -> Boolean;
coherence;
end;
registration
let X be non empty set;
cluster BoolePoset X -> non trivial;
coherence
proof
Top BoolePoset X = X & Bottom BoolePoset X = {} by YELLOW_1:18,19;
hence thesis;
end;
end;
theorem Th4:
for L being lower-bounded non empty Poset, F being Filter of L
holds F is proper iff not Bottom L in F
proof
let L be lower-bounded non empty Poset, F be Filter of L;
hereby
assume F is proper;
then F <> the carrier of L;
then consider a being object such that
A1: not (a in F iff a in the carrier of L) by TARSKI:2;
reconsider a as Element of L by A1;
a >= Bottom L by YELLOW_0:44;
hence not Bottom L in F by A1,WAYBEL_0:def 20;
end;
assume not Bottom L in F;
then F <> the carrier of L;
hence thesis;
end;
registration
cluster non trivial Boolean strict for LATTICE;
existence
proof
take BoolePoset {{}};
thus thesis;
end;
end;
registration
let L be upper-bounded non trivial Poset;
cluster proper for Filter of L;
existence
proof
take F = uparrow Top L;
assume F is not proper;
then
A1: F = the carrier of L;
now
let x,y be Element of L;
A2: F = {Top L} by WAYBEL_4:24;
then x = Top L by A1,TARSKI:def 1;
hence x = y by A1,A2,TARSKI:def 1;
end;
hence thesis by STRUCT_0:def 10;
end;
end;
theorem Th5:
for X being set, a being Element of BoolePoset X holds 'not' a = X \ a
proof
let X be set, a be Element of BoolePoset X;
A1: the carrier of BoolePoset X = bool X by Th2;
reconsider b = X\a as Element of BoolePoset X by Th2;
A2: a misses b by XBOOLE_1:79;
A3: a"/\"b = a /\ b by YELLOW_1:17
.= {} by A2
.= Bottom BoolePoset X by YELLOW_1:18;
a"\/"b = a \/ b by YELLOW_1:17
.= X by A1,XBOOLE_1:45
.= Top BoolePoset X by YELLOW_1:19;
then b is_a_complement_of a by A3,WAYBEL_1:def 23;
hence thesis by YELLOW_5:11;
end;
theorem
for X being set, Y being Subset of BoolePoset X holds Y is lower iff
for x,y being set st x c= y & y in Y holds x in Y
proof
let X be set, Y be Subset of BoolePoset X;
A1: the carrier of BoolePoset X = bool X by Th2;
hereby
assume
A2: Y is lower;
let x,y be set;
assume that
A3: x c= y and
A4: y in Y;
reconsider a = x, b = y as Element of BoolePoset X by A1,A3,A4,XBOOLE_1:1;
a <= b by A3,YELLOW_1:2;
hence x in Y by A2,A4;
end;
assume
A5: for x,y being set st x c= y & y in Y holds x in Y;
let a,b be Element of BoolePoset X;
assume that
A6: a in Y and
A7: b <= a;
b c= a by A7,YELLOW_1:2;
hence thesis by A5,A6;
end;
theorem Th7:
for X being set, Y being Subset of BoolePoset X holds Y is upper
iff for x,y being set st x c= y & y c= X & x in Y holds y in Y
proof
let X be set, Y be Subset of BoolePoset X;
A1: the carrier of BoolePoset X = bool X by Th2;
hereby
assume
A2: Y is upper;
let x,y be set;
assume that
A3: x c= y and
A4: y c= X and
A5: x in Y;
reconsider a = x, b = y as Element of BoolePoset X by A4,A5,Th2;
a <= b by A3,YELLOW_1:2;
hence y in Y by A2,A5;
end;
assume
A6: for x,y being set st x c= y & y c= X & x in Y holds y in Y;
let a,b be Element of BoolePoset X;
assume that
A7: a in Y and
A8: b >= a;
a c= b by A8,YELLOW_1:2;
hence thesis by A1,A6,A7;
end;
theorem
for X being set, Y being lower Subset of BoolePoset X holds Y is
directed iff for x,y being set st x in Y & y in Y holds x \/ y in Y
proof
let X be set, Y be lower Subset of BoolePoset X;
hereby
assume
A1: Y is directed;
let x,y be set;
assume
A2: x in Y & y in Y;
then reconsider a = x, b = y as Element of BoolePoset X;
a"\/"b in Y by A1,A2,WAYBEL_0:40;
hence x \/ y in Y by YELLOW_1:17;
end;
assume
A3: for x,y being set st x in Y & y in Y holds x \/ y in Y;
now
let a,b be Element of BoolePoset X;
assume a in Y & b in Y;
then a \/ b in Y by A3;
hence a"\/"b in Y by YELLOW_1:17;
end;
hence thesis by WAYBEL_0:40;
end;
theorem Th9:
for X being set, Y being upper Subset of BoolePoset X holds Y is
filtered iff for x,y being set st x in Y & y in Y holds x /\ y in Y
proof
let X be set, Y be upper Subset of BoolePoset X;
hereby
assume
A1: Y is filtered;
let x,y be set;
assume
A2: x in Y & y in Y;
then reconsider a = x, b = y as Element of BoolePoset X;
a"/\"b in Y by A1,A2,WAYBEL_0:41;
hence x /\ y in Y by YELLOW_1:17;
end;
assume
A3: for x,y being set st x in Y & y in Y holds x /\ y in Y;
now
let a,b be Element of BoolePoset X;
assume a in Y & b in Y;
then a /\ b in Y by A3;
hence a"/\"b in Y by YELLOW_1:17;
end;
hence thesis by WAYBEL_0:41;
end;
theorem
for X being set, Y being non empty lower Subset of BoolePoset X holds
Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds union Z
in Y
proof
let X be set, Y be non empty lower Subset of BoolePoset X;
hereby
assume
A1: Y is directed;
let Z be finite Subset-Family of X;
reconsider B = Z as Subset of BoolePoset X by Th2;
assume Z c= Y;
then reconsider A = Z as finite Subset of Y;
A2: A <> {} implies sup B in Y by A1,WAYBEL_0:42;
Bottom BoolePoset X in Y by A1,WAYBEL_4:21;
hence union Z in Y by A2,YELLOW_1:18,21,ZFMISC_1:2;
end;
assume
A3: for Z being finite Subset-Family of X st Z c= Y holds union Z in Y;
A4: the carrier of BoolePoset X = bool X by Th2;
now
let A be finite Subset of Y;
reconsider Z = A as finite Subset-Family of X by A4,XBOOLE_1:1;
assume A <> {};
reconsider Z as finite Subset-Family of X;
A c= the carrier of BoolePoset X by XBOOLE_1:1;
then union Z = "\/"(A, BoolePoset X) by YELLOW_1:21;
hence "\/"(A, BoolePoset X) in Y by A3;
end;
hence thesis by WAYBEL_0:42;
end;
theorem Th11:
for X being set, Y being non empty upper Subset of BoolePoset X
holds Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y
proof
let X be set, Y be non empty upper Subset of BoolePoset X;
hereby
assume
A1: Y is filtered;
then Top BoolePoset X in Y by WAYBEL_4:22;
then
A2: X in Y by YELLOW_1:19;
let Z be finite Subset-Family of X;
reconsider B = Z as Subset of BoolePoset X by Th2;
assume Z c= Y;
then reconsider A = Z as finite Subset of Y;
A <> {} implies inf B in Y & inf B = meet B by A1,WAYBEL_0:43,YELLOW_1:20;
hence Intersect Z in Y by A2,SETFAM_1:def 9;
end;
assume
A3: for Z being finite Subset-Family of X st Z c= Y holds Intersect Z in Y;
A4: the carrier of BoolePoset X = bool X by Th2;
now
let A be finite Subset of Y;
reconsider Z = A as finite Subset-Family of X by A4,XBOOLE_1:1;
assume
A5: A <> {};
reconsider Z as finite Subset-Family of X;
A c= the carrier of BoolePoset X by XBOOLE_1:1;
then "/\"(A, BoolePoset X) = meet Z by A5,YELLOW_1:20
.= Intersect Z by A5,SETFAM_1:def 9;
hence "/\"(A, BoolePoset X) in Y by A3;
end;
hence thesis by WAYBEL_0:43;
end;
begin :: Prime ideals and filters
definition
let L be with_infima Poset;
let I be Ideal of L;
attr I is prime means
: Def1:
for x,y being Element of L st x"/\"y in I holds x in I or y in I;
end;
theorem Th12:
for L being with_infima Poset, I being Ideal of L holds I is
prime iff for A being finite non empty Subset of L st inf A in I ex a being
Element of L st a in A & a in I
proof
let L be with_infima Poset, I be Ideal of L;
thus I is prime implies for A being finite non empty Subset of L st inf A in
I ex a being Element of L st a in A & a in I
proof
defpred P[set] means $1 is non empty & "/\"($1,L) in I implies ex a being
Element of L st a in $1 & a in I;
assume
A1: for x,y being Element of L st x"/\"y in I holds x in I or y in I;
let A be finite non empty Subset of L;
A2: now
let x,B be set such that
A3: x in A and
A4: B c= A and
A5: P[B];
thus P[B \/ {x}]
proof
reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by A4,XBOOLE_1:1;
assume that
B \/ {x} is non empty and
A6: "/\"(B \/ {x},L) in I;
per cases;
suppose
B = {};
then "/\"(B \/ {a},L) = a & a in B \/ {a} by TARSKI:def 1,YELLOW_0:39
;
hence thesis by A6;
end;
suppose
A7: B <> {};
A8: inf {a} = a by YELLOW_0:39;
A9: ex_inf_of {a}, L by YELLOW_0:55;
ex_inf_of C, L by A7,YELLOW_0:55;
then
A10: "/\"(B \/ {x},L) = (inf C)"/\"inf {a} by A9,YELLOW_2:4;
hereby
per cases by A1,A6,A10,A8;
suppose
inf C in I;
then consider b being Element of L such that
A11: b in B & b in I by A5,A7;
take b;
thus b in B \/ {x} & b in I by A11,XBOOLE_0:def 3;
end;
suppose
A12: a in I;
take a;
a in {a} by TARSKI:def 1;
hence a in B \/ {x} & a in I by A12,XBOOLE_0:def 3;
end;
end;
end;
end;
end;
A13: P[{}];
A14: A is finite;
P[A] from FINSET_1:sch 2(A14,A13,A2);
hence thesis;
end;
assume
A15: for A being finite non empty Subset of L st inf A in I ex a being
Element of L st a in A & a in I;
let a,b be Element of L;
assume a"/\"b in I;
then inf {a,b} in I by YELLOW_0:40;
then ex x being Element of L st x in {a,b} & x in I by A15;
hence thesis by TARSKI:def 2;
end;
registration
let L be LATTICE;
cluster prime for Ideal of L;
existence
proof
take [#]L;
let x,y be Element of L;
thus thesis;
end;
end;
theorem
for L1, L2 being LATTICE st the RelStr of L1 = the RelStr of L2 for x
being set st x is prime Ideal of L1 holds x is prime Ideal of L2
proof
let L1,L2 be LATTICE such that
A1: the RelStr of L1 = the RelStr of L2;
let x be set;
assume x is prime Ideal of L1;
then reconsider I = x as prime Ideal of L1;
reconsider I9 = I as Subset of L2 by A1;
reconsider I9 as Ideal of L2 by A1,WAYBEL_0:3,25;
I9 is prime
proof
let x,y be Element of L2;
reconsider a = x, b = y as Element of L1 by A1;
A2: x"/\"y = inf {x,y} by YELLOW_0:40;
ex_inf_of {a,b}, L1 & a"/\"b = inf {a,b} by YELLOW_0:21,40;
then a"/\"b = x"/\"y by A1,A2,YELLOW_0:27;
hence thesis by Def1;
end;
hence thesis;
end;
definition
let L be with_suprema Poset;
let F be Filter of L;
attr F is prime means
: Def2:
for x,y being Element of L st x"\/"y in F holds x in F or y in F;
end;
theorem
for L being with_suprema Poset, F being Filter of L holds F is prime
iff for A being finite non empty Subset of L st sup A in F ex a being Element
of L st a in A & a in F
proof
let L be with_suprema Poset, I be Filter of L;
thus I is prime implies for A being finite non empty Subset of L st sup A in
I ex a being Element of L st a in A & a in I
proof
defpred P[set] means $1 is non empty & "\/"($1,L) in I implies ex a being
Element of L st a in $1 & a in I;
assume
A1: for x,y being Element of L st x"\/"y in I holds x in I or y in I;
let A be finite non empty Subset of L;
A2: now
let x,B be set such that
A3: x in A and
A4: B c= A and
A5: P[B];
thus P[B \/ {x}]
proof
reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by A4,XBOOLE_1:1;
assume that
B \/ {x} is non empty and
A6: "\/"(B \/ {x},L) in I;
per cases;
suppose
B = {};
then "\/"(B \/ {a},L) = a & a in B \/ {a} by TARSKI:def 1,YELLOW_0:39
;
hence thesis by A6;
end;
suppose
A7: B <> {};
A8: sup {a} = a by YELLOW_0:39;
A9: ex_sup_of {a}, L by YELLOW_0:54;
ex_sup_of C, L by A7,YELLOW_0:54;
then
A10: "\/"(B \/ {x},L) = (sup C)"\/"sup {a} by A9,YELLOW_2:3;
hereby
per cases by A1,A6,A10,A8;
suppose
sup C in I;
then consider b being Element of L such that
A11: b in B & b in I by A5,A7;
take b;
thus b in B \/ {x} & b in I by A11,XBOOLE_0:def 3;
end;
suppose
A12: a in I;
take a;
a in {a} by TARSKI:def 1;
hence a in B \/ {x} & a in I by A12,XBOOLE_0:def 3;
end;
end;
end;
end;
end;
A13: P[{}];
A14: A is finite;
P[A] from FINSET_1:sch 2(A14,A13,A2);
hence thesis;
end;
assume
A15: for A being finite non empty Subset of L st sup A in I ex a being
Element of L st a in A & a in I;
let a,b be Element of L;
assume a"\/"b in I;
then sup {a,b} in I by YELLOW_0:41;
then ex x being Element of L st x in {a,b} & x in I by A15;
hence thesis by TARSKI:def 2;
end;
registration
let L be LATTICE;
cluster prime for Filter of L;
existence
proof
take [#]L;
let x,y be Element of L;
thus thesis;
end;
end;
theorem Th15:
for L1, L2 being LATTICE st the RelStr of L1 = the RelStr of L2
for x being set st x is prime Filter of L1 holds x is prime Filter of L2
proof
let L1,L2 be LATTICE such that
A1: the RelStr of L1 = the RelStr of L2;
let x be set;
assume x is prime Filter of L1;
then reconsider I = x as prime Filter of L1;
reconsider I9 = I as Subset of L2 by A1;
reconsider I9 as Filter of L2 by A1,WAYBEL_0:4,25;
I9 is prime
proof
let x,y be Element of L2;
reconsider a = x, b = y as Element of L1 by A1;
A2: x"\/"y = sup {x,y} by YELLOW_0:41;
ex_sup_of {a,b}, L1 & a"\/"b = sup {a,b} by YELLOW_0:20,41;
then a"\/"b = x"\/"y by A1,A2,YELLOW_0:26;
hence thesis by Def2;
end;
hence thesis;
end;
theorem Th16:
for L being LATTICE, x being set holds x is prime Ideal of L iff
x is prime Filter of L opp
proof
let L be LATTICE, x be set;
hereby
assume x is prime Ideal of L;
then reconsider I = x as prime Ideal of L;
reconsider F = I as Filter of L opp by YELLOW_7:26,28;
F is prime
proof
let x,y be Element of L opp;
A1: x"\/"y = (~x)"/\"(~y) by YELLOW_7:22;
~x = x & ~y = y by LATTICE3:def 7;
hence thesis by A1,Def1;
end;
hence x is prime Filter of L opp;
end;
assume x is prime Filter of L opp;
then reconsider I = x as prime Filter of L opp;
reconsider F = I as Ideal of L by YELLOW_7:26,28;
F is prime
proof
let x,y be Element of L;
A2: x"/\"y = (x~)"\/"(y~) by YELLOW_7:21;
x~ = x & y~ = y by LATTICE3:def 6;
hence thesis by A2,Def2;
end;
hence thesis;
end;
theorem Th17:
for L being LATTICE, x being set holds x is prime Filter of L
iff x is prime Ideal of L opp
proof
let L be LATTICE, x be set;
L opp opp = the RelStr of L by LATTICE3:8;
then x is prime Filter of L iff x is prime Filter of L opp opp by Th15;
hence thesis by Th16;
end;
:: Remark 3.16: (3) iff (2)
theorem
for L being with_infima Poset, I being Ideal of L holds I is prime iff
I` is Filter of L or I` = {}
proof
let L be with_infima Poset, I be Ideal of L;
set F = I`;
thus I is prime implies I` is Filter of L or I` = {}
proof
assume
A1: for x,y being Element of L st x"/\"y in I holds x in I or y in I;
A2: F is filtered
proof
let x,y be Element of L;
assume x in F & y in F;
then ( not x in I)& not y in I by XBOOLE_0:def 5;
then
A3: x"/\"y in F by A1,SUBSET_1:29;
x"/\"y <= x & x"/\" y <= y by YELLOW_0:23;
hence thesis by A3;
end;
F is upper
proof
let x,y be Element of L;
assume that
A4: x in F and
A5: y >= x;
y in I implies x in I by A5,WAYBEL_0:def 19;
hence thesis by A4,XBOOLE_0:def 5;
end;
hence thesis by A2;
end;
assume
A6: I` is Filter of L or I` = {};
let x,y be Element of L;
assume x"/\"y in I;
then not x"/\"y in F by XBOOLE_0:def 5;
then not x in F or not y in F by A6,WAYBEL_0:41;
hence thesis by SUBSET_1:29;
end;
:: Remark 3.16: (3) iff (1)
theorem
for L being LATTICE, I being Ideal of L holds I is prime iff I in
PRIME InclPoset Ids L
proof
let L be LATTICE, I be Ideal of L;
set P = InclPoset Ids L;
A1: P = RelStr(#Ids L, RelIncl Ids L#) by YELLOW_1:def 1;
I in Ids L;
then reconsider i = I as Element of InclPoset Ids L by A1;
thus I is prime implies I in PRIME InclPoset Ids L
proof
assume
A2: for x,y being Element of L st x"/\"y in I holds x in I or y in I;
i is prime
proof
let x,y be Element of P;
y in Ids L by A1;
then
A3: ex J being Ideal of L st y = J;
x in Ids L by A1;
then ex J being Ideal of L st x = J;
then reconsider X = x, Y = y as Ideal of L by A3;
assume x "/\" y <= i;
then x "/\" y c= I by YELLOW_1:3;
then
A4: X /\ Y c= I by YELLOW_2:43;
assume that
A5: not x <= i and
A6: not y <= i;
not X c= I by A5,YELLOW_1:3;
then consider a being object such that
A7: a in X and
A8: not a in I;
not Y c= I by A6,YELLOW_1:3;
then consider b being object such that
A9: b in Y and
A10: not b in I;
reconsider a,b as Element of L by A7,A9;
a "/\" b <= b by YELLOW_0:23;
then
A11: a"/\"b in Y by A9,WAYBEL_0:def 19;
a "/\" b <= a by YELLOW_0:23;
then a"/\"b in X by A7,WAYBEL_0:def 19;
then a"/\"b in X /\ Y by A11,XBOOLE_0:def 4;
hence thesis by A2,A4,A8,A10;
end;
hence thesis by WAYBEL_6:def 7;
end;
assume
A12: I in PRIME P;
let x,y be Element of L;
reconsider X = downarrow x, Y = downarrow y as Ideal of L;
X in Ids L & Y in Ids L;
then reconsider X, Y as Element of P by A1;
A13: X /\ Y = X"/\"Y by YELLOW_2:43;
assume
A14: x"/\"y in I;
X"/\"Y c= I
proof
let a be object;
assume
A15: a in X"/\"Y;
then
A16: a in X by A13,XBOOLE_0:def 4;
A17: a in Y by A13,A15,XBOOLE_0:def 4;
reconsider a as Element of L by A16;
A18: a <= y by A17,WAYBEL_0:17;
a <= x by A16,WAYBEL_0:17;
then a <= x"/\"y by A18,YELLOW_0:23;
hence thesis by A14,WAYBEL_0:def 19;
end;
then
A19: X"/\"Y <= i by YELLOW_1:3;
i is prime by A12,WAYBEL_6:def 7;
then X <= i or Y <= i by A19;
then
A20: X c= I or Y c= I by YELLOW_1:3;
y <= y;
then
A21: y in Y by WAYBEL_0:17;
x <= x;
then x in X by WAYBEL_0:17;
hence thesis by A21,A20;
end;
theorem Th20:
for L being Boolean LATTICE, F being Filter of L holds F is
prime iff for a being Element of L holds a in F or 'not' a in F
proof
let L be Boolean LATTICE;
let F be Filter of L;
hereby
assume
A1: F is prime;
let a be Element of L;
set b = 'not' a;
a"\/"b = Top L by YELLOW_5:34;
then a"\/"b in F by WAYBEL_4:22;
hence a in F or b in F by A1;
end;
assume
A2: for a being Element of L holds a in F or 'not' a in F;
let a,b be Element of L;
assume that
A3: a"\/"b in F and
A4: not a in F and
A5: not b in F;
'not' a in F & 'not' b in F by A2,A4,A5;
then ('not' a)"/\"'not' b in F by WAYBEL_0:41;
then 'not' (a"\/"b) in F by YELLOW_5:36;
then 'not' (a"\/"b)"/\"(a"\/"b) in F by A3,WAYBEL_0:41;
then
A6: Bottom L in F by YELLOW_5:34;
a >= Bottom L by YELLOW_0:44;
hence contradiction by A4,A6,WAYBEL_0:def 20;
end;
:: Remark 3.18: (1) iff (2)
theorem Th21:
for X being set, F being Filter of BoolePoset X holds F is prime
iff for A being Subset of X holds A in F or X\A in F
proof
let X be set;
set L = BoolePoset X;
let F be Filter of L;
L = InclPoset bool X by YELLOW_1:4;
then
A1: L = RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
hereby
assume
A2: F is prime;
let A be Subset of X;
reconsider a = A as Element of L by A1;
a in F or 'not' a in F by A2,Th20;
hence A in F or X\A in F by Th5;
end;
assume
A3: for A being Subset of X holds A in F or X\A in F;
now
let a be Element of L;
'not' a = X\a by Th5;
hence a in F or 'not' a in F by A1,A3;
end;
hence thesis by Th20;
end;
definition
let L be non empty Poset;
let F be Filter of L;
attr F is ultra means
F is proper & for G being Filter of L st F c=
G holds F = G or G = the carrier of L;
end;
registration
let L be non empty Poset;
cluster ultra -> proper for Filter of L;
coherence;
end;
Lm1: for L being with_infima Poset for F being Filter of L, X being finite non
empty Subset of L for x being Element of L st x in uparrow fininfs (F \/ X) ex
a being Element of L st a in F & x >= a "/\" inf X
proof
let L be with_infima Poset;
let I be Filter of L, X be finite non empty Subset of L;
let x be Element of L;
set i = the Element of I;
reconsider i as Element of L;
assume x in uparrow fininfs (I \/ X);
then consider u being Element of L such that
A1: u <= x and
A2: u in fininfs (I \/ X) by WAYBEL_0:def 16;
consider Y being finite Subset of I \/ X such that
A3: u = "/\"(Y,L) and
A4: ex_inf_of Y,L by A2;
Y\X c= I
proof
let a be object;
assume
A5: a in Y\X;
then not a in X by XBOOLE_0:def 5;
hence thesis by A5,XBOOLE_0:def 3;
end;
then reconsider Z = Y\X as finite Subset of I;
reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z9 \/ X as finite Subset of L;
per cases;
suppose
A6: Z = {};
A7: inf X >= i"/\"inf X by YELLOW_0:23;
take i;
A8: ex_inf_of X,L by YELLOW_0:55;
Y c= X by A6,XBOOLE_1:37;
then u >= inf X by A3,A4,A8,YELLOW_0:35;
then u >= i"/\"inf X by A7,ORDERS_2:3;
hence thesis by A1,ORDERS_2:3;
end;
suppose
A9: Z <> {};
take inf Z9;
A10: ex_inf_of X, L by YELLOW_0:55;
A11: ex_inf_of ZX,L by YELLOW_0:55;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z9 \/ X by XBOOLE_1:39;
then
A12: inf Y9 >= inf ZX by A4,A11,YELLOW_0:35;
ex_inf_of Z9,L by A9,YELLOW_0:55;
then inf (Z9 \/ X) = (inf Z9)"/\"inf X by A10,A11,YELLOW_0:37;
hence thesis by A1,A3,A9,A12,ORDERS_2:3,WAYBEL_0:43;
end;
end;
:: Remark 3.18: (1)+proper iff (3)
theorem Th22:
for L being Boolean LATTICE, F being Filter of L holds F is
proper prime iff F is ultra
proof
let L be Boolean LATTICE;
let F be Filter of L;
thus F is proper prime implies F is ultra
proof
assume
A1: F is proper;
assume
A2: for x,y being Element of L st x"\/"y in F holds x in F or y in F;
thus F is proper by A1;
let G be Filter of L;
assume that
A3: F c= G and
A4: F <> G;
consider x being object such that
A5: not (x in F iff x in G) by A4,TARSKI:2;
reconsider x as Element of L by A5;
set y = 'not' x;
x"\/"y = Top L by YELLOW_5:34;
then y in F by A2,A3,A5,WAYBEL_4:22;
then x"/\"y in G by A3,A5,WAYBEL_0:41;
then
A6: Bottom L in G by YELLOW_5:34;
thus G c= the carrier of L;
let x be object;
assume x in the carrier of L;
then reconsider x as Element of L;
x >= Bottom L by YELLOW_0:44;
hence thesis by A6,WAYBEL_0:def 20;
end;
assume that
A7: F is proper and
A8: for G being Filter of L st F c= G holds F = G or G = the carrier of L;
thus F is proper by A7;
now
let a be Element of L;
assume that
A9: not a in F and
A10: not 'not' a in F;
set b = 'not' a;
A11: F \/ {a} c= uparrow fininfs (F \/ { a}) by WAYBEL_0:62;
{a} c= F \/ {a} & a in {a} by TARSKI:def 1,XBOOLE_1:7;
then a in F \/ {a};
then F c= F \/ {a} & a in uparrow fininfs (F \/ {a}) by A11,XBOOLE_1:7;
then uparrow fininfs (F \/ {a}) = the carrier of L by A8,A9,A11,XBOOLE_1:1;
then consider c being Element of L such that
A12: c in F and
A13: b >= c "/\" inf {a} by Lm1;
c <= Top L by YELLOW_0:45;
then
A14: c = c"/\"Top L by YELLOW_0:25
.= c"/\"(a"\/"b) by YELLOW_5:34
.= (c"/\"a) "\/" (c"/\"b) by WAYBEL_1:def 3;
inf {a} = a & c"/\"b <= b by YELLOW_0:23,39;
then c <= b by A13,A14,YELLOW_0:22;
hence contradiction by A10,A12,WAYBEL_0:def 20;
end;
hence thesis by Th20;
end;
Lm2: for L being with_suprema Poset for I being Ideal of L, X being finite non
empty Subset of L for x being Element of L st x in downarrow finsups (I \/ X)
ex i being Element of L st i in I & x <= i "\/" sup X
proof
let L be with_suprema Poset;
let I be Ideal of L, X be finite non empty Subset of L;
let x be Element of L;
set i = the Element of I;
reconsider i as Element of L;
assume x in downarrow finsups (I \/ X);
then consider u being Element of L such that
A1: u >= x and
A2: u in finsups (I \/ X) by WAYBEL_0:def 15;
consider Y being finite Subset of I \/ X such that
A3: u = "\/"(Y,L) and
A4: ex_sup_of Y,L by A2;
Y\X c= I
proof
let a be object;
assume
A5: a in Y\X;
then not a in X by XBOOLE_0:def 5;
hence thesis by A5,XBOOLE_0:def 3;
end;
then reconsider Z = Y\X as finite Subset of I;
reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z9 \/ X as finite Subset of L;
per cases;
suppose
A6: Z = {};
A7: sup X <= i"\/"sup X by YELLOW_0:22;
take i;
A8: ex_sup_of X,L by YELLOW_0:54;
Y c= X by A6,XBOOLE_1:37;
then u <= sup X by A3,A4,A8,YELLOW_0:34;
then u <= i"\/"sup X by A7,ORDERS_2:3;
hence thesis by A1,ORDERS_2:3;
end;
suppose
A9: Z <> {};
take sup Z9;
A10: ex_sup_of X, L by YELLOW_0:54;
A11: ex_sup_of ZX,L by YELLOW_0:54;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z9 \/ X by XBOOLE_1:39;
then
A12: sup Y9 <= sup ZX by A4,A11,YELLOW_0:34;
ex_sup_of Z9,L by A9,YELLOW_0:54;
then sup (Z9 \/ X) = (sup Z9)"\/"sup X by A10,A11,YELLOW_0:36;
hence thesis by A1,A3,A9,A12,ORDERS_2:3,WAYBEL_0:42;
end;
end;
:: Lemma 3.19
theorem Th23:
for L being distributive LATTICE, I being Ideal of L, F being
Filter of L st I misses F ex P being Ideal of L st P is prime & I c= P & P
misses F
proof
let L be distributive LATTICE, I be Ideal of L, F be Filter of L such that
A1: I misses F;
set X = {P where P is Ideal of L: I c= P & P misses F};
A2: now
let A be set;
assume A in X;
then ex P being Ideal of L st A = P & I c= P & P misses F;
hence I c= A & A misses F;
end;
A3: now
let Z be set such that
A4: Z <> {} and
A5: Z c= X and
A6: Z is c=-linear;
Z c= bool the carrier of L
proof
let x be object;
assume x in Z;
then x in X by A5;
then ex P being Ideal of L st x = P & I c= P & P misses F;
hence thesis;
end;
then reconsider ZI = Z as Subset-Family of L;
now
let A be Subset of L;
assume A in ZI;
then A in X by A5;
then ex P being Ideal of L st A = P & I c= P & P misses F;
hence A is lower;
end;
then reconsider J = union ZI as lower Subset of L by WAYBEL_0:26;
A7: now
set y = the Element of Z;
y in Z by A4;
then
A8: I c= y by A2,A5;
A9: y c= J by A4,ZFMISC_1:74;
hence I c= J by A8;
thus J is non empty by A8,A9;
let A,B be Subset of L;
assume
A10: A in ZI & B in ZI;
then A, B are_c=-comparable by A6,ORDINAL1:def 8;
then A c= B or B c= A;
then A \/ B = A or A \/ B = B by XBOOLE_1:12;
hence ex C being Subset of L st C in ZI & A \/ B c= C by A10;
end;
now
let A be Subset of L;
assume A in ZI;
then A in X by A5;
then ex P being Ideal of L st A = P & I c= P & P misses F;
hence A is directed;
end;
then reconsider J as Ideal of L by A7,WAYBEL_0:46;
now
let x be object;
assume x in J;
then consider A being set such that
A11: x in A and
A12: A in Z by TARSKI:def 4;
A misses F by A2,A5,A12;
hence not x in F by A11,XBOOLE_0:3;
end;
then J misses F by XBOOLE_0:3;
hence union Z in X by A7;
end;
I in X by A1;
then consider Y being set such that
A13: Y in X and
A14: for Z being set st Z in X & Z <> Y holds not Y c= Z by A3,ORDERS_1:67;
consider P being Ideal of L such that
A15: P = Y and
A16: I c= P and
A17: P misses F by A13;
take P;
hereby
let x,y be Element of L;
assume that
A18: x"/\"y in P and
A19: not x in P and
A20: not y in P;
set Py = downarrow finsups (P \/ {y});
A21: P \/ {y} c= Py by WAYBEL_0:61;
A22: P c= P \/ {y} by XBOOLE_1:7;
then P c= Py by A21;
then
A23: I c= Py by A16;
y in {y} by TARSKI:def 1;
then y in P \/ {y} by XBOOLE_0:def 3;
then
A24: y in Py by A21;
now
assume Py misses F;
then Py in X by A23;
hence contradiction by A14,A15,A20,A21,A22,A24,XBOOLE_1:1;
end;
then consider v being object such that
A25: v in Py and
A26: v in F by XBOOLE_0:3;
set Px = downarrow finsups (P \/ {x});
A27: P \/ {x} c= Px by WAYBEL_0:61;
A28: P c= P \/ {x} by XBOOLE_1:7;
then P c= Px by A27;
then
A29: I c= Px by A16;
x in {x} by TARSKI:def 1;
then x in P \/ {x} by XBOOLE_0:def 3;
then
A30: x in Px by A27;
now
assume Px misses F;
then Px in X by A29;
hence contradiction by A14,A15,A19,A27,A28,A30,XBOOLE_1:1;
end;
then consider u being object such that
A31: u in Px and
A32: u in F by XBOOLE_0:3;
reconsider u, v as Element of L by A31,A25;
consider u9 being Element of L such that
A33: u9 in P and
A34: u <= u9 "\/" sup {x} by A31,Lm2;
consider v9 being Element of L such that
A35: v9 in P and
A36: v <= v9 "\/" sup {y} by A25,Lm2;
set w = u9"\/"v9;
(v9"\/"u9)"\/"x = v9"\/"(u9"\/"x) by LATTICE3:14;
then sup {x} = x & w"\/"x >= u9"\/"x by YELLOW_0:22,39;
then w"\/"x >= u by A34,ORDERS_2:3;
then
A37: w"\/"x in F by A32,WAYBEL_0:def 20;
w"\/"y = u9"\/"(v9"\/"y) by LATTICE3:14;
then sup {y} = y & w"\/"y >= v9"\/"y by YELLOW_0:22,39;
then w"\/"y >= v by A36,ORDERS_2:3;
then w"\/"y in F by A26,WAYBEL_0:def 20;
then (w"\/"x)"/\"(w"\/"y) in F by A37,WAYBEL_0:41;
then
A38: w"\/"(x"/\"y) in F by WAYBEL_1:5;
w in P by A33,A35,WAYBEL_0:40;
then w"\/"(x"/\"y) in P by A18,WAYBEL_0:40;
hence contradiction by A17,A38,XBOOLE_0:3;
end;
thus thesis by A16,A17;
end;
theorem Th24:
for L being distributive LATTICE, I being Ideal of L, x being
Element of L st not x in I ex P being Ideal of L st P is prime & I c= P & not x
in P
proof
let L be distributive LATTICE, I be Ideal of L, x be Element of L such that
A1: not x in I;
now
let a be object;
assume that
A2: a in I and
A3: a in uparrow x;
reconsider a as Element of L by A2;
a >= x by A3,WAYBEL_0:18;
hence contradiction by A1,A2,WAYBEL_0:def 19;
end;
then I misses uparrow x by XBOOLE_0:3;
then consider P being Ideal of L such that
A4: P is prime & I c= P and
A5: P misses uparrow x by Th23;
take P;
thus P is prime & I c= P by A4;
assume x in P;
then not x in uparrow x by A5,XBOOLE_0:3;
then not x <= x by WAYBEL_0:18;
hence thesis;
end;
theorem Th25:
for L being distributive LATTICE, I being Ideal of L, F being
Filter of L st I misses F ex P being Filter of L st P is prime & F c= P & I
misses P
proof
let L be distributive LATTICE, I be Ideal of L, F be Filter of L such that
A1: I misses F;
reconsider I9 = F as Ideal of L opp by YELLOW_7:27,29;
reconsider F9 = I as Filter of L opp by YELLOW_7:26,28;
consider P9 being Ideal of L opp such that
A2: P9 is prime & I9 c= P9 & P9 misses F9 by A1,Th23;
reconsider P = P9 as Filter of L by YELLOW_7:27,29;
take P;
thus thesis by A2,Th17;
end;
theorem Th26:
for L being non trivial Boolean LATTICE, F being proper Filter
of L ex G being Filter of L st F c= G & G is ultra
proof
let L be non trivial Boolean LATTICE;
let F be proper Filter of L;
downarrow Bottom L = {Bottom L} by WAYBEL_4:23;
then reconsider I = {Bottom L} as Ideal of L;
now
let a be object;
assume a in I;
then a = Bottom L by TARSKI:def 1;
hence not a in F by Th4;
end;
then I misses F by XBOOLE_0:3;
then consider G being Filter of L such that
A1: G is prime & F c= G and
A2: I misses G by Th25;
take G;
now
assume Bottom L in G;
then not Bottom L in I by A2,XBOOLE_0:3;
hence contradiction by TARSKI:def 1;
end;
then G is proper;
hence thesis by A1,Th22;
end;
begin :: Cluster points of a filter of sets
definition
let T be TopSpace;
let F be set,x be object;
pred x is_a_cluster_point_of F,T means
for A being Subset of T st A
is open & x in A for B being set st B in F holds A meets B;
pred x is_a_convergence_point_of F,T means
for A being Subset of T st A is open & x in A holds A in F;
end;
registration
let X be non empty set;
cluster ultra for Filter of BoolePoset X;
existence
proof
set F = the proper Filter of BoolePoset X;
ex G being Filter of BoolePoset X st F c= G & G is ultra by Th26;
hence thesis;
end;
end;
theorem Th27:
for T being non empty TopSpace for F being ultra Filter of
BoolePoset the carrier of T for p being set holds p is_a_cluster_point_of F,T
iff p is_a_convergence_point_of F,T
proof
let T be non empty TopSpace;
set L = BoolePoset the carrier of T;
let F be ultra Filter of L;
let p be set;
thus p is_a_cluster_point_of F,T implies p is_a_convergence_point_of F,T
proof
assume
A1: for A being Subset of T st A is open & p in A for B being set st B
in F holds A meets B;
let A be Subset of T;
assume that
A2: A is open & p in A and
A3: not A in F;
F is prime by Th22;
then (the carrier of T)\A in F by A3,Th21;
then A meets (the carrier of T)\A by A1,A2;
hence contradiction by XBOOLE_1:79;
end;
assume
A4: for A being Subset of T st A is open & p in A holds A in F;
let A be Subset of T;
assume A is open & p in A;
then
A5: A in F by A4;
Bottom L = {} by YELLOW_1:18;
then
A6: not {} in F by Th4;
let B be set;
assume
A7: B in F;
then reconsider a = A, b = B as Element of L by A5;
a"/\"b = A /\ B by YELLOW_1:17;
then A /\ B in F by A5,A7,WAYBEL_0:41;
hence thesis by A6;
end;
:: Proposition 3.20 (1) => (2)
theorem Th28:
for T being non empty TopSpace for x,y being Element of
InclPoset the topology of T st x << y for F being proper Filter of BoolePoset
the carrier of T st x in F ex p being Element of T st p in y & p
is_a_cluster_point_of F,T
proof
defpred P[object,object] means ex A,B being set st
A = $1 & B = $2 & A misses B;
let T be non empty TopSpace;
set L = InclPoset the topology of T;
set B = BoolePoset the carrier of T;
let x,y be Element of L such that
A1: x << y;
B = InclPoset bool the carrier of T by YELLOW_1:4;
then
A2: B = RelStr(#bool the carrier of T, RelIncl bool the carrier of T#) by
YELLOW_1:def 1;
x in the carrier of L & L = RelStr(#the topology of T, RelIncl the
topology of T#) by YELLOW_1:def 1;
then reconsider x9 = x as Element of B by A2;
let F be proper Filter of B such that
A3: x in F and
A4: for x being Element of T st x in y holds not x is_a_cluster_point_of F,T;
set V = {A where A is Subset of T: A is open & A meets y & ex B being set st
B in F & A misses B};
V c= bool the carrier of T
proof
let a be object;
assume a in V;
then ex C being Subset of T st a = C & C is open & C meets y & ex B being
set st B in F & C misses B;
hence thesis;
end;
then reconsider V as Subset-Family of T;
reconsider V as Subset-Family of T;
A5: y c= union V
proof
let x be object;
assume
A6: x in y;
L = RelStr(#the topology of T, RelIncl the topology of T#) by
YELLOW_1:def 1;
then y in the topology of T;
then not x is_a_cluster_point_of F,T by A4,A6;
then consider A being Subset of T such that
A7: A is open and
A8: x in A and
A9: ex B being set st B in F & A misses B;
A meets y by A6,A8,XBOOLE_0:3;
then A in V by A7,A9;
hence thesis by A8,TARSKI:def 4;
end;
V is open
proof
let a be Subset of T;
assume a in V;
then ex C being Subset of T st a = C & C is open & C meets y & ex B being
set st B in F & C misses B;
hence thesis;
end;
then consider W being finite Subset of V such that
A10: x c= union W by A1,A5,WAYBEL_3:34;
A11: now
let A be object;
assume A in W;
then A in V;
then ex C being Subset of T st A = C & C is open & C meets y & ex B being
set st B in F & C misses B;
hence ex B being object st B in F & P[A,B];
end;
consider f being Function such that
A12: dom f = W & rng f c= F & for A being object st A in W holds P[A,f.A]
from FUNCT_1:sch 6(A11);
rng f is finite by A12,FINSET_1:8;
then consider z being Element of BoolePoset the carrier of T such that
A13: z in F and
A14: z is_<=_than rng f by A12,WAYBEL_0:2;
set a = the Element of x9"/\"z;
x9"/\"z in F by A3,A13,WAYBEL_0:41;
then x9"/\"z <> Bottom B by Th4;
then x9"/\"z <> {} by YELLOW_1:18;
then
A15: a in x9"/\"z;
A16: x9"/\"z c= x9 /\ z by YELLOW_1:17;
then a in x by A15,XBOOLE_0:def 4;
then consider A being set such that
A17: a in A and
A18: A in W by A10,TARSKI:def 4;
A19: a in z by A15,A16,XBOOLE_0:def 4;
A20: f.A in rng f by A12,A18,FUNCT_1:def 3;
then f.A in F by A12;
then reconsider b = f.A as Element of B;
z <= b by A14,A20,LATTICE3:def 8;
then
A21: z c= b by YELLOW_1:2;
P[A,f.A] by A12,A18;
then A misses b;
hence contradiction by A19,A17,A21,XBOOLE_0:3;
end;
:: Proposition 3.20: (1) => (3)
theorem
for T being non empty TopSpace for x,y being Element of InclPoset the
topology of T st x << y for F being ultra Filter of BoolePoset the carrier of T
st x in F ex p being Element of T st p in y & p is_a_convergence_point_of F,T
proof
let T be non empty TopSpace;
let x,y be Element of InclPoset the topology of T such that
A1: x << y;
let F be ultra Filter of BoolePoset the carrier of T;
assume x in F;
then consider p being Element of T such that
A2: p in y & p is_a_cluster_point_of F,T by A1,Th28;
take p;
thus thesis by A2,Th27;
end;
:: Proposition 3.20: (3) => (1)
theorem Th30:
for T being non empty TopSpace for x,y being Element of
InclPoset the topology of T st x c= y & for F being ultra Filter of BoolePoset
the carrier of T st x in F ex p being Element of T st p in y & p
is_a_convergence_point_of F,T holds x << y
proof
let T be non empty TopSpace;
set B = BoolePoset the carrier of T;
let x,y be Element of InclPoset the topology of T such that
A1: x c= y and
A2: for F being ultra Filter of B st x in F ex p being Element of T st p
in y & p is_a_convergence_point_of F,T;
InclPoset the topology of T = RelStr(#the topology of T, RelIncl the
topology of T#) by YELLOW_1:def 1;
then x in the topology of T;
then reconsider X = x as Subset of T;
reconsider X as Subset of T;
assume not x << y;
then consider F being Subset-Family of T such that
A3: F is open and
A4: y c= union F and
A5: not ex G being finite Subset of F st x c= union G by WAYBEL_3:35;
set xF = {x\z where z is Subset of T: z in F};
set z = the Element of F;
A6: now
assume
A7: F = {};
then
y = {} by A4,ZFMISC_1:2;
then x = y by A1;
hence contradiction by A4,A5,A7;
end;
then
A8: z in F;
B = InclPoset bool the carrier of T by YELLOW_1:4;
then
A9: B = RelStr(#bool the carrier of T, RelIncl bool the carrier of T#) by
YELLOW_1:def 1;
xF c= the carrier of B
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in xF;
then ex z being Subset of T st a = x\z & z in F;
then aa c= X;
then aa c= the carrier of T by XBOOLE_1:1;
hence thesis by A9;
end;
then reconsider xF as Subset of B;
set FF = uparrow fininfs xF;
now
defpred P[object,object] means
ex A being set st A = $2 & $1 = x\A;
assume Bottom B in FF;
then consider a being Element of B such that
A10: a <= Bottom B and
A11: a in fininfs xF by WAYBEL_0:def 16;
consider s being finite Subset of xF such that
A12: a = "/\"(s,B) and
ex_inf_of s,B by A11;
reconsider t = s as Subset of B by XBOOLE_1:1;
A13: now
let v be object;
assume v in s;
then v in xF;
then ex z being Subset of T st v = x\z & z in F;
hence ex z being object st z in F & P[v,z];
end;
consider f being Function such that
A14: dom f = s & rng f c= F & for v being object st v in s holds P[v,f.v]
from FUNCT_1:sch 6(A13);
reconsider G = rng f as finite Subset of F by A14,FINSET_1:8;
Bottom B = {} by YELLOW_1:18;
then
A15: a c= {} by A10,YELLOW_1:2;
A16: now
assume s = {};
then a = Top B by A12;
hence contradiction by A15,YELLOW_1:19;
end;
then
A17: a = meet t by A12,YELLOW_1:20;
x c= union G
proof
let c be object;
assume that
A18: c in x and
A19: not c in union G;
now
let v be set;
assume
A20: v in s;
then f.v in rng f by A14,FUNCT_1:def 3;
then
A21: not c in (f.v) by A19,TARSKI:def 4;
P[v,f.v] by A14,A20;
then v = x\(f.v);
hence c in v by A18,A21,XBOOLE_0:def 5;
end;
hence contradiction by A15,A16,A17,SETFAM_1:def 1;
end;
hence contradiction by A5;
end;
then FF is proper;
then consider GG being Filter of B such that
A22: FF c= GG and
A23: GG is ultra by Th26;
reconsider z as Subset of T by A8;
A24: xF c= FF by WAYBEL_0:62;
x\z in xF by A6;
then
A25: x\z in FF by A24;
x\z c= X;
then x in GG by A22,A25,Th7;
then consider p being Element of T such that
A26: p in y and
A27: p is_a_convergence_point_of GG,T by A2,A23;
consider W being set such that
A28: p in W and
A29: W in F by A4,A26,TARSKI:def 4;
reconsider W as Subset of T by A29;
W is open by A3,A29;
then
A30: W in GG by A27,A28;
A31: xF c= FF by WAYBEL_0:62;
x\W in xF by A29;
then x\W in FF by A31;
then W misses (x\W) & W/\(x\W) in GG by A22,A30,Th9,XBOOLE_1:79;
then {} in GG;
then Bottom B in GG by YELLOW_1:18;
hence thesis by A23,Th4;
end;
:: Proposition 3.21
::$N Alexander's Lemma
theorem
for T being non empty TopSpace for B being prebasis of T for x,y being
Element of InclPoset the topology of T st x c= y holds x << y iff for F being
Subset of B st y c= union F ex G being finite Subset of F st x c= union G
proof
let T be non empty TopSpace, B be prebasis of T;
consider BB being Basis of T such that
A1: BB c= FinMeetCl B by CANTOR_1:def 4;
set BT = BoolePoset the carrier of T;
set L = InclPoset the topology of T;
let x,y be Element of L such that
A2: x c= y;
A3: B c= the topology of T by TOPS_2:64;
hereby
assume
A4: x << y;
let F be Subset of B such that
A5: y c= union F;
reconsider FF = F as Subset-Family of T by XBOOLE_1:1;
FF is open
proof
let a be Subset of T;
assume a in FF;
then a in B;
hence a in the topology of T by A3;
end;
hence ex G being finite Subset of F st x c= union G by A4,A5,WAYBEL_3:34;
end;
BT = InclPoset bool the carrier of T by YELLOW_1:4;
then
A6: BT = RelStr(#bool the carrier of T, RelIncl bool the carrier of T#) by
YELLOW_1:def 1;
L = RelStr(#the topology of T, RelIncl the topology of T#) by YELLOW_1:def 1;
then x in the topology of T & y in the topology of T;
then reconsider X = x, Y = y as Subset of T;
assume
A7: for F being Subset of B st y c= union F ex G being finite Subset of
F st x c= union G;
A8: the topology of T c= UniCl BB by CANTOR_1:def 2;
now
deffunc F(set) = x\$1;
let F be ultra Filter of BoolePoset the carrier of T such that
A9: x in F and
A10: not ex p being Element of T st p in y & p is_a_convergence_point_of F,T;
defpred P[object,object] means
ex A being set st A = $2 & $1 in A & not $2 in F;
A11: now
let p be object;
assume
A12: p in y;
then p in Y;
then reconsider q = p as Element of T;
not q is_a_convergence_point_of F,T by A10,A12;
then consider A being Subset of T such that
A13: A is open and
A14: q in A and
A15: not A in F;
A in the topology of T by A13;
then consider AY being Subset-Family of T such that
A16: AY c= BB and
A17: A = union AY by A8,CANTOR_1:def 1;
consider ay being set such that
A18: q in ay and
A19: ay in AY by A14,A17,TARSKI:def 4;
reconsider ay as Subset of T by A19;
ay in BB by A16,A19;
then consider BY being Subset-Family of T such that
A20: BY c= B and
A21: BY is finite and
A22: ay = Intersect BY by A1,CANTOR_1:def 3;
ay c= A by A17,A19,ZFMISC_1:74;
then not ay in F by A15,Th7;
then BY is not Subset of F by A21,A22,Th11;
then consider r being object such that
A23: r in BY & not r in F by TARSKI:def 3;
reconsider A=r as set by TARSKI:1;
take r;
thus r in B by A20,A23;
thus P[p,r]
proof
take A;
thus A = r & p in A & not r in F by A18,A22,A23,SETFAM_1:43;
end;
end;
consider f being Function such that
A24: dom f = y & rng f c= B and
A25: for p being object st p in y holds P[p,f.p] from FUNCT_1:sch 6(A11);
reconsider FF = rng f as Subset of B by A24;
y c= union FF
proof
let p be object;
assume
A26: p in y;
then consider A being set such that
A27: A = f.p & p in A & not f.p in F by A25;
f.p in FF & p in f.p by A24,FUNCT_1:def 3,A27,A26;
hence thesis by TARSKI:def 4;
end;
then consider G being finite Subset of FF such that
A28: x c= union G by A7;
set gg = the Element of G;
consider g being Function such that
A29: dom g = G & for z being set st z in G holds g.z = F(z) from
FUNCT_1:sch 5;
A30: rng g c= F
proof
let a be object;
A31: F is prime by Th22;
assume a in rng g;
then consider b being object such that
A32: b in G and
A33: a = g.b by A29,FUNCT_1:def 3;
b in FF by A32;
then b in B;
then reconsider b as Subset of T;
consider p being object such that
A34: p in y & b = f.p by A24,A32,FUNCT_1:def 3;
P[p,f.p] by A25,A34;
then not b in F by A34;
then
A35: (the carrier of T)\b in F by A31,Th21;
a = x\b by A29,A32,A33
.= X /\ b` by SUBSET_1:13
.= x /\ ((the carrier of T)\b);
hence thesis by A9,A35,Th9;
end;
then reconsider GG = rng g as finite Subset-Family of T by A6,A29,
FINSET_1:8,XBOOLE_1:1;
x <> Bottom BoolePoset the carrier of T by A9,Th4;
then x <> {} by YELLOW_1:18;
then
A36: G <> {} by A28,ZFMISC_1:2;
now
let a be object;
assume
A37: a in Intersect GG;
now
let z be set;
assume z in G;
then g.z in GG & g.z = x\z by A29,FUNCT_1:def 3;
then a in x\z by A37,SETFAM_1:43;
hence not a in z by XBOOLE_0:def 5;
end;
then not ex z being set st a in z & z in G;
then
A38: not a in x by A28,TARSKI:def 4;
g.gg in GG & g.gg = x\gg by A36,A29,FUNCT_1:def 3;
then a in x\gg by A37,SETFAM_1:43;
hence contradiction by A38;
end;
then
A39: Intersect GG = {} by XBOOLE_0:def 1;
Intersect GG in F by A30,Th11;
then Bottom BoolePoset the carrier of T in F by A39,YELLOW_1:18;
hence contradiction by Th4;
end;
hence thesis by A2,Th30;
end;
:: Proposition 3.22
theorem
for L being distributive complete LATTICE for x,y being Element of L
holds x << y iff for P being prime Ideal of L st y <= sup P holds x in P
proof
let L be distributive complete LATTICE;
let x,y be Element of L;
thus x << y implies for P being prime Ideal of L st y <= sup P holds x in P
by WAYBEL_3:20;
assume
A1: for P being prime Ideal of L st y <= sup P holds x in P;
now
let I be Ideal of L;
assume that
A2: y <= sup I and
A3: not x in I;
consider P being Ideal of L such that
A4: P is prime and
A5: I c= P and
A6: not x in P by A3,Th24;
sup I <= sup P by A5,Th1;
hence contradiction by A1,A2,A4,A6,ORDERS_2:3;
end;
hence thesis by WAYBEL_3:21;
end;
theorem Th33:
for L being LATTICE, p being Element of L st p is prime holds
downarrow p is prime
proof
let L be LATTICE, p be Element of L such that
A1: for x,y being Element of L st x"/\"y <= p holds x <= p or y <= p;
let x,y be Element of L;
assume x"/\"y in downarrow p;
then x"/\"y <= p by WAYBEL_0:17;
then x <= p or y <= p by A1;
hence thesis by WAYBEL_0:17;
end;
begin :: Pseudo prime elements
definition
let L be LATTICE;
let p be Element of L;
attr p is pseudoprime means
ex P being prime Ideal of L st p = sup P;
end;
theorem Th34:
for L being LATTICE for p being Element of L st p is prime holds
p is pseudoprime
proof
let L be LATTICE, p be Element of L;
assume p is prime;
then
A1: downarrow p is prime by Th33;
p = sup downarrow p by WAYBEL_0:34;
hence ex P being prime Ideal of L st p = sup P by A1;
end;
:: Proposition 3.24: (1) => (2)
theorem Th35:
for L being continuous LATTICE for p being Element of L st p is
pseudoprime for A being finite non empty Subset of L st inf A << p ex a being
Element of L st a in A & a <= p
proof
let L be continuous LATTICE;
let p be Element of L;
given P being prime Ideal of L such that
A1: p = sup P;
let A be finite non empty Subset of L;
assume inf A << p;
then
A2: inf A in waybelow p;
waybelow p c= P by A1,WAYBEL_5:1;
then consider a being Element of L such that
A3: a in A & a in P by A2,Th12;
take a;
ex_sup_of P,L by WAYBEL_0:75;
then P is_<=_than p by A1,YELLOW_0:30;
hence thesis by A3,LATTICE3:def 9;
end;
:: Proposition 3.24: (2)+? => (3)
theorem
for L being continuous LATTICE for p being Element of L st (p <> Top L
or Top L is not compact) & for A being finite non empty Subset of L st inf A <<
p ex a being Element of L st a in A & a <= p holds uparrow fininfs (downarrow p
)` misses waybelow p
proof
let L be continuous LATTICE, p be Element of L such that
A1: p <> Top L or Top L is not compact and
A2: for A being finite non empty Subset of L st inf A << p ex a being
Element of L st a in A & a <= p;
now
let x be object;
assume
A3: x in uparrow fininfs (downarrow p)`;
then reconsider a = x as Element of L;
consider b being Element of L such that
A4: a >= b and
A5: b in fininfs (downarrow p)` by A3,WAYBEL_0:def 16;
assume x in waybelow p;
then
A6: a << p by WAYBEL_3:7;
then
A7: b << p by A4,WAYBEL_3:2;
consider Y being finite Subset of (downarrow p)` such that
A8: b = "/\"(Y,L) and
ex_inf_of Y,L by A5;
reconsider Y as finite Subset of L by XBOOLE_1:1;
per cases;
suppose
Y <> {};
then consider c being Element of L such that
A9: c in Y and
A10: c <= p by A2,A4,A8,A6,WAYBEL_3:2;
c in downarrow p by A10,WAYBEL_0:17;
then (downarrow p) misses (downarrow p)` & c in (downarrow p)/\(
downarrow p)` by A9,XBOOLE_0:def 4,XBOOLE_1:79;
hence contradiction;
end;
suppose
A11: Y = {};
b <= p & p <= Top L by A7,WAYBEL_3:1,YELLOW_0:45;
then p = Top L by A8,A11,ORDERS_2:2;
hence contradiction by A1,A8,A7,A11;
end;
end;
hence thesis by XBOOLE_0:3;
end;
:: It is not true that: Proposition 3.24: (2) => (3)
theorem
for L being continuous LATTICE st Top L is compact holds (for A being
finite non empty Subset of L st inf A << Top L ex a being Element of L st a in
A & a <= Top L) & uparrow fininfs (downarrow Top L)` meets waybelow Top L
proof
let L be continuous LATTICE such that
A1: Top L << Top L;
A2: now
take x = Top L;
thus x in uparrow fininfs (downarrow Top L)` by WAYBEL_4:22;
thus x in waybelow Top L by A1;
end;
hereby
let A be finite non empty Subset of L such that
inf A << Top L;
set a = the Element of A;
reconsider a as Element of L;
take a;
thus a in A & a <= Top L by YELLOW_0:45;
end;
thus thesis by A2,XBOOLE_0:3;
end;
:: Proposition 3.24: (2) <= (3)
theorem
for L being continuous LATTICE for p being Element of L st uparrow
fininfs (downarrow p)` misses waybelow p for A being finite non empty Subset of
L st inf A << p ex a being Element of L st a in A & a <= p
proof
let L be continuous LATTICE, p be Element of L such that
A1: uparrow fininfs (downarrow p)` misses waybelow p;
let A be finite non empty Subset of L;
assume inf A << p;
then inf A in waybelow p;
then not inf A in uparrow fininfs (downarrow p)` by A1,XBOOLE_0:3;
then (downarrow p)` c= uparrow fininfs (downarrow p)` & not A c= uparrow
fininfs (downarrow p)` by WAYBEL_0:43,62;
then not A c= (downarrow p)`;
then consider a being object such that
A2: a in A and
A3: not a in (downarrow p)`;
reconsider a as Element of L by A2;
take a;
a in downarrow p by A3,SUBSET_1:29;
hence thesis by A2,WAYBEL_0:17;
end;
:: Proposition 3.24: (3) => (1)
theorem
for L being distributive continuous LATTICE for p being Element of L
st uparrow fininfs (downarrow p)` misses waybelow p holds p is pseudoprime
proof
let L be distributive continuous LATTICE;
let p be Element of L;
set I = waybelow p;
set F = uparrow fininfs (downarrow p)`;
A1: ex_sup_of downarrow p, L & sup downarrow p = p by WAYBEL_0:34;
(downarrow p)` c= F by WAYBEL_0:62;
then
A2: F` c= (downarrow p)`` by SUBSET_1:12;
assume F misses I;
then consider P being Ideal of L such that
A3: P is prime and
A4: I c= P and
A5: P misses F by Th23;
reconsider P as prime Ideal of L by A3;
A6: ex_sup_of P, L by WAYBEL_0:75;
ex_sup_of I, L & p = sup I by WAYBEL_0:75,WAYBEL_3:def 5;
then
A7: sup P >= p by A4,A6,YELLOW_0:34;
take P;
P c= F` by A5,SUBSET_1:23;
then sup P <= p by A6,A2,A1,XBOOLE_1:1,YELLOW_0:34;
hence thesis by A7,ORDERS_2:2;
end;
definition
let L be non empty RelStr;
let R be Relation of the carrier of L;
attr R is multiplicative means
for a,x,y being Element of L st [a,x]
in R & [a,y] in R holds [a,x"/\" y] in R;
end;
registration
let L be lower-bounded sup-Semilattice;
let R be auxiliary Relation of L;
let x be Element of L;
cluster R-above x -> upper;
coherence
proof
let y,z be Element of L;
assume that
A1: y in R-above x and
A2: y <= z;
x <= x & [x,y] in R by A1,WAYBEL_4:14;
then [x,z] in R by A2,WAYBEL_4:def 4;
hence thesis by WAYBEL_4:14;
end;
end;
:: Lemma 3.25: (1) iff (2)-[non empty]
theorem
for L being lower-bounded LATTICE, R being auxiliary Relation of L
holds R is multiplicative iff for x being Element of L holds R-above x is
filtered
proof
let L be lower-bounded LATTICE, R be auxiliary Relation of L;
hereby
assume
A1: R is multiplicative;
let x be Element of L;
thus R-above x is filtered
proof
let y,z be Element of L;
assume y in R-above x & z in R-above x;
then [x,y] in R & [x,z] in R by WAYBEL_4:14;
then [x,y"/\"z] in R by A1;
then
A2: y"/\"z in R-above x by WAYBEL_4:14;
y >= y"/\"z & z >= y"/\"z by YELLOW_0:23;
hence thesis by A2;
end;
end;
assume
A3: for x being Element of L holds R-above x is filtered;
let a,x,y be Element of L;
assume [a,x] in R & [a,y] in R;
then
A4: x in R-above a & y in R-above a by WAYBEL_4:14;
R-above a is filtered by A3;
then x"/\"y in R-above a by A4,WAYBEL_0:41;
hence [a,x"/\"y] in R by WAYBEL_4:14;
end;
:: Lemma 3.25: (1) iff (3)
theorem Th41:
for L being lower-bounded LATTICE, R being auxiliary Relation of
L holds R is multiplicative iff for a,b,x,y being Element of L st [a,x] in R &
[b,y] in R holds [a"/\"b,x"/\"y] in R
proof
let L be lower-bounded LATTICE, R be auxiliary Relation of L;
hereby
assume
A1: R is multiplicative;
let a,b,x,y be Element of L;
assume that
A2: [a,x] in R and
A3: [b,y] in R;
a"/\"b <= b & y <= y by YELLOW_0:23;
then
A4: [a"/\"b,y] in R by A3,WAYBEL_4:def 4;
a >= a"/\"b & x <= x by YELLOW_0:23;
then [a"/\"b,x] in R by A2,WAYBEL_4:def 4;
hence [a"/\"b,x"/\"y] in R by A1,A4;
end;
assume
A5: for a,b,x,y being Element of L st [a,x] in R & [b,y] in R holds [a
"/\"b,x"/\"y] in R;
let a be Element of L;
a"/\"a = a by YELLOW_0:25;
hence thesis by A5;
end;
:: Lemma 3.25: (1) iff (4)
theorem
for L being lower-bounded LATTICE, R being auxiliary Relation of L
holds R is multiplicative iff for S being full SubRelStr of [:L,L:] st the
carrier of S = R holds S is meet-inheriting
proof
let L be lower-bounded LATTICE, R be auxiliary Relation of L;
reconsider X = R as Subset of [:L,L:] by YELLOW_3:def 2;
A1: X = the carrier of subrelstr X by YELLOW_0:def 15;
hereby
assume
A2: R is multiplicative;
let S be full SubRelStr of [:L,L:] such that
A3: the carrier of S = R;
thus S is meet-inheriting
proof
let x,y be Element of [:L,L:];
assume
A4: x in the carrier of S & y in the carrier of S;
the carrier of [:L,L:] = [:the carrier of L, the carrier of L:] by
YELLOW_3:def 2;
then
A5: x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:21;
ex_inf_of {x,y}, [:L,L:] by YELLOW_0:21;
then inf {x,y} = [inf proj1 {x,y}, inf proj2 {x,y}] by YELLOW_3:47
.= [inf {x`1,y`1}, inf proj2 {x,y}] by A5,FUNCT_5:13
.= [inf {x`1,y`1}, inf {x`2,y`2}] by A5,FUNCT_5:13
.= [x`1"/\"y`1, inf {x`2,y`2}] by YELLOW_0:40
.= [x`1"/\"y`1, x`2"/\"y`2] by YELLOW_0:40;
hence thesis by A2,A3,A4,A5,Th41;
end;
end;
assume for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting;
then
A6: subrelstr X is meet-inheriting by A1;
let a,x,y be Element of L;
A7: ex_inf_of {[a,x],[a,y]}, [:L,L:] by YELLOW_0:21;
assume [a,x] in R & [a,y] in R;
then inf {[a,x],[a,y]} in R by A1,A6,A7;
then
A8: [a,x]"/\"[a,y] in R by YELLOW_0:40;
set ax = [a,x], ay = [a,y];
[a,x]"/\"[a,y] = inf {ax,ay} by YELLOW_0:40
.= [inf proj1 {ax,ay}, inf proj2 {ax,ay}] by A7,YELLOW_3:47
.= [inf {a,a}, inf proj2 {ax,ay}] by FUNCT_5:13
.= [inf {a,a}, inf {x,y}] by FUNCT_5:13
.= [a"/\"a, inf {x,y}] by YELLOW_0:40
.= [a"/\"a, x"/\"y] by YELLOW_0:40;
hence [a,x"/\"y] in R by A8,YELLOW_0:25;
end;
:: Lemma 3.25: (1) iff (5)
theorem
for L being lower-bounded LATTICE, R being auxiliary Relation of L
holds R is multiplicative iff R-below is meet-preserving
proof
let L be lower-bounded LATTICE, R be auxiliary Relation of L;
hereby
assume
A1: R is multiplicative;
thus R-below is meet-preserving
proof
let x,y be Element of L;
A2: (R-below).y = R-below y by WAYBEL_4:def 12;
A3: R-below (x"/\"y) = (R-below x) /\ (R-below y)
proof
hereby
let a be object;
assume a in R-below (x"/\"y);
then a in {z where z is Element of L: [z,x"/\"y] in R} by
WAYBEL_4:def 10;
then consider z being Element of L such that
A4: a = z and
A5: [z,x"/\"y] in R;
A6: z <= z;
x"/\"y <= y by YELLOW_0:23;
then [z,y] in R by A5,A6,WAYBEL_4:def 4;
then
A7: z in R-below y by WAYBEL_4:13;
x"/\"y <= x by YELLOW_0:23;
then [z,x] in R by A5,A6,WAYBEL_4:def 4;
then z in R-below x by WAYBEL_4:13;
hence a in (R-below x) /\ (R-below y) by A4,A7,XBOOLE_0:def 4;
end;
let a be object;
assume
A8: a in (R-below x) /\ (R-below y);
then reconsider z = a as Element of L;
a in R-below y by A8,XBOOLE_0:def 4;
then
A9: [z,y] in R by WAYBEL_4:13;
a in R-below x by A8,XBOOLE_0:def 4;
then [z,x] in R by WAYBEL_4:13;
then [z,x"/\"y] in R by A1,A9;
hence thesis by WAYBEL_4:13;
end;
(R-below).(x"/\"y) = R-below (x"/\"y) & (R-below).x = R-below x by
WAYBEL_4:def 12;
then (R-below).(x"/\"y) = (R-below).x"/\"(R-below).y by A2,A3,YELLOW_2:43
;
hence thesis by YELLOW_3:8;
end;
end;
assume
A10: for x,y being Element of L holds R-below preserves_inf_of {x,y};
let a,x,y be Element of L;
R-below preserves_inf_of {x,y} by A10;
then
A11: (R-below).(x"/\"y) = (R-below).x"/\"(R-below).y by YELLOW_3:8
.= (R-below).x /\ (R-below).y by YELLOW_2:43;
A12: (R-below).y = R-below y by WAYBEL_4:def 12;
assume [a,x] in R & [a,y] in R;
then
A13: a in R-below x & a in R-below y by WAYBEL_4:13;
(R-below).(x"/\"y) = R-below (x"/\"y) & (R-below).x = R-below x by
WAYBEL_4:def 12;
then a in R-below (x"/\"y) by A11,A12,A13,XBOOLE_0:def 4;
hence thesis by WAYBEL_4:13;
end;
Lm3: now
let L be continuous lower-bounded LATTICE, p be Element of L such that
A1: L-waybelow is multiplicative and
A2: for a,b being Element of L st a"/\"b << p holds a <= p or b <= p and
A3: p is not prime;
consider x,y being Element of L such that
A4: x"/\"y <= p and
A5: not x <= p and
A6: not y <= p by A3;
A7: for a being Element of L holds waybelow a is non empty directed;
then consider u being Element of L such that
A8: u << x and
A9: not u <= p by A5,WAYBEL_3:24;
consider v being Element of L such that
A10: v << y and
A11: not v <= p by A6,A7,WAYBEL_3:24;
A12: [v,y] in L-waybelow by A10,WAYBEL_4:def 1;
[u,x] in L-waybelow by A8,WAYBEL_4:def 1;
then [u"/\"v,x"/\"y] in L-waybelow by A1,A12,Th41;
then u"/\"v << x"/\"y by WAYBEL_4:def 1;
then u"/\"v << p by A4,WAYBEL_3:2;
hence contradiction by A2,A9,A11;
end;
theorem Th44:
for L being continuous lower-bounded LATTICE st L-waybelow is
multiplicative for p being Element of L holds p is pseudoprime iff for a,b
being Element of L st a"/\"b << p holds a <= p or b <= p
proof
let L be continuous lower-bounded LATTICE such that
A1: L-waybelow is multiplicative;
let p be Element of L;
hereby
assume
A2: p is pseudoprime;
let a,b be Element of L;
assume a"/\"b << p;
then inf {a,b} << p by YELLOW_0:40;
then ex c being Element of L st c in {a,b} & c <= p by A2,Th35;
hence a <= p or b <= p by TARSKI:def 2;
end;
assume for a,b being Element of L st a"/\" b << p holds a <= p or b <= p;
hence thesis by A1,Lm3,Th34;
end;
theorem
for L being continuous lower-bounded LATTICE st L-waybelow is
multiplicative for p being Element of L st p is pseudoprime holds p is prime
proof
let L be continuous lower-bounded LATTICE such that
A1: L-waybelow is multiplicative;
let p be Element of L;
assume p is pseudoprime;
then
for a,b being Element of L st a"/\"b << p holds a <= p or b <= p by A1,Th44;
hence thesis by A1,Lm3;
end;
theorem
for L being distributive continuous lower-bounded LATTICE st for p
being Element of L st p is pseudoprime holds p is prime holds L-waybelow is
multiplicative
proof
let L be distributive continuous lower-bounded LATTICE such that
A1: for p being Element of L st p is pseudoprime holds p is prime;
given a,x,y being Element of L such that
A2: [a,x] in L-waybelow & [a,y] in L-waybelow and
A3: not [a,x"/\"y] in L-waybelow;
now
let z be object;
assume that
A4: z in waybelow (x"/\"y) and
A5: z in uparrow a;
reconsider z as Element of L by A4;
z << x"/\"y & z >= a by A4,A5,WAYBEL_0:18,WAYBEL_3:7;
then a << x"/\"y by WAYBEL_3:2;
hence contradiction by A3,WAYBEL_4:def 1;
end;
then waybelow (x"/\"y) misses uparrow a by XBOOLE_0:3;
then consider P being Ideal of L such that
A6: P is prime and
A7: waybelow (x"/\"y) c= P and
A8: P misses uparrow a by Th23;
set p = sup P;
p is pseudoprime by A6;
then
A9: p is prime by A1;
a <= a;
then
A10: a in uparrow a by WAYBEL_0:18;
A11: x"/\"y = sup waybelow (x"/\"y) & ex_sup_of waybelow (x"/\"y), L by
WAYBEL_0:75,WAYBEL_3:def 5;
ex_sup_of P, L by WAYBEL_0:75;
then x"/\"y <= p by A7,A11,YELLOW_0:34;
then x <= p & a << x or y <= p & a << y by A2,A9,WAYBEL_4:def 1;
then a in P by WAYBEL_3:20;
hence thesis by A8,A10,XBOOLE_0:3;
end;