:: Prime Ideals and Filters
:: by Grzegorz Bancerek
::
:: Received December 1, 1996
:: Copyright (c) 1996-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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;
begin
theorem :: WAYBEL_7:1
for L being complete LATTICE, X,Y being set st X c= Y holds "\/"(
X,L) <= "\/"(Y,L) & "/\"(X,L) >= "/\"(Y,L);
theorem :: WAYBEL_7:2
for X being set holds the carrier of BoolePoset X = bool X;
theorem :: WAYBEL_7:3
for L being bounded antisymmetric non empty RelStr holds L is
trivial iff Top L = Bottom L;
registration
let X be set;
cluster BoolePoset X -> Boolean;
end;
registration
let X be non empty set;
cluster BoolePoset X -> non trivial;
end;
theorem :: WAYBEL_7:4
for L being lower-bounded non empty Poset, F being Filter of L
holds F is proper iff not Bottom L in F;
registration
cluster non trivial Boolean strict for LATTICE;
end;
registration
let L be upper-bounded non trivial Poset;
cluster proper for Filter of L;
end;
theorem :: WAYBEL_7:5
for X being set, a being Element of BoolePoset X holds 'not' a = X \ a;
theorem :: WAYBEL_7:6
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;
theorem :: WAYBEL_7:7
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;
theorem :: WAYBEL_7:8
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;
theorem :: WAYBEL_7:9
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;
theorem :: WAYBEL_7:10
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;
theorem :: WAYBEL_7:11
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;
begin :: Prime ideals and filters
definition
let L be with_infima Poset;
let I be Ideal of L;
attr I is prime means
:: WAYBEL_7:def 1
for x,y being Element of L st x"/\"y in I holds x in I or y in I;
end;
theorem :: WAYBEL_7:12
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;
registration
let L be LATTICE;
cluster prime for Ideal of L;
end;
theorem :: WAYBEL_7:13
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;
definition
let L be with_suprema Poset;
let F be Filter of L;
attr F is prime means
:: WAYBEL_7:def 2
for x,y being Element of L st x"\/"y in F holds x in F or y in F;
end;
theorem :: WAYBEL_7:14
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;
registration
let L be LATTICE;
cluster prime for Filter of L;
end;
theorem :: WAYBEL_7:15
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;
theorem :: WAYBEL_7:16
for L being LATTICE, x being set holds x is prime Ideal of L iff
x is prime Filter of L opp;
theorem :: WAYBEL_7:17
for L being LATTICE, x being set holds x is prime Filter of L
iff x is prime Ideal of L opp;
:: Remark 3.16: (3) iff (2)
theorem :: WAYBEL_7:18
for L being with_infima Poset, I being Ideal of L holds I is prime iff
I` is Filter of L or I` = {};
:: Remark 3.16: (3) iff (1)
theorem :: WAYBEL_7:19
for L being LATTICE, I being Ideal of L holds I is prime iff I in
PRIME InclPoset Ids L;
theorem :: WAYBEL_7:20
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;
:: Remark 3.18: (1) iff (2)
theorem :: WAYBEL_7:21
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;
definition
let L be non empty Poset;
let F be Filter of L;
attr F is ultra means
:: WAYBEL_7:def 3
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;
end;
:: Remark 3.18: (1)+proper iff (3)
theorem :: WAYBEL_7:22
for L being Boolean LATTICE, F being Filter of L holds F is
proper prime iff F is ultra;
:: Lemma 3.19
theorem :: WAYBEL_7:23
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;
theorem :: WAYBEL_7:24
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;
theorem :: WAYBEL_7:25
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;
theorem :: WAYBEL_7:26
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;
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
:: WAYBEL_7:def 4
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
:: WAYBEL_7:def 5
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;
end;
theorem :: WAYBEL_7:27
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;
:: Proposition 3.20 (1) => (2)
theorem :: WAYBEL_7:28
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;
:: Proposition 3.20: (1) => (3)
theorem :: WAYBEL_7:29
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
;
:: Proposition 3.20: (3) => (1)
theorem :: WAYBEL_7:30
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;
:: Proposition 3.21
::$N Alexander's Lemma
theorem :: WAYBEL_7:31
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;
:: Proposition 3.22
theorem :: WAYBEL_7:32
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;
theorem :: WAYBEL_7:33
for L being LATTICE, p being Element of L st p is prime holds
downarrow p is prime;
begin :: Pseudo prime elements
definition
let L be LATTICE;
let p be Element of L;
attr p is pseudoprime means
:: WAYBEL_7:def 6
ex P being prime Ideal of L st p = sup P;
end;
theorem :: WAYBEL_7:34
for L being LATTICE for p being Element of L st p is prime holds
p is pseudoprime;
:: Proposition 3.24: (1) => (2)
theorem :: WAYBEL_7:35
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;
:: Proposition 3.24: (2)+? => (3)
theorem :: WAYBEL_7:36
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;
:: It is not true that: Proposition 3.24: (2) => (3)
theorem :: WAYBEL_7:37
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;
:: Proposition 3.24: (2) <= (3)
theorem :: WAYBEL_7:38
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;
:: Proposition 3.24: (3) => (1)
theorem :: WAYBEL_7:39
for L being distributive continuous LATTICE for p being Element of L
st uparrow fininfs (downarrow p)` misses waybelow p holds p is pseudoprime;
definition
let L be non empty RelStr;
let R be Relation of the carrier of L;
attr R is multiplicative means
:: WAYBEL_7:def 7
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;
end;
:: Lemma 3.25: (1) iff (2)-[non empty]
theorem :: WAYBEL_7:40
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;
:: Lemma 3.25: (1) iff (3)
theorem :: WAYBEL_7:41
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;
:: Lemma 3.25: (1) iff (4)
theorem :: WAYBEL_7:42
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;
:: Lemma 3.25: (1) iff (5)
theorem :: WAYBEL_7:43
for L being lower-bounded LATTICE, R being auxiliary Relation of L
holds R is multiplicative iff R-below is meet-preserving;
theorem :: WAYBEL_7:44
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;
theorem :: WAYBEL_7:45
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;
theorem :: WAYBEL_7:46
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;