:: More on the Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received October 29, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

theorem Th1: :: WAYBEL15:1
for R being RelStr
for S being full SubRelStr of R
for T being full SubRelStr of S holds T is full SubRelStr of R
proofend;

Lm1:  for X being set
for Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
by FUNCT_2:27;

theorem :: WAYBEL15:2
for X being set
for a being Element of (BoolePoset X) holds uparrow a =  {  Y where Y is Subset of X : a c= Y  }
proofend;

theorem :: WAYBEL15:3
for L being non empty antisymmetric upper-bounded RelStr
for a being Element of L st Top L <= a holds
a = Top L
proofend;

theorem Th4: :: WAYBEL15:4
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st g is onto &amp; [g,d] is Galois holds
T, Image d are_isomorphic
proofend;

theorem Th5: :: WAYBEL15:5
for L1, L2, L3 being non empty Poset
for g1 being Function of L1,L2
for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois &amp; [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
proofend;

theorem Th6: :: WAYBEL15:6
for L1, L2 being non empty Poset
for f being Function of L1,L2
for f1 being Function of L2,L1 st f1 = f " &amp; f is isomorphic holds
( [f,f1] is Galois &amp; [f1,f] is Galois )
proofend;

theorem Th7: :: WAYBEL15:7
for X being set holds BoolePoset X is arithmetic
proofend;

registration
let X be set ;
cluster BoolePoset X ->  arithmetic ;
coherence
 BoolePoset X is arithmetic by Th7;
end;

theorem Th8: :: WAYBEL15:8
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds f .: (waybelow x) = waybelow (f . x)
proofend;

theorem Th9: :: WAYBEL15:9
for L1, L2 being non empty Poset st L1,L2 are_isomorphic &amp; L1 is continuous holds
L2 is continuous
proofend;

theorem Th10: :: WAYBEL15:10
for L1, L2 being LATTICE st L1,L2 are_isomorphic &amp; L1 is lower-bounded &amp; L1 is arithmetic holds
L2 is arithmetic
proofend;

Lm2:  for L being lower-bounded LATTICE st L is continuous holds
ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto &amp; g is infs-preserving &amp; g is directed-sups-preserving )
proofend;

theorem Th11: :: WAYBEL15:11
for L1, L2, L3 being non empty Poset
for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving &amp; g is directed-sups-preserving holds
g * f is directed-sups-preserving
proofend;

begin

theorem :: WAYBEL15:12
for L1, L2 being non empty RelStr
for f being Function of L1,L2
for X being Subset of (Image f) holds (inclusion f) .: X = X by FUNCT_1:92;

theorem Th13: :: WAYBEL15:13
for X being set
for c being Function of (BoolePoset X),(BoolePoset X) st c is idempotent &amp; c is directed-sups-preserving holds
inclusion c is directed-sups-preserving
proofend;

Lm3:  for L being lower-bounded LATTICE st ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto &amp; g is infs-preserving &amp; g is directed-sups-preserving ) holds
ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving &amp; L, Image p are_isomorphic )
proofend;

theorem Th14: :: WAYBEL15:14
for L being complete continuous LATTICE
for p being kernel Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
proofend;

theorem Th15: :: WAYBEL15:15
for L being complete continuous LATTICE
for p being projection Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
proofend;

Lm4:  for L being LATTICE st ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving &amp; L, Image p are_isomorphic ) holds
L is continuous
proofend;

theorem :: WAYBEL15:16
for L being lower-bounded LATTICE holds
( L is continuous iff ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto &amp; g is infs-preserving &amp; g is directed-sups-preserving ) )
proofend;

theorem :: WAYBEL15:17
for L being lower-bounded LATTICE holds
( L is continuous iff ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto &amp; g is infs-preserving &amp; g is directed-sups-preserving ) )
proofend;

theorem :: WAYBEL15:18
for L being lower-bounded LATTICE holds
( ( L is continuous implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving &amp; L, Image p are_isomorphic ) ) &amp; ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving &amp; L, Image p are_isomorphic ) implies L is continuous ) )
proofend;

begin

theorem :: WAYBEL15:19
for L being non empty RelStr
for x being Element of L holds
( x in PRIME (L opp) iff x is co-prime )
proofend;

