:: Representation theorem for free continuous lattices :: by Piotr Rudnicki :: :: Received July 21, 1998 :: Copyright (c) 1998-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 REWRITE1, WAYBEL_0, TARSKI, ZFMISC_1, STRUCT_0, LATTICES, ORDINAL2, SUBSET_1, EQREL_1, XBOOLE_0, YELLOW_1, ARYTM_0, ORDERS_2, WAYBEL16, RELAT_1, YELLOW_0, LATTICE3, WAYBEL_5, WELLORD2, CARD_FIL, WELLORD1, CAT_1, SETFAM_1, XXREAL_0, FUNCT_1, CARD_1, SEQM_3, PBOOLE, FUNCOP_1, YELLOW_2, CARD_3, FUNCT_6, WAYBEL22, FUNCT_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_6, ORDERS_1, STRUCT_0, WELLORD1, CARD_1, CARD_3, ORDERS_2, LATTICE3, FUNCOP_1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL16; constructors DOMAIN_1, TOLER_1, ORDERS_3, PRALG_3, WAYBEL_5, WAYBEL_8, WAYBEL16, RELSET_1, WAYBEL20; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_5, YELLOW_7, WAYBEL_8, WAYBEL16, FUNCT_1, RELAT_1; requirements SUBSET, BOOLE; begin theorem :: WAYBEL22:1 :: cf. WAYBEL13:9 for L being upper-bounded Semilattice, F being non empty directed Subset of InclPoset Filt L holds sup F = union F; theorem :: WAYBEL22:2 for L, S, T being complete non empty Poset, f being CLHomomorphism of L, S, g being CLHomomorphism of S, T holds g*f is CLHomomorphism of L, T; theorem :: WAYBEL22:3 for L being non empty RelStr holds id L is infs-preserving; theorem :: WAYBEL22:4 for L being non empty RelStr holds id L is directed-sups-preserving; theorem :: WAYBEL22:5 for L being complete non empty Poset holds id L is CLHomomorphism of L, L; theorem :: WAYBEL22:6 for L being upper-bounded with_infima non empty Poset holds InclPoset Filt L is CLSubFrame of BoolePoset the carrier of L; registration let L be upper-bounded with_infima non empty Poset; cluster InclPoset Filt L -> continuous; end; registration let L be upper-bounded non empty Poset; cluster -> non empty for Element of InclPoset Filt L; end; begin :: Free generators of continuous lattices definition let S be continuous complete non empty Poset; let A be set; pred A is_FreeGen_set_of S means :: WAYBEL22:def 1 for T be continuous complete non empty Poset for f be Function of A, the carrier of T ex h be CLHomomorphism of S, T st h|A = f & for h9 being CLHomomorphism of S,T st h9|A = f holds h9 = h; end; theorem :: WAYBEL22:7 for S being continuous complete non empty Poset, A being set st A is_FreeGen_set_of S holds A is Subset of S; theorem :: WAYBEL22:8 for S being continuous complete non empty Poset, A being set st A is_FreeGen_set_of S for h9 being CLHomomorphism of S, S st h9|A = id A holds h9 = id S; begin :: Representation theorem for free continuous lattices reserve X for set, F for Filter of BoolePoset X, x for Element of BoolePoset X , z for Element of X; definition :: See proof of Theorem 4.17, p. 90 let X; func FixedUltraFilters X -> Subset-Family of BoolePoset X equals :: WAYBEL22:def 2 { uparrow x : ex z st x = {z} }; end; theorem :: WAYBEL22:9 FixedUltraFilters X c= Filt BoolePoset X; theorem :: WAYBEL22:10 card FixedUltraFilters X = card X; theorem :: WAYBEL22:11 F = "\/"({"/\"({uparrow x : ex z st x = {z} & z in Y}, InclPoset Filt BoolePoset X) where Y is Subset of X : Y in F}, InclPoset Filt BoolePoset X); definition :: See proof of Theorem 4.17, p. 90 let X; let L be continuous complete non empty Poset; let f be Function of FixedUltraFilters X, the carrier of L; func f-extension_to_hom -> Function of InclPoset Filt BoolePoset X, L means :: WAYBEL22:def 3 for Fi being Element of InclPoset Filt BoolePoset X holds it.Fi = "\/"({ "/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is Subset of X : Y in Fi }, L); end; theorem :: WAYBEL22:12 for L being continuous complete non empty Poset, f being Function of FixedUltraFilters X, the carrier of L holds f-extension_to_hom is monotone; theorem :: WAYBEL22:13 for L being continuous complete non empty Poset, f being Function of FixedUltraFilters X, the carrier of L holds (f-extension_to_hom). Top (InclPoset Filt BoolePoset X) = Top L; registration :: See proof of Theorem 4.17, p. 91 let X; let L be continuous complete non empty Poset, f be Function of FixedUltraFilters X, the carrier of L; cluster f-extension_to_hom -> directed-sups-preserving; end; registration :: See proof of Theorem 4.17, p. 91 let X; let L be continuous complete non empty Poset, f be Function of FixedUltraFilters X, the carrier of L; cluster f-extension_to_hom -> infs-preserving; end; theorem :: WAYBEL22:14 for L being continuous complete non empty Poset, f being Function of FixedUltraFilters X, the carrier of L holds f-extension_to_hom | FixedUltraFilters X = f; theorem :: WAYBEL22:15 for L being continuous complete non empty Poset, f being Function of FixedUltraFilters X, the carrier of L, h being CLHomomorphism of InclPoset Filt BoolePoset X, L st h | FixedUltraFilters X = f holds h = f -extension_to_hom; theorem :: WAYBEL22:16 FixedUltraFilters X is_FreeGen_set_of InclPoset Filt BoolePoset X; theorem :: WAYBEL22:17 for L, M being continuous complete LATTICE, F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds L, M are_isomorphic; ::$N Representation Theorem for Free Continuous Lattices theorem :: WAYBEL22:18 :: Theorem 4.17, p. 90-91 for L being continuous complete LATTICE, G being set st G is_FreeGen_set_of L & card G = card X holds L, InclPoset Filt BoolePoset X are_isomorphic;