The abstract of the Mizar article:

Algebraic Lattices

by

Robert Milewski

Received December 1, 1996

MML identifier: WAYBEL_8

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_2, ORDERS_1, CAT_1, YELLOW_0, COMPTS_1, WELLORD1, LATTICES,
      BHSP_3, WAYBEL_0, WAYBEL_3, WAYBEL_6, FILTER_0, LATTICE3, ORDINAL2,
      BOOLE, QUANTAL1, FINSET_1, REALSET1, WAYBEL_4, COHSP_1, WAYBEL_7,
      WAYBEL_1, PRE_TOPC, GROUP_6, RELAT_1, SUBSET_1, BINOP_1, SEQM_3, FUNCT_1,
      YELLOW_1, FILTER_1, SETFAM_1, TARSKI, WAYBEL_8;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FINSET_1, RELAT_1,
      REALSET1, STRUCT_0, ORDERS_1, TOLER_1, FUNCT_1, LATTICE3, PRE_TOPC,
      QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3,
      WAYBEL_4, WAYBEL_6, WAYBEL_7, GRCAT_1;
 constructors TOLER_1, ORDERS_3, QUANTAL1, YELLOW_3, WAYBEL_1, WAYBEL_3,
      WAYBEL_4, WAYBEL_6, WAYBEL_7, GRCAT_1;
 clusters STRUCT_0, RELSET_1, FINSET_1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_0,
      WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: The Subset of All Compact Elements

  definition  :: DEFINITION 4.1
   let L be non empty reflexive RelStr;
   func CompactSublatt L -> strict full SubRelStr of L means
:: WAYBEL_8:def 1
    for x be Element of L holds x in the carrier of it iff x is compact;
  end;

  definition
   let L be lower-bounded non empty reflexive antisymmetric RelStr;
   cluster CompactSublatt L -> non empty;
  end;

  theorem :: WAYBEL_8:1
     for L be complete LATTICE
   for x,y,k be Element of L holds
    x <= k & k <= y & k in the carrier of CompactSublatt L implies x << y;

  theorem :: WAYBEL_8:2  :: REMARK 4.2
     for L be complete LATTICE
   for x be Element of L holds
    uparrow x is Open Filter of L iff x is compact;

  theorem :: WAYBEL_8:3  :: REMARK 4.3
     for L be lower-bounded with_suprema non empty Poset holds
    CompactSublatt L is join-inheriting &
     Bottom L in the carrier of CompactSublatt L;

  definition
   let L be non empty reflexive RelStr;
   let x be Element of L;
   func compactbelow x -> Subset of L equals
:: WAYBEL_8:def 2
     {y where y is Element of L: x >= y & y is compact};
  end;

  theorem :: WAYBEL_8:4
   for L be non empty reflexive RelStr
   for x,y be Element of L holds
    y in compactbelow x iff x >= y & y is compact;

  theorem :: WAYBEL_8:5
   for L be non empty reflexive RelStr
   for x be Element of L holds
    compactbelow x = downarrow x /\ the carrier of CompactSublatt L;

  theorem :: WAYBEL_8:6
   for L be non empty reflexive transitive RelStr
   for x be Element of L holds
    compactbelow x c= waybelow x;

  definition
   let L be non empty lower-bounded reflexive antisymmetric RelStr;
   let x be Element of L;
   cluster compactbelow x -> non empty;
  end;

begin :: Algebraic Lattices

  definition
   let L be non empty reflexive RelStr;
   attr L is satisfying_axiom_K means
:: WAYBEL_8:def 3
    for x be Element of L holds x = sup compactbelow x;
  end;

  definition :: DEFINITION 4.4
   let L be non empty reflexive RelStr;
   attr L is algebraic means
