:: Kernel Projections and Quotient Lattices
:: by Piotr Rudnicki
::
:: Received July 6, 1998
:: Copyright (c) 1998-2026 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;
definitions TARSKI, RELAT_2, LATTICE3, LATTICE5, YELLOW_0, WAYBEL_0, WAYBEL_1,
WAYBEL_3;
equalities YELLOW_0, WAYBEL_3, YELLOW_2, BINOP_1, STRUCT_0;
expansions RELAT_2, LATTICE3, LATTICE5, YELLOW_0, WAYBEL_0, WAYBEL_1,
WAYBEL_3;
theorems TARSKI, ZFMISC_1, RELAT_1, RELAT_2, FUNCT_1, FUNCT_2, FUNCT_3,
FUNCT_5, FUNCT_7, CARD_3, ORDERS_2, QUANTAL1, EQREL_1, YELLOW_0,
YELLOW_2, YELLOW_3, YELLOW10, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5,
WAYBEL13, WAYBEL15, WAYBEL16, WAYBEL17, XBOOLE_0, XBOOLE_1, PARTFUN1,
ORDERS_1, XTUPLE_0;
schemes YELLOW_0, FUNCT_2, PBOOLE;
begin :: Preliminaries
theorem Th1:
for X being set, S being Subset of id X holds proj1 S = proj2 S
proof
let X be set, S be Subset of id X;
now
let x be object;
hereby
assume x in proj1 S;
then consider y being object such that
A1: [x, y] in S by XTUPLE_0:def 12;
x = y by A1,RELAT_1:def 10;
hence x in proj2 S by A1,XTUPLE_0:def 13;
end;
assume x in proj2 S;
then consider y being object such that
A2: [y, x] in S by XTUPLE_0:def 13;
x = y by A2,RELAT_1:def 10;
hence x in proj1 S by A2,XTUPLE_0:def 12;
end;
hence thesis by TARSKI:2;
end;
theorem Th2:
for X, Y being non empty set, f being Function of X, Y holds [:f,
f:]"(id Y) is Equivalence_Relation of X
proof
let X, Y be non empty set, f be Function of X, Y;
set ff = [:f, f:]"(id Y);
A1: dom f = X by FUNCT_2:def 1;
reconsider R9 = ff as Relation of X;
A2: dom [:f, f:] = [:dom f, dom f:] by FUNCT_3:def 8;
R9 is_reflexive_in X
proof
let x be object;
assume
A3: x in X;
then reconsider x9 = x as Element of X;
A4: [f.x9, f.x9] in id Y by RELAT_1:def 10;
[x, x] in dom [:f, f:] & [f.x, f.x] = [:f, f:].(x,x) by A2,A1,A3,
FUNCT_3:def 8,ZFMISC_1:def 2;
hence thesis by A4,FUNCT_1:def 7;
end;
then
A5: dom R9 = X & field R9 = X by ORDERS_1:13;
A6: R9 is_symmetric_in X
proof
let x, y be object;
assume that
A7: x in X & y in X and
A8: [x,y] in R9;
reconsider x9 = x, y9 = y as Element of X by A7;
A9: [y, x] in dom [:f, f:] & [f.y, f.x] = [:f, f:].(y, x) by A2,A1,A7,
FUNCT_3:def 8,ZFMISC_1:def 2;
A10: [:f, f:].[x,y] in id Y & [f.x, f.y] = [:f, f:].(x, y) by A1,A7,A8,
FUNCT_1:def 7,FUNCT_3:def 8;
then f.x9 = f.y9 by RELAT_1:def 10;
hence thesis by A10,A9,FUNCT_1:def 7;
end;
R9 is_transitive_in X
proof
let x, y, z be object such that
A11: x in X and
A12: y in X and
A13: z in X and
A14: [x,y] in R9 and
A15: [y,z] in R9;
A16: [x, z] in dom [:f, f:] & [f.x, f.z] = [:f, f:].(x, z) by A2,A1,A11,A13,
FUNCT_3:def 8,ZFMISC_1:def 2;
reconsider y9=y, z9=z as Element of X by A12,A13;
[:f, f:].[y, z] in id Y & [f.y, f.z] = [:f, f:].(y, z) by A1,A12,A13,A15,
FUNCT_1:def 7,FUNCT_3:def 8;
then
A17: f.y9 = f.z9 by RELAT_1:def 10;
[:f, f:].[x,y] in id Y & [f.x, f.y] = [:f, f:].(x, y) by A1,A11,A12,A14,
FUNCT_1:def 7,FUNCT_3:def 8;
hence thesis by A17,A16,FUNCT_1:def 7;
end;
hence thesis by A5,A6,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;
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:]; :: redefines [: (FUNCT_3, definition)
coherence
proof
the carrier of [:L1, L2:] = [:the carrier of L1, the carrier of L2:] &
the carrier of [:T1, T2:] = [:the carrier of T1, the carrier of T2:] by
YELLOW_3:def 2;
hence [:f, g:] is Function of [:L1, L2:], [:T1, T2:];
end;
end;
theorem Th3:
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
proof
let f, g be Function, X be set;
A1: dom [:f, g:] = [:dom f, dom g:] by FUNCT_3:def 8;
hereby
let x be object;
assume x in proj1 ([:f, g:].:X);
then consider y being object such that
A2: [x, y] in [:f, g:].:X by XTUPLE_0:def 12;
consider xy being object such that
A3: xy in dom [:f, g:] and
A4: xy in X and
A5: [x, y] = [:f, g:].xy by A2,FUNCT_1:def 6;
consider x9,y9 being object such that
A6: x9 in dom f and
A7: y9 in dom g and
A8: xy = [x9,y9] by A1,A3,ZFMISC_1:def 2;
[x, y] = [:f, g:].(x9,y9) by A5,A8
.= [f.x9, g.y9] by A6,A7,FUNCT_3:def 8;
then
A9: x = f.x9 by XTUPLE_0:1;
x9 in proj1 X by A4,A8,XTUPLE_0:def 12;
hence x in f.:proj1 X by A6,A9,FUNCT_1:def 6;
end;
let y be object;
assume y in proj2 ([:f, g:].:X);
then consider x being object such that
A10: [x, y] in [:f, g:].:X by XTUPLE_0:def 13;
consider xy being object such that
A11: xy in dom [:f, g:] and
A12: xy in X and
A13: [x, y] = [:f, g:].xy by A10,FUNCT_1:def 6;
consider x9,y9 being object such that
A14: x9 in dom f and
A15: y9 in dom g and
A16: xy = [x9,y9] by A1,A11,ZFMISC_1:def 2;
[x, y] = [:f, g:].(x9,y9) by A13,A16
.= [f.x9, g.y9] by A14,A15,FUNCT_3:def 8;
then
A17: y = g.y9 by XTUPLE_0:1;
y9 in proj2 X by A12,A16,XTUPLE_0:def 13;
hence thesis by A15,A17,FUNCT_1:def 6;
end;
theorem Th4:
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
proof
let f, g be Function, X be set such that
A1: X c= [:dom f, dom g:];
A2: dom [:f, g:] = [:dom f, dom g:] by FUNCT_3:def 8;
A3: proj1 ([:f, g:].:X) c= f.:proj1 X by Th3;
now
let x be object;
thus x in proj1 ([:f, g:].:X) implies x in f.:proj1 X by A3;
assume x in f.:proj1 X;
then consider x9 being object such that
A4: x9 in dom f and
A5: x9 in proj1 X and
A6: x = f.x9 by FUNCT_1:def 6;
consider y9 being object such that
A7: [x9, y9] in X by A5,XTUPLE_0:def 12;
y9 in dom g by A1,A7,ZFMISC_1:87;
then [:f, g:].(x9, y9) = [f.x9, g.y9] by A4,FUNCT_3:def 8;
then [x, g.y9] in [:f, g:].:X by A1,A2,A6,A7,FUNCT_1:def 6;
hence x in proj1 ([:f, g:].:X) by XTUPLE_0:def 12;
end;
hence proj1 ([:f, g:].:X) = f.:proj1 X by TARSKI:2;
A8: proj2 ([:f, g:].:X) c= g.:proj2 X by Th3;
now
let x be object;
thus x in proj2 ([:f, g:].:X) implies x in g.:proj2 X by A8;
assume x in g.:proj2 X;
then consider x9 being object such that
A9: x9 in dom g and
A10: x9 in proj2 X and
A11: x = g.x9 by FUNCT_1:def 6;
consider y9 being object such that
A12: [y9, x9] in X by A10,XTUPLE_0:def 13;
y9 in dom f by A1,A12,ZFMISC_1:87;
then [:f, g:].(y9, x9) = [f.y9, g.x9] by A9,FUNCT_3:def 8;
then [f.y9, x] in [:f, g:].:X by A1,A2,A11,A12,FUNCT_1:def 6;
hence x in proj2 ([:f, g:].:X) by XTUPLE_0:def 13;
end;
hence thesis by TARSKI:2;
end;
theorem Th5:
for S being non empty antisymmetric RelStr st ex_inf_of {},S
holds S is upper-bounded
proof
let S be non empty antisymmetric RelStr;
assume
A1: ex_inf_of {},S;
take Top S;
let x be Element of S;
{} is_>=_than x;
hence thesis by A1,YELLOW_0:31;
end;
theorem Th6:
for S being non empty antisymmetric RelStr st ex_sup_of {},S
holds S is lower-bounded
proof
let S be non empty antisymmetric RelStr;
assume
A1: ex_sup_of {},S;
take Bottom S;
let x be Element of S;
{} is_<=_than x;
hence thesis by A1,YELLOW_0:30;
end;
theorem Th7: :: 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]
proof
let L1,L2 be antisymmetric non empty RelStr, D be Subset of [:L1,L2:] such
that
A1: ex_inf_of D,[:L1,L2:];
per cases;
suppose
D <> {};
hence thesis by A1,YELLOW_3:47;
end;
suppose
A2: D = {};
then ex_inf_of {},L2 by A1,FUNCT_5:8,YELLOW_3:42;
then
A3: L2 is upper-bounded by Th5;
ex_inf_of {},L1 by A1,A2,FUNCT_5:8,YELLOW_3:42;
then L1 is upper-bounded by Th5;
hence thesis by A1,A3,YELLOW10:6;
end;
end;
theorem Th8: :: 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]
proof
let L1,L2 be antisymmetric non empty RelStr, D be Subset of [:L1,L2:] such
that
A1: ex_sup_of D,[:L1,L2:];
per cases;
suppose
D <> {};
hence thesis by A1,YELLOW_3:46;
end;
suppose
A2: D = {};
then ex_sup_of {},L2 by A1,FUNCT_5:8,YELLOW_3:41;
then
A3: L2 is lower-bounded by Th6;
ex_sup_of {},L1 by A1,A2,FUNCT_5:8,YELLOW_3:41;
then L1 is lower-bounded by Th6;
hence thesis by A1,A3,YELLOW10:5;
end;
end;
theorem Th9:
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
proof
let L1, L2, T1, T2 be antisymmetric non empty RelStr, f be Function of L1,
T1, g be Function of L2, T2 such that
A1: f is infs-preserving and
A2: g is infs-preserving;
let X be Subset of [:L1, L2:];
A3: f preserves_inf_of proj1 X by A1;
A4: g preserves_inf_of proj2 X by A2;
set iX = [:f, g:].:X;
A5: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
assume
A6: ex_inf_of X, [:L1, L2:];
then
A7: ex_inf_of proj1 X, L1 by YELLOW_3:42;
A8: ex_inf_of proj2 X, L2 by A6,YELLOW_3:42;
X c= the carrier of [:L1, L2:];
then
A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then
A10: proj2 iX = g.:proj2 X by A5,Th4;
then
A11: ex_inf_of proj2 iX, T2 by A4,A8;
A12: proj1 iX = f.:proj1 X by A5,A9,Th4;
then ex_inf_of proj1 iX, T1 by A3,A7;
hence ex_inf_of ([:f, g:].:X), [:T1, T2:] by A11,YELLOW_3:42;
hence inf ([:f, g:].:X) = [inf (f.:proj1 X), inf (g.:proj2 X)] by A12,A10,Th7
.= [f.inf proj1 X, inf (g.:proj2 X)] by A3,A7
.= [f.inf proj1 X, g.inf proj2 X] by A4,A8
.= [:f, g:].(inf proj1 X, inf proj2 X) by A5,FUNCT_3:def 8
.= [:f, g:].inf X by A6,Th7;
end;
theorem
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
proof
let L1, L2, T1, T2 be antisymmetric reflexive non empty RelStr, f be
Function of L1, T1, g be Function of L2, T2 such that
A1: f is filtered-infs-preserving and
A2: g is filtered-infs-preserving;
let X be Subset of [:L1, L2:];
assume
A3: X is non empty filtered;
then proj1 X is non empty filtered by YELLOW_3:21,24;
then
A4: f preserves_inf_of proj1 X by A1;
proj2 X is non empty filtered by A3,YELLOW_3:21,24;
then
A5: g preserves_inf_of proj2 X by A2;
set iX = [:f, g:].:X;
A6: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
assume
A7: ex_inf_of X, [:L1, L2:];
then
A8: ex_inf_of proj1 X, L1 by YELLOW_3:42;
X c= the carrier of [:L1, L2:];
then
A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then
A10: proj2 iX = g.:proj2 X by A6,Th4;
A11: ex_inf_of proj2 X, L2 by A7,YELLOW_3:42;
then
A12: ex_inf_of proj2 iX, T2 by A5,A10;
A13: proj1 iX = f.:proj1 X by A6,A9,Th4;
then ex_inf_of proj1 iX, T1 by A4,A8;
hence ex_inf_of ([:f, g:].:X), [:T1, T2:] by A12,YELLOW_3:42;
hence inf ([:f, g:].:X) = [inf (f.:proj1 X), inf (g.:proj2 X)] by A13,A10,Th7
.= [f.inf proj1 X, inf (g.:proj2 X)] by A4,A8
.= [f.inf proj1 X, g.inf proj2 X] by A5,A11
.= [:f, g:].(inf proj1 X, inf proj2 X) by A6,FUNCT_3:def 8
.= [:f, g:].inf X by A7,Th7;
end;
theorem
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
proof
let L1, L2, T1, T2 be antisymmetric non empty RelStr, f be Function of L1,
T1, g be Function of L2, T2 such that
A1: f is sups-preserving and
A2: g is sups-preserving;
let X be Subset of [:L1, L2:];
A3: f preserves_sup_of proj1 X by A1;
A4: g preserves_sup_of proj2 X by A2;
set iX = [:f, g:].:X;
A5: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
assume
A6: ex_sup_of X, [:L1, L2:];
then
A7: ex_sup_of proj1 X, L1 by YELLOW_3:41;
A8: ex_sup_of proj2 X, L2 by A6,YELLOW_3:41;
X c= the carrier of [:L1, L2:];
then
A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then
A10: proj2 iX = g.:proj2 X by A5,Th4;
then
A11: ex_sup_of proj2 iX, T2 by A4,A8;
A12: proj1 iX = f.:proj1 X by A5,A9,Th4;
then ex_sup_of proj1 iX, T1 by A3,A7;
hence ex_sup_of ([:f, g:].:X), [:T1, T2:] by A11,YELLOW_3:41;
hence sup ([:f, g:].:X) = [sup (f.:proj1 X), sup (g.:proj2 X)] by A12,A10,Th8
.= [f.sup proj1 X, sup (g.:proj2 X)] by A3,A7
.= [f.sup proj1 X, g.sup proj2 X] by A4,A8
.= [:f, g:].(sup proj1 X, sup proj2 X) by A5,FUNCT_3:def 8
.= [:f, g:].sup X by A6,Th8;
end;
theorem Th12:
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
proof
let L1, L2, T1, T2 be antisymmetric reflexive non empty RelStr, f be
Function of L1, T1, g be Function of L2, T2 such that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving;
let X be Subset of [:L1, L2:];
assume
A3: X is non empty directed;
then proj1 X is non empty directed by YELLOW_3:21,22;
then
A4: f preserves_sup_of proj1 X by A1;
proj2 X is non empty directed by A3,YELLOW_3:21,22;
then
A5: g preserves_sup_of proj2 X by A2;
set iX = [:f, g:].:X;
A6: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
assume
A7: ex_sup_of X, [:L1, L2:];
then
A8: ex_sup_of proj1 X, L1 by YELLOW_3:41;
X c= the carrier of [:L1, L2:];
then
A9: X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then
A10: proj2 iX = g.:proj2 X by A6,Th4;
A11: ex_sup_of proj2 X, L2 by A7,YELLOW_3:41;
then
A12: ex_sup_of proj2 iX, T2 by A5,A10;
A13: proj1 iX = f.:proj1 X by A6,A9,Th4;
then ex_sup_of proj1 iX, T1 by A4,A8;
hence ex_sup_of ([:f, g:].:X), [:T1, T2:] by A12,YELLOW_3:41;
hence sup ([:f, g:].:X) = [sup (f.:proj1 X), sup (g.:proj2 X)] by A13,A10,Th8
.= [f.sup proj1 X, sup (g.:proj2 X)] by A4,A8
.= [f.sup proj1 X, g.sup proj2 X] by A5,A11
.= [:f, g:].(sup proj1 X, sup proj2 X) by A6,FUNCT_3:def 8
.= [:f, g:].sup X by A7,Th8;
end;
theorem Th13:
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
proof
let L be antisymmetric non empty RelStr, X be Subset of [:L, L:];
assume X c= id the carrier of L & ex_inf_of X, [:L, L:];
then inf X = [inf proj1 X, inf proj2 X] & inf proj1 X = inf proj2 X by Th1
,Th7;
hence thesis by RELAT_1:def 10;
end;
theorem Th14:
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
proof
let L be antisymmetric non empty RelStr, X be Subset of [:L, L:];
assume X c= id the carrier of L & ex_sup_of X, [:L, L:];
then sup X = [sup proj1 X, sup proj2 X] & sup proj1 X = sup proj2 X by Th1
,Th8;
hence thesis by RELAT_1:def 10;
end;
theorem Th15:
for L, M being non empty RelStr st L, M are_isomorphic & L is
reflexive holds M is reflexive
proof
let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is reflexive;
let x be Element of M;
M, L are_isomorphic by A1,WAYBEL_1:6;
then consider f being Function of M, L such that
A3: f is isomorphic;
reconsider fx = f.x as Element of L;
fx <= fx by A2;
hence thesis by A3,WAYBEL_0:66;
end;
theorem Th16:
for L, M being non empty RelStr st L, M are_isomorphic & L is
transitive holds M is transitive
proof
let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is transitive;
M, L are_isomorphic by A1,WAYBEL_1:6;
then consider f being Function of M, L such that
A3: f is isomorphic;
let x, y, z be Element of M such that
A4: x <= y & y <= z;
reconsider fz = f.z as Element of L;
reconsider fy = f.y as Element of L;
reconsider fx = f.x as Element of L;
fx <= fy & fy <= fz by A3,A4,WAYBEL_0:66;
then fx <= fz by A2;
hence thesis by A3,WAYBEL_0:66;
end;
theorem Th17:
for L, M being non empty RelStr st L, M are_isomorphic & L is
antisymmetric holds M is antisymmetric
proof
let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is antisymmetric;
M, L are_isomorphic by A1,WAYBEL_1:6;
then consider f being Function of M, L such that
A3: f is isomorphic;
let x, y be Element of M such that
A4: x <= y & y <= x;
reconsider fy = f.y as Element of L;
reconsider fx = f.x as Element of L;
fx <= fy & fy <= fx by A3,A4,WAYBEL_0:66;
then dom f = the carrier of M & fx = fy by A2,FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 4;
end;
theorem Th18: :: stolen from WAYBEL13:30
for L, M being non empty RelStr st L, M are_isomorphic & L is
complete holds M is complete
proof
let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is complete;
let X be Subset of M;
M, L are_isomorphic by A1,WAYBEL_1:6;
then consider f being Function of M, L such that
A3: f is isomorphic;
reconsider fX = f.:X as Subset of L;
consider fa being Element of L such that
A4: fa is_<=_than fX and
A5: for fb being Element of L st fb is_<=_than fX holds fb <= fa by A2;
set a = (f qua Function)".fa;
A6: rng f = the carrier of L by A3,WAYBEL_0:66;
then a in dom f by A3,FUNCT_1:32;
then reconsider a as Element of M;
A7: fa = f.a by A3,A6,FUNCT_1:35;
take a;
A8: dom f = the carrier of M by FUNCT_2:def 1;
hereby
let b be Element of M such that
A9: b in X;
reconsider fb = f.b as Element of L;
fb in fX by A8,A9,FUNCT_1:def 6;
then fa <= fb by A4;
hence a <= b by A3,A7,WAYBEL_0:66;
end;
let b be Element of M such that
A10: b is_<=_than X;
reconsider fb = f.b as Element of L;
fb is_<=_than fX
proof
let fc be Element of L;
assume fc in fX;
then consider c being object such that
A11: c in dom f and
A12: c in X and
A13: fc = f.c by FUNCT_1:def 6;
reconsider c as Element of M by A11;
b <= c by A10,A12;
hence thesis by A3,A13,WAYBEL_0:66;
end;
then fb <= fa by A5;
hence thesis by A3,A7,WAYBEL_0:66;
end;
theorem Th19:
for L being non empty transitive RelStr, k being Function of L,
L st k is infs-preserving holds corestr k is infs-preserving
proof
let L be non empty transitive RelStr, k be Function of L, L such that
A1: k is infs-preserving;
let X be Subset of L;
assume
A2: ex_inf_of X,L;
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
A4: k preserves_inf_of X by A1;
then
A5: ex_inf_of k.:X, L by A2;
reconsider fX = f.:X as Subset of Image k;
dom k = the carrier of L by FUNCT_2:def 1;
then rng k = the carrier of Image k & k.inf X in rng k by FUNCT_1:def 3
,YELLOW_0:def 15;
then "/\"(fX, L) is Element of Image k by A4,A3,A2;
hence ex_inf_of f.:X, Image k by A3,A5,YELLOW_0:63;
inf (k.:X) = k.inf X by A4,A2;
hence thesis by A3,A5,YELLOW_0:63;
end;
theorem
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
proof
let L be non empty transitive RelStr, k be Function of L, L such that
A1: k is filtered-infs-preserving;
let X be Subset of L;
assume X is non empty filtered;
then
A2: k preserves_inf_of X by A1;
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
assume
A4: ex_inf_of X,L;
then
A5: ex_inf_of k.:X, L by A2;
reconsider fX = f.:X as Subset of Image k;
dom k = the carrier of L by FUNCT_2:def 1;
then rng k = the carrier of Image k & k.inf X in rng k by FUNCT_1:def 3
,YELLOW_0:def 15;
then "/\"(fX, L) is Element of Image k by A2,A3,A4;
hence ex_inf_of f.:X, Image k by A3,A5,YELLOW_0:63;
inf (k.:X) = k.inf X by A2,A4;
hence thesis by A3,A5,YELLOW_0:63;
end;
theorem
for L being non empty transitive RelStr, k being Function of L, L st k
is sups-preserving holds corestr k is sups-preserving
proof
let L be non empty transitive RelStr, k be Function of L, L such that
A1: k is sups-preserving;
let X be Subset of L;
assume
A2: ex_sup_of X,L;
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
A4: k preserves_sup_of X by A1;
then
A5: ex_sup_of k.:X, L by A2;
reconsider fX = f.:X as Subset of Image k;
dom k = the carrier of L by FUNCT_2:def 1;
then rng k = the carrier of Image k & k.sup X in rng k by FUNCT_1:def 3
,YELLOW_0:def 15;
then "\/"(fX, L) is Element of Image k by A4,A3,A2;
hence ex_sup_of f.:X, Image k by A3,A5,YELLOW_0:64;
sup (k.:X) = k.sup X by A4,A2;
hence thesis by A3,A5,YELLOW_0:64;
end;
theorem Th22:
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
proof
let L be non empty transitive RelStr, k be Function of L, L such that
A1: k is directed-sups-preserving;
let X be Subset of L;
assume X is non empty directed;
then
A2: k preserves_sup_of X by A1;
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
assume
A4: ex_sup_of X,L;
then
A5: ex_sup_of k.:X, L by A2;
reconsider fX = f.:X as Subset of Image k;
dom k = the carrier of L by FUNCT_2:def 1;
then rng k = the carrier of Image k & k.sup X in rng k by FUNCT_1:def 3
,YELLOW_0:def 15;
then "\/"(fX, L) is Element of Image k by A2,A3,A4;
hence ex_sup_of f.:X, Image k by A3,A5,YELLOW_0:64;
sup (k.:X) = k.sup X by A2,A4;
hence thesis by A3,A5,YELLOW_0:64;
end;
theorem Th23: :: 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
proof
let S, T be reflexive antisymmetric non empty RelStr, f be Function of S, T;
assume
A1: f is filtered-infs-preserving;
let x, y be Element of S such that
A2: x <= y;
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: for b being Element of S st {x, y} is_>=_than b holds x >= b by YELLOW_0:8;
A5: x <= x;
then
A6: {x, y} is_>=_than x by A2,YELLOW_0:8;
then
A7: ex_inf_of {x, y},S by A4,YELLOW_0:31;
for a, b being Element of S st a in {x, y} & b in {x, y} ex z being
Element of S st z in {x, y} & a >= z & b >= z
proof
let a, b be Element of S such that
A8: a in {x, y} & b in {x, y};
take x;
thus x in {x, y} by TARSKI:def 2;
thus thesis by A2,A5,A8,TARSKI:def 2;
end;
then {x, y} is filtered non empty;
then
A9: f preserves_inf_of {x, y} by A1;
x = inf {x, y} by A6,A4,YELLOW_0:31;
then inf(f.:{x, y}) = f.x by A7,A9;
then
A10: f.x = inf{f.x, f.y} by A3,FUNCT_1:60;
f.:{x, y} = {f.x, f.y} by A3,FUNCT_1:60;
then ex_inf_of {f.x, f.y}, T by A7,A9;
then {f.x, f.y} is_>=_than f.x by A10,YELLOW_0:def 10;
hence f.x <= f.y by YELLOW_0:8;
end;
theorem Th24: :: 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)
proof
let S,T be non empty RelStr, f be Function of S,T;
assume
A1: f is monotone;
let X be Subset of S such that
A2: X is filtered;
let x,y be Element of T;
assume x in f.:X;
then consider a being object such that
A3: a in the carrier of S and
A4: a in X and
A5: x = f.a by FUNCT_2:64;
assume y in f.:X;
then consider b being object such that
A6: b in the carrier of S and
A7: b in X and
A8: y = f.b by FUNCT_2:64;
reconsider a,b as Element of S by A3,A6;
consider c being Element of S such that
A9: c in X and
A10: c <= a & c <= b by A2,A4,A7;
take z = f.c;
thus z in f.:X by A9,FUNCT_2:35;
thus thesis by A1,A5,A8,A10;
end;
theorem Th25:
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
proof
let L1, L2, L3 be non empty RelStr, f be Function of L1,L2, g be Function of
L2,L3 such that
A1: f is infs-preserving and
A2: g is infs-preserving;
set gf = g*f;
let X be Subset of L1 such that
A3: ex_inf_of X, L1;
set fX = f.:X;
set gfX = gf.:X;
A4: f preserves_inf_of X by A1;
then
A5: gfX = g.:(f.:X) & ex_inf_of fX, L2 by A3,RELAT_1:126;
A6: dom f = the carrier of L1 by FUNCT_2:def 1;
A7: g preserves_inf_of fX by A2;
hence ex_inf_of gfX, L3 by A5;
thus inf gfX = g.inf fX by A7,A5
.= g.(f.inf X) by A3,A4
.= gf.inf X by A6,FUNCT_1:13;
end;
theorem
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
proof
let L1, L2, L3 be non empty reflexive antisymmetric RelStr, f be Function of
L1,L2, g be Function of L2,L3 such that
A1: f is filtered-infs-preserving and
A2: g is filtered-infs-preserving;
set gf = g*f;
let X be Subset of L1 such that
A3: X is non empty filtered and
A4: ex_inf_of X, L1;
set xx = the Element of X;
set fX = f.:X;
set gfX = gf.:X;
A5: f preserves_inf_of X by A1,A3;
then
A6: gfX = g.:(f.:X) & ex_inf_of fX, L2 by A4,RELAT_1:126;
xx in X by A3;
then f.xx in fX by FUNCT_2:35;
then fX is non empty filtered by A1,A3,Th23,Th24;
then
A7: g preserves_inf_of fX by A2;
hence ex_inf_of gfX, L3 by A6;
A8: dom f = the carrier of L1 by FUNCT_2:def 1;
thus inf gfX = g.inf fX by A7,A6
.= g.(f.inf X) by A4,A5
.= gf.inf X by A8,FUNCT_1:13;
end;
theorem
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
proof
let L1, L2, L3 be non empty RelStr, f be Function of L1,L2, g be Function of
L2,L3 such that
A1: f is sups-preserving and
A2: g is sups-preserving;
set gf = g*f;
let X be Subset of L1 such that
A3: ex_sup_of X, L1;
set fX = f.:X;
set gfX = gf.:X;
A4: f preserves_sup_of X by A1;
then
A5: gfX = g.:(f.:X) & ex_sup_of fX, L2 by A3,RELAT_1:126;
A6: dom f = the carrier of L1 by FUNCT_2:def 1;
A7: g preserves_sup_of fX by A2;
hence ex_sup_of gfX, L3 by A5;
thus sup gfX = g.sup fX by A7,A5
.= g.(f.sup X) by A3,A4
.= gf.sup X by A6,FUNCT_1:13;
end;
theorem :: 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
proof
let L1, L2, L3 be non empty reflexive antisymmetric RelStr, f be Function of
L1,L2, g be Function of L2,L3 such that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving;
set gf = g*f;
let X be Subset of L1 such that
A3: X is non empty directed and
A4: ex_sup_of X, L1;
set xx = the Element of X;
set fX = f.:X;
set gfX = gf.:X;
A5: f preserves_sup_of X by A1,A3;
then
A6: gfX = g.:(f.:X) & ex_sup_of fX, L2 by A4,RELAT_1:126;
xx in X by A3;
then f.xx in fX by FUNCT_2:35;
then fX is non empty directed by A1,A3,WAYBEL17:3,YELLOW_2:15;
then
A7: g preserves_sup_of fX by A2;
hence ex_sup_of gfX, L3 by A6;
A8: dom f = the carrier of L1 by FUNCT_2:def 1;
thus sup gfX = g.sup fX by A7,A6
.= g.(f.sup X) by A4,A5
.= gf.sup X by A8,FUNCT_1:13;
end;
begin :: Some remarks on lattice product
theorem
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
proof
let I be non empty set, J be RelStr-yielding non-Empty ManySortedSet of I
such that
A1: for i being Element of I holds J.i is lower-bounded antisymmetric RelStr;
deffunc F(Element of I) = Bottom (J.$1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A3: now
let i be Element of I;
f.i = Bottom (J.i) by A2;
hence f.i is Element of J.i;
end;
dom f = I by PARTFUN1:def 2;
then reconsider f as Element of product J by A3,WAYBEL_3:27;
take f;
let b be Element of product J such that
b in the carrier of product J;
now
let i be Element of I;
f.i = Bottom (J.i) & J.i is lower-bounded antisymmetric non empty
RelStr by A1,A2;
hence f.i <= b.i by YELLOW_0:44;
end;
hence thesis by WAYBEL_3:28;
end;
theorem
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
proof
let I be non empty set, J be RelStr-yielding non-Empty ManySortedSet of I
such that
A1: for i being Element of I holds J.i is upper-bounded antisymmetric RelStr;
deffunc F(Element of I) = Top (J.$1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A3: now
let i be Element of I;
f.i = Top (J.i) by A2;
hence f.i is Element of J.i;
end;
dom f = I by PARTFUN1:def 2;
then reconsider f as Element of product J by A3,WAYBEL_3:27;
take f;
let b be Element of product J such that
b in the carrier of product J;
now
let i be Element of I;
f.i = Top (J.i) & J.i is upper-bounded antisymmetric non empty RelStr
by A1,A2;
hence f.i >= b.i by YELLOW_0:45;
end;
hence thesis by WAYBEL_3:28;
end;
theorem
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)
proof
let I be non empty set, J be RelStr-yielding non-Empty ManySortedSet of I
such that
A1: for i being Element of I holds J.i is lower-bounded antisymmetric RelStr;
deffunc F(Element of I) = Bottom (J.$1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A3: now
let i be Element of I;
f.i = Bottom (J.i) by A2;
hence f.i is Element of J.i;
end;
dom f = I by PARTFUN1:def 2;
then reconsider f as Element of product J by A3,WAYBEL_3:27;
let i be Element of I;
A4: {} is_<=_than f;
A5: now
let c be Element of product J such that
{} is_<=_than c and
A6: for b being Element of product J st {} is_<=_than b holds b >= c;
now
let i be Element of I;
f.i = Bottom (J.i) & J.i is lower-bounded antisymmetric non empty
RelStr by A1,A2;
hence f.i <= c.i by YELLOW_0:44;
end;
then
A7: f <= c by WAYBEL_3:28;
for i being Element of I holds J.i is antisymmetric by A1;
then
A8: product J is antisymmetric by WAYBEL_3:30;
c <= f by A6,YELLOW_0:6;
hence c = f by A8,A7;
end;
A9: now
let a be Element of product J such that
{} is_<=_than a;
now
let i be Element of I;
f.i = Bottom (J.i) & J.i is lower-bounded antisymmetric non empty
RelStr by A1,A2;
hence f.i <= a.i by YELLOW_0:44;
end;
hence f <= a by WAYBEL_3:28;
end;
now
let b be Element of product J such that
{} is_<=_than b;
now
let i be Element of I;
f.i = Bottom (J.i) & J.i is lower-bounded antisymmetric non empty
RelStr by A1,A2;
hence f.i <= b.i by YELLOW_0:44;
end;
hence f <= b by WAYBEL_3:28;
end;
then ex_sup_of {}, product J by A4,A5;
then f = "\/"({}, product J) by A4,A9,YELLOW_0:def 9;
hence thesis by A2;
end;
theorem
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)
proof
let I be non empty set, J be RelStr-yielding non-Empty ManySortedSet of I
such that
A1: for i being Element of I holds J.i is upper-bounded antisymmetric RelStr;
deffunc F(Element of I) = Top (J.$1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A3: now
let i be Element of I;
f.i = Top (J.i) by A2;
hence f.i is Element of J.i;
end;
dom f = I by PARTFUN1:def 2;
then reconsider f as Element of product J by A3,WAYBEL_3:27;
let i be Element of I;
A4: {} is_>=_than f;
A5: now
let c be Element of product J such that
{} is_>=_than c and
A6: for b being Element of product J st {} is_>=_than b holds b <= c;
now
let i be Element of I;
f.i = Top (J.i) & J.i is upper-bounded antisymmetric non empty
RelStr by A1,A2;
hence f.i >= c.i by YELLOW_0:45;
end;
then
A7: f >= c by WAYBEL_3:28;
for i being Element of I holds J.i is antisymmetric by A1;
then
A8: product J is antisymmetric by WAYBEL_3:30;
c >= f by A6,YELLOW_0:6;
hence c = f by A8,A7;
end;
A9: now
let a be Element of product J such that
{} is_>=_than a;
now
let i be Element of I;
f.i = Top (J.i) & J.i is upper-bounded antisymmetric non empty
RelStr by A1,A2;
hence f.i >= a.i by YELLOW_0:45;
end;
hence f >= a by WAYBEL_3:28;
end;
now
let b be Element of product J such that
{} is_>=_than b;
now
let i be Element of I;
f.i = Top (J.i) & J.i is upper-bounded antisymmetric non empty
RelStr by A1,A2;
hence f.i >= b.i by YELLOW_0:45;
end;
hence f >= b by WAYBEL_3:28;
end;
then ex_inf_of {}, product J by A4,A5;
then f = "/\"({}, product J) by A4,A9,YELLOW_0:def 10;
hence thesis by A2;
end;
theorem :: 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
proof
let I be non empty set, J be RelStr-yielding non-Empty reflexive-yielding
ManySortedSet of I such that
A1: for i being Element of I holds J.i is continuous complete LATTICE;
A2: for i being Element of I holds J.i is complete LATTICE by A1;
set pJ = product J;
reconsider pJ9 = pJ as complete LATTICE by A2,WAYBEL_3:31;
hereby
let x be Element of pJ;
reconsider x9 = x as Element of pJ9;
waybelow x9 is non empty;
hence waybelow x is non empty;
waybelow x9 is directed;
hence waybelow x is directed;
end;
pJ9 is up-complete;
hence pJ is up-complete;
let x be Element of pJ;
set swx = sup waybelow x;
now
thus dom x = I by WAYBEL_3:27;
thus dom swx = I by WAYBEL_3:27;
let i be object;
assume i in I;
then reconsider i9 = i as Element of I;
now
reconsider K = {i9} as finite Subset of I;
deffunc F(Element of I) = Bottom (J.$1);
let a be object;
consider g being ManySortedSet of I such that
A3: for i being Element of I holds g.i = F(i) from PBOOLE:sch 5;
set f = g+*(i, a);
hereby
assume a in pi(waybelow x, i9);
then consider f being Function such that
A4: f in waybelow x and
A5: a = f.i by CARD_3:def 6;
reconsider f as Element of pJ by A4;
f << x by A4,WAYBEL_3:7;
then f.i9 << x.i9 by A2,WAYBEL_3:33;
hence a in waybelow x.i9 by A5;
end;
A6: dom g = I by PARTFUN1:def 2;
then
A7: dom f = I by FUNCT_7:30;
assume
A8: a in waybelow x.i9;
now
let j be Element of I;
per cases;
suppose
i9 = j;
hence f.j is Element of J.j by A8,A6,FUNCT_7:31;
end;
suppose
i9 <> j;
then f.j = g.j by FUNCT_7:32
.= Bottom (J.j) by A3;
hence f.j is Element of J.j;
end;
end;
then reconsider f as Element of pJ by A7,WAYBEL_3:27;
A9: now
let j be Element of I;
per cases;
suppose
A10: i9 = j;
f.i9 = a by A6,FUNCT_7:31;
hence f.j << x.j by A8,A10,WAYBEL_3:7;
end;
suppose
A11: i9 <> j;
A12: J.j is complete LATTICE by A1;
f.j = g.j by A11,FUNCT_7:32
.= Bottom (J.j) by A3;
hence f.j << x.j by A12,WAYBEL_3:4;
end;
end;
now
let j be Element of I;
assume not j in K;
then j <> i9 by TARSKI:def 1;
hence f.j = g.j by FUNCT_7:32
.= Bottom (J.j) by A3;
end;
then f << x by A2,A9,WAYBEL_3:33;
then
A13: f in waybelow x;
a = f.i9 by A6,FUNCT_7:31;
hence a in pi(waybelow x, i9) by A13,CARD_3:def 6;
end;
then
A14: pi(waybelow x, i9) = waybelow (x.i9) by TARSKI:2;
swx.i9 = sup pi(waybelow x, i9) & J.i9 is
satisfying_axiom_of_approximation by A1,A2,WAYBEL_3:32;
hence x.i = swx.i by A14;
end;
hence thesis by FUNCT_1:2;
end;
begin :: Kernel projections and quotient lattices
theorem Th34:
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:]
proof
let L, T be continuous complete LATTICE, g be CLHomomorphism of L, T, SL be
Subset of [:L, L:] such that
A1: SL = [:g, g:]"(id the carrier of T);
set x = the Element of L;
A2: dom g = the carrier of L by FUNCT_2:def 1;
then
A3: [x, x] in [:dom g, dom g:] by ZFMISC_1:87;
[g.x, g.x] in id the carrier of T by RELAT_1:def 10;
then
dom [:g, g:] = [: dom g, dom g :] & [:g, g:].(x, x) in id the carrier of
T by A2,FUNCT_3:def 8;
then reconsider nSL = SL as non empty Subset of [:L, L:] by A1,A3,
FUNCT_1:def 7;
set pL = [:L, L:], pg = [:g, g:];
A4: g is infs-preserving directed-sups-preserving by WAYBEL16:def 1;
A5: the carrier of pL=[:the carrier of L,the carrier of L:] by YELLOW_3:def 2;
A6: subrelstr nSL is non empty;
A7: subrelstr SL is directed-sups-inheriting
proof
let X be directed Subset of subrelstr SL such that
A8: X <> {} and
A9: ex_sup_of X, pL;
reconsider X9 = X as directed non empty Subset of pL by A6,A8,YELLOW_2:7;
pg is directed-sups-preserving by A4,Th12;
then pg preserves_sup_of X9;
then
A10: sup (pg.:X9)=pg.sup X9 by A9;
X c= the carrier of subrelstr SL;
then X c= SL by YELLOW_0:def 15;
then
A11: pg.:X c= pg.:SL by RELAT_1:123;
pg.:SL c= id the carrier of T & ex_sup_of pg.:X9, [:T, T:] by A1,FUNCT_1:75
,YELLOW_0:17;
then
A12: sup (pg.:X9) in id the carrier of T by A11,Th14,XBOOLE_1:1;
consider x, y being object such that
A13: x in the carrier of L & y in the carrier of L and
A14: sup X9 = [x, y] by A5,ZFMISC_1:def 2;
[x, y] in [:dom g, dom g:] by A2,A13,ZFMISC_1:87;
then [x, y] in dom [:g, g:] by FUNCT_3:def 8;
then [x, y] in [:g, g:]"(id the carrier of T) by A14,A10,A12,FUNCT_1:def 7;
hence thesis by A1,A14,YELLOW_0:def 15;
end;
subrelstr SL is infs-inheriting
proof
let X be Subset of subrelstr SL such that
A15: ex_inf_of X, pL;
X c= the carrier of subrelstr SL;
then
A16: X c= SL by YELLOW_0:def 15;
then reconsider X9 = X as Subset of pL by XBOOLE_1:1;
A17: pg.:SL c= id the carrier of T & ex_inf_of pg.:X9, [:T, T:] by A1,
FUNCT_1:75,YELLOW_0:17;
pg is infs-preserving by A4,Th9;
then pg preserves_inf_of X9;
then
A18: inf (pg.:X9)=pg.inf X9 by A15;
pg.:X c= pg.:SL by A16,RELAT_1:123;
then
A19: inf (pg.:X9) in id the carrier of T by A17,Th13,XBOOLE_1:1;
consider x, y being object such that
A20: x in the carrier of L & y in the carrier of L and
A21: inf X9 = [x, y] by A5,ZFMISC_1:def 2;
[x, y] in [:dom g, dom g:] by A2,A20,ZFMISC_1:87;
then [x, y] in dom [:g, g:] by FUNCT_3:def 8;
then [x, y] in [:g, g:]"(id the carrier of T) by A21,A18,A19,FUNCT_1:def 7;
hence thesis by A1,A21,YELLOW_0:def 15;
end;
hence thesis by A7;
end;
:: 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
A1: R is Equivalence_Relation of the carrier of L;
func EqRel R -> Equivalence_Relation of the carrier of L equals
:Def1:
R;
correctness by A1;
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
R is Equivalence_Relation of the carrier
of L & subrelstr R is CLSubFrame of [:L, L:];
end;
theorem Th35:
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
proof
let L be complete LATTICE, R be non empty Subset of [:L, L:];
assume
A1: R is CLCongruence;
let x be Element of L;
set CRx = Class(EqRel R, x);
reconsider SR = [:CRx, {x}:] as Subset of [:L, L:];
R is Equivalence_Relation of the carrier of L by A1;
then
A2: R = EqRel R by Def1;
SR c= the carrier of subrelstr R
proof
let a be object;
assume a in SR;
then consider a1, a2 being object such that
A3: a1 in CRx and
A4: a2 in {x} and
A5: a = [a1, a2] by ZFMISC_1:def 2;
a2 = x by A4,TARSKI:def 1;
then a in R by A2,A3,A5,EQREL_1:19;
hence thesis by YELLOW_0:def 15;
end;
then reconsider SR9 = SR as Subset of subrelstr R;
A6: ex_inf_of SR, [:L, L:] by YELLOW_0:17;
subrelstr R is CLSubFrame of [:L, L:] by A1;
then
A7: "/\"(SR9, [:L, L:]) in the carrier of subrelstr R by A6,YELLOW_0:def 18;
A8: x in CRx by EQREL_1:20;
inf SR = [inf proj1 SR, inf proj2 SR] by Th7,YELLOW_0:17
.= [inf CRx, inf proj2 SR] by FUNCT_5:9
.= [inf CRx, inf {x}] by A8,FUNCT_5:9
.= [inf CRx, x] by YELLOW_0:39;
hence thesis by A7,YELLOW_0:def 15;
end;
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
A1: R is CLCongruence;
func kernel_op R -> kernel Function of L, L means
:Def3:
for x being Element of L holds it.x = inf Class(EqRel R, x);
existence
proof
deffunc F(Element of L) = inf Class(EqRel R, $1);
consider k being Function of the carrier of L, the carrier of L such that
A2: for x being Element of L holds k.x = F(x) from FUNCT_2:sch 4;
reconsider k as Function of L, L;
R is Equivalence_Relation of the carrier of L by A1;
then
A3: R = EqRel R by Def1;
A4: subrelstr R is CLSubFrame of [:L, L:] by A1;
A5: k is monotone
proof
let x, y be Element of L such that
A6: x <= y;
set CRy = Class(EqRel R, y);
set CRx = Class(EqRel R, x);
reconsider SR = {[inf CRx, x], [inf CRy, y]} as Subset of [:L, L:];
A7: inf SR = [inf proj1 SR, inf proj2 SR] by Th7,YELLOW_0:17
.= [inf {inf CRx, inf CRy}, inf proj2 SR] by FUNCT_5:13
.= [inf {inf CRx, inf CRy}, inf {x, y}] by FUNCT_5:13;
[inf CRx, x] in R & [inf CRy, y] in R by A1,Th35;
then SR c= R by ZFMISC_1:32;
then reconsider SR9 = SR as Subset of subrelstr R by YELLOW_0:def 15;
ex_inf_of SR, [:L, L:] by YELLOW_0:17;
then
A8: "/\"(SR9, [:L, L:]) in the carrier of subrelstr R by A4,YELLOW_0:def 18;
inf {x, y} = x"/\"y by YELLOW_0:40
.= x by A6,YELLOW_0:25;
then [inf {inf CRx, inf CRy}, x] in R by A7,A8,YELLOW_0:def 15;
then inf {inf CRx, inf CRy} in CRx by A3,EQREL_1:19;
then
A9: inf CRx <= inf {inf CRx, inf CRy} by YELLOW_2:22;
inf CRy in {inf CRx, inf CRy} by TARSKI:def 2;
then
A10: inf {inf CRx, inf CRy} <= inf CRy by YELLOW_2:22;
k.x = inf CRx & k.y = inf CRy by A2;
hence k.x <= k.y by A9,A10,YELLOW_0:def 2;
end;
now
let x be Element of L;
set CRx = Class(EqRel R, x);
[inf CRx, x] in R by A1,Th35;
then inf CRx in CRx by A3,EQREL_1:19;
then
A11: Class(EqRel R, inf CRx) = CRx by EQREL_1:23;
A12: k.x = inf CRx by A2;
then k.(k.x) = inf Class(EqRel R, inf CRx) by A2;
hence (k*k).x = k.x by A12,A11,FUNCT_2:15;
end;
then k*k = k by FUNCT_2:63;
then k is idempotent by QUANTAL1:def 9;
then
A13: k is projection by A5;
now
let x be Element of L;
set CRx = Class(EqRel R, x);
x in CRx & inf CRx is_<=_than CRx by EQREL_1:20,YELLOW_0:33;
then
A14: inf CRx <= x;
k.x = inf Class(EqRel R, x) by A2;
hence k.x <= id(L).x by A14,FUNCT_1:18;
end;
then k <= id (L) by YELLOW_2:9;
then reconsider k as kernel Function of L, L by A13,WAYBEL_1:def 15;
take k;
thus thesis by A2;
end;
uniqueness
proof
let it1, it2 be kernel Function of L, L such that
A15: for x being Element of L holds it1.x = inf Class(EqRel R, x) and
A16: for x being Element of L holds it2.x = inf Class(EqRel R, x);
now
let x be object;
assume x in the carrier of L;
then reconsider x9 = x as Element of L;
thus it1.x = inf Class(EqRel R, x9) by A15
.= it2.x by A16;
end;
hence it1 = it2 by FUNCT_2:12;
end;
end;
theorem Th36: :: 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)
proof
let L be complete LATTICE, R be non empty Subset of [:L, L:];
set k = kernel_op R;
set cL = the carrier of L;
A1: dom k = cL by FUNCT_2:def 1;
assume
A2: R is CLCongruence;
then
A3: R is Equivalence_Relation of the carrier of L;
then
A4: EqRel R = R by Def1;
A5: subrelstr R is CLSubFrame of [:L, L:] by A2;
thus k is directed-sups-preserving
proof
let D be Subset of L such that
A6: D is non empty directed and
ex_sup_of D, L;
consider e being object such that
A7: e in D by A6,XBOOLE_0:def 1;
set S = {[k.x, x] where x is Element of L : x in D};
A8: S c= R
proof
let x be object;
assume x in S;
then consider a being Element of L such that
A9: x = [k.a, a] and
a in D;
k.a = inf Class(EqRel R, a) by A2,Def3;
hence thesis by A2,A9,Th35;
end;
then reconsider S9 = S as Subset of subrelstr R by YELLOW_0:def 15;
reconsider S as Subset of [:L, L:] by A8,XBOOLE_1:1;
thus ex_sup_of k.:D, L by YELLOW_0:17;
set d = sup D;
set ds = sup (k.:D);
A10: the carrier of subrelstr R = R & ex_sup_of S, [:L, L:] by YELLOW_0:17
,def 15;
reconsider e as Element of L by A7;
A11: [k.e, e] in S by A7;
A12: S9 is directed
proof
let x, y be Element of subrelstr R;
assume that
A13: x in S9 and
A14: y in S9;
consider a being Element of L such that
A15: x = [k.a, a] and
A16: a in D by A13;
consider b being Element of L such that
A17: y = [k.b, b] and
A18: b in D by A14;
consider c being Element of L such that
A19: c in D and
A20: a <= c and
A21: b <= c by A6,A16,A18;
set z = [k.c, c];
z in S9 by A19;
then reconsider z as Element of subrelstr R;
take z;
thus z in S9 by A19;
k.a <= k.c by A20,WAYBEL_1:def 2;
then [k.a, a] <= [k.c, c] by A20,YELLOW_3:11;
hence x <= z by A15,YELLOW_0:60;
k.b <= k.c by A21,WAYBEL_1:def 2;
then [k.b, b] <= [k.c, c] by A21,YELLOW_3:11;
hence y <= z by A17,YELLOW_0:60;
end;
now
let x be object;
hereby
assume x in proj1 S;
then consider y being object such that
A22: [x, y] in S by XTUPLE_0:def 12;
consider a being Element of L such that
A23: [x, y] = [k.a, a] and
A24: a in D by A22;
x = k.a by A23,XTUPLE_0:1;
hence x in k.:D by A1,A24,FUNCT_1:def 6;
end;
assume x in k.:D;
then consider y being object such that
A25: y in dom k and
A26: y in D and
A27: x = k.y by FUNCT_1:def 6;
reconsider y as Element of L by A25;
[k.y, y] in S by A26;
hence x in proj1 S by A27,XTUPLE_0:def 12;
end;
then
A28: proj1 S = k.:D by TARSKI:2;
now
let x be object;
hereby
assume x in proj2 S;
then consider y being object such that
A29: [y, x] in S by XTUPLE_0:def 13;
ex a being Element of L st [y, x] = [k.a, a] & a in D by A29;
hence x in D by XTUPLE_0:1;
end;
assume
A30: x in D;
then reconsider x9 = x as Element of L;
[k.x9, x9] in S by A30;
hence x in proj2 S by XTUPLE_0:def 13;
end;
then proj2 S = D by TARSKI:2;
then sup S = [ds, d] by A28,Th8,YELLOW_0:17;
then [ds, d] in R by A5,A10,A11,A12,WAYBEL_0:def 4;
then
A31: ds in Class(EqRel R, d) by A4,EQREL_1:19;
k.:D is_<=_than k.d
proof
let b be Element of L;
assume b in k.:D;
then consider a being object such that
A32: a in dom k and
A33: a in D and
A34: b = k.a by FUNCT_1:def 6;
reconsider a as Element of L by A32;
D is_<=_than d by YELLOW_0:32;
then a <= d by A33;
hence b <= k.d by A34,WAYBEL_1:def 2;
end;
then
A35: ds <= k.d by YELLOW_0:32;
k.d = inf Class(EqRel R, d) by A2,Def3;
then k.d <= ds by A31,YELLOW_2:22;
hence thesis by A35,YELLOW_0:def 3;
end;
now
let x be object;
hereby
assume
A36: x in R;
then x in the carrier of [:L, L:];
then x in [:cL, cL:] by YELLOW_3:def 2;
then consider x1, x2 being object such that
A37: x1 in cL & x2 in cL and
A38: x = [x1, x2] by ZFMISC_1:def 2;
reconsider x1, x2 as Element of L by A37;
A39: k.x1=inf Class(EqRel R, x1) & k.x2 = inf Class(EqRel R, x2) by A2,Def3;
x1 in Class(EqRel R, x2) by A4,A36,A38,EQREL_1:19;
then k.x1 = k.x2 by A39,EQREL_1:23;
then
A40: [k.x1, k.x2] in id cL by RELAT_1:def 10;
dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 8;
then
A41: [x1, x2] in dom [:k, k:] by A1,ZFMISC_1:87;
[:k, k:].(x1, x2) = [k.x1, k.x2] by A1,FUNCT_3:def 8;
hence x in [:k, k:]"(id cL) by A38,A40,A41,FUNCT_1:def 7;
end;
assume
A42: x in [:k, k:]"(id cL);
then
A43: [:k, k:].x in id cL by FUNCT_1:def 7;
x in dom [:k, k:] by A42,FUNCT_1:def 7;
then x in [:dom k, dom k:] by FUNCT_3:def 8;
then consider x1, x2 being object such that
A44: x1 in dom k & x2 in dom k and
A45: x = [x1, x2] by ZFMISC_1:def 2;
reconsider x1, x2 as Element of L by A44;
[:k, k:].(x1, x2) = [k.x1, k.x2] by A44,FUNCT_3:def 8;
then
A46: k.x1 = k.x2 by A43,A45,RELAT_1:def 10;
k.x1=inf Class(EqRel R, x1) by A2,Def3;
then [k.x1, x1] in R by A2,Th35;
then
A47: [x1, k.x1] in R by A3,EQREL_1:6;
k.x2 = inf Class(EqRel R, x2) by A2,Def3;
then [k.x2, x2] in R by A2,Th35;
hence x in R by A3,A45,A46,A47,EQREL_1:7;
end;
hence thesis by TARSKI:2;
end;
theorem Th37: :: 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
proof
let L be continuous complete LATTICE, R be Subset of [:L, L:], k be kernel
Function of L, L such that
A1: k is directed-sups-preserving and
A2: R = [:k, k:]"(id the carrier of L);
set ER = EqRel R;
R is Equivalence_Relation of the carrier of L by A2,Th2;
then
A3: ER = R by Def1;
reconsider rngk = rng k as non empty set;
defpred P[set,set] means ex x, y being Element of L st $1 = Class(ER, x) &
$2 = Class(ER, y) & k.x <= k.y;
set xx = the Element of L;
set cL = the carrier of L;
Class(ER, xx) in Class ER by EQREL_1:def 3;
then reconsider CER = Class ER as non empty Subset-Family of cL;
consider LR being non empty strict RelStr such that
A4: the carrier of LR = CER and
A5: for a, b being Element of LR holds a <= b iff P[a,b] from YELLOW_0:
sch 1;
defpred P[set, set] means ex a being Element of cL st $1 = Class(ER, a) & $2
= k.a;
A6: dom k = cL by FUNCT_2:def 1;
A7: for x being Element of CER ex y being Element of rngk st P[x, y]
proof
let x be Element of CER;
consider y being object such that
A8: y in cL and
A9: x = Class(ER, y) by EQREL_1:def 3;
reconsider y as Element of L by A8;
reconsider ky = k.y as Element of rngk by A6,FUNCT_1:def 3;
take ky;
thus thesis by A9;
end;
consider f being Function of CER, rngk such that
A10: for x being Element of CER holds P[x, f.x] from FUNCT_2:sch 3(A7);
A11: dom [:k, k:] = [:cL, cL:] by A6,FUNCT_3:def 8;
A12: for a, b being Element of cL holds Class(ER, a) = Class(ER, b) iff k.a
= k.b
proof
let a, b be Element of cL;
hereby
assume Class(ER, a) = Class(ER, b);
then a in Class(ER, b) by EQREL_1:23;
then [a, b] in R by A3,EQREL_1:19;
then [:k, k:].(a, b) in id cL by A2,FUNCT_1:def 7;
then [k.a, k.b] in id cL by A6,FUNCT_3:def 8;
hence k.a = k.b by RELAT_1:def 10;
end;
assume k.a = k.b;
then [k.a, k.b] in id cL by RELAT_1:def 10;
then [a, b] in [:cL, cL:] & [:k, k:].(a, b) in id cL by A6,FUNCT_3:def 8
,ZFMISC_1:def 2;
then [a, b] in ER by A2,A3,A11,FUNCT_1:def 7;
then a in Class(ER, b) by EQREL_1:19;
hence thesis by EQREL_1:23;
end;
A13: for x being Element of L holds f.Class(ER, x) = k.x
proof
let x be Element of L;
reconsider CERx = Class(ER, x) as Element of CER by EQREL_1:def 3;
ex a being Element of cL st CERx = Class(ER, a) & f.CERx = k.a by A10;
hence thesis by A12;
end;
A14: for x being Element of LR ex a being Element of L st x = Class(ER, a)
proof
let x be Element of LR;
x in CER by A4;
then consider a being object such that
A15: a in cL and
A16: x = Class(ER, a) by EQREL_1:def 3;
reconsider a as Element of L by A15;
take a;
thus thesis by A16;
end;
now
let x1, x2 be object;
assume that
A17: x1 in CER and
A18: x2 in CER and
A19: f.x1 = f.x2;
reconsider x19 = x1 as Element of LR by A4,A17;
consider a being Element of L such that
A20: x19 = Class(ER, a) by A14;
reconsider x29 = x2 as Element of LR by A4,A18;
consider b being Element of L such that
A21: x29 = Class(ER, b) by A14;
A22: f.x29 = k.b by A13,A21;
f.x19 = k.a by A13,A20;
hence x1 = x2 by A12,A19,A20,A21,A22;
end;
then
A23: f is one-to-one by FUNCT_2:19;
set tIR = the InternalRel of LR;
A24: dom f = CER by FUNCT_2:def 1;
reconsider f as Function of LR, Image k by A4,YELLOW_0:def 15;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A25: x in dom f and
A26: y = f.x by FUNCT_1:def 3;
reconsider x as Element of LR by A25;
consider a being Element of L such that
A27: x = Class(ER, a) by A14;
f.x = k.a by A13,A27;
hence y in rngk by A6,A26,FUNCT_1:def 3;
end;
assume y in rngk;
then consider x being object such that
A28: x in dom k and
A29: y = k.x by FUNCT_1:def 3;
reconsider x as Element of L by A28;
Class(ER, x) in CER & f.Class(ER, x) = k.x by A13,EQREL_1:def 3;
hence y in rng f by A24,A29,FUNCT_1:def 3;
end;
then
A30: the carrier of Image k = rngk & rng f = rngk by TARSKI:2,YELLOW_0:def 15;
for x, y being Element of LR holds x <= y iff f.x <= f.y
proof
let x, y be Element of LR;
x in CER by A4;
then consider a being object such that
A31: a in cL and
A32: x = Class(ER, a) by EQREL_1:def 3;
hereby
assume x <= y;
then consider c, d being Element of L such that
A33: x = Class(ER, c) & y = Class(ER, d) and
A34: k.c <= k.d by A5;
f.x = k.c & f.y = k.d by A13,A33;
hence f.x <= f.y by A34,YELLOW_0:60;
end;
reconsider a as Element of L by A31;
assume
A35: f.x <= f.y;
y in CER by A4;
then consider b being object such that
A36: b in cL and
A37: y = Class(ER, b) by EQREL_1:def 3;
reconsider b as Element of L by A36;
A38: f.y = k.b by A13,A37;
f.x = k.a by A13,A32;
then k.a <= k.b by A38,A35,YELLOW_0:59;
hence thesis by A5,A32,A37;
end;
then
A39: f is isomorphic by A23,A30,WAYBEL_0:66;
then
A40: LR, Image k are_isomorphic;
then Image k, LR are_isomorphic by WAYBEL_1:6;
then reconsider LR as non empty strict Poset by Th15,Th16,Th17;
Image k is complete by WAYBEL_1:54;
then reconsider LR as complete non empty strict Poset by A40,Th18,WAYBEL_1:6;
reconsider LR as complete strict LATTICE;
Image k is continuous LATTICE by A1,WAYBEL15:14;
then reconsider LR as continuous complete strict LATTICE by A40,WAYBEL15:9
,WAYBEL_1:6;
reconsider f9 = ((f qua Function)") as Function of Image k, LR by A23,A30,
FUNCT_2:25;
set IR = {[Class(ER, x), Class(ER, y)] where x, y is Element of L : k.x <= k
.y };
A41: f9 is isomorphic by A39,WAYBEL_0:68;
then
A42: corestr k is infs-preserving & f9 is infs-preserving by WAYBEL13:20
,WAYBEL_1:56;
take LR;
thus the carrier of LR = Class ER by A4;
now
let z be object;
hereby
assume
A43: z in tIR;
then consider a, b being object such that
A44: a in CER & b in CER and
A45: z = [a, b] by A4,ZFMISC_1:def 2;
reconsider a, b as Element of LR by A4,A44;
a <= b by A43,A45,ORDERS_2:def 5;
then ex x, y being Element of L st a = Class(ER, x) & b = Class(ER, y) &
k.x <= k.y by A5;
hence z in IR by A45;
end;
assume z in IR;
then consider x, y being Element of L such that
A46: z = [Class(ER, x), Class(ER, y)] and
A47: k.x <= k.y;
reconsider b = Class(ER, y) as Element of LR by A4,EQREL_1:def 3;
reconsider a = Class(ER, x) as Element of LR by A4,EQREL_1:def 3;
a <= b by A5,A47;
hence z in tIR by A46,ORDERS_2:def 5;
end;
hence the InternalRel of LR = {[Class(ER, x), Class(ER, y)] where x, y is
Element of L : k.x <= k.y } by TARSKI:2;
let g be Function of L, LR such that
A48: for x being Element of L holds g.x = Class(ER, x);
now
let x be object;
assume
A49: x in cL;
then reconsider x9 = x as Element of L;
A50: f.Class(ER, x9) = k.x9 & Class(ER, x9) in CER by A13,EQREL_1:def 3;
dom corestr k = cL by FUNCT_2:def 1;
hence (f9*corestr k).x = f9.((corestr k).x) by A49,FUNCT_1:13
.= f9.(k.x) by WAYBEL_1:30
.= Class(ER, x9) by A24,A23,A50,FUNCT_1:32
.= g.x by A48;
end;
then
A51: g = f9*corestr k by FUNCT_2:12;
A52: corestr k is directed-sups-preserving by A1,Th22;
reconsider f9 as sups-preserving Function of Image k, LR by A41,WAYBEL13:20;
f9 is directed-sups-preserving;
then
A53: g is directed-sups-preserving by A51,A52,WAYBEL15:11;
g is infs-preserving by A51,A42,Th25;
hence thesis by A53,WAYBEL16:def 1;
end;
theorem Th38: :: 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:]
proof
let L be continuous complete LATTICE, R be Subset of [:L, L:];
assume R is Equivalence_Relation of the carrier of L;
then
A1: EqRel R = R by Def1;
set ER = EqRel R;
given LR being continuous complete LATTICE such that
A2: the carrier of LR = Class EqRel R and
A3: 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;
deffunc F(object) = Class(ER, $1);
set CER = Class ER;
set cL = the carrier of L, cLR = the carrier of LR;
A4: for x be object st x in cL holds F(x) in CER by EQREL_1:def 3;
consider g being Function of cL, CER such that
A5: for x being object st x in cL holds g.x = F(x) from FUNCT_2:sch 2(A4);
reconsider g as Function of L, LR by A2;
set k = g;
A6: dom g = cL by FUNCT_2:def 1;
now
let x be object;
hereby
assume
A7: x in R;
then x in the carrier of [:L, L:];
then x in [:cL, cL:] by YELLOW_3:def 2;
then consider x1, x2 being object such that
A8: x1 in cL & x2 in cL and
A9: x = [x1, x2] by ZFMISC_1:def 2;
reconsider x1, x2 as Element of L by A8;
A10: k.x1 = Class(EqRel R, x1) & k.x2 = Class(EqRel R, x2) by A5;
x1 in Class(EqRel R, x2) by A1,A7,A9,EQREL_1:19;
then k.x1 = k.x2 by A10,EQREL_1:23;
then
A11: [k.x1, k.x2] in id cLR by RELAT_1:def 10;
dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 8;
then
A12: [x1, x2] in dom [:k, k:] by A6,ZFMISC_1:87;
[:k, k:].(x1, x2) = [k.x1, k.x2] by A6,FUNCT_3:def 8;
hence x in [:k, k:]"(id cLR) by A9,A11,A12,FUNCT_1:def 7;
end;
assume
A13: x in [:k, k:]"(id cLR);
then
A14: [:k, k:].x in id cLR by FUNCT_1:def 7;
x in dom [:k, k:] by A13,FUNCT_1:def 7;
then x in [:dom k, dom k:] by FUNCT_3:def 8;
then consider x1, x2 being object such that
A15: x1 in dom k & x2 in dom k and
A16: x = [x1, x2] by ZFMISC_1:def 2;
reconsider x1, x2 as Element of L by A15;
A17: k.x1=Class(EqRel R, x1) & k.x2 = Class(EqRel R, x2) by A5;
[:k, k:].(x1, x2) = [k.x1, k.x2] by A15,FUNCT_3:def 8;
then k.x1 = k.x2 by A14,A16,RELAT_1:def 10;
then x1 in Class(ER, x2) by A17,EQREL_1:23;
hence x in R by A1,A16,EQREL_1:19;
end;
then
A18: R = [:g, g:]"(id the carrier of LR) by TARSKI:2;
for x being Element of L holds g.x = Class(EqRel R, x) by A5;
then g is CLHomomorphism of L, LR by A3;
hence thesis by A18,Th34;
end;
registration
let L be non empty reflexive RelStr;
cluster directed-sups-preserving kernel for Function of L, L;
existence
proof
reconsider k = id L as directed-sups-preserving kernel Function of L, L;
take k;
thus thesis;
end;
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
[:k, k:]"(id
the carrier of L);
coherence
proof
set cL = the carrier of L;
set x = the Element of cL;
A1: dom k = cL by FUNCT_2:def 1;
then
A2: [k.x, k.x] in id cL & [:k, k:].(x,x) = [k.x, k.x] by FUNCT_3:def 8
,RELAT_1:def 10;
dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 8;
then [x, x] in dom [:k, k:] by A1,ZFMISC_1:def 2;
hence thesis by A2,FUNCT_1:def 7;
end;
end;
theorem
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 by Th2;
theorem Th40: :: 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
proof
let L be continuous complete LATTICE, k be directed-sups-preserving kernel
Function of L, L;
set R = kernel_congruence k;
thus
A1: R is Equivalence_Relation of the carrier of L by Th2;
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 by Th37;
hence thesis by A1,Th38;
end;
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
A1: R is CLCongruence;
func L ./. R -> continuous complete strict LATTICE means
:Def5:
the carrier
of it = Class EqRel R & for x, y being Element of it holds x <= y iff "/\"(x, L
) <= "/\"(y, L);
existence
proof
set k = kernel_op R;
k is directed-sups-preserving & R = [:k, k:]"(id the carrier of L) by A1
,Th36;
then consider LR being continuous complete strict LATTICE such that
A2: the carrier of LR = Class EqRel R and
A3: the InternalRel of LR = {[Class(EqRel R, x), Class(EqRel R, y)]
where x, y is Element of L : k.x <= k.y } and
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 by Th37;
take LR;
thus the carrier of LR = Class EqRel R by A2;
let x, y be Element of LR;
x in the carrier of LR;
then consider u being object such that
A4: u in the carrier of L and
A5: x = Class(EqRel R, u) by A2,EQREL_1:def 3;
y in the carrier of LR;
then consider v being object such that
A6: v in the carrier of L and
A7: y = Class(EqRel R, v) by A2,EQREL_1:def 3;
hereby
assume x <= y;
then [x, y] in the InternalRel of LR by ORDERS_2:def 5;
then consider u9, v9 being Element of L such that
A8: [x, y] = [Class(EqRel R, u9), Class(EqRel R, v9)] and
A9: k.u9 <= k.v9 by A3;
A10: x = Class(EqRel R, u9) & y = Class(EqRel R, v9) by A8,XTUPLE_0:1;
k.u9 = inf Class(EqRel R, u9) by A1,Def3;
hence "/\"(x, L) <= "/\"(y, L) by A1,A9,A10,Def3;
end;
assume
A11: "/\"(x, L) <= "/\"(y, L);
reconsider u, v as Element of L by A4,A6;
k.u = inf Class(EqRel R, u) & k.v = inf Class(EqRel R, v) by A1,Def3;
then [x, y] in the InternalRel of LR by A3,A5,A7,A11;
hence thesis by ORDERS_2:def 5;
end;
uniqueness
proof
let LR1, LR2 be continuous complete strict LATTICE such that
A12: the carrier of LR1 = Class EqRel R and
A13: for x, y being Element of LR1 holds x <= y iff "/\"(x, L) <= "/\"
(y, L) and
A14: the carrier of LR2 = Class EqRel R and
A15: for x, y being Element of LR2 holds x <= y iff "/\"(x, L) <= "/\" (y, L);
set cLR2 = the carrier of LR2;
set cLR1 = the carrier of LR1;
now
let z be object;
hereby
assume
A16: z in the InternalRel of LR1;
then consider x, y being object such that
A17: x in cLR1 & y in cLR1 and
A18: z = [x, y] by ZFMISC_1:def 2;
reconsider x, y as Element of LR1 by A17;
reconsider x9 = x, y9 = y as Element of LR2 by A12,A14;
x <= y by A16,A18,ORDERS_2:def 5;
then "/\"(x, L) <= "/\"(y, L) by A13;
then x9 <= y9 by A15;
hence z in the InternalRel of LR2 by A18,ORDERS_2:def 5;
end;
assume
A19: z in the InternalRel of LR2;
then consider x, y being object such that
A20: x in cLR2 & y in cLR2 and
A21: z = [x, y] by ZFMISC_1:def 2;
reconsider x, y as Element of LR2 by A20;
reconsider x9 = x, y9 = y as Element of LR1 by A12,A14;
x <= y by A19,A21,ORDERS_2:def 5;
then "/\"(x, L) <= "/\"(y, L) by A15;
then x9 <= y9 by A13;
hence z in the InternalRel of LR1 by A21,ORDERS_2:def 5;
end;
hence thesis by A12,A14,TARSKI:2;
end;
end;
theorem
:: 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)
proof
let L be continuous complete LATTICE, R be non empty Subset of [:L, L:];
assume R is CLCongruence;
then
A1: the carrier of (L./.R) = Class EqRel R by Def5;
let x be set;
hereby
assume x is Element of L./.R;
then x in Class EqRel R by A1;
then consider y being object such that
A2: y in the carrier of L and
A3: x = Class(EqRel R, y) by EQREL_1:def 3;
reconsider y as Element of L by A2;
take y;
thus x = Class(EqRel R, y) by A3;
end;
given y being Element of L such that
A4: x = Class(EqRel R, y);
thus thesis by A1,A4,EQREL_1:def 3;
end;
theorem
:: 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 by Th36;
theorem
:: 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
proof
let L be continuous complete LATTICE, k be directed-sups-preserving kernel
Function of L, L;
set kc = kernel_congruence k, cL = the carrier of L, km = kernel_op kc;
A1: dom k = cL by FUNCT_2:def 1;
A2: km <= id L by WAYBEL_1:def 15;
A3: k <= id L by WAYBEL_1:def 15;
A4: kc is CLCongruence by Th40;
then
A5: kc = [:km, km:]"(id cL) by Th36;
reconsider kc9 = kc as Equivalence_Relation of cL by A4;
field kc9 = cL by ORDERS_1:12;
then
A6: kc9 is_transitive_in cL by RELAT_2:def 16;
A7: dom [:km, km:] = [:dom km, dom km:] by FUNCT_3:def 8;
A8: dom km = cL by FUNCT_2:def 1;
A9: dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 8;
now
let x be object;
assume x in cL;
then reconsider x9 = x as Element of L;
A10: k.(k.x9) = (k*k).x9 by A1,FUNCT_1:13
.= k.x9 by QUANTAL1:def 9;
A11: [k.x9, k.x9] in id cL & [:k, k:].(k.x9, x9) = [k.(k.x9), k.x9] by A1,
FUNCT_3:def 8,RELAT_1:def 10;
[k.x9, x9] in dom [:k, k:] by A1,A9,ZFMISC_1:def 2;
then
A12: [k.x9, x9] in kc by A10,A11,FUNCT_1:def 7;
A13: km.(km.x9) = (km*km).x9 by A8,FUNCT_1:13
.= km.x9 by QUANTAL1:def 9;
km.(k.x9) <= (id L).(k.x9) by A2,YELLOW_2:9;
then
A14: km.(k.x9) <= k.x9 by FUNCT_1:18;
A15: [km.x9, km.x9] in id cL & [:km, km:].(x9, km.x9) = [km.x9, km.(km.x9)
] by A8,FUNCT_3:def 8,RELAT_1:def 10;
[x9, km.x9] in dom [:km, km:] by A8,A7,ZFMISC_1:def 2;
then [x9, km.x9] in kc by A5,A13,A15,FUNCT_1:def 7;
then
A16: [k.x9, km.x9] in kc by A6,A12;
then [:k, k:].(k.x9, km.x9) in id cL by FUNCT_1:def 7;
then [k.(k.x9), k.(km.x9)] in id cL by A1,FUNCT_3:def 8;
then
A17: k.(km.x9) = k.(k.x9) by RELAT_1:def 10
.= (k*k).x9 by A1,FUNCT_1:13
.= k.x9 by QUANTAL1:def 9;
[:km, km:].(k.x9, km.x9) in id cL by A5,A16,FUNCT_1:def 7;
then [km.(k.x9), km.(km.x9)] in id cL by A8,FUNCT_3:def 8;
then
A18: km.(k.x9) = km.(km.x9) by RELAT_1:def 10
.= (km*km).x9 by A8,FUNCT_1:13
.= km.x9 by QUANTAL1:def 9;
k.(km.x9) <= (id L).(km.x9) by A3,YELLOW_2:9;
then k.(km.x9) <= km.x9 by FUNCT_1:18;
hence k.x = km.x by A17,A18,A14,YELLOW_0:def 3;
end;
hence thesis by FUNCT_2:12;
end;
theorem
:: 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
proof
let L be continuous complete LATTICE, p be projection Function of L, L such
that
A1: p is infs-preserving;
reconsider Lc = {c where c is Element of L: c <= p.c} as non empty Subset of
L by WAYBEL_1:43;
reconsider pc = p|Lc as Function of subrelstr Lc, subrelstr Lc by WAYBEL_1:45
;
A2: subrelstr Lc is infs-inheriting by A1,WAYBEL_1:51;
then
A3: subrelstr Lc is complete by YELLOW_2:30;
A4: pc is infs-preserving
proof
let X be Subset of subrelstr Lc;
assume ex_inf_of X, subrelstr Lc;
thus ex_inf_of pc.:X, subrelstr Lc by A3,YELLOW_0:17;
the carrier of subrelstr Lc = Lc by YELLOW_0:def 15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
A5: ex_inf_of X9, L & p preserves_inf_of X9 by A1,YELLOW_0:17;
X c= the carrier of subrelstr Lc;
then X c= Lc by YELLOW_0:def 15;
then
A6: pc.:X = p.:X by RELAT_1:129;
A7: ex_inf_of X, L by YELLOW_0:17;
then "/\"(X9,L) in the carrier of subrelstr Lc by A2;
then
A8: dom pc = the carrier of subrelstr Lc & inf X9 = inf X by A7,FUNCT_2:def 1
,YELLOW_0:63;
ex_inf_of p.:X, L & "/\"(pc.:X,L) in the carrier of subrelstr Lc by A2,
YELLOW_0:17;
hence inf (pc.:X) = inf (p.:X) by A6,YELLOW_0:63
.= p.inf X9 by A5
.= pc.inf X by A8,FUNCT_1:47;
end;
reconsider cpc = corestr pc as Function of subrelstr Lc, Image pc;
A9: the carrier of subrelstr rng p = rng p by YELLOW_0:def 15
.= rng pc by WAYBEL_1:44
.= the carrier of subrelstr rng pc by YELLOW_0:def 15;
subrelstr rng pc is full SubRelStr of L by WAYBEL15:1;
then
A10: Image p = Image pc by A9,YELLOW_0:57;
pc is closure by WAYBEL_1:47;
then
A11: cpc is sups-preserving by WAYBEL_1:55;
subrelstr Lc is sups-inheriting SubRelStr of L by WAYBEL_1:49;
then subrelstr Lc is continuous LATTICE by A2,WAYBEL_5:28;
hence Image p is continuous LATTICE by A3,A10,A4,A11,Th19,WAYBEL_5:33;
thus thesis by A1,A2,WAYBEL_1:51;
end;