:: by Adam Grabowski

::

:: Received October 7, 2013

:: Copyright (c) 2013-2017 Association of Mizar Users

definition

let IT be set ;

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

for p1, p2 being set st p1 in IT & p2 in IT & p1 <> p2 holds

p1,p2 are_c=-incomparable ;

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

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

not for b_{1} being B_Lattice holds b_{1} is trivial
end;

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

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 ` = {} ) )

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 ` = {} ) )

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;

{ F where F is Filter of L : F is prime } is Subset-Family of L

end;
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 } ;

{ F where F is Filter of L : F is prime } is Subset-Family of L

proof end;

:: deftheorem defines PFilters LATTICEA:def 2 :

for L being Lattice holds PFilters L = { F where F is Filter of L : F is prime } ;

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;

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 = {{{}}} )

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 = {{{}}} )

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.) )

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

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)}

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

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;

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

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

registration

let L be Lattice;

for b_{1} being Filter of L st b_{1} is maximal holds

b_{1} is being_ultrafilter

for b_{1} being Filter of L st b_{1} is being_ultrafilter holds

b_{1} is maximal

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

coherence for b

b

proof end;

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

coherence for b

b

proof 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 ) ) );

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

registration

let L be Lattice;

coherence

for b_{1} being Ideal of L st b_{1} is maximal holds

b_{1} is max-ideal
by LemM;

coherence

for b_{1} being Ideal of L st b_{1} is max-ideal holds

b_{1} is maximal
by LemM;

end;
coherence

for b

b

coherence

for b

b

registration
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 )

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 )

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

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

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;

registration

let L be distributive Lattice;

coherence

for b_{1} being Filter of L st b_{1} is maximal holds

b_{1} is prime
by MaxPrime;

end;
coherence

for b

b

registration

let L be distributive Lattice;

coherence

for b_{1} being Ideal of L st b_{1} is maximal holds

b_{1} is prime
by MaxIPrime;

end;
coherence

for b

b

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

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 )

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 ) )

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 )

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 ) }

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;

ex b_{1} being Function st

( dom b_{1} = the carrier of L & ( for a being Element of L holds b_{1} . a = { F where F is Filter of L : ( F is prime & a in F ) } ) )

for b_{1}, b_{2} being Function st dom b_{1} = the carrier of L & ( for a being Element of L holds b_{1} . a = { F where F is Filter of L : ( F is prime & a in F ) } ) & dom b_{2} = the carrier of L & ( for a being Element of L holds b_{2} . a = { F where F is Filter of L : ( F is prime & a in F ) } ) holds

b_{1} = b_{2}

end;
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 ( 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 ) } ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines PrimeFilters LATTICEA:def 5 :

for L being Lattice

for b_{2} being Function holds

( b_{2} = PrimeFilters L iff ( dom b_{2} = the carrier of L & ( for a being Element of L holds b_{2} . a = { F where F is Filter of L : ( F is prime & a in F ) } ) ) );

for L being Lattice

for b

( b

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 ) )

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 ) )

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)

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)

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))

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

:: deftheorem defines StoneR LATTICEA:def 6 :

for L being distributive Lattice holds StoneR L = rng (PrimeFilters L);

for L being distributive Lattice holds StoneR L = rng (PrimeFilters L);

registration
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 )

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;

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = PFilters L & the topology of b_{1} = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } )

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = PFilters L & the topology of b_{1} = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } & the carrier of b_{2} = PFilters L & the topology of b_{2} = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = PFilters L & the topology of it = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem StoneDef defines StoneSpace LATTICEA:def 7 :

for L being distributive upper-bounded Lattice

for b_{2} being strict TopSpace holds

( b_{2} = StoneSpace L iff ( the carrier of b_{2} = PFilters L & the topology of b_{2} = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } ) );

for L being distributive upper-bounded Lattice

for b

( b

registration

let L be non trivial distributive upper-bounded Lattice;

coherence

not StoneSpace L is empty

end;
coherence

not StoneSpace L is empty

proof end;

definition

let L be Lattice;

let a be Element of L;

{ x where x is Element of L : a "/\" x = Bottom L } is Subset of L

{ x where x is Element of L : a "\/" x = Top L } is Subset of L

end;
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 } ;

{ 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 } ;

{ x where x is Element of L : a "\/" x = Top L } is Subset of L

proof 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 } ;

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

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;

coherence

( PseudoComplements a is initial & not PseudoComplements a is empty & PseudoComplements a is join-closed )

( PseudoCocomplements a is final & not PseudoCocomplements a is empty & PseudoCocomplements a is meet-closed )

end;
let a be Element of L;

coherence

( PseudoComplements a is initial & not PseudoComplements a is empty & PseudoComplements a is join-closed )

proof end;

coherence ( PseudoCocomplements a is final & not PseudoCocomplements a is empty & PseudoCocomplements a is meet-closed )

proof 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 )

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 )

for a, b being Element of L holds

( b in PseudoCocomplements a iff b "\/" a = Top L )

proof end;

definition

let L be Lattice;

{ I where I is Ideal of L : ( I is prime & I is proper ) } is Subset-Family of L

end;
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 ) } ;

{ I where I is Ideal of L : ( I is prime & I is proper ) } is Subset-Family of L

proof 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 ) } ;

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

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 )

( L is Boolean iff for I being Ideal of L st I is proper & I is prime holds

I is maximal )

proof end;

registration
end;