:: WAYBEL_8:def 4
    (for x being Element of L holds compactbelow x is non empty directed) &
    L is up-complete satisfying_axiom_K;
  end;

  theorem :: WAYBEL_8:7   :: PROPOSITION 4.5
   for L be LATTICE holds
    L is algebraic iff
     ( L is continuous & for x,y be Element of L st x << y
        ex k be Element of L st k in the carrier of CompactSublatt L &
         x <= k & k <= y );

  definition
   cluster algebraic -> continuous LATTICE;
  end;

  definition
   cluster algebraic ->
                 up-complete satisfying_axiom_K (non empty reflexive RelStr);
  end;

  definition
   let L be non empty with_suprema Poset;
   cluster CompactSublatt L -> join-inheriting;
  end;

  definition
   let L be non empty reflexive RelStr;
   attr L is arithmetic means
:: WAYBEL_8:def 5
    L is algebraic & CompactSublatt L is meet-inheriting;
  end;

begin :: Arithmetic Lattices

  definition
   cluster arithmetic -> algebraic LATTICE;
  end;

  definition
   cluster trivial -> arithmetic LATTICE;
  end;

  definition
   cluster trivial strict LATTICE;
  end;

  theorem :: WAYBEL_8:8
   for L1,L2 be non empty reflexive antisymmetric RelStr
      st the RelStr of L1 = the RelStr of L2 & L1 is up-complete
   for x1,y1 be Element of L1
   for x2,y2 be Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
    x2 << y2;

  theorem :: WAYBEL_8:9
   for L1,L2 be non empty reflexive antisymmetric RelStr
      st the RelStr of L1 = the RelStr of L2 & L1 is up-complete
   for x be Element of L1
   for y be Element of L2 st x = y & x is compact holds
    y is compact;

  theorem :: WAYBEL_8:10
   for L1,L2 be up-complete (non empty reflexive antisymmetric RelStr)
      st the RelStr of L1 = the RelStr of L2
   for x be Element of L1
   for y be Element of L2 st x = y holds
    compactbelow x = compactbelow y;

  theorem :: WAYBEL_8:11
   for L1,L2 be RelStr
    st the RelStr of L1 = the RelStr of L2 & L1 is non empty
    holds L2 is non empty;

  theorem :: WAYBEL_8:12
   for L1,L2 be non empty RelStr
    st the RelStr of L1 = the RelStr of L2 & L1 is reflexive
    holds L2 is reflexive;

  theorem :: WAYBEL_8:13
   for L1,L2 be RelStr
    st the RelStr of L1 = the RelStr of L2 & L1 is transitive
    holds L2 is transitive;

  theorem :: WAYBEL_8:14
   for L1,L2 be RelStr
    st the RelStr of L1 = the RelStr of L2 & L1 is antisymmetric
    holds L2 is antisymmetric;

  theorem :: WAYBEL_8:15
   for L1,L2 be non empty reflexive RelStr
    st the RelStr of L1 = the RelStr of L2 & L1 is up-complete
    holds L2 is up-complete;

  theorem :: WAYBEL_8:16
   for L1,L2 be up-complete (non empty reflexive antisymmetric RelStr)
    st the RelStr of L1 = the RelStr of L2 & L1 is satisfying_axiom_K &
     for x be Element of L1 holds compactbelow x is non empty directed
    holds L2 is satisfying_axiom_K;

  theorem :: WAYBEL_8:17
   for L1,L2 be non empty reflexive antisymmetric RelStr
    st the RelStr of L1 = the RelStr of L2 & L1 is algebraic
    holds L2 is algebraic;

  theorem :: WAYBEL_8:18
   for L1,L2 be LATTICE
    st the RelStr of L1 = the RelStr of L2 & L1 is arithmetic
    holds L2 is arithmetic;

  definition
   let L be non empty RelStr;
   cluster the RelStr of L -> non empty;
  end;

  definition
   let L be non empty reflexive RelStr;
   cluster the RelStr of L -> reflexive;
  end;

  definition
   let L be transitive RelStr;
   cluster the RelStr of L -> transitive;
  end;

  definition
   let L be antisymmetric RelStr;
   cluster the RelStr of L -> antisymmetric;
  end;

  definition
   let L be with_infima RelStr;
   cluster the RelStr of L -> with_infima;
  end;

  definition
   let L be with_suprema RelStr;
   cluster the RelStr of L -> with_suprema;
  end;

  definition
   let L be up-complete (non empty reflexive RelStr);
   cluster the RelStr of L -> up-complete;
  end;

  definition
   let L be algebraic (non empty reflexive antisymmetric RelStr);
   cluster the RelStr of L -> algebraic;
  end;

  definition
   let L be arithmetic LATTICE;
   cluster the RelStr of L -> arithmetic;
  end;

  theorem :: WAYBEL_8:19
   for L be non empty transitive RelStr
   for S be non empty full SubRelStr of L
   for X be Subset of S st ex_sup_of X,L & "\/"(X,L) is Element of S holds
    ex_sup_of X,S & sup X = "\/"(X,L);

  theorem :: WAYBEL_8:20
     for L be non empty transitive RelStr
   for S be non empty full SubRelStr of L
   for X be Subset of S st ex_inf_of X,L & "/\"(X,L) is Element of S holds
    ex_inf_of X,S & inf X = "/\"(X,L);

  theorem :: WAYBEL_8:21  :: PROPOSITION 4.7 a)
     for L be algebraic LATTICE holds
    L is arithmetic iff CompactSublatt L is LATTICE;

  theorem :: WAYBEL_8:22  :: PROPOSITION 4.7 b)
   for L be algebraic lower-bounded LATTICE holds
    L is arithmetic iff L-waybelow is multiplicative;

  theorem :: WAYBEL_8:23  :: COROLLARY 4.8.a)
     for L be arithmetic lower-bounded LATTICE,
       p be Element of L holds
    p is pseudoprime implies p is prime;

  theorem :: WAYBEL_8:24  :: COROLLARY 4.8.b)
     for L be algebraic distributive lower-bounded LATTICE
    st for p being Element of L st p is pseudoprime holds p is prime
    holds L is arithmetic;

  definition
   let L be algebraic LATTICE;
   let c be closure map of L,L;
   cluster non empty directed Subset of Image c;
  end;

  theorem :: WAYBEL_8:25
   for L be algebraic LATTICE
   for c be closure map of L,L st c is directed-sups-preserving holds
    c.:([#]CompactSublatt L) c= [#]CompactSublatt Image c;

  theorem :: WAYBEL_8:26  :: PROPOSITION 4.9.(i)
     for L be algebraic lower-bounded LATTICE
   for c be closure map of L,L st c is directed-sups-preserving holds
    Image c is algebraic LATTICE;

  theorem :: WAYBEL_8:27  :: PROPOSITION 4.9.(ii)
     for L be algebraic lower-bounded LATTICE,
       c be closure map of L,L st c is directed-sups-preserving holds
    c.:([#]CompactSublatt L) = [#]CompactSublatt Image c;

begin :: Boolean Posets as Algebraic Lattices

  theorem :: WAYBEL_8:28
   for X,x be set holds
    x is Element of BoolePoset X iff x c= X;

  theorem :: WAYBEL_8:29
   for X be set
   for x,y be Element of BoolePoset X holds
    x << y
      iff
    for Y be Subset-Family of X st y c= union Y
    ex Z be finite Subset of Y st x c= union Z;

  theorem :: WAYBEL_8:30
   for X be set
   for x be Element of BoolePoset X holds
    x is finite iff x is compact;

  theorem :: WAYBEL_8:31
   for X be set
   for x be Element of BoolePoset X holds
    compactbelow x = {y where y is finite Subset of x : not contradiction};

  theorem :: WAYBEL_8:32  :: EXAMPLES 4.11.(1a)
     for X be set
   for F be Subset of X holds
    F in the carrier of CompactSublatt BoolePoset X iff F is finite;

  definition
   let X be set;
   let x be Element of BoolePoset X;
   cluster compactbelow x -> lower directed;
  end;

  theorem :: WAYBEL_8:33  :: EXAMPLES 4.11.(1b)
   for X be set holds BoolePoset X is algebraic;

  definition
   let X be set;
   cluster BoolePoset X -> algebraic;
  end;