:: Homomorphisms of Lattices \\ Finite Join and Finite Meet
:: by Jolanta Kamie\'nska and Jaros\l aw Stanis\l aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

theorem :: LATTICE4:1
for X being set st X <> {} &amp; ( for Z being set st Z <> {} &amp; Z c= X &amp; Z is c=-linear holds
ex Y being set st
( Y in X &amp; ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ) holds
ex Y being set st
( Y in X &amp; ( for Z being set st Z in X &amp; Z <> Y holds
not Y c= Z ) )
proofend;

begin

registration
let L be Lattice;
cluster<.L.) ->  prime ;
coherence
 <.L.) is prime
proofend;
end;

theorem :: LATTICE4:2
for L being Lattice
for F, H being Filter of L holds
( F c= <.(F \/ H).) &amp; H c= <.(F \/ H).) )
proofend;

theorem :: LATTICE4:3
for L being Lattice
for F being Filter of L
for p, q being Element of L st p in <.(<.q.) \/ F).) holds
ex r being Element of L st
( r in F &amp; q "/\" r [= p )
proofend;

definition
let L1, L2 be Lattice;
mode Homomorphism of L1,L2 ->  Function of the carrier of L1, the carrier of L2 means :Def1: :: LATTICE4:def 1
 for a1, b1 being Element of L1 holds
( it . (a1 "\/" b1) = (it . a1) "\/" (it . b1) &amp; it . (a1 "/\" b1) = (it . a1) "/\" (it . b1) );
existence
 ex b1 being Function of the carrier of L1, the carrier of L2 st
for a1, b1 being Element of L1 holds
( b1 . (a1 "\/" b1) = (b1 . a1) "\/" (b1 . b1) &amp; b1 . (a1 "/\" b1) = (b1 . a1) "/\" (b1 . b1) )
proofend;
end;

:: deftheorem Def1 defines Homomorphism LATTICE4:def_1_:_
 for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is Homomorphism of L1,L2 iff for a1, b1 being Element of L1 holds
( b3 . (a1 "\/" b1) = (b3 . a1) "\/" (b3 . b1) &amp; b3 . (a1 "/\" b1) = (b3 . a1) "/\" (b3 . b1) ) );

theorem Th4: :: LATTICE4:4
for L1, L2 being Lattice
for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st a1 [= b1 holds
f . a1 [= f . b1
proofend;

theorem Th5: :: LATTICE4:5
for L1, L2 being Lattice
for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st f is one-to-one holds
( a1 [= b1 iff f . a1 [= f . b1 )
proofend;

theorem Th6: :: LATTICE4:6
for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 st f is onto holds
for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
proofend;

definition
let L1, L2 be Lattice;
redefine pred L1,L2 are_isomorphic  means :: LATTICE4:def 2
 ex f being Homomorphism of L1,L2 st f is bijective ;
compatibility
 ( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective )
proofend;
end;

:: deftheorem  defines are_isomorphic LATTICE4:def_2_:_
 for L1, L2 being Lattice holds
( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective );

definition
let L1, L2 be Lattice;
let f be Homomorphism of L1,L2;
predf preserves_implication  means :Def3: :: LATTICE4:def 3
 for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1);
predf preserves_top  means :Def4: :: LATTICE4:def 4
f . (Top L1) = Top L2;
predf preserves_bottom  means :Def5: :: LATTICE4:def 5
f . (Bottom L1) = Bottom L2;
predf preserves_complement  means :Def6: :: LATTICE4:def 6
 for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` ;
end;

:: deftheorem Def3 defines preserves_implication LATTICE4:def_3_:_
 for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_implication iff for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1) );

:: deftheorem Def4 defines preserves_top LATTICE4:def_4_:_
 for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_top iff f . (Top L1) = Top L2 );

:: deftheorem Def5 defines preserves_bottom LATTICE4:def_5_:_
 for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_bottom iff f . (Bottom L1) = Bottom L2 );

:: deftheorem Def6 defines preserves_complement LATTICE4:def_6_:_
 for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_complement iff for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` );

definition
let L be Lattice;
mode ClosedSubset of L is meet-closed join-closed Subset of L;
end;

theorem Th7: :: LATTICE4:7
for L being Lattice holds the carrier of L is ClosedSubset of L
proofend;

registration
let L be Lattice;
cluster non empty meet-closed join-closed for Element of bool the carrier of L;
existence
 not for b1 being ClosedSubset of L holds b1 is empty
proofend;
end;

theorem :: LATTICE4:8
for L being Lattice
for F being Filter of L holds F is ClosedSubset of L ;

definition
let L be Lattice;
let B be Finite_Subset of the carrier of L;
func FinJoin B ->  Element of L equals :: LATTICE4:def 7
 FinJoin (B,(id L));
coherence
 FinJoin (B,(id L)) is Element of L ;
func FinMeet B ->  Element of L equals :: LATTICE4:def 8
 FinMeet (B,(id L));
coherence
 FinMeet (B,(id L)) is Element of L ;
end;

:: deftheorem  defines FinJoin LATTICE4:def_7_:_
 for L being Lattice
for B being Finite_Subset of the carrier of L holds FinJoin B = FinJoin (B,(id L));

:: deftheorem  defines FinMeet LATTICE4:def_8_:_
 for L being Lattice
for B being Finite_Subset of the carrier of L holds FinMeet B = FinMeet (B,(id L));

theorem Th9: :: LATTICE4:9
for L being Lattice
for p being Element of L holds FinJoin {.p.} = p
proofend;

theorem Th10: :: LATTICE4:10
for L being Lattice
for p being Element of L holds FinMeet {.p.} = p
proofend;

begin

theorem Th11: :: LATTICE4:11
for L2 being Lattice
for DL being distributive Lattice
for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
proofend;

begin

theorem Th12: :: LATTICE4:12
for L2 being Lattice
for 0L being lower-bounded Lattice
for f being Homomorphism of 0L,L2 st f is onto holds
( L2 is lower-bounded &amp; f preserves_bottom )
proofend;

theorem Th13: :: LATTICE4:13
for 0L being lower-bounded Lattice
for B being Finite_Subset of the carrier of 0L
for b being Element of 0L
for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)
proofend;

theorem Th14: :: LATTICE4:14
for 0L being lower-bounded Lattice
for B being Finite_Subset of the carrier of 0L
for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
proofend;

theorem :: LATTICE4:15
for 0L being lower-bounded Lattice
for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)
proofend;

Lm1:  for 0L being lower-bounded Lattice
for f being Function of the carrier of 0L, the carrier of 0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L
proofend;

theorem :: LATTICE4:16
for 0L being lower-bounded Lattice holds FinJoin ({}. the carrier of 0L) = Bottom 0L by Lm1;

theorem Th17: :: LATTICE4:17
for 0L being lower-bounded Lattice
for A being ClosedSubset of 0L st Bottom 0L in A holds
for B being Finite_Subset of the carrier of 0L st B c= A holds
FinJoin B in A
proofend;

begin

theorem Th18: :: LATTICE4:18
for L2 being Lattice
for 1L being upper-bounded Lattice
for f being Homomorphism of 1L,L2 st f is onto holds
( L2 is upper-bounded &amp; f preserves_top )
proofend;

Lm2:  for 1L being upper-bounded Lattice
for f being Function of the carrier of 1L, the carrier of 1L holds FinMeet (({}. the carrier of 1L),f) = Top 1L
proofend;

theorem :: LATTICE4:19
for 1L being upper-bounded Lattice holds FinMeet ({}. the carrier of 1L) = Top 1L by Lm2;

theorem Th20: :: LATTICE4:20
for 1L being upper-bounded Lattice
for B being Finite_Subset of the carrier of 1L
for b being Element of 1L
for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)
proofend;

theorem Th21: :: LATTICE4:21
for 1L being upper-bounded Lattice
for B being Finite_Subset of the carrier of 1L
for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b
proofend;

theorem Th22: :: LATTICE4:22
for 1L being upper-bounded Lattice
for B being Finite_Subset of the carrier of 1L
for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))
proofend;

theorem Th23: :: LATTICE4:23
for 1L being upper-bounded Lattice
for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
proofend;

theorem Th24: :: LATTICE4:24
for 1L being upper-bounded Lattice
for F being ClosedSubset of 1L st Top 1L in F holds
for B being Finite_Subset of the carrier of 1L st B c= F holds
FinMeet B in F
proofend;

begin

Lm3:  for DL being distributive upper-bounded Lattice
for B being Finite_Subset of the carrier of DL
for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))
proofend;

theorem Th25: :: LATTICE4:25
for DL being distributive upper-bounded Lattice
for B being Finite_Subset of the carrier of DL
for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)
proofend;

begin

theorem Th26: :: LATTICE4:26
for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j
proofend;

theorem Th27: :: LATTICE4:27
for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, k, j being Element of IL st f is one-to-one &amp; (f . i) "/\" (f . k) [= f . j holds
f . k [= f . (i => j)
proofend;

theorem :: LATTICE4:28
for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative &amp; f preserves_implication )
proofend;

begin

theorem Th29: :: LATTICE4:29
for BL being Boolean Lattice holds (Top BL) ` = Bottom BL
proofend;

theorem Th30: :: LATTICE4:30
for BL being Boolean Lattice holds (Bottom BL) ` = Top BL
proofend;

theorem :: LATTICE4:31
for CL being C_Lattice
for BL being Boolean Lattice
for f being Homomorphism of BL,CL st f is onto holds
( CL is Boolean &amp; f preserves_complement )
proofend;

definition
let BL be Boolean Lattice;
mode Field of BL ->  non empty Subset of BL means :Def9: :: LATTICE4:def 9
 for a, b being Element of BL st a in it &amp; b in it holds
( a "/\" b in it &amp; a ` in it );
existence
 ex b1 being non empty Subset of BL st
for a, b being Element of BL st a in b1 &amp; b in b1 holds
( a "/\" b in b1 &amp; a ` in b1 )
proofend;
end;

:: deftheorem Def9 defines Field LATTICE4:def_9_:_
 for BL being Boolean Lattice
for b2 being non empty Subset of BL holds
( b2 is Field of BL iff for a, b being Element of BL st a in b2 &amp; b in b2 holds
( a "/\" b in b2 &amp; a ` in b2 ) );

theorem Th32: :: LATTICE4:32
for BL being Boolean Lattice
for a, b being Element of BL
for F being Field of BL st a in F &amp; b in F holds
a "\/" b in F
proofend;

theorem Th33: :: LATTICE4:33
for BL being Boolean Lattice
for a, b being Element of BL
for F being Field of BL st a in F &amp; b in F holds
a => b in F
proofend;

theorem Th34: :: LATTICE4:34
for BL being Boolean Lattice holds the carrier of BL is Field of BL
proofend;

theorem Th35: :: LATTICE4:35
for BL being Boolean Lattice
for F being Field of BL holds F is ClosedSubset of BL
proofend;

definition
let BL be Boolean Lattice;
let A be non empty Subset of BL;
func field_by A ->  Field of BL means :Def10: :: LATTICE4:def 10
( A c= it &amp; ( for F being Field of BL st A c= F holds
it c= F ) );
existence
 ex b1 being Field of BL st
( A c= b1 &amp; ( for F being Field of BL st A c= F holds
b1 c= F ) )
proofend;
uniqueness
 for b1, b2 being Field of BL st A c= b1 &amp; ( for F being Field of BL st A c= F holds
b1 c= F ) &amp; A c= b2 &amp; ( for F being Field of BL st A c= F holds
b2 c= F ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines field_by LATTICE4:def_10_:_
 for BL being Boolean Lattice
for A being non empty Subset of BL
for b3 being Field of BL holds
( b3 = field_by A iff ( A c= b3 &amp; ( for F being Field of BL st A c= F holds
b3 c= F ) ) );

definition
let BL be Boolean Lattice;
let A be non empty Subset of BL;
func SetImp A ->  Subset of BL equals :: LATTICE4:def 11
 {  (a => b) where a, b is Element of BL : ( a in A &amp; b in A )  }  ;
coherence
  {  (a => b) where a, b is Element of BL : ( a in A &amp; b in A )  }  is Subset of BL
proofend;
end;

:: deftheorem  defines SetImp LATTICE4:def_11_:_
 for BL being Boolean Lattice
for A being non empty Subset of BL holds SetImp A =  {  (a => b) where a, b is Element of BL : ( a in A &amp; b in A )  }  ;

registration
let BL be Boolean Lattice;
let A be non empty Subset of BL;
cluster SetImp A ->  non empty ;
coherence
 not SetImp A is empty
proofend;
end;

theorem :: LATTICE4:36
for x being set
for BL being Boolean Lattice
for A being non empty Subset of BL holds
( x in SetImp A iff ex p, q being Element of BL st
( x = p => q &amp; p in A &amp; q in A ) ) ;

theorem Th37: :: LATTICE4:37
for BL being Boolean Lattice
for A being non empty Subset of BL
for c being Element of BL holds
( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q &amp; p in A &amp; q in A ) )
proofend;

definition
let BL be Boolean Lattice;
deffunc H1( Element of BL) ->  Element of the carrier of BL = $1 ` ;
func comp BL ->  Function of the carrier of BL, the carrier of BL means :Def12: :: LATTICE4:def 12
 for a being Element of BL holds it . a = a ` ;
existence
 ex b1 being Function of the carrier of BL, the carrier of BL st
for a being Element of BL holds b1 . a = a `
proofend;
uniqueness
 for b1, b2 being Function of the carrier of BL, the carrier of BL st ( for a being Element of BL holds b1 . a = a ` ) &amp; ( for a being Element of BL holds b2 . a = a ` ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines comp LATTICE4:def_12_:_
 for BL being Boolean Lattice
for b2 being Function of the carrier of BL, the carrier of BL holds
( b2 = comp BL iff for a being Element of BL holds b2 . a = a ` );

theorem Th38: :: LATTICE4:38
for BL being Boolean Lattice
for b being Element of BL
for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)
proofend;

theorem :: LATTICE4:39
for BL being Boolean Lattice
for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))
proofend;

theorem :: LATTICE4:40
for BL being Boolean Lattice
for b being Element of BL
for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)
proofend;

theorem Th41: :: LATTICE4:41
for BL being Boolean Lattice
for B being Finite_Subset of the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL))
proofend;

theorem Th42: :: LATTICE4:42
for BL being Boolean Lattice
for AF being non empty ClosedSubset of BL st Bottom BL in AF &amp; Top BL in AF holds
for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF &amp; FinJoin (B,(comp BL)) = FinMeet B0 )
proofend;

theorem :: LATTICE4:43
for BL being Boolean Lattice
for AF being non empty ClosedSubset of BL st Bottom BL in AF &amp; Top BL in AF holds
{  (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF  }  = field_by AF
proofend;