:: Algebraic Lattices
:: by Robert Milewski
::
:: Received December 1, 1996
:: Copyright (c) 1996-2012 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 b1 being strict full SubRelStr of L st
for x being Element of L holds
( x in the carrier of b1 iff x is compact )
proof end;
uniqueness
for b1, b2 being strict full SubRelStr of L st ( for x being Element of L holds
( x in the carrier of b1 iff x is compact ) ) & ( for x being Element of L holds
( x in the carrier of b2 iff x is compact ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def 1 :
for L being non empty reflexive RelStr
for b2 being strict full SubRelStr of L holds
( b2 = CompactSublatt L iff for x being Element of L holds
( x in the carrier of b2 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 for RelStr ;
coherence
for b1 being LATTICE st b1 is algebraic holds
b1 is continuous
by Th7;
end;

registration
cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K for RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is algebraic holds
( b1 is up-complete & b1 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 for RelStr ;
coherence
for b1 being LATTICE st b1 is arithmetic holds
b1 is algebraic
by Def5;
end;

registration
cluster trivial reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ;
coherence
for b1 being LATTICE st b1 is trivial holds
b1 is arithmetic
proof end;
end;

registration
cluster non empty 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;
existence
ex b1 being LATTICE st
( b1 is 1 -element & b1 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
for L being algebraic LATTICE holds
( L is arithmetic iff CompactSublatt L is LATTICE )
proof end;

theorem Th20: :: WAYBEL_8:20
for L being lower-bounded algebraic LATTICE holds
( L is arithmetic iff L -waybelow is multiplicative )
proof end;

theorem :: WAYBEL_8:21
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:22
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 for Element of bool the carrier of (Image c);
existence
ex b1 being Subset of (Image c) st
( not b1 is empty & b1 is directed )
proof end;
end;

theorem Th23: :: WAYBEL_8:23
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:24
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:25
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 Th26: :: WAYBEL_8:26
for X, x being set holds
( x is Element of (BoolePoset X) iff x c= X )
proof end;

theorem Th27: :: WAYBEL_8:27
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 Th28: :: WAYBEL_8:28
for X being set
for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )
proof end;

theorem Th29: :: WAYBEL_8:29
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:30
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 Th31: :: WAYBEL_8:31
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 Th31;
end;