The abstract of the Mizar article:

Kernel Projections and Quotient Lattices

by

Piotr Rudnicki

Received July 6, 1998

MML identifier: WAYBEL20

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FUNCT_5, FUNCT_1, EQREL_1, RELAT_2, ORDERS_1, PRE_TOPC,
      YELLOW_0, BOOLE, LATTICES, LATTICE3, ORDINAL2, WAYBEL_0, QUANTAL1,
      WELLORD1, CAT_1, BHSP_3, WAYBEL_1, GROUP_6, SEQM_3, YELLOW_1, WAYBEL_3,
      PBOOLE, CARD_3, FUNCT_4, FINSET_1, WAYBEL16, WAYBEL_5, BINOP_1, SETFAM_1,
      WAYBEL20, PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, SETFAM_1,
      RELAT_2, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, DOMAIN_1, EQREL_1, PBOOLE,
      FUNCT_3, FUNCT_5, FUNCT_7, STRUCT_0, ORDERS_1, LATTICE3, GRCAT_1,
      PRE_TOPC, QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, WAYBEL_0,
      WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL16;
 constructors DOMAIN_1, FUNCT_7, GRCAT_1, QUANTAL1, ORDERS_3, TOPS_2, YELLOW_3,
      WAYBEL_1, WAYBEL16;
 clusters STRUCT_0, FINSET_1, LATTICE3, RELSET_1, YELLOW_0, YELLOW_2, YELLOW_3,
      YELLOW_9, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL10, SUBSET_1, RELAT_1,
      FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

theorem :: WAYBEL20:1
 for X being set, S being Subset of id X holds proj1 S = proj2 S;

theorem :: WAYBEL20:2
 for X, Y being non empty set, f being Function of X, Y
  holds [:f, f:]"(id Y) is Equivalence_Relation of X;

definition
 let L1, L2, T1, T2 be RelStr, f be map of L1, T1, g be map of L2, T2;
 redefine func [:f, g:] -> map of [:L1, L2:], [:T1, T2:];
end;

theorem :: WAYBEL20:3
 for f, g being Function, X being set holds
  proj1 ([:f, g:].:X) c= f.:proj1 X & proj2 ([:f, g:].:X) c= g.:proj2 X;

theorem :: WAYBEL20:4
 for f, g being Function, X being set
  st X c= [:dom f, dom g:]
   holds proj1 ([:f, g:].:X) = f.:proj1 X & proj2 ([:f, g:].:X) = g.:proj2 X;

theorem :: WAYBEL20:5  :: Grzesiek
 for S being non empty antisymmetric RelStr st ex_inf_of {},S
  holds S is upper-bounded;

theorem :: WAYBEL20:6
 for S being non empty antisymmetric RelStr st ex_sup_of {},S
  holds S is lower-bounded;

theorem :: WAYBEL20:7  :: generealized YELLOW_3:47, YELLOW10:6
for L1,L2 being antisymmetric (non empty RelStr), D being Subset of [:L1,L2:]
  st ex_inf_of D,[:L1,L2:] holds inf D = [inf proj1 D,inf proj2 D];

theorem :: WAYBEL20:8  :: generealized YELLOW_3:46, YELLOW10:5
for L1,L2 being antisymmetric (non empty RelStr), D being Subset of [:L1,L2:]
 st ex_sup_of D,[:L1,L2:] holds sup D = [sup proj1 D,sup proj2 D];

theorem :: WAYBEL20:9
 for L1, L2, T1, T2 being antisymmetric non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is infs-preserving & g is infs-preserving
   holds [:f, g:] is infs-preserving;

theorem :: WAYBEL20:10
   for L1, L2, T1, T2 being antisymmetric reflexive non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is filtered-infs-preserving & g is filtered-infs-preserving
   holds [:f, g:] is filtered-infs-preserving;

theorem :: WAYBEL20:11
   for L1, L2, T1, T2 being antisymmetric non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is sups-preserving & g is sups-preserving
   holds [:f, g:] is sups-preserving;

theorem :: WAYBEL20:12
 for L1, L2, T1, T2 being antisymmetric reflexive non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is directed-sups-preserving & g is directed-sups-preserving
   holds [:f, g:] is directed-sups-preserving;

theorem :: WAYBEL20:13
 for L being antisymmetric non empty RelStr, X being Subset of [:L, L:]
  st X c= id the carrier of L & ex_inf_of X, [:L, L:]
   holds inf X in id the carrier of L;

theorem :: WAYBEL20:14
 for L being antisymmetric non empty RelStr, X being Subset of [:L, L:]
  st X c= id the carrier of L & ex_sup_of X, [:L, L:]
   holds sup X in id the carrier of L;

