:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, TARSKI, ORDINAL1, SUBSET_1, LATTICES, CARD_FIL, FILTER_0, INT_2, PBOOLE, GROUP_6, FUNCT_1, STRUCT_0, EQREL_1, FUNCT_2, RELAT_1, WELLORD1, FILTER_1, XBOOLEAN, FINSUB_1, LATTICE2, SETWISEO, BINOP_1, FUNCOP_1, XXREAL_2, VECTSP_1, ZFMISC_1, SETFAM_1, LATTICE4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, LATTICES, LATTICE2, FILTER_0, FUNCOP_1, SETWISEO, WELLORD1, FILTER_1; constructors WELLORD1, DOMAIN_1, SETWISEO, LATTICE2, FILTER_1, GRCAT_1, FUNCOP_1, RELSET_1, FILTER_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE2; requirements BOOLE, SUBSET; begin :: Preliminaries reserve x,y,X,X1,Y,Z for set; theorem :: LATTICE4:1 for X st X <> {} & for Z st Z <> {} & Z c= X & Z is c=-linear ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z; begin :: Lattice Theory reserve L for Lattice; reserve F,H for Filter of L; reserve p,q,r for Element of L; registration let L; cluster <.L.) -> prime; end; theorem :: LATTICE4:2 F c= <.F \/ H.) & H c= <.F \/ H.); theorem :: LATTICE4:3 p in <.<.q.) \/ F.) implies ex r st r in F & q "/\" r [= p; reserve L1, L2 for Lattice; reserve a1,b1 for Element of L1; reserve a2 for Element of L2; definition let L1,L2 be non empty \/-SemiLattStr; let f be Function of L1,L2; attr f is "\/"-preserving means :: LATTICE4:def 1 for a,b being Element of L1 holds f.(a"\/"b) = f.a "\/" f.b; end; definition let L1,L2 be non empty /\-SemiLattStr; let f be Function of L1,L2; attr f is "/\"-preserving means :: LATTICE4:def 2 for a,b being Element of L1 holds f.(a"/\"b) = f.a "/\" f.b; end; registration let L1,L2 be meet-absorbing join-absorbing meet-commutative non empty LattStr; cluster "\/"-preserving "/\"-preserving for Function of L1,L2; end; definition let L1,L2 be Lattice; mode Homomorphism of L1,L2 is "\/"-preserving "/\"-preserving Function of L1,L2; end; reserve f for Homomorphism of L1,L2; theorem :: LATTICE4:4 a1 [= b1 implies f.a1 [= f.b1; theorem :: LATTICE4:5 f is one-to-one implies (a1 [= b1 iff (f.a1) [= (f.b1)); theorem :: LATTICE4:6 for f being Function of L1,L2 holds f is onto implies for a2 ex a1 st a2 = f.a1; definition let L1,L2; redefine pred L1,L2 are_isomorphic means :: LATTICE4:def 3 ex f st f is bijective; end; definition let L1,L2,f; pred f preserves_implication means :: LATTICE4:def 4 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 f.(a1`) = (f.a1)`; end; definition let L; mode ClosedSubset of L is meet-closed join-closed Subset of L; end; theorem :: LATTICE4:7 the carrier of L is ClosedSubset of L; registration let L; cluster non empty for ClosedSubset of L; end; theorem :: LATTICE4:8 for F being Filter of L holds F is ClosedSubset of L; reserve B for Element of Fin the carrier of L; definition let L,B; func FinJoin B -> Element of L equals :: LATTICE4:def 8 FinJoin (B,id L); func FinMeet B -> Element of L equals :: LATTICE4:def 9 FinMeet (B,id L); end; theorem :: LATTICE4:9 FinJoin {.p.} = p; theorem :: LATTICE4:10 FinMeet {.p.} = p; begin :: Distributive Lattices reserve DL for distributive Lattice; reserve f for Homomorphism of DL,L2; theorem :: LATTICE4:11 f is onto implies L2 is distributive; begin :: Lower-bounded Lattices reserve 0L for lower-bounded Lattice, B,B1,B2 for Element of Fin the carrier of 0L, b for Element of 0L; theorem :: LATTICE4:12 for f being Homomorphism of 0L,L2 st f is onto holds L2 is lower-bounded & f preserves_bottom; reserve f for UnOp of the carrier of 0L; theorem :: LATTICE4:13 FinJoin(B \/ {.b.},f) = FinJoin (B,f) "\/" f.b; theorem :: LATTICE4:14 FinJoin(B \/ {.b.}) = FinJoin B "\/" b; theorem :: LATTICE4:15 FinJoin B1 "\/" FinJoin B2 = FinJoin (B1 \/ B2); theorem :: LATTICE4:16 FinJoin {}.the carrier of 0L = Bottom 0L; theorem :: LATTICE4:17 for A being ClosedSubset of 0L st Bottom 0L in A for B holds B c= A implies FinJoin B in A; begin :: Upper-bounded Lattices reserve 1L for upper-bounded Lattice, B,B1,B2 for Element of Fin the carrier of 1L, b for Element of 1L; theorem :: LATTICE4:18 for f being Homomorphism of 1L,L2 st f is onto holds L2 is upper-bounded & f preserves_top; theorem :: LATTICE4:19 FinMeet {}.the carrier of 1L = Top 1L; reserve f,g for UnOp of the carrier of 1L; theorem :: LATTICE4:20 FinMeet(B \/ {.b.},f) = FinMeet (B,f) "/\" f.b; theorem :: LATTICE4:21 FinMeet(B \/ {.b.}) = FinMeet B "/\" b; theorem :: LATTICE4:22 FinMeet(f.:B,g) = FinMeet(B,g*f); theorem :: LATTICE4:23 FinMeet B1 "/\" FinMeet B2 = FinMeet (B1 \/ B2); theorem :: LATTICE4:24 for F being ClosedSubset of 1L st Top 1L in F for B holds B c= F implies FinMeet B in F; begin :: Distributive Upper-bounded Lattices reserve DL for distributive upper-bounded Lattice, B for Element of Fin the carrier of DL, p for Element of DL, f for UnOp of the carrier of DL; theorem :: LATTICE4:25 FinMeet B "\/" p = FinMeet (((the L_join of DL)[:](id DL,p)).:B); begin :: Implicative Lattices reserve CL for C_Lattice; reserve IL for implicative Lattice; reserve f for Homomorphism of IL,CL; reserve i,j,k for Element of IL; theorem :: LATTICE4:26 f.i "/\" f.(i => j) [= f.j; theorem :: LATTICE4:27 f is one-to-one implies (f.i "/\" f.k [= f.j implies f.k [= f.(i => j)); theorem :: LATTICE4:28 f is bijective implies CL is implicative & f preserves_implication; begin ::Boolean Lattices reserve BL for Boolean Lattice; reserve f for Homomorphism of BL,CL; reserve A for non empty Subset of BL; reserve a1,a,b,c,p,q for Element of BL; reserve B,B0,B1,B2,A1,A2 for Element of Fin the carrier of BL; theorem :: LATTICE4:29 (Top BL)`=Bottom BL; theorem :: LATTICE4:30 (Bottom BL)`=Top BL; theorem :: LATTICE4:31 f is onto implies CL is Boolean & f preserves_complement; definition let BL; mode Field of BL -> non empty Subset of BL means :: LATTICE4:def 10 a in it & b in it implies a "/\" b in it & a` in it; end; reserve F,H for Field of BL; theorem :: LATTICE4:32 a in F & b in F implies a "\/" b in F; theorem :: LATTICE4:33 a in F & b in F implies a => b in F; theorem :: LATTICE4:34 the carrier of BL is Field of BL; theorem :: LATTICE4:35 F is ClosedSubset of BL; definition let BL,A; func field_by A -> Field of BL means :: LATTICE4:def 11 A c= it & for F st A c= F holds it c= F; end; definition let BL,A; func SetImp A -> Subset of BL equals :: LATTICE4:def 12 { a => b : a in A & b in A}; end; registration let BL,A; cluster SetImp A -> non empty; end; theorem :: LATTICE4:36 x in SetImp A iff ex p,q st x = p => q & p in A & q in A; theorem :: LATTICE4:37 c in SetImp A iff ex p,q st c = p` "\/" q & p in A & q in A; definition let BL; func comp BL -> Function of the carrier of BL, the carrier of BL means :: LATTICE4:def 13 it.a = a`; end; theorem :: LATTICE4:38 FinJoin(B \/ {.b.},comp BL) = FinJoin (B,comp BL) "\/" b`; theorem :: LATTICE4:39 (FinJoin B)` = FinMeet (B,comp BL); theorem :: LATTICE4:40 FinMeet(B \/ {.b.},comp BL) = FinMeet (B,comp BL) "/\" b`; theorem :: LATTICE4:41 (FinMeet B)` = FinJoin (B,comp BL); theorem :: LATTICE4:42 for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF for B holds B c= SetImp AF implies ex B0 st B0 c= SetImp AF & FinJoin( B,comp BL) = FinMeet B0; theorem :: LATTICE4:43 for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds { FinMeet B : B c= SetImp AF } = field_by AF;