:: Prime Filters and Ideals in Distributive Lattices
:: by Adam Grabowski
::
:: Received October 7, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


definition
let IT be set ;
attr IT is unordered means :: LATTICEA:def 1
for p1, p2 being set st p1 in IT & p2 in IT & p1 <> p2 holds
p1,p2 are_c=-incomparable ;
end;

:: deftheorem defines unordered LATTICEA:def 1 :
for IT being set holds
( IT is unordered iff for p1, p2 being set st p1 in IT & p2 in IT & p1 <> p2 holds
p1,p2 are_c=-incomparable );

registration
cluster non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean for LattStr ;
existence
not for b1 being B_Lattice holds b1 is trivial
proof end;
end;

theorem TopBot: :: LATTICEA:1
for L being non trivial bounded Lattice holds Top L <> Bottom L
proof end;

theorem :: LATTICEA:2
for L being Lattice
for I being Ideal of L holds
( I is prime iff ( I ` is Filter of L or I ` = {} ) )
proof end;

theorem :: LATTICEA:3
for L being Lattice
for F being Filter of L holds
( F is prime iff ( F ` is Ideal of L or F ` = {} ) )
proof end;

definition
let L be Lattice;
func PFilters L -> Subset-Family of L equals :: LATTICEA:def 2
{ F where F is Filter of L : F is prime } ;
coherence
{ F where F is Filter of L : F is prime } is Subset-Family of L
proof end;
end;

:: deftheorem defines PFilters LATTICEA:def 2 :
for L being Lattice holds PFilters L = { F where F is Filter of L : F is prime } ;

IIsPrime: for L being Lattice holds (.L.> is prime
proof end;

registration
let L be Lattice;
cluster (.L.> -> prime ;
coherence
(.L.> is prime
by IIsPrime;
end;

theorem PrimFil: :: LATTICEA:4
for L being distributive Lattice holds F_primeSet L c< PFilters L
proof end;

theorem lemma3: :: LATTICEA:5
the carrier of (BooleLatt {{}}) = {{},{{}}}
proof end;

theorem lemma1: :: LATTICEA:6
for L being Lattice
for A being Subset of L holds
( not L = BooleLatt {{}} or A = {} or A = {{}} or A = {{},{{}}} or A = {{{}}} )
proof end;

theorem lemma2: :: LATTICEA:7
for L being Lattice
for A being Filter of L holds
( not L = BooleLatt {{}} or A = {} or A = {{},{{}}} or A = {{{}}} )
proof end;

theorem :: LATTICEA:8
for L being Lattice
for A being Filter of L holds
( not L = BooleLatt {{}} or A = {(Top L)} or A = <.L.) )
proof end;

theorem :: LATTICEA:9
for L being non trivial Boolean Lattice
for A being Filter of L st L = BooleLatt {{}} & A = {(Top L)} holds
A is prime
proof end;

theorem :: LATTICEA:10
for L being Lattice
for A being Filter of L st L = BooleLatt {{}} & A is being_ultrafilter holds
A = {(Top L)}
proof end;

theorem Th16: :: LATTICEA:11
for L being Lattice
for a being Element of L holds { F where F is Filter of L : ( F is prime & a in F ) } c= PFilters L
proof end;

definition
let L be Lattice;
let F be Filter of L;
attr F is maximal means :: LATTICEA:def 3
( F is proper & ( for G being Filter of L st G is proper & F c= G holds
F = G ) );
end;

:: deftheorem defines maximal LATTICEA:def 3 :
for L being Lattice
for F being Filter of L holds
( F is maximal iff ( F is proper & ( for G being Filter of L st G is proper & F c= G holds
F = G ) ) );

registration
let L be Lattice;
cluster non empty final meet-closed maximal -> proper for Element of K19( the carrier of L);
coherence
for b1 being Filter of L st b1 is maximal holds
b1 is proper
;
end;

registration
let L be Lattice;
cluster non empty final meet-closed maximal -> being_ultrafilter for Element of K19( the carrier of L);
coherence
for b1 being Filter of L st b1 is maximal holds
b1 is being_ultrafilter
proof end;
cluster non empty final meet-closed being_ultrafilter -> maximal for Element of K19( the carrier of L);
coherence
for b1 being Filter of L st b1 is being_ultrafilter holds
b1 is maximal
proof end;
end;

definition
let L be Lattice;
let I be Ideal of L;
attr I is maximal means :: LATTICEA:def 4
( I is proper & ( for J being Ideal of L st J is proper & I c= J holds
I = J ) );
end;

:: deftheorem defines maximal LATTICEA:def 4 :
for L being Lattice
for I being Ideal of L holds
( I is maximal iff ( I is proper & ( for J being Ideal of L st J is proper & I c= J holds
I = J ) ) );

theorem LemM: :: LATTICEA:12
for L being Lattice
for I being Ideal of L holds
( I is max-ideal iff I is maximal )
proof end;

registration
let L be Lattice;
cluster non empty initial join-closed maximal -> max-ideal for Element of K19( the carrier of L);
coherence
for b1 being Ideal of L st b1 is maximal holds
b1 is max-ideal
by LemM;
cluster non empty initial join-closed max-ideal -> maximal for Element of K19( the carrier of L);
coherence
for b1 being Ideal of L st b1 is max-ideal holds
b1 is maximal
by LemM;
end;

registration
let L be Lattice;
cluster non empty initial join-closed maximal -> proper for Element of K19( the carrier of L);
coherence
for b1 being Ideal of L st b1 is maximal holds
b1 is proper
;
end;

theorem Lem1: :: LATTICEA:13
for L being Lattice
for F being Filter of L st not F is prime holds
ex a, b being Element of L st
( a "\/" b in F & not a in F & not b in F )
proof end;

theorem Lem2: :: LATTICEA:14
for L being Lattice
for F being Ideal of L st not F is prime holds
ex a, b being Element of L st
( a "/\" b in F & not a in F & not b in F )
proof end;

theorem HelpMaxPrime: :: LATTICEA:15
for L being Lattice
for F being Filter of L
for a being Element of L
for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x )
}
& a in G holds
G is Filter of L
proof end;

theorem HelpMaxPrime2: :: LATTICEA:16
for L being Lattice
for F being Ideal of L
for a being Element of L
for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u )
}
& a in G holds
G is Ideal of L
proof end;

