:: Kernel Projections and Quotient Lattices
:: by Piotr Rudnicki
::
:: Received July 6, 1998
:: Copyright (c) 1998-2017 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;