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

registration

cluster non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for LattStr ;

existence
ex b₁ being Lattice st b₁ 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 b₁ being Lattice st b₁ is finite holds
b₁ 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 b₁ being Lattice st
( b₁ is noetherian & b₁ is upper-bounded & b₁ is lower-bounded & b₁ 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 b₁ being Lattice st
( b₁ is co-noetherian & b₁ is upper-bounded & b₁ is lower-bounded & b₁ 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 )
by Lm6;

registration

cluster non empty finite Lattice-like -> noetherian for LattStr ;

coherence
for b₁ being Lattice st b₁ is finite holds
b₁ is noetherian ;

cluster non empty finite Lattice-like -> co-noetherian for LattStr ;

coherence
for b₁ being Lattice st b₁ is finite holds
b₁ 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 :: 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 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 :: LATTICE6:def 8
a *' <> a;

attr a is completely-join-irreducible means :: LATTICE6:def 9
*' a <> a;

end;

:: deftheorem 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 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 :: LATTICE6:def 10
a is-upper-neighbour-of Bottom L;

attr a is co-atomic means :: LATTICE6:def 11
a is-lower-neighbour-of Top L;

end;

:: deftheorem 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 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 :: 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 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 b₁ being Lattice st
( b₁ is strict & b₁ 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 b₁ being Lattice st
( b₁ is atomic & b₁ is complete )

proof end;

end;

definition

let L be complete Lattice;
let D be Subset of L;

attr D is supremum-dense means :: 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 :: LATTICE6:def 14
for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L);

end;

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