:: Noetherian Lattices
:: by Christoph Schwarzweller
::
:: Received June 9, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

registration
cluster non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for LattStr ;
existence
ex b1 being Lattice st b1 is finite
proof end;
end;

Lm1: for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )

proof end;

Lm2: for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )

proof end;

Lm3: for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )

proof end;

Lm4: for L being finite Lattice ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a

proof end;

Lm5: for L being finite Lattice holds L is complete
proof end;

registration
cluster non empty finite Lattice-like -> complete for LattStr ;
coherence
for b1 being Lattice st b1 is finite holds
b1 is complete
by Lm5;
end;

definition
let L be Lattice;
let D be Subset of L;
func D % -> Subset of (LattPOSet L) equals :: LATTICE6:def 1
{ (d %) where d is Element of L : d in D } ;
coherence
{ (d %) where d is Element of L : d in D } is Subset of (LattPOSet L)
proof end;
end;

:: deftheorem defines % LATTICE6:def 1 :
for L being Lattice
for D being Subset of L holds D % = { (d %) where d is Element of L : d in D } ;

definition
let L be Lattice;
let D be Subset of (LattPOSet L);
func % D -> Subset of L equals :: LATTICE6:def 2
{ (% d) where d is Element of (LattPOSet L) : d in D } ;
coherence
{ (% d) where d is Element of (LattPOSet L) : d in D } is Subset of L
proof end;
end;

:: deftheorem defines % LATTICE6:def 2 :
for L being Lattice
for D being Subset of (LattPOSet L) holds % D = { (% d) where d is Element of (LattPOSet L) : d in D } ;

registration
let L be finite Lattice;
cluster LattPOSet L -> well_founded ;
coherence
LattPOSet L is well_founded
proof end;
end;

Lm6: for L being finite Lattice holds (LattPOSet L) ~ is well_founded
proof end;

definition
let L be Lattice;
attr L is noetherian means :Def3: :: LATTICE6:def 3
LattPOSet L is well_founded ;
attr L is co-noetherian means :Def4: :: LATTICE6:def 4
(LattPOSet L) ~ is well_founded ;
end;

:: deftheorem Def3 defines noetherian LATTICE6:def 3 :
for L being Lattice holds
( L is noetherian iff LattPOSet L is well_founded );

:: deftheorem Def4 defines co-noetherian LATTICE6:def 4 :
for L being Lattice holds
( L is co-noetherian iff (LattPOSet L) ~ is well_founded );

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded complete noetherian for LattStr ;
existence
ex b1 being Lattice st
( b1 is noetherian & b1 is upper-bounded & b1 is lower-bounded & b1 is complete )
proof end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded complete co-noetherian for LattStr ;
existence
ex b1 being Lattice st
( b1 is co-noetherian & b1 is upper-bounded & b1 is lower-bounded & b1 is complete )
proof end;
end;

theorem :: LATTICE6:1
for L being Lattice holds
( L is noetherian iff L .: is co-noetherian )
proof end;

Lm7: for L being finite Lattice holds
( L is noetherian & L is co-noetherian )

proof end;

registration
cluster non empty finite Lattice-like -> noetherian for LattStr ;
coherence
for b1 being Lattice st b1 is finite holds
b1 is noetherian
by Lm7;
cluster non empty finite Lattice-like -> co-noetherian for LattStr ;
coherence
for b1 being Lattice st b1 is finite holds
b1 is co-noetherian
by Lm7;
end;

definition
let L be Lattice;
let a, b be Element of L;
pred a is-upper-neighbour-of b means :Def5: :: LATTICE6:def 5
( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) );
end;

:: deftheorem Def5 defines is-upper-neighbour-of LATTICE6:def 5 :
for L being Lattice
for a, b being Element of L holds
( a is-upper-neighbour-of b iff ( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) ) );

notation
let L be Lattice;
let a, b be Element of L;
synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;
end;

theorem Th2: :: LATTICE6:2
for L being Lattice
for a, b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )
proof end;

theorem Th3: :: LATTICE6:3
for L being noetherian Lattice
for a, d being Element of L st a [= d & a <> d holds
ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )
proof end;

