:: Kernel Projections and Quotient Lattices :: by Piotr Rudnicki :: :: Received July 6, 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 SUBSET_1, RELAT_1, XBOOLE_0, FUNCT_1, ZFMISC_1, EQREL_1, RELAT_2, ORDERS_2, STRUCT_0, TARSKI, YELLOW_0, LATTICES, LATTICE3, ORDINAL2, WAYBEL_0, WELLORD1, CAT_1, XXREAL_0, REWRITE1, WAYBEL_1, GROUP_6, SEQM_3, YELLOW_1, WAYBEL_3, PBOOLE, CARD_3, FINSET_1, FUNCT_4, WAYBEL16, WAYBEL_5, BINOP_1, SETFAM_1, WAYBEL20; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, SETFAM_1, RELAT_2, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, FINSET_1, DOMAIN_1, EQREL_1, FUNCT_3, FUNCT_7, STRUCT_0, ORDERS_2, LATTICE3, QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL16; constructors DOMAIN_1, FUNCT_7, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_1, YELLOW_3, WAYBEL16, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FUNCT_2, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL10, YELLOW_9, RELSET_1; 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 Function of L1, T1, g be Function of L2, T2; redefine func [:f, g:] -> Function 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 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 Function of L1, T1, g being Function 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 Function of L1, T1, g being Function 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 Function of L1, T1, g being Function 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 Function of L1, T1, g being Function 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 Function 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 Function 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 Function 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 Function of L, L st k is directed-sups-preserving holds corestr k is directed-sups-preserving; theorem :: WAYBEL20:23 :: Generalized YELLOW_2:19 for S, T being reflexive antisymmetric non empty RelStr, f being Function of S, T st f is filtered-infs-preserving holds f is monotone; theorem :: WAYBEL20:24 :: see YELLOW_2:17, for directed for S,T being non empty RelStr, f being Function of S,T st f is monotone for X being Subset of S holds (X is filtered implies f.:X is filtered) ; theorem :: WAYBEL20:25 for L1, L2, L3 being non empty RelStr, f be Function of L1,L2, g be Function of L2,L3 st f is infs-preserving & g is infs-preserving holds g*f is infs-preserving; theorem :: WAYBEL20:26 for L1, L2, L3 being non empty reflexive antisymmetric RelStr, f be Function of L1,L2, g be Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds g*f is filtered-infs-preserving; theorem :: WAYBEL20:27 for L1, L2, L3 being non empty RelStr, f be Function of L1,L2, g be Function of L2, L3 st f is sups-preserving & g is sups-preserving holds g*f is sups-preserving; theorem :: WAYBEL20:28 :: see also WAYBEL15:13 for L1, L2, L3 being non empty reflexive antisymmetric RelStr, f be Function of L1,L2, g be Function 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:29 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: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 upper-bounded antisymmetric RelStr holds product J is upper-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 lower-bounded antisymmetric RelStr holds for i being Element of I holds Bottom (product J).i = Bottom (J.i); 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 upper-bounded antisymmetric RelStr holds for i being Element of I holds Top (product J).i = Top (J.i); theorem :: WAYBEL20:33 :: 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:34 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:35 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 Function of L, L means :: WAYBEL20:def 3 for x being Element of L holds it.x = inf Class(EqRel R, x); end; theorem :: WAYBEL20:36 :: 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:37 :: Theorem 2.11, p. 61-62, (3) implies (2) for L being continuous complete LATTICE, R be Subset of [:L, L:] , k being kernel Function 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 Function 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:38 :: 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 Function 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:]; registration let L be non empty reflexive RelStr; cluster directed-sups-preserving kernel for Function of L, L; end; definition let L be non empty reflexive RelStr, k be kernel Function 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:39 for L being non empty reflexive RelStr, k being kernel Function of L, L holds kernel_congruence k is Equivalence_Relation of the carrier of L; theorem :: WAYBEL20:40 :: 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 Function 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:41 :: 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 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:42 :: Corollary 2.13, p. 62, (kernel --> congruence --> kernel) 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:43 :: Theorem 2.14, p. 63, see WAYBEL15:17 for L being continuous complete LATTICE, k being directed-sups-preserving kernel Function of L, L holds k = kernel_op kernel_congruence k; theorem :: WAYBEL20:44 :: 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 Function of L, L st p is infs-preserving holds Image p is continuous LATTICE & Image p is infs-inheriting;