:: Representation theorem for free continuous lattices
:: by Piotr Rudnicki
::
:: Received July 21, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

Lm1:  for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"/\" ((union X),L) = "/\" ( {  (inf Y) where Y is Subset of L : Y in X  }  ,L)
proofend;

Lm2:  for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"\/" ((union X),L) = "\/" ( {  (sup Y) where Y is Subset of L : Y in X  }  ,L)
proofend;

theorem Th1: :: WAYBEL22:1
for L being upper-bounded Semilattice
for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F
proofend;

theorem Th2: :: WAYBEL22:2
for L, S, T being non empty complete Poset
for f being CLHomomorphism of L,S
for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
proofend;

theorem Th3: :: WAYBEL22:3
for L being non empty RelStr holds id L is infs-preserving
proofend;

theorem Th4: :: WAYBEL22:4
for L being non empty RelStr holds id L is directed-sups-preserving
proofend;

theorem Th5: :: WAYBEL22:5
for L being non empty complete Poset holds id L is CLHomomorphism of L,L
proofend;

theorem Th6: :: WAYBEL22:6
for L being non empty upper-bounded with_infima Poset holds InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
proofend;

registration
let L be non empty upper-bounded with_infima Poset;
cluster InclPoset (Filt L) ->  continuous ;
coherence
 InclPoset (Filt L) is continuous
proofend;
end;

registration
let L be non empty upper-bounded Poset;
cluster  ->  non empty for Element of the carrier of (InclPoset (Filt L));
coherence
 for b1 being Element of (InclPoset (Filt L)) holds not b1 is empty
proofend;
end;

begin

definition
let S be non empty complete continuous Poset;
let A be set ;
predA is_FreeGen_set_of S means :Def1: :: WAYBEL22:def 1
 for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) );
end;

:: deftheorem Def1 defines is_FreeGen_set_of WAYBEL22:def_1_:_
 for S being non empty complete continuous Poset
for A being set holds
( A is_FreeGen_set_of S iff for T being non empty complete continuous Poset
for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) ) );

theorem Th7: :: WAYBEL22:7
for S being non empty complete continuous Poset
for A being set st A is_FreeGen_set_of S holds
A is Subset of S
proofend;

theorem Th8: :: WAYBEL22:8
for S being non empty complete continuous Poset
for A being set st A is_FreeGen_set_of S holds
for h9 being CLHomomorphism of S,S st h9 | A = id A holds
h9 = id S
proofend;

begin

definition
let X be set ;
func FixedUltraFilters X ->  Subset-Family of (BoolePoset X) equals :: WAYBEL22:def 2
 {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  ;
coherence
  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  is Subset-Family of (BoolePoset X)
proofend;
end;

:: deftheorem  defines FixedUltraFilters WAYBEL22:def_2_:_
 for X being set holds FixedUltraFilters X =  {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z}  }  ;

theorem Th9: :: WAYBEL22:9
for X being set holds FixedUltraFilters X c= Filt (BoolePoset X)
proofend;

theorem Th10: :: WAYBEL22:10
for X being set holds card (FixedUltraFilters X) = card X
proofend;

theorem Th11: :: WAYBEL22:11
for X being set
for F being Filter of (BoolePoset X) holds F = "\/" ( {  ("/\" ( {  (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F  }  ,(InclPoset (Filt (BoolePoset X))))
proofend;

definition
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
funcf -extension_to_hom  ->  Function of (InclPoset (Filt (BoolePoset X))),L means :Def3: :: WAYBEL22:def 3
 for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L);
existence
 ex b1 being Function of (InclPoset (Filt (BoolePoset X))),L st
for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L)
proofend;
uniqueness
 for b1, b2 being Function of (InclPoset (Filt (BoolePoset X))),L st ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b2 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines -extension_to_hom WAYBEL22:def_3_:_
 for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for b4 being Function of (InclPoset (Filt (BoolePoset X))),L holds
( b4 = f -extension_to_hom iff for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b4 . Fi = "\/" ( {  ("/\" ( {  (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y )  }  ,L)) where Y is Subset of X : Y in Fi  }  ,L) );

theorem :: WAYBEL22:12
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds f -extension_to_hom is monotone
proofend;

theorem Th13: :: WAYBEL22:13
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) . (Top (InclPoset (Filt (BoolePoset X)))) = Top L
proofend;

registration
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
clusterf -extension_to_hom  ->  directed-sups-preserving ;
coherence
 f -extension_to_hom is directed-sups-preserving
proofend;
end;

registration
let X be set ;
let L be non empty complete continuous Poset;
let f be Function of (FixedUltraFilters X), the carrier of L;
clusterf -extension_to_hom  ->  infs-preserving ;
coherence
 f -extension_to_hom is infs-preserving
proofend;
end;

theorem Th14: :: WAYBEL22:14
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
proofend;

theorem Th15: :: WAYBEL22:15
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L
for h being CLHomomorphism of InclPoset (Filt (BoolePoset X)),L st h | (FixedUltraFilters X) = f holds
h = f -extension_to_hom
proofend;

theorem Th16: :: WAYBEL22:16
for X being set holds FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))
proofend;

theorem Th17: :: WAYBEL22:17
for L, M being complete continuous LATTICE
for 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
proofend;

:: [WP: ] Representation_Theorem_for_Free_Continuous_Lattices
theorem :: WAYBEL22:18
for X being set
for L being complete continuous LATTICE
for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
proofend;