theorem Th4: :: LATTICE6:4
for L being co-noetherian Lattice
for a, d being Element of L st d [= a & a <> d holds
ex c being Element of L st
( d [= c & c is-lower-neighbour-of a )
proof end;

theorem Th5: :: LATTICE6:5
for L being upper-bounded Lattice
for b being Element of L holds not b is-upper-neighbour-of Top L
proof end;

theorem Th6: :: LATTICE6:6
for L being upper-bounded noetherian Lattice
for a being Element of L holds
( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a )
proof end;

theorem Th7: :: LATTICE6:7
for L being lower-bounded Lattice
for b being Element of L holds not b is-lower-neighbour-of Bottom L
proof end;

theorem Th8: :: LATTICE6:8
for L being lower-bounded co-noetherian Lattice
for a being Element of L holds
( a = Bottom L iff for b being Element of L holds not b is-lower-neighbour-of a )
proof end;

definition
let L be complete Lattice;
let a be Element of L;
func a *' -> Element of L equals :: LATTICE6:def 6
"/\" ( { d where d is Element of L : ( a [= d & d <> a ) } ,L);
correctness
coherence
"/\" ( { d where d is Element of L : ( a [= d & d <> a ) } ,L) is Element of L
;
;
func *' a -> Element of L equals :: LATTICE6:def 7
"\/" ( { d where d is Element of L : ( d [= a & d <> a ) } ,L);
correctness
coherence
"\/" ( { d where d is Element of L : ( d [= a & d <> a ) } ,L) is Element of L
;
;
end;

:: deftheorem defines *' LATTICE6:def 6 :
for L being complete Lattice
for a being Element of L holds a *' = "/\" ( { d where d is Element of L : ( a [= d & d <> a ) } ,L);

:: deftheorem defines *' LATTICE6:def 7 :
for L being complete Lattice
for a being Element of L holds *' a = "\/" ( { d where d is Element of L : ( d [= a & d <> a ) } ,L);

definition
let L be complete Lattice;
let a be Element of L;
attr a is completely-meet-irreducible means :Def8: :: LATTICE6:def 8
a *' <> a;
attr a is completely-join-irreducible means :Def9: :: LATTICE6:def 9
*' a <> a;
end;

:: deftheorem Def8 defines completely-meet-irreducible LATTICE6:def 8 :
for L being complete Lattice
for a being Element of L holds
( a is completely-meet-irreducible iff a *' <> a );

:: deftheorem Def9 defines completely-join-irreducible LATTICE6:def 9 :
for L being complete Lattice
for a being Element of L holds
( a is completely-join-irreducible iff *' a <> a );

theorem Th9: :: LATTICE6:9
for L being complete Lattice
for a being Element of L holds
( a [= a *' & *' a [= a )
proof end;

theorem :: LATTICE6:10
for L being complete Lattice holds
( (Top L) *' = Top L & (Top L) % is meet-irreducible )
proof end;

theorem :: LATTICE6:11
for L being complete Lattice holds
( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible )
proof end;

theorem Th12: :: LATTICE6:12
for L being complete Lattice
for a being Element of L st a is completely-meet-irreducible holds
( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) )
proof end;

theorem Th13: :: LATTICE6:13
for L being complete Lattice
for a being Element of L st a is completely-join-irreducible holds
( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) )
proof end;

theorem Th14: :: LATTICE6:14
for L being complete noetherian Lattice
for a being Element of L holds
( a is completely-meet-irreducible iff ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) )
proof end;

theorem Th15: :: LATTICE6:15
for L being complete co-noetherian Lattice
for a being Element of L holds
( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) )
proof end;

theorem Th16: :: LATTICE6:16
for L being complete Lattice
for a being Element of L st a is completely-meet-irreducible holds
a % is meet-irreducible
proof end;

Lm8: for L being Lattice
for a, b being Element of L holds
( a "/\" b = (a %) "/\" (b %) & a "\/" b = (a %) "\/" (b %) )

proof end;

theorem Th17: :: LATTICE6:17
for L being complete noetherian Lattice
for a being Element of L st a <> Top L holds
( a is completely-meet-irreducible iff a % is meet-irreducible )
proof end;

theorem Th18: :: LATTICE6:18
for L being complete Lattice
for a being Element of L st a is completely-join-irreducible holds
a % is join-irreducible
proof end;

theorem Th19: :: LATTICE6:19
for L being complete co-noetherian Lattice
for a being Element of L st a <> Bottom L holds
( a is completely-join-irreducible iff a % is join-irreducible )
proof end;

theorem :: LATTICE6:20
for L being finite Lattice
for a being Element of L st a <> Bottom L & a <> Top L holds
( ( a is completely-meet-irreducible implies a % is meet-irreducible ) & ( a % is meet-irreducible implies a is completely-meet-irreducible ) & ( a is completely-join-irreducible implies a % is join-irreducible ) & ( a % is join-irreducible implies a is completely-join-irreducible ) ) by Th17, Th19;

definition
let L be Lattice;
let a be Element of L;
attr a is atomic means :Def10: :: LATTICE6:def 10
a is-upper-neighbour-of Bottom L;
attr a is co-atomic means :Def11: :: LATTICE6:def 11
a is-lower-neighbour-of Top L;
end;

:: deftheorem Def10 defines atomic LATTICE6:def 10 :
for L being Lattice
for a being Element of L holds
( a is atomic iff a is-upper-neighbour-of Bottom L );

:: deftheorem Def11 defines co-atomic LATTICE6:def 11 :
for L being Lattice
for a being Element of L holds
( a is co-atomic iff a is-lower-neighbour-of Top L );

theorem :: LATTICE6:21
for L being complete Lattice
for a being Element of L st a is atomic holds
a is completely-join-irreducible
proof end;

theorem :: LATTICE6:22
for L being complete Lattice
for a being Element of L st a is co-atomic holds
a is completely-meet-irreducible
proof end;

definition
let L be Lattice;
attr L is atomic means :Def12: :: LATTICE6:def 12
for a being Element of L ex X being Subset of L st
( ( for x being Element of L st x in X holds
x is atomic ) & a = "\/" (X,L) );
end;

:: deftheorem Def12 defines atomic LATTICE6:def 12 :
for L being Lattice holds
( L is atomic iff for a being Element of L ex X being Subset of L st
( ( for x being Element of L st x in X holds
x is atomic ) & a = "\/" (X,L) ) );

registration
cluster non empty 1 -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for LattStr ;
existence
ex b1 being Lattice st
( b1 is strict & b1 is 1 -element )
proof end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete atomic for LattStr ;
existence
ex b1 being Lattice st
( b1 is atomic & b1 is complete )
proof end;
end;

definition
let L be complete Lattice;
let D be Subset of L;
attr D is supremum-dense means :Def13: :: LATTICE6:def 13
for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L);
attr D is infimum-dense means :Def14: :: LATTICE6:def 14
for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L);
end;

:: deftheorem Def13 defines supremum-dense LATTICE6:def 13 :
for L being complete Lattice
for D being Subset of L holds
( D is supremum-dense iff for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L) );

:: deftheorem Def14 defines infimum-dense LATTICE6:def 14 :
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L) );

theorem Th23: :: LATTICE6:23
for L being complete Lattice
for D being Subset of L holds
( D is supremum-dense iff for a being Element of L holds a = "\/" ( { d where d is Element of L : ( d in D & d [= a ) } ,L) )
proof end;

theorem Th24: :: LATTICE6:24
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L holds a = "/\" ( { d where d is Element of L : ( d in D & a [= d ) } ,L) )
proof end;

theorem :: LATTICE6:25
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff D % is order-generating )
proof end;

definition
let L be complete Lattice;
func MIRRS L -> Subset of L equals :: LATTICE6:def 15
{ a where a is Element of L : a is completely-meet-irreducible } ;
correctness
coherence
{ a where a is Element of L : a is completely-meet-irreducible } is Subset of L
;
proof end;
func JIRRS L -> Subset of L equals :: LATTICE6:def 16
{ a where a is Element of L : a is completely-join-irreducible } ;
correctness
coherence
{ a where a is Element of L : a is completely-join-irreducible } is Subset of L
;
proof end;
end;

:: deftheorem defines MIRRS LATTICE6:def 15 :
for L being complete Lattice holds MIRRS L = { a where a is Element of L : a is completely-meet-irreducible } ;

:: deftheorem defines JIRRS LATTICE6:def 16 :
for L being complete Lattice holds JIRRS L = { a where a is Element of L : a is completely-join-irreducible } ;

theorem :: LATTICE6:26
for L being complete Lattice
for D being Subset of L st D is supremum-dense holds
JIRRS L c= D
proof end;

theorem :: LATTICE6:27
for L being complete Lattice
for D being Subset of L st D is infimum-dense holds
MIRRS L c= D
proof end;

Lm9: for L being complete co-noetherian Lattice holds MIRRS L is infimum-dense
proof end;

registration
let L be complete co-noetherian Lattice;
cluster MIRRS L -> infimum-dense ;
coherence
MIRRS L is infimum-dense
by Lm9;
end;

Lm10: for L being complete noetherian Lattice holds JIRRS L is supremum-dense
proof end;

registration
let L be complete noetherian Lattice;
cluster JIRRS L -> supremum-dense ;
coherence
JIRRS L is supremum-dense
by Lm10;
end;