:: Irreducible and Prime Elements
:: by Beata Madras
::
:: Received December 1, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

:: Preliminaries
scheme :: WAYBEL_6:sch 1
NonUniqExD1{ F1() -> non empty RelStr , F2() -> Subset of F1(), F3() -> non empty Subset of F1(), P1[ set , set ] } :
ex f being Function of F2(),F3() st
for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
provided
A1: for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & P1[e,u] )
proof end;

definition
let L be LATTICE;
let A be non empty Subset of L;
let f be Function of A,A;
let n be Element of NAT ;
:: original: iter
redefine func iter (f,n) -> Function of A,A;
coherence
iter (f,n) is Function of A,A
by FUNCT_7:83;
end;

definition
let L be LATTICE;
let C, D be non empty Subset of L;
let f be Function of C,D;
let c be Element of C;
:: original: .
redefine func f . c -> Element of L;
coherence
f . c is Element of L
proof end;
end;

registration
let L be non empty Poset;
cluster strongly_connected -> directed filtered for Element of bool the carrier of L;
coherence
for b1 being Chain of L holds
( b1 is filtered & b1 is directed )
proof end;
end;

registration
cluster non empty strict V110() reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous for RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & b1 is continuous & b1 is distributive & b1 is lower-bounded )
proof end;
end;

theorem Th1: :: WAYBEL_6:1
for S, T being Semilattice
for f being Function of S,T holds
( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )
proof end;

theorem Th2: :: WAYBEL_6:2
for S, T being sup-Semilattice
for f being Function of S,T holds
( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )
proof end;

theorem Th3: :: WAYBEL_6:3
for S, T being LATTICE
for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds
S is distributive
proof end;

registration
let S, T be complete LATTICE;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V32( the carrier of S, the carrier of T) sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
ex b1 being Function of S,T st b1 is sups-preserving
proof end;
end;

Lm1: for S, T being non empty with_suprema Poset
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone

proof end;

theorem Th4: :: WAYBEL_6:4
for S, T being complete LATTICE
for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds
S is meet-continuous
proof end;

begin

definition
let L be non empty reflexive RelStr ;
let X be Subset of L;
attr X is Open means :Def1: :: WAYBEL_6:def 1
for x being Element of L st x in X holds
ex y being Element of L st
( y in X & y << x );
end;

:: deftheorem Def1 defines Open WAYBEL_6:def 1 :
for L being non empty reflexive RelStr
for X being Subset of L holds
( X is Open iff for x being Element of L st x in X holds
ex y being Element of L st
( y in X & y << x ) );

theorem :: WAYBEL_6:5
for L being up-complete LATTICE
for X being upper Subset of L holds
( X is Open iff for x being Element of L st x in X holds
waybelow x meets X )
proof end;

theorem :: WAYBEL_6:6
for L being up-complete LATTICE
for X being upper Subset of L holds
( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } )
proof end;

registration
let L be lower-bounded up-complete LATTICE;
cluster non empty filtered upper Open for Element of bool the carrier of L;
existence
ex b1 being Filter of L st b1 is Open
proof end;
end;

theorem :: WAYBEL_6:7
for L being lower-bounded continuous LATTICE
for x being Element of L holds wayabove x is Open
proof end;

theorem Th8: :: WAYBEL_6:8
for L being lower-bounded continuous LATTICE
for x, y being Element of L st x << y holds
ex F being Open Filter of L st
( y in F & F c= wayabove x )
proof end;

theorem Th9: :: WAYBEL_6:9
for L being complete LATTICE
for X being upper Open Subset of L
for x being Element of L st x in X ` holds
ex m being Element of L st
( x <= m & m is_maximal_in X ` )
proof end;

begin