theorem MaxPrime: :: LATTICEA:17
for L being distributive Lattice
for F being Filter of L st F is maximal holds
F is prime
proof end;

registration
let L be distributive Lattice;
cluster non empty final meet-closed maximal -> prime for Element of K19( the carrier of L);
coherence
for b1 being Filter of L st b1 is maximal holds
b1 is prime
by MaxPrime;
end;

theorem MaxIPrime: :: LATTICEA:18
for L being distributive Lattice
for F being Ideal of L st F is maximal holds
F is prime
proof end;

registration
let L be distributive Lattice;
cluster non empty initial join-closed maximal -> prime for Element of K19( the carrier of L);
coherence
for b1 being Ideal of L st b1 is maximal holds
b1 is prime
by MaxIPrime;
end;

:: WP: Prime ideal theorem for distributive lattices
theorem Th15: :: LATTICEA:19
for L being distributive Lattice
for I being Ideal of L
for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
proof end;

theorem Cor16: :: LATTICEA:20
for L being distributive Lattice
for I being Ideal of L
for a being Element of L st not a in I holds
ex P being Ideal of L st
( P is prime & I c= P & not a in P )
proof end;

theorem :: LATTICEA:21
for L being distributive Lattice
for a, b being Element of L st a <> b holds
ex P being Ideal of L st
( ( P is prime & a in P & not b in P ) or ( not a in P & b in P ) )
proof end;

