WAYBEL15: More on the Algebraic and Arithmetic Lattices

:: More on the Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received October 29, 1997
:: Copyright (c) 1997-2011 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

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

theorem :: WAYBEL15:2

canceled;

theorem :: WAYBEL15:3

canceled;

theorem :: WAYBEL15:4

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

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 Th6: :: WAYBEL15:6

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 Th7: :: WAYBEL15:7

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 Th8: :: WAYBEL15:8

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 Th9: :: WAYBEL15:9

for X being set holds BoolePoset X is arithmetic

proof end;

registration

let X be set ;
cluster BoolePoset X -> arithmetic ;
coherence by Th9;

end;

theorem Th10: :: WAYBEL15:10

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 Th11: :: WAYBEL15:11

for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is continuous holds
L2 is continuous

proof end;

theorem Th12: :: WAYBEL15:12

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 Th13: :: WAYBEL15:13

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;

begin

theorem :: WAYBEL15:14

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

theorem Th15: :: WAYBEL15:15

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 Th16: :: WAYBEL15:16

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 Th17: :: WAYBEL15:17

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

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

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

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;

begin

theorem :: WAYBEL15:21

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 :Def1: :: WAYBEL15:def 1
( Bottom L < a & ( for b being Element of L st Bottom L < b & b <= a holds
b = a ) );

end;

:: deftheorem Def1 defines atom WAYBEL15:def 1 :

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

proof end;

proof end;

end;

:: deftheorem Def2 defines ATOM WAYBEL15:def 2 :

theorem :: WAYBEL15:22

canceled;

theorem Th23: :: WAYBEL15:23

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 Element of the carrier of L;
coherence by Th23;

end;

theorem :: WAYBEL15:24

for L being Boolean LATTICE holds ATOM L = (PRIME (L opp)) \ {(Bottom L)}

proof end;

theorem :: WAYBEL15:25

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 Th26: :: WAYBEL15:26

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 Th27: :: WAYBEL15:27

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 Th28: :: WAYBEL15:28

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 Th29: :: WAYBEL15:29

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;

begin

theorem :: WAYBEL15:30

for L being Boolean LATTICE holds
( L is arithmetic iff ex X being set st L, BoolePoset X are_isomorphic )

proof end;

theorem :: WAYBEL15:31

for L being Boolean LATTICE holds
( L is arithmetic iff L is algebraic )

proof end;

theorem :: WAYBEL15:32

for L being Boolean LATTICE holds
( L is arithmetic iff L is continuous )

proof end;

theorem :: WAYBEL15:33

for L being Boolean LATTICE holds
( L is arithmetic iff ( L is continuous & L opp is continuous ) )

proof end;

theorem :: WAYBEL15:34

for L being Boolean LATTICE holds
( L is arithmetic iff L is completely-distributive )

proof end;

theorem :: WAYBEL15:35

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;