:: 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 b₁ being Function of L1,L2 st
( b₁ is "\/"-preserving & b₁ 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 b₁ being ClosedSubset of L holds b₁ 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 b₁ being non empty Subset of BL st
for a, b being Element of BL st a in b₁ & b in b₁ holds
( a "/\" b in b₁ & a ` in b₁ )

proof end;

end;

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

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 b₁ being Field of BL st
( A c= b₁ & ( for F being Field of BL st A c= F holds
b₁ c= F ) )

proof end;

uniqueness
for b₁, b₂ being Field of BL st A c= b₁ & ( for F being Field of BL st A c= F holds
b₁ c= F ) & A c= b₂ & ( for F being Field of BL st A c= F holds
b₂ c= F ) holds
b₁ = b₂

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 b₃ being Field of BL holds
( b₃ = field_by A iff ( A c= b₃ & ( for F being Field of BL st A c= F holds
b₃ 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 H₁( 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 b₁ being Function of the carrier of BL, the carrier of BL st
for a being Element of BL holds b₁ . a = a `

proof end;

uniqueness
for b₁, b₂ being Function of the carrier of BL, the carrier of BL st ( for a being Element of BL holds b₁ . a = a ` ) & ( for a being Element of BL holds b<sub>2</sub> . a = a ` ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines comp LATTICE4:def 13 :
for BL being Boolean Lattice
for b₂ being Function of the carrier of BL, the carrier of BL holds
( b₂ = comp BL iff for a being Element of BL holds b₂ . 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;