:: 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-2021 Association of Mizar Users


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

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

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

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 & q "/\" r [= p )
proof end;

definition
let L1, L2 be non empty \/-SemiLattStr ;
let f be Function of L1,L2;
attr f is "\/"-preserving means :D1: :: LATTICE4:def 1
 for a, b being Element of L1 holds f . (a "\/" b) = (f . a) "\/" (f . b);
end;

:: deftheorem D1 defines "\/"-preserving LATTICE4:def 1 :
for L1, L2 being non empty \/-SemiLattStr
for f being Function of L1,L2 holds
( f is "\/"-preserving iff for a, b being Element of L1 holds f . (a "\/" b) = (f . a) "\/" (f . b) );

definition
let L1, L2 be non empty /\-SemiLattStr ;
let f be Function of L1,L2;
attr f is "/\"-preserving means :D2: :: LATTICE4:def 2
 for a, b being Element of L1 holds f . (a "/\" b) = (f . a) "/\" (f . b);
end;

:: deftheorem D2 defines "/\"-preserving LATTICE4:def 2 :
for L1, L2 being non empty /\-SemiLattStr
for f being Function of L1,L2 holds
( f is "/\"-preserving iff for a, b being Element of L1 holds f . (a "/\" b) = (f . a) "/\" (f . b) );

registration
let L1, L2 be non empty meet-commutative meet-absorbing join-absorbing LattStr ;
cluster Relation-like the carrier of L1 -defined the carrier of L2 -valued Function-like non empty V19( the carrier of L1) quasi_total "\/"-preserving "/\"-preserving for Element of bool [: the carrier of L1, the carrier of L2:];
existence
ex b1 being Function of L1,L2 st
( b1 is "\/"-preserving & b1 is "/\"-preserving )
proof end;
end;

definition
let L1, L2 be Lattice;
mode Homomorphism of L1,L2 is "\/"-preserving "/\"-preserving Function of L1,L2;
end;

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 by D1;

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 )
proof end;

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

definition
let L1, L2 be Lattice;
redefine pred L1,L2 are_isomorphic means :: LATTICE4:def 3
 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 )
proof end;
end;

:: deftheorem defines are_isomorphic LATTICE4:def 3 :
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;
pred f preserves_implication means :: LATTICE4:def 4
 for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1);
pred f preserves_top means :: LATTICE4:def 5
f . (Top L1) = Top L2;
pred f preserves_bottom means :: LATTICE4:def 6
f . (Bottom L1) = Bottom L2;
pred f preserves_complement means :: LATTICE4:def 7
 for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` ;
end;

:: deftheorem defines preserves_implication LATTICE4:def 4 :
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 defines preserves_top LATTICE4:def 5 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_top iff f . (Top L1) = Top L2 );

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

:: deftheorem defines preserves_complement LATTICE4:def 7 :
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
proof end;

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
proof end;
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 Element of Fin the carrier of L;
func FinJoin B -> Element of L equals :: LATTICE4:def 8
 FinJoin (B,(id L));
coherence
FinJoin (B,(id L)) is Element of L ;
func FinMeet B -> Element of L equals :: LATTICE4:def 9
 FinMeet (B,(id L));
coherence
FinMeet (B,(id L)) is Element of L ;
end;

:: deftheorem defines FinJoin LATTICE4:def 8 :
for L being Lattice
for B being Element of Fin the carrier of L holds FinJoin B = FinJoin (B,(id L));

:: deftheorem defines FinMeet LATTICE4:def 9 :
for L being Lattice
for B being Element of Fin 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
proof end;

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

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
proof end;

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 & f preserves_bottom )
proof end;

theorem Th13: :: LATTICE4:13
for 0L being lower-bounded Lattice
for B being Element of Fin 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)
proof end;

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

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

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

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 Element of Fin the carrier of 0L st B c= A holds
FinJoin B in A
proof end;

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 & f preserves_top )
proof end;

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
proof end;

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 Element of Fin 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)
proof end;

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

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

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

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 Element of Fin the carrier of 1L st B c= F holds
FinMeet B in F
proof end;

Lm3: for DL being distributive upper-bounded Lattice
for B being Element of Fin 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)))
proof end;

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

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
proof end;

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

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 & f preserves_implication )
proof end;

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

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

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 & f preserves_complement )
proof end;

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

:: deftheorem Def9 defines Field LATTICE4:def 10 :
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 & b in b2 holds
( a "/\" b in b2 & 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 & b in F holds
a "\/" b in F
proof end;

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 & b in F holds
a => b in F
proof end;

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

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

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 11
( A c= it & ( 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 & ( for F being Field of BL st A c= F holds
b1 c= F ) )
proof end;
uniqueness
for b1, b2 being Field of BL st A c= b1 & ( for F being Field of BL st A c= F holds
b1 c= F ) & A c= b2 & ( for F being Field of BL st A c= F holds
b2 c= F ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines field_by LATTICE4:def 11 :
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 & ( 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 12
 { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
coherence
{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL
proof end;
end;

:: deftheorem defines SetImp LATTICE4:def 12 :
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 & 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
proof end;
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 & p in A & 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 & p in A & q in A ) )
proof end;

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 13
 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 `
proof end;
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 ` ) & ( for a being Element of BL holds b2 . a = a ` ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines comp LATTICE4:def 13 :
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 Element of Fin the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)
proof end;

theorem :: LATTICE4:39
for BL being Boolean Lattice
for B being Element of Fin the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))
proof end;

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

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

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

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