:: Kernel Projections and Quotient Lattices
:: by Piotr Rudnicki
::
:: Received July 6, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users


theorem Th1: :: WAYBEL20:1
for X being set
for S being Subset of (id X) holds proj1 S = proj2 S
proof end;

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

definition
let L1, L2, T1, T2 be RelStr ;
let f be Function of L1,T1;
let g be Function of L2,T2;
:: original: [:
redefine func [:f,g:] -> Function of [:L1,L2:],[:T1,T2:];
coherence
[:f,g:] is Function of [:L1,L2:],[:T1,T2:]
proof end;
end;

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

theorem Th4: :: WAYBEL20:4
for f, g being Function
for 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 end;

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

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

theorem Th7: :: WAYBEL20:7
for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
proof end;

theorem Th8: :: WAYBEL20:8
for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
proof end;

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

theorem :: WAYBEL20:10
for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for 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 end;

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

theorem Th12: :: WAYBEL20:12
for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for 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 end;

theorem Th13: :: WAYBEL20:13
for L being non empty antisymmetric RelStr
for 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 end;

theorem Th14: :: WAYBEL20:14
for L being non empty antisymmetric RelStr
for 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 end;

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

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

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

theorem Th18: :: WAYBEL20:18
for L, M being non empty RelStr st L,M are_isomorphic & L is complete holds
M is complete
proof end;

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

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

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

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

theorem Th23: :: WAYBEL20:23
for S, T being non empty reflexive antisymmetric RelStr
for f being Function of S,T st f is filtered-infs-preserving holds
f is monotone
proof end;

theorem Th24: :: WAYBEL20:24
for S, T being non empty RelStr
for f being Function of S,T st f is monotone holds
for X being Subset of S st X is filtered holds
f .: X is filtered
proof end;

theorem Th25: :: WAYBEL20:25
for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds
g * f is infs-preserving
proof end;

theorem :: WAYBEL20:26
for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving
proof end;

theorem :: WAYBEL20:27
for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving
proof end;

theorem :: WAYBEL20:28
for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
proof end;

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 antisymmetric lower-bounded RelStr ) holds
product J is lower-bounded
proof end;

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 antisymmetric upper-bounded RelStr ) holds
product J is upper-bounded
proof end;

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 antisymmetric lower-bounded RelStr ) holds
for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)
proof end;

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 antisymmetric upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)
proof end;

theorem :: WAYBEL20:33
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds
product J is continuous
proof end;

theorem Th34: :: WAYBEL20:34
for L, T being complete continuous LATTICE
for g being CLHomomorphism of L,T
for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]
proof end;

:: Proposition 2.9, p. 61, see WAYBEL10
:: Lemma 2.10, p. 61, see WAYBEL15:16
definition
let L be RelStr ;
let R be Subset of [:L,L:];
assume A1: R is Equivalence_Relation of the carrier of L ;
func EqRel R -> Equivalence_Relation of the carrier of L equals :Def1: :: WAYBEL20:def 1
R;
correctness
coherence
R is Equivalence_Relation of the carrier of L;
by A1;
end;

:: deftheorem Def1 defines EqRel WAYBEL20:def 1 :
for L being RelStr
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L holds
EqRel R = R;

definition
let L be non empty RelStr ;
let 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;

:: deftheorem defines CLCongruence WAYBEL20:def 2 :
for L being non empty RelStr
for R being Subset of [:L,L:] holds
( R is CLCongruence iff ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ) );

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

definition
let L be complete LATTICE;
let R be non empty Subset of [:L,L:];
assume A1: R is CLCongruence ;
func kernel_op R -> kernel Function of L,L means :Def3: :: WAYBEL20:def 3
 for x being Element of L holds it . x = inf (Class ((EqRel R),x));
existence
ex b1 being kernel Function of L,L st
for x being Element of L holds b1 . x = inf (Class ((EqRel R),x))
proof end;
uniqueness
for b1, b2 being kernel Function of L,L st ( for x being Element of L holds b1 . x = inf (Class ((EqRel R),x)) ) & ( for x being Element of L holds b2 . x = inf (Class ((EqRel R),x)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :
for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b3 being kernel Function of L,L holds
( b3 = kernel_op R iff for x being Element of L holds b3 . x = inf (Class ((EqRel R),x)) );

theorem Th36: :: WAYBEL20:36
for L being complete LATTICE
for R being 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 end;

theorem Th37: :: WAYBEL20:37
for L being 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 ) )
proof end;

theorem Th38: :: WAYBEL20:38
for L being complete continuous LATTICE
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous 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 end;

registration
let L be non empty reflexive RelStr ;
cluster non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V28( the carrier of L, the carrier of L) directed-sups-preserving kernel for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being Function of L,L st
( b1 is directed-sups-preserving & b1 is kernel )
proof end;
end;

definition
let L be non empty reflexive RelStr ;
let 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);
coherence
[:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:]
proof end;
end;

:: deftheorem defines kernel_congruence WAYBEL20:def 4 :
for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k = [:k,k:] " (id the carrier of L);

theorem :: WAYBEL20:39
for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k is Equivalence_Relation of the carrier of L by Th2;

theorem Th40: :: WAYBEL20:40
for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence
proof end;

definition
let L be complete continuous LATTICE;
let R be non empty Subset of [:L,L:];
assume A1: R is CLCongruence ;
func L ./. R -> strict complete continuous LATTICE means :Def5: :: 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) ) ) );
existence
ex b1 being strict complete continuous LATTICE st
( the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) )
proof end;
uniqueness
for b1, b2 being strict complete continuous LATTICE st the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of b2 = Class (EqRel R) & ( for x, y being Element of b2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines ./. WAYBEL20:def 5 :
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b3 being strict complete continuous LATTICE holds
( b3 = L ./. R iff ( the carrier of b3 = Class (EqRel R) & ( for x, y being Element of b3 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) );

theorem :: WAYBEL20:41
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
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 end;

theorem :: WAYBEL20:42
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
R = kernel_congruence (kernel_op R) by Th36;

theorem :: WAYBEL20:43
for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)
proof end;

theorem :: WAYBEL20:44
for L being complete continuous LATTICE
for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )
proof end;