theorem :: LATTICEA:22
for L being distributive Lattice
for a, b being Element of L st not a [= b holds
ex P being Ideal of L st
( P is prime & not a in P & b in P )
proof end;

theorem :: LATTICEA:23
for L being distributive Lattice
for I being Ideal of L holds I = meet { P where P is Ideal of L : ( P is prime & I c= P ) }
proof end;

definition
let L be Lattice;
func PrimeFilters L -> Function means :Def6: :: LATTICEA:def 5
( dom it = the carrier of L & ( for a being Element of L holds it . a = { F where F is Filter of L : ( F is prime & a in F ) } ) );
existence
ex b1 being Function st
( dom b1 = the carrier of L & ( for a being Element of L holds b1 . a = { F where F is Filter of L : ( F is prime & a in F ) } ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = the carrier of L & ( for a being Element of L holds b1 . a = { F where F is Filter of L : ( F is prime & a in F ) } ) & dom b2 = the carrier of L & ( for a being Element of L holds b2 . a = { F where F is Filter of L : ( F is prime & a in F ) } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines PrimeFilters LATTICEA:def 5 :
for L being Lattice
for b2 being Function holds
( b2 = PrimeFilters L iff ( dom b2 = the carrier of L & ( for a being Element of L holds b2 . a = { F where F is Filter of L : ( F is prime & a in F ) } ) ) );

theorem Th17: :: LATTICEA:24
for L being Lattice
for a being Element of L
for x being set holds
( x in (PrimeFilters L) . a iff ex F being Filter of L st
( F = x & F is prime & a in F ) )
proof end;

theorem :: LATTICEA:25
for L being Lattice
for a being Element of L
for F being Filter of L holds
( F in (PrimeFilters L) . a iff ( F is prime & a in F ) )
proof end;

theorem :: LATTICEA:26
for L being distributive Lattice
for a, b being Element of L holds (PrimeFilters L) . (a "/\" b) = ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b)
proof end;

theorem :: LATTICEA:27
for L being distributive Lattice
for a, b being Element of L holds (PrimeFilters L) . (a "\/" b) = ((PrimeFilters L) . a) \/ ((PrimeFilters L) . b)
proof end;

definition
let L be distributive Lattice;
:: original: PrimeFilters
redefine func PrimeFilters L -> Function of the carrier of L,(bool (PFilters L));
coherence
PrimeFilters L is Function of the carrier of L,(bool (PFilters L))
proof end;
end;

definition
let L be distributive Lattice;
func StoneR L -> set equals :: LATTICEA:def 6
rng (PrimeFilters L);
coherence
rng (PrimeFilters L) is set
;
end;

:: deftheorem defines StoneR LATTICEA:def 6 :
for L being distributive Lattice holds StoneR L = rng (PrimeFilters L);

registration
let L be distributive Lattice;
cluster StoneR L -> non empty ;
coherence
not StoneR L is empty
;
end;

theorem Th23: :: LATTICEA:28
for L being distributive Lattice
for x being set holds
( x in StoneR L iff ex a being Element of L st (PrimeFilters L) . a = x )
proof end;

definition
let L be distributive upper-bounded Lattice;
func StoneSpace L -> strict TopSpace means :StoneDef: :: LATTICEA:def 7
( the carrier of it = PFilters L & the topology of it = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = PFilters L & the topology of b1 = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } )
proof end;
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = PFilters L & the topology of b1 = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } & the carrier of b2 = PFilters L & the topology of b2 = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } holds
b1 = b2
;
end;

:: deftheorem StoneDef defines StoneSpace LATTICEA:def 7 :
for L being distributive upper-bounded Lattice
for b2 being strict TopSpace holds
( b2 = StoneSpace L iff ( the carrier of b2 = PFilters L & the topology of b2 = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } ) );

registration
let L be non trivial distributive upper-bounded Lattice;
cluster StoneSpace L -> non empty strict ;
coherence
not StoneSpace L is empty
proof end;
end;

definition
let L be Lattice;
let a be Element of L;
func PseudoComplements a -> Subset of L equals :: LATTICEA:def 8
{ x where x is Element of L : a "/\" x = Bottom L } ;
coherence
{ x where x is Element of L : a "/\" x = Bottom L } is Subset of L
proof end;
func PseudoCocomplements a -> Subset of L equals :: LATTICEA:def 9
{ x where x is Element of L : a "\/" x = Top L } ;
coherence
{ x where x is Element of L : a "\/" x = Top L } is Subset of L
proof end;
end;

:: deftheorem defines PseudoComplements LATTICEA:def 8 :
for L being Lattice
for a being Element of L holds PseudoComplements a = { x where x is Element of L : a "/\" x = Bottom L } ;

:: deftheorem defines PseudoCocomplements LATTICEA:def 9 :
for L being Lattice
for a being Element of L holds PseudoCocomplements a = { x where x is Element of L : a "\/" x = Top L } ;

LemDistr: for L being distributive Lattice
for a, x1, x2 being Element of L holds a "\/" (x1 "/\" x2) = (a "\/" x1) "/\" (a "\/" x2)

proof end;

registration
let L be distributive bounded Lattice;
let a be Element of L;
cluster PseudoComplements a -> non empty initial join-closed ;
coherence
( PseudoComplements a is initial & not PseudoComplements a is empty & PseudoComplements a is join-closed )
proof end;
cluster PseudoCocomplements a -> non empty final meet-closed ;
coherence
( PseudoCocomplements a is final & not PseudoCocomplements a is empty & PseudoCocomplements a is meet-closed )
proof end;
end;

theorem :: LATTICEA:29
for L being Lattice
for a, b being Element of L holds
( b in PseudoComplements a iff b "/\" a = Bottom L )
proof end;

theorem :: LATTICEA:30
for L being Lattice
for a, b being Element of L holds
( b in PseudoCocomplements a iff b "\/" a = Top L )
proof end;

theorem :: LATTICEA:31
for L being bounded Lattice
for a being Element of L holds Bottom L in PseudoComplements a
proof end;

theorem :: LATTICEA:32
for L being bounded Lattice
for a being Element of L holds Top L in PseudoCocomplements a
proof end;

definition
let L be Lattice;
func Spectrum L -> Subset-Family of L equals :: LATTICEA:def 10
{ I where I is Ideal of L : ( I is prime & I is proper ) } ;
coherence
{ I where I is Ideal of L : ( I is prime & I is proper ) } is Subset-Family of L
proof end;
end;

:: deftheorem defines Spectrum LATTICEA:def 10 :
for L being Lattice holds Spectrum L = { I where I is Ideal of L : ( I is prime & I is proper ) } ;

:: WP: Nachbin's theorem for bounded distributive lattices
theorem :: LATTICEA:33
for L being distributive bounded Lattice holds
( L is Boolean iff for I being Ideal of L st I is proper & I is prime holds
I is maximal )
proof end;

registration
let L be non trivial distributive bounded Lattice;
cluster Spectrum L -> non empty ;
coherence
not Spectrum L is empty
proof end;
end;

:: WP: Nachbin theorem for spectra of distributive lattices
theorem NachSpec: :: LATTICEA:34
for L being distributive bounded Lattice holds
( L is Boolean iff Spectrum L is unordered )
proof end;

registration
let L be Boolean Lattice;
cluster Spectrum L -> unordered ;
coherence
Spectrum L is unordered
by NachSpec;
end;