definition
let G be non empty RelStr ;
let g be Element of G;
attr g is meet-irreducible means :Def2: :: WAYBEL_6:def 2
for x, y being Element of G holds
( not g = x "/\" y or x = g or y = g );
end;

:: deftheorem Def2 defines meet-irreducible WAYBEL_6:def 2 :
for G being non empty RelStr
for g being Element of G holds
( g is meet-irreducible iff for x, y being Element of G holds
( not g = x "/\" y or x = g or y = g ) );

notation
let G be non empty RelStr ;
let g be Element of G;
synonym irreducible g for meet-irreducible ;
end;

definition
let G be non empty RelStr ;
let g be Element of G;
attr g is join-irreducible means :: WAYBEL_6:def 3
for x, y being Element of G holds
( not g = x "\/" y or x = g or y = g );
end;

:: deftheorem defines join-irreducible WAYBEL_6:def 3 :
for G being non empty RelStr
for g being Element of G holds
( g is join-irreducible iff for x, y being Element of G holds
( not g = x "\/" y or x = g or y = g ) );

definition
let L be non empty RelStr ;
func IRR L -> Subset of L means :Def4: :: WAYBEL_6:def 4
for x being Element of L holds
( x in it iff x is irreducible );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is irreducible )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is irreducible ) ) & ( for x being Element of L holds
( x in b2 iff x is irreducible ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines IRR WAYBEL_6:def 4 :
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = IRR L iff for x being Element of L holds
( x in b2 iff x is irreducible ) );

theorem Th10: :: WAYBEL_6:10
for L being non empty antisymmetric upper-bounded with_infima RelStr holds Top L is irreducible
proof end;

registration
let L be non empty antisymmetric upper-bounded with_infima RelStr ;
cluster irreducible for Element of the carrier of L;
existence
ex b1 being Element of L st b1 is irreducible
proof end;
end;

theorem :: WAYBEL_6:11
for L being Semilattice
for x being Element of L holds
( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds
x in A )
proof end;

theorem :: WAYBEL_6:12
for L being LATTICE
for l being Element of L st (uparrow l) \ {l} is Filter of L holds
l is irreducible
proof end;

theorem Th13: :: WAYBEL_6:13
for L being LATTICE
for p being Element of L
for F being Filter of L st p is_maximal_in F ` holds
p is irreducible
proof end;

theorem Th14: :: WAYBEL_6:14
for L being lower-bounded continuous LATTICE
for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is irreducible & x <= p & not y <= p )
proof end;

begin

definition
let L be non empty RelStr ;
let X be Subset of L;
attr X is order-generating means :Def5: :: WAYBEL_6:def 5
for x being Element of L holds
( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) );
end;

:: deftheorem Def5 defines order-generating WAYBEL_6:def 5 :
for L being non empty RelStr
for X being Subset of L holds
( X is order-generating iff for x being Element of L holds
( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) );

theorem Th15: :: WAYBEL_6:15
for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) )
proof end;

theorem :: WAYBEL_6:16
for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )
proof end;

theorem Th17: :: WAYBEL_6:17
for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
proof end;

theorem Th18: :: WAYBEL_6:18
for L being lower-bounded continuous LATTICE
for X being Subset of L st X = (IRR L) \ {(Top L)} holds
X is order-generating
proof end;

theorem Th19: :: WAYBEL_6:19
for L being lower-bounded continuous LATTICE
for X, Y being Subset of L st X is order-generating & X c= Y holds
Y is order-generating
proof end;

begin

definition
let L be non empty RelStr ;
let l be Element of L;
attr l is prime means :Def6: :: WAYBEL_6:def 6
for x, y being Element of L holds
( not x "/\" y <= l or x <= l or y <= l );
end;

:: deftheorem Def6 defines prime WAYBEL_6:def 6 :
for L being non empty RelStr
for l being Element of L holds
( l is prime iff for x, y being Element of L holds
( not x "/\" y <= l or x <= l or y <= l ) );

definition
let L be non empty RelStr ;
func PRIME L -> Subset of L means :Def7: :: WAYBEL_6:def 7
for x being Element of L holds
( x in it iff x is prime );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is prime )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is prime ) ) & ( for x being Element of L holds
( x in b2 iff x is prime ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines PRIME WAYBEL_6:def 7 :
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = PRIME L iff for x being Element of L holds
( x in b2 iff x is prime ) );

definition
let L be non empty RelStr ;
let l be Element of L;
attr l is co-prime means :Def8: :: WAYBEL_6:def 8
l ~ is prime ;
end;

:: deftheorem Def8 defines co-prime WAYBEL_6:def 8 :
for L being non empty RelStr
for l being Element of L holds
( l is co-prime iff l ~ is prime );

theorem Th20: :: WAYBEL_6:20
for L being non empty antisymmetric upper-bounded RelStr holds Top L is prime
proof end;

theorem :: WAYBEL_6:21
for L being non empty antisymmetric lower-bounded RelStr holds Bottom L is co-prime
proof end;

registration
let L be non empty antisymmetric upper-bounded RelStr ;
cluster prime for Element of the carrier of L;
existence
ex b1 being Element of L st b1 is prime
proof end;
end;

theorem Th22: :: WAYBEL_6:22
for L being Semilattice
for l being Element of L holds
( l is prime iff for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) )
proof end;

theorem Th23: :: WAYBEL_6:23
for L being sup-Semilattice
for x being Element of L holds
( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) )
proof end;

theorem Th24: :: WAYBEL_6:24
for L being LATTICE
for l being Element of L st l is prime holds
l is irreducible
proof end;

theorem Th25: :: WAYBEL_6:25
for L being LATTICE
for l being Element of L holds
( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
proof end;

theorem Th26: :: WAYBEL_6:26
for L being upper-bounded LATTICE
for l being Element of L st l <> Top L holds
( l is prime iff (downarrow l) ` is Filter of L )
proof end;