theorem :: WAYBEL20:15
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is reflexive holds M is reflexive;

theorem :: WAYBEL20:16
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is transitive holds M is transitive;

theorem :: WAYBEL20:17
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is antisymmetric holds M is antisymmetric;

theorem :: WAYBEL20:18   :: stolen from WAYBEL13:30
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is complete holds M is complete;

theorem :: WAYBEL20:19
 for L being non empty transitive RelStr, k being map of L, L
  st k is infs-preserving holds corestr k is infs-preserving;

theorem :: WAYBEL20:20
   for L being non empty transitive RelStr, k being map of L, L
  st k is filtered-infs-preserving
   holds corestr k is filtered-infs-preserving;

theorem :: WAYBEL20:21
   for L being non empty transitive RelStr, k being map of L, L
  st k is sups-preserving holds corestr k is sups-preserving;

theorem :: WAYBEL20:22
 for L being non empty transitive RelStr, k being map of L, L
  st k is directed-sups-preserving
   holds corestr k is directed-sups-preserving;

canceled;

theorem :: WAYBEL20:24  :: Generalized YELLOW_2:19
for S, T being reflexive antisymmetric non empty RelStr,
    f being map of S, T
  st f is filtered-infs-preserving holds f is monotone;

theorem :: WAYBEL20:25  ::  see YELLOW_2:17, for directed
 for S,T being non empty RelStr, f being map of S,T
  st f is monotone
   for X being Subset of S holds
    (X is filtered implies f.:X is filtered);

theorem :: WAYBEL20:26
 for L1, L2, L3 being non empty RelStr, f be map of L1,L2, g be map of L2,L3
  st f is infs-preserving & g is infs-preserving
   holds g*f is infs-preserving;

theorem :: WAYBEL20:27
   for L1, L2, L3 being non empty reflexive antisymmetric RelStr,
     f be map of L1,L2, g be map of L2,L3
  st f is filtered-infs-preserving & g is filtered-infs-preserving
   holds g*f is filtered-infs-preserving;

theorem :: WAYBEL20:28
   for L1, L2, L3 being non empty RelStr, f be map of L1,L2, g be map of L2,L3
  st f is sups-preserving & g is sups-preserving
   holds g*f is sups-preserving;

theorem :: WAYBEL20:29   :: see also WAYBEL15:13
   for L1, L2, L3 being non empty reflexive antisymmetric RelStr,
     f be map of L1,L2, g be map of L2,L3
  st f is directed-sups-preserving & g is directed-sups-preserving
   holds g*f is directed-sups-preserving;

begin :: Some remarks on lattice product

theorem :: WAYBEL20:30
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is lower-bounded antisymmetric RelStr
   holds product J is lower-bounded;

theorem :: WAYBEL20:31
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is upper-bounded antisymmetric RelStr
   holds product J is upper-bounded;

theorem :: WAYBEL20:32
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is lower-bounded antisymmetric RelStr
   holds for i being Element of I holds Bottom (product J).i = Bottom (J.i);

theorem :: WAYBEL20:33
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is upper-bounded antisymmetric RelStr
   holds for i being Element of I holds Top (product J).i = Top (J.i);

theorem :: WAYBEL20:34 :: Theorem 2.7, p. 60, (i)
   :: The hint in CCL suggest employing the distributivity equations.
   :: However, we prove it directly from the definition of continuity;
   :: it seems easier to do so.

  for I being non empty set,
    J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
 st for i being Element of I holds J.i is continuous complete LATTICE
  holds product J is continuous;

begin :: Kernel projections and quotient lattices

theorem :: WAYBEL20:35  :: Proposition 2.8 p. 61
for L, T being continuous complete LATTICE, g being CLHomomorphism of L, T,
    S being Subset of [:L, L:]
 st S = [:g, g:]"(id the carrier of T)
  holds subrelstr S is CLSubFrame of [:L, L:];

:: Proposition 2.9, p. 61, see WAYBEL10

:: Lemma 2.10, p. 61, see WAYBEL15:16

definition
 let L be RelStr, R be Subset of [:L, L:] such that
 R is Equivalence_Relation of the carrier of L;
 func EqRel R -> Equivalence_Relation of the carrier of L equals
:: WAYBEL20:def 1
   R;
end;

definition :: Definition 2.12, p. 62, part I (congruence)
 let L be non empty RelStr, R be Subset of [:L, L:];
 attr R is CLCongruence means
:: WAYBEL20:def 2
  R is Equivalence_Relation of the carrier of L &
  subrelstr R is CLSubFrame of [:L, L:];
end;

