WAYBEL_6: Irreducible and Prime Elements

:: 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{ F₁() -> non empty RelStr , F₂() -> Subset of F₁(), F₃() -> non empty Subset of F₁(), P₁[ set , set ] } :

ex f being Function of F₂(),F₃() st
for e being Element of F₁() st e in F₂() holds
ex u being Element of F₁() st
( u in F₃() & u = f . e & P₁[e,u] )

provided

A1: for e being Element of F₁() st e in F₂() holds
ex u being Element of F₁() st
( u in F₃() & P₁[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 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

proof end;

end;

registration

let L be non empty Poset;

cluster strongly_connected -> directed filtered for Element of bool the carrier of L;

coherence

proof end;

end;

registration

cluster non empty strict V110() reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous for RelStr ;

existence

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

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 :

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

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 :

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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines IRR WAYBEL_6:def 4 :

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

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 :

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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines PRIME WAYBEL_6:def 7 :

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 :

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

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;