:: 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 b₁ being B_Lattice holds b₁ 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 b₁ being Filter of L st b₁ is maximal holds
b₁ 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 b₁ being Filter of L st b₁ is maximal holds
b₁ is being_ultrafilter

proof end;

cluster non empty final meet-closed being_ultrafilter -> maximal for Element of K19( the carrier of L);

coherence
for b₁ being Filter of L st b₁ is being_ultrafilter holds
b₁ 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 b₁ being Ideal of L st b₁ is maximal holds
b₁ is max-ideal by LemM;

cluster non empty initial join-closed max-ideal -> maximal for Element of K19( the carrier of L);

coherence
for b₁ being Ideal of L st b₁ is max-ideal holds
b₁ 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 b₁ being Ideal of L st b₁ is maximal holds
b₁ 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 b₁ being Filter of L st b₁ is maximal holds
b₁ 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 b₁ being Ideal of L st b₁ is maximal holds
b₁ is prime by MaxIPrime;

end;

:: 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 b₁ being Function st
( dom b₁ = the carrier of L & ( for a being Element of L holds b₁ . a = { F where F is Filter of L : ( F is prime & a in F ) } ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = the carrier of L & ( for a being Element of L holds b₁ . a = { F where F is Filter of L : ( F is prime & a in F ) } ) & dom b₂ = the carrier of L & ( for a being Element of L holds b₂ . a = { F where F is Filter of L : ( F is prime & a in F ) } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines PrimeFilters LATTICEA:def 5 :
for L being Lattice
for b₂ being Function holds
( b₂ = PrimeFilters L iff ( dom b₂ = the carrier of L & ( for a being Element of L holds b₂ . 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 b₁ being strict TopSpace st
( the carrier of b₁ = PFilters L & the topology of b₁ = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } )

proof end;

uniqueness
for b₁, b₂ being strict TopSpace st the carrier of b₁ = PFilters L & the topology of b₁ = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } & the carrier of b₂ = PFilters L & the topology of b₂ = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } holds
b₁ = b₂ ;

end;

:: deftheorem StoneDef defines StoneSpace LATTICEA:def 7 :
for L being distributive upper-bounded Lattice
for b₂ being strict TopSpace holds
( b₂ = StoneSpace L iff ( the carrier of b₂ = PFilters L & the topology of b₂ = { (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 ) } ;

:: 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;

:: 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;