:: Algebraic Lattices
:: by Robert Milewski
::
:: Received December 1, 1996
:: Copyright (c) 1996-2011 Association of Mizar Users

begin

definition

let L be non empty reflexive RelStr ;
func CompactSublatt L -> strict full SubRelStr of L means :Def1: :: WAYBEL_8:def 1
for x being Element of L holds
( x in the carrier of it iff x is compact );
existence
ex b₁ being strict full SubRelStr of L st
for x being Element of L holds
( x in the carrier of b₁ iff x is compact )

proof end;

uniqueness
for b₁, b₂ being strict full SubRelStr of L st ( for x being Element of L holds
( x in the carrier of b₁ iff x is compact ) ) & ( for x being Element of L holds
( x in the carrier of b₂ iff x is compact ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def 1 :
for L being non empty reflexive RelStr
for b₂ being strict full SubRelStr of L holds
( b₂ = CompactSublatt L iff for x being Element of L holds
( x in the carrier of b₂ iff x is compact ) );

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster CompactSublatt L -> non empty strict full ;
coherence
not CompactSublatt L is empty

proof end;

end;

theorem :: WAYBEL_8:1

for L being complete LATTICE
for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y

proof end;

theorem :: WAYBEL_8:2

for L being complete LATTICE
for x being Element of L holds
( uparrow x is Open Filter of L iff x is compact )

proof end;

theorem :: WAYBEL_8:3

for L being non empty with_suprema lower-bounded Poset holds
( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )

proof end;

definition

let L be non empty reflexive RelStr ;
let x be Element of L;
func compactbelow x -> Subset of L equals :: WAYBEL_8:def 2
{ y where y is Element of L : ( x >= y & y is compact ) } ;
coherence
{ y where y is Element of L : ( x >= y & y is compact ) } is Subset of L

proof end;

end;

:: deftheorem defines compactbelow WAYBEL_8:def 2 :
for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x = { y where y is Element of L : ( x >= y & y is compact ) } ;

theorem Th4: :: WAYBEL_8:4

for L being non empty reflexive RelStr
for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )

proof end;

theorem Th5: :: WAYBEL_8:5

for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)

proof end;

theorem Th6: :: WAYBEL_8:6

for L being non empty reflexive transitive RelStr
for x being Element of L holds compactbelow x c= waybelow x

proof end;

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;
let x be Element of L;
cluster compactbelow x -> non empty ;
coherence
not compactbelow x is empty

proof end;

end;

begin

definition

let L be non empty reflexive RelStr ;
attr L is satisfying_axiom_K means :Def3: :: WAYBEL_8:def 3
for x being Element of L holds x = sup (compactbelow x);

end;

:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def 3 :
for L being non empty reflexive RelStr holds
( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) );

definition

let L be non empty reflexive RelStr ;
attr L is algebraic means :Def4: :: WAYBEL_8:def 4
( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K );

end;

:: deftheorem Def4 defines algebraic WAYBEL_8:def 4 :
for L being non empty reflexive RelStr holds
( L is algebraic iff ( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) );

theorem Th7: :: WAYBEL_8:7

for L being LATTICE holds
( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )

proof end;

registration

cluster reflexive transitive antisymmetric with_suprema with_infima algebraic -> continuous RelStr ;
coherence
for b₁ being LATTICE st b₁ is algebraic holds
b₁ is continuous by Th7;

end;

registration

cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K RelStr ;
coherence
for b₁ being non empty reflexive RelStr st b₁ is algebraic holds
( b₁ is up-complete & b₁ is satisfying_axiom_K ) by Def4;

end;

registration

let L be non empty with_suprema Poset;
cluster CompactSublatt L -> strict full join-inheriting ;
coherence
CompactSublatt L is join-inheriting

proof end;

end;

definition

let L be non empty reflexive RelStr ;
attr L is arithmetic means :Def5: :: WAYBEL_8:def 5
( L is algebraic & CompactSublatt L is meet-inheriting );

end;

:: deftheorem Def5 defines arithmetic WAYBEL_8:def 5 :
for L being non empty reflexive RelStr holds
( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) );

begin

registration

cluster reflexive transitive antisymmetric with_suprema with_infima arithmetic -> algebraic RelStr ;
coherence
for b₁ being LATTICE st b₁ is arithmetic holds
b₁ is algebraic by Def5;

end;

registration

cluster trivial reflexive transitive antisymmetric with_suprema with_infima -> arithmetic RelStr ;
coherence
for b₁ being LATTICE st b₁ is trivial holds
b₁ is arithmetic