definition
let L be non empty RelStr ;
let a be Element of L;
attra is atom  means :Def1: :: WAYBEL15:def 1
( Bottom L < a &amp; ( for b being Element of L st Bottom L < b &amp; b <= a holds
b = a ) );
end;

:: deftheorem Def1 defines atom WAYBEL15:def_1_:_
 for L being non empty RelStr
for a being Element of L holds
( a is atom iff ( Bottom L < a &amp; ( for b being Element of L st Bottom L < b &amp; b <= a holds
b = a ) ) );

definition
let L be non empty RelStr ;
func ATOM L ->  Subset of L means :Def2: :: WAYBEL15:def 2
 for x being Element of L holds
( x in it iff x is atom );
existence
 ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is atom )
proofend;
uniqueness
 for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is atom ) ) &amp; ( for x being Element of L holds
( x in b2 iff x is atom ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ATOM WAYBEL15:def_2_:_
 for L being non empty RelStr
for b2 being Subset of L holds
( b2 = ATOM L iff for x being Element of L holds
( x in b2 iff x is atom ) );

theorem Th20: :: WAYBEL15:20
for L being Boolean LATTICE
for a being Element of L holds
( a is atom iff ( a is co-prime &amp; a <> Bottom L ) )
proofend;

registration
let L be Boolean LATTICE;
cluster atom  ->  co-prime for Element of the carrier of L;
coherence
 for b1 being Element of L st b1 is atom holds
b1 is co-prime by Th20;
end;

theorem :: WAYBEL15:21
for L being Boolean LATTICE holds ATOM L = (PRIME (L opp)) \ {(Bottom L)}
proofend;

theorem :: WAYBEL15:22
for L being Boolean LATTICE
for x, a being Element of L st a is atom holds
( a <= x iff not a <= 'not' x )
proofend;

theorem Th23: :: WAYBEL15:23
for L being complete Boolean LATTICE
for X being Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" ( {  (x "/\" y) where y is Element of L : y in X  }  ,L)
proofend;

theorem Th24: :: WAYBEL15:24
for L being non empty antisymmetric with_infima lower-bounded RelStr
for x, y being Element of L st x is atom &amp; y is atom &amp; x <> y holds
x "/\" y = Bottom L
proofend;

theorem Th25: :: WAYBEL15:25
for L being complete Boolean LATTICE
for x being Element of L
for A being Subset of L st A c= ATOM L holds
( x in A iff ( x is atom &amp; x <= sup A ) )
proofend;

theorem Th26: :: WAYBEL15:26
for L being complete Boolean LATTICE
for X, Y being Subset of L st X c= ATOM L &amp; Y c= ATOM L holds
( X c= Y iff sup X <= sup Y )
proofend;

Lm5:  for L being Boolean LATTICE st L is completely-distributive holds
( L is complete &amp; ( for x being Element of L ex X being Subset of L st
( X c= ATOM L &amp; x = sup X ) ) )
proofend;

Lm6:  for L being Boolean LATTICE st L is complete &amp; ( for x being Element of L ex X being Subset of L st
( X c= ATOM L &amp; x = sup X ) ) holds
ex Y being set st L, BoolePoset Y are_isomorphic
proofend;

begin

theorem :: WAYBEL15:27
for L being Boolean LATTICE holds
( L is arithmetic iff ex X being set st L, BoolePoset X are_isomorphic )
proofend;

theorem :: WAYBEL15:28
for L being Boolean LATTICE holds
( L is arithmetic iff L is algebraic )
proofend;

theorem :: WAYBEL15:29
for L being Boolean LATTICE holds
( L is arithmetic iff L is continuous )
proofend;

theorem :: WAYBEL15:30
for L being Boolean LATTICE holds
( L is arithmetic iff ( L is continuous &amp; L opp is continuous ) )
proofend;

theorem :: WAYBEL15:31
for L being Boolean LATTICE holds
( L is arithmetic iff L is completely-distributive )
proofend;

theorem :: WAYBEL15:32
for L being Boolean LATTICE holds
( L is arithmetic iff ( L is complete &amp; ( for x being Element of L ex X being Subset of L st
( X c= ATOM L &amp; x = sup X ) ) ) )
proofend;