let L be complete continuous LATTICE; for R being Subset of [:L,L:]
for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous 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 ) )
let R be Subset of [:L,L:]; for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous 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 ) )
let k be kernel Function of L,L; ( k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) implies ex LR being strict complete continuous 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 ) ) )
assume that
A1:
k is directed-sups-preserving
and
A2:
R = [:k,k:] " (id the carrier of L)
; ex LR being strict complete continuous 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 ) )
set ER = EqRel R;
R is Equivalence_Relation of the carrier of L
by A2, Th2;
then A3:
EqRel R = R
by Def1;
reconsider rngk = rng k as non empty set ;
defpred S1[ set , set ] means ex x, y being Element of L st
( $1 = Class ((EqRel R),x) & $2 = Class ((EqRel R),y) & k . x <= k . y );
set xx = the Element of L;
set cL = the carrier of L;
Class ((EqRel R), the Element of L) in Class (EqRel R)
by EQREL_1:def 3;
then reconsider CER = Class (EqRel R) as non empty Subset-Family of the carrier of L ;
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 S1[a,b] )
from YELLOW_0:sch 1();
defpred S2[ set , set ] means ex a being Element of the carrier of L st
( $1 = Class ((EqRel R),a) & $2 = k . a );
A6:
dom k = the carrier of L
by FUNCT_2:def 1;
A7:
for x being Element of CER ex y being Element of rngk st S2[x,y]
consider f being Function of CER,rngk such that
A10:
for x being Element of CER holds S2[x,f . x]
from FUNCT_2:sch 3(A7);
A11:
dom [:k,k:] = [: the carrier of L, the carrier of L:]
by A6, FUNCT_3:def 8;
A12:
for a, b being Element of the carrier of L holds
( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b )
proof
let a,
b be
Element of the
carrier of
L;
( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b )
hereby ( k . a = k . b implies Class ((EqRel R),a) = Class ((EqRel R),b) )
assume
Class (
(EqRel R),
a)
= Class (
(EqRel R),
b)
;
k . a = k . bthen
a in Class (
(EqRel R),
b)
by EQREL_1:23;
then
[a,b] in R
by A3, EQREL_1:19;
then
[:k,k:] . (
a,
b)
in id the
carrier of
L
by A2, FUNCT_1:def 7;
then
[(k . a),(k . b)] in id the
carrier of
L
by A6, FUNCT_3:def 8;
hence
k . a = k . b
by RELAT_1:def 10;
verum
end;
assume
k . a = k . b
;
Class ((EqRel R),a) = Class ((EqRel R),b)
then
[(k . a),(k . b)] in id the
carrier of
L
by RELAT_1:def 10;
then
(
[a,b] in [: the carrier of L, the carrier of L:] &
[:k,k:] . (
a,
b)
in id the
carrier of
L )
by A6, FUNCT_3:def 8, ZFMISC_1:def 2;
then
[a,b] in EqRel R
by A2, A3, A11, FUNCT_1:def 7;
then
a in Class (
(EqRel R),
b)
by EQREL_1:19;
hence
Class (
(EqRel R),
a)
= Class (
(EqRel R),
b)
by EQREL_1:23;
verum
end;
A13:
for x being Element of L holds f . (Class ((EqRel R),x)) = k . x
A14:
for x being Element of LR ex a being Element of L st x = Class ((EqRel R),a)
now for x1, x2 being object st x1 in CER & x2 in CER & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in CER & x2 in CER & f . x1 = f . x2 implies x1 = x2 )assume that A17:
x1 in CER
and A18:
x2 in CER
and A19:
f . x1 = f . x2
;
x1 = x2reconsider x19 =
x1 as
Element of
LR by A4, A17;
consider a being
Element of
L such that A20:
x19 = Class (
(EqRel R),
a)
by A14;
reconsider x29 =
x2 as
Element of
LR by A4, A18;
consider b being
Element of
L such that A21:
x29 = Class (
(EqRel R),
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;
verum 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 = f as Function of LR,(Image k) by A4, YELLOW_0:def 15;
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 )
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 = LR as non empty strict Poset by Th15, Th16, Th17;
Image k is complete
by WAYBEL_1:54;
then reconsider LR = LR as non empty strict complete Poset by A40, Th18, WAYBEL_1:6;
reconsider LR = LR as strict complete LATTICE ;
Image k is continuous LATTICE
by A1, WAYBEL15:14;
then reconsider LR = LR as strict complete continuous LATTICE by A40, WAYBEL15:9, WAYBEL_1:6;
reconsider f9 = f " as Function of (Image k),LR by A23, A30, FUNCT_2:25;
set IR = { [(Class ((EqRel R),x)),(Class ((EqRel R),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
; ( 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 ) )
thus
the carrier of LR = Class (EqRel R)
by A4; ( 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 ) )
now for z being object holds
( ( z in the InternalRel of LR implies z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ) & ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR ) )let z be
object ;
( ( z in the InternalRel of LR implies z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ) & ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR ) )hereby ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR )
assume A43:
z in the
InternalRel of
LR
;
z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } 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 =
a,
b =
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 (
(EqRel R),
x) &
b = Class (
(EqRel R),
y) &
k . x <= k . y )
by A5;
hence
z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y }
by A45;
verum
end; assume
z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y }
;
z in the InternalRel of LRthen consider x,
y being
Element of
L such that A46:
z = [(Class ((EqRel R),x)),(Class ((EqRel R),y))]
and A47:
k . x <= k . y
;
reconsider b =
Class (
(EqRel R),
y) as
Element of
LR by A4, EQREL_1:def 3;
reconsider a =
Class (
(EqRel R),
x) as
Element of
LR by A4, EQREL_1:def 3;
a <= b
by A5, A47;
hence
z in the
InternalRel of
LR
by A46, ORDERS_2:def 5;
verum end;
hence
the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y }
by TARSKI:2; 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
let g be Function of L,LR; ( ( for x being Element of L holds g . x = Class ((EqRel R),x) ) implies g is CLHomomorphism of L,LR )
assume A48:
for x being Element of L holds g . x = Class ((EqRel R),x)
; g is CLHomomorphism of L,LR
then A51:
g = f9 * (corestr k)
by FUNCT_2:12;
A52:
corestr k is directed-sups-preserving
by A1, Th22;
reconsider f9 = 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
g is CLHomomorphism of L,LR
by A53, WAYBEL16:def 1; verum