proof end;

end;

registration

cluster non empty trivial strict reflexive transitive antisymmetric with_suprema with_infima RelStr ;
existence
ex b₁ being LATTICE st
( b₁ is trivial & b₁ is strict )

proof end;

end;

theorem Th8: :: WAYBEL_8:8

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2

proof end;

theorem Th9: :: WAYBEL_8:9

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact

proof end;

theorem Th10: :: WAYBEL_8:10

for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y

proof end;

theorem :: WAYBEL_8:11

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & not L1 is empty holds
not L2 is empty ;

theorem Th12: :: WAYBEL_8:12

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive holds
L2 is reflexive

proof end;

theorem Th13: :: WAYBEL_8:13

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive holds
L2 is transitive

proof end;

theorem Th14: :: WAYBEL_8:14

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric holds
L2 is antisymmetric

proof end;

theorem Th15: :: WAYBEL_8:15

for L1, L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
L2 is up-complete

proof end;

theorem Th16: :: WAYBEL_8:16

for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) holds
L2 is satisfying_axiom_K

proof end;

theorem Th17: :: WAYBEL_8:17

for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic holds
L2 is algebraic

proof end;

theorem Th18: :: WAYBEL_8:18

for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic holds
L2 is arithmetic

proof end;

registration

let L be non empty RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> non empty ;
coherence
not RelStr(# the carrier of L, the InternalRel of L #) is empty ;

end;

registration

let L be non empty reflexive RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> reflexive ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is reflexive by Th12;

end;

registration

let L be transitive RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> transitive ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is transitive by Th13;

end;

registration

let L be antisymmetric RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> antisymmetric ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is antisymmetric by Th14;

end;

registration

let L be with_infima RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_infima ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is with_infima by YELLOW_7:14;

end;

registration

let L be with_suprema RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_suprema ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is with_suprema by YELLOW_7:15;

end;

registration

let L be non empty reflexive up-complete RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> up-complete ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is up-complete by Th15;

end;

registration

let L be non empty reflexive antisymmetric algebraic RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> algebraic ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is algebraic by Th17;

end;

registration

let L be arithmetic LATTICE;
cluster RelStr(# the carrier of L, the InternalRel of L #) -> arithmetic ;
coherence
RelStr(# the carrier of L, the InternalRel of L #) is arithmetic by Th18;

end;

theorem :: WAYBEL_8:19

canceled;

theorem :: WAYBEL_8:20

canceled;

theorem :: WAYBEL_8:21

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

proof end;

theorem Th22: :: WAYBEL_8:22

for L being lower-bounded algebraic LATTICE holds
( L is arithmetic iff L -waybelow is multiplicative )

proof end;

theorem :: WAYBEL_8:23

for L being lower-bounded arithmetic LATTICE
for p being Element of L st p is pseudoprime holds
p is prime

proof end;

theorem :: WAYBEL_8:24

for L being lower-bounded distributive algebraic LATTICE st ( for p being Element of L st p is pseudoprime holds
p is prime ) holds
L is arithmetic

proof end;

registration

let L be algebraic LATTICE;
let c be closure Function of L,L;
cluster non empty directed Element of bool the carrier of (Image c);
existence
ex b₁ being Subset of (Image c) st
( not b₁ is empty & b₁ is directed )

proof end;

end;

theorem Th25: :: WAYBEL_8:25

for L being algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))

proof end;

theorem :: WAYBEL_8:26

for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
Image c is algebraic LATTICE

proof end;

theorem :: WAYBEL_8:27

for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))

proof end;

begin

theorem Th28: :: WAYBEL_8:28

for X, x being set holds
( x is Element of (BoolePoset X) iff x c= X )

proof end;

theorem Th29: :: WAYBEL_8:29

for X being set
for x, y being Element of (BoolePoset X) holds
( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )

proof end;

theorem Th30: :: WAYBEL_8:30

for X being set
for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )

proof end;

theorem Th31: :: WAYBEL_8:31

for X being set
for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }

proof end;

theorem :: WAYBEL_8:32

for X being set
for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )

proof end;

registration

let X be set ;
let x be Element of (BoolePoset X);
cluster compactbelow x -> directed lower ;
coherence
( compactbelow x is lower & compactbelow x is directed )

proof end;

end;

theorem Th33: :: WAYBEL_8:33

for X being set holds BoolePoset X is algebraic

proof end;

registration

let X be set ;
cluster BoolePoset X -> algebraic ;
coherence
BoolePoset X is algebraic by Th33;

end;