theorem :: WAYBEL20:36
 for L being complete LATTICE, R being non empty Subset of [:L, L:]
  st R is CLCongruence
   for x be Element of L holds [inf Class(EqRel R, x), x] in R;

definition :: Theorem 2.11, p. 61-62, (1) implies (3) (part a)
 let L be complete LATTICE, R be non empty Subset of [:L, L:] such that
 R is CLCongruence;
 func kernel_op R -> kernel map of L, L means
:: WAYBEL20:def 3
 for x being Element of L holds it.x = inf Class(EqRel R, x);
end;

theorem :: WAYBEL20:37  :: Theorem 2.11, p. 61-62, (1) implies (3) (part b)
 for L being complete LATTICE, R be non empty Subset of [:L, L:]
  st R is CLCongruence
   holds kernel_op R is directed-sups-preserving &
         R = [:kernel_op R, kernel_op R:]"(id the carrier of L);

theorem :: WAYBEL20:38  :: Theorem 2.11, p. 61-62, (3) implies (2)
 for L being continuous complete LATTICE, R be Subset of [:L, L:],
     k being kernel map of L, L
  st k is directed-sups-preserving & R = [:k, k:]"(id the carrier of L)
   ex LR being continuous complete strict LATTICE st
     the carrier of LR = Class EqRel R &
     the InternalRel of LR = {[Class(EqRel R, x), Class(EqRel R, y)]
                                where x, y is Element of L : k.x <= k.y } &
     for g being map of L, LR
      st for x being Element of L holds g.x = Class(EqRel R, x)
       holds g is CLHomomorphism of L, LR;

theorem :: WAYBEL20:39  :: Theorem 2.11, p. 61-62, (2) implies (1)
    :: CCL: Immediate from 2.8. (?)  One has to construct a homomorphism.
 for L being continuous complete LATTICE, R being Subset of [:L, L:]
  st R is Equivalence_Relation of the carrier of L &
     ex LR being continuous complete LATTICE st
          the carrier of LR = Class EqRel R &
          for g being map of L, LR
           st for x being Element of L holds g.x = Class(EqRel R, x)
            holds g is CLHomomorphism of L, LR
   holds subrelstr R is CLSubFrame of [:L, L:];

definition
 let L be non empty reflexive RelStr;
 cluster directed-sups-preserving kernel map of L, L;
end;

definition
 let L be non empty reflexive RelStr, k be kernel map of L, L;
 func kernel_congruence k -> non empty Subset of [:L, L:] equals
:: WAYBEL20:def 4
 [:k, k:]"(id the carrier of L);
end;

theorem :: WAYBEL20:40
 for L being non empty reflexive RelStr, k being kernel map of L, L
  holds kernel_congruence k is Equivalence_Relation of the carrier of L;

theorem :: WAYBEL20:41  :: Theorem 2.11, p. 61-62 (3) implies (1)
               :: Not in CCL, consequence of other implications.
 for L being continuous complete LATTICE,
     k being directed-sups-preserving kernel map of L, L
  holds kernel_congruence k is CLCongruence;

definition :: Definition 2.12, p. 62, part II (lattice quotient)
 let L be continuous complete LATTICE,
     R be non empty Subset of [:L, L:] such that
 R is CLCongruence;
 func L ./. R -> continuous complete strict LATTICE means
:: WAYBEL20:def 5
  the carrier of it = Class EqRel R &
  for x, y being Element of it holds x <= y iff "/\"(x, L) <= "/\"(y, L);
end;

theorem :: WAYBEL20:42
  for L being continuous complete LATTICE, R being non empty Subset of [:L, L:]
 st R is CLCongruence
  for x being set holds
    x is Element of L./.R iff ex y being Element of L st x = Class(EqRel R, y);

theorem :: WAYBEL20:43
 :: Corollary 2.13, p. 62, (congruence --> kernel --> congruence)
   for L being continuous complete LATTICE,
     R being non empty Subset of [:L, L:]
  st R is CLCongruence
   holds R = kernel_congruence kernel_op R;

theorem :: WAYBEL20:44
 :: Corollary 2.13, p. 62, (kernel --> congruence --> kernel)
   for L being continuous complete LATTICE,
     k being directed-sups-preserving kernel map of L, L
   holds k = kernel_op kernel_congruence k;

:: Theorem 2.14, p. 63, see WAYBEL15:17

theorem :: WAYBEL20:45 :: Proposition 2.15, p. 63
        :: That Image p is infs-inheriting follows from O-3.11 (iii)
   for L being continuous complete LATTICE,
     p being projection map of L, L
  st p is infs-preserving
   holds Image p is continuous LATTICE & Image p is infs-inheriting;