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


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

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

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

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 & [g,d] is Galois holds
T, Image d are_isomorphic
proof end;

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 & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
proof end;

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 " & f is isomorphic holds
( [f,f1] is Galois & [f1,f] is Galois )
proof end;

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

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

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

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

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 & g is infs-preserving & g is directed-sups-preserving )

proof end;

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 & g is directed-sups-preserving holds
g * f is directed-sups-preserving
proof end;

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 & c is directed-sups-preserving holds
inclusion c is directed-sups-preserving
proof end;

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 & g is infs-preserving & 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 & L, Image p are_isomorphic )

proof end;

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

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

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 & L, Image p are_isomorphic ) holds
L is continuous

proof end;

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 & g is infs-preserving & g is directed-sups-preserving ) )
proof end;

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 & g is infs-preserving & g is directed-sups-preserving ) )
proof end;

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 & L, Image p are_isomorphic ) ) & ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) )
proof end;

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

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

:: deftheorem 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 & ( for b being Element of L st Bottom L < b & 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 )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is atom ) ) & ( for x being Element of L holds
( x in b2 iff x is atom ) ) holds
b1 = b2
proof end;
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 & a <> Bottom L ) )
proof end;

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

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

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

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 & y is atom & x <> y holds
x "/\" y = Bottom L
proof end;

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 & x <= sup A ) )
proof end;

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

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

proof end;

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

proof end;

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

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

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

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

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

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