theorem Th27: :: WAYBEL_6:27
for L being distributive LATTICE
for l being Element of L holds
( l is prime iff l is irreducible )
proof end;

theorem Th28: :: WAYBEL_6:28
for L being distributive LATTICE holds PRIME L = IRR L
proof end;

theorem :: WAYBEL_6:29
for L being Boolean LATTICE
for l being Element of L st l <> Top L holds
( l is prime iff for x being Element of L st x > l holds
x = Top L )
proof end;

theorem :: WAYBEL_6:30
for L being lower-bounded distributive continuous LATTICE
for l being Element of L st l <> Top L holds
( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` )
proof end;

theorem Th31: :: WAYBEL_6:31
for L being RelStr
for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}})
proof end;

theorem Th32: :: WAYBEL_6:32
for L being non empty RelStr
for p, x being Element of L holds
( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p )
proof end;

theorem Th33: :: WAYBEL_6:33
for L being upper-bounded LATTICE
for f being Function of L,(BoolePoset {{}})
for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds
( f is meet-preserving & f is join-preserving )
proof end;

theorem Th34: :: WAYBEL_6:34
for L being complete LATTICE st PRIME L is order-generating holds
( L is distributive & L is meet-continuous )
proof end;

theorem Th35: :: WAYBEL_6:35
for L being lower-bounded continuous LATTICE holds
( L is distributive iff PRIME L is order-generating )
proof end;

theorem :: WAYBEL_6:36
for L being lower-bounded continuous LATTICE holds
( L is distributive iff L is Heyting )
proof end;

theorem Th37: :: WAYBEL_6:37
for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) holds
for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)
proof end;

Lm2: for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) holds
L is completely-distributive

proof end;

Lm3: for L being complete completely-distributive LATTICE holds
( L is distributive & L is continuous & L ~ is continuous )

proof end;

Lm4: for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds
for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )

proof end;

theorem :: WAYBEL_6:38
for L being complete LATTICE holds
( L is completely-distributive iff ( L is continuous & ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) ) )
proof end;

theorem :: WAYBEL_6:39
for L being complete LATTICE holds
( L is completely-distributive iff ( L is distributive & L is continuous & L opp is continuous ) )
proof end;