:: Closure Operators and Subalgebras
:: by Grzegorz Bancerek
::
:: Received January 15, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

scheme :: WAYBEL10:sch 1
SubrelstrEx{ F1() ->  non empty RelStr , P1[ set ], F2() ->  set } :
 ex S being non empty strict full SubRelStr of F1() st
for x being Element of F1() holds
( x is Element of S iff P1[x] )
provided
A1: P1[F2()] and
A2: F2() in the carrier of F1()
proofend;

scheme :: WAYBEL10:sch 2
RelstrEq{ F1() ->  non empty RelStr , F2() ->  non empty RelStr , P1[ set ], P2[ set , set ] } :
 RelStr(# the carrier of F1(), the InternalRel of F1() #) = RelStr(# the carrier of F2(), the InternalRel of F2() #)
provided
A1: for x being set holds
( x is Element of F1() iff P1[x] ) and
A2: for x being set holds
( x is Element of F2() iff P1[x] ) and
A3: for a, b being Element of F1() holds
( a <= b iff P2[a,b] ) and
A4: for a, b being Element of F2() holds
( a <= b iff P2[a,b] )
proofend;

scheme :: WAYBEL10:sch 3
SubrelstrEq1{ F1() ->  non empty RelStr , F2() ->  non empty full SubRelStr of F1(), F3() ->  non empty full SubRelStr of F1(), P1[ set ] } :
 RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #)
provided
A1: for x being set holds
( x is Element of F2() iff P1[x] ) and
A2: for x being set holds
( x is Element of F3() iff P1[x] )
proofend;

scheme :: WAYBEL10:sch 4
SubrelstrEq2{ F1() ->  non empty RelStr , F2() ->  non empty full SubRelStr of F1(), F3() ->  non empty full SubRelStr of F1(), P1[ set ] } :
 RelStr(# the carrier of F2(), the InternalRel of F2() #) = RelStr(# the carrier of F3(), the InternalRel of F3() #)
provided
A1: for x being Element of F1() holds
( x is Element of F2() iff P1[x] ) and
A2: for x being Element of F1() holds
( x is Element of F3() iff P1[x] )
proofend;

theorem Th1: :: WAYBEL10:1
for R, Q being Relation holds
( ( R c= Q implies R ~ c= Q ~ ) &amp; ( R ~ c= Q ~ implies R c= Q ) &amp; ( R ~ c= Q implies R c= Q ~ ) &amp; ( R c= Q ~ implies R ~ c= Q ) )
proofend;

theorem Th2: :: WAYBEL10:2
for L, S being RelStr holds
( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) &amp; ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) &amp; ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) &amp; ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )
proofend;

theorem Th3: :: WAYBEL10:3
for L, S being RelStr holds
( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) &amp; ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) &amp; ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) &amp; ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )
proofend;

definition
let L be RelStr ;
let S be full SubRelStr of L;
:: original:~
redefine funcS opp  ->  strict full SubRelStr of L opp ;
coherence
 S ~ is strict full SubRelStr of L opp by Th3;
end;

registration
let X be set ;
let L be non empty RelStr ;
clusterX --> L ->  non-Empty ;
coherence
 X --> L is non-Empty
proofend;
end;

registration
let S be RelStr ;
let T be non empty reflexive RelStr ;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V24( the carrier of S) quasi_total monotone for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is monotone
proofend;
end;

registration
let L be non empty RelStr ;
cluster Function-like quasi_total projection  ->  idempotent monotone for Element of bool [: the carrier of L, the carrier of L:];
coherence
 for b1 being Function of L,L st b1 is projection holds
( b1 is monotone &amp; b1 is idempotent ) by WAYBEL_1:def_13;
end;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
cluster corestr f ->  monotone ;
coherence
 corestr f is monotone
proofend;
end;

registration
let L be non empty reflexive RelStr ;
cluster id L ->  infs-preserving sups-preserving ;
coherence
 ( id L is sups-preserving &amp; id L is infs-preserving )
proofend;
end;

theorem :: WAYBEL10:4
for L being RelStr
for S being Subset of L holds
( id S is Function of (subrelstr S),L &amp; ( for f being Function of (subrelstr S),L st f = id S holds
f is monotone ) )
proofend;

registration
let L be non empty reflexive RelStr ;
cluster Relation-like the carrier of L -defined the carrier of L -valued Function-like V7() non empty V24( the carrier of L) quasi_total infs-preserving sups-preserving closure kernel for Element of bool [: the carrier of L, the carrier of L:];
existence
 ex b1 being Function of L,L st
( b1 is sups-preserving &amp; b1 is infs-preserving &amp; b1 is closure &amp; b1 is kernel &amp; b1 is V7() )
proofend;
end;

theorem Th5: :: WAYBEL10:5
for L being non empty reflexive RelStr
for c being closure Function of L,L
for x being Element of L holds c . x >= x
proofend;

theorem Th6: :: WAYBEL10:6
for S, T being RelStr
for R being SubRelStr of S
for f being Function of the carrier of S, the carrier of T holds
( f | R = f | the carrier of R &amp; ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
proofend;

theorem Th7: :: WAYBEL10:7
for S, T being RelStr
for f being Function of S,T st f is one-to-one holds
for R being SubRelStr of S holds f | R is one-to-one
proofend;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
let R be SubRelStr of S;
clusterf | R ->  monotone ;
coherence
 f | R is monotone
proofend;
end;

theorem Th8: :: WAYBEL10:8
for S, T being non empty RelStr
for R being non empty SubRelStr of S
for f being Function of S,T
for g being Function of T,S st f is V7() &amp; g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R &amp; g | (Image (f | R)) = (f | R) " )
proofend;

begin

registration
let S be RelStr ;
let T be non empty reflexive RelStr ;
cluster MonMaps (S,T) ->  non empty ;
coherence
 not MonMaps (S,T) is empty
proofend;
end;

theorem Th9: :: WAYBEL10:9
for S being RelStr
for T being non empty reflexive RelStr
for x being set holds
( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )
proofend;

definition
let L be non empty reflexive RelStr ;
func ClOpers L ->  non empty strict full SubRelStr of MonMaps (L,L) means :Def1: :: WAYBEL10:def 1
 for f being Function of L,L holds
( f is Element of it iff f is closure );
existence
 ex b1 being non empty strict full SubRelStr of MonMaps (L,L) st
for f being Function of L,L holds
( f is Element of b1 iff f is closure )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of MonMaps (L,L) st ( for f being Function of L,L holds
( f is Element of b1 iff f is closure ) ) &amp; ( for f being Function of L,L holds
( f is Element of b2 iff f is closure ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def1 defines ClOpers WAYBEL10:def_1_:_
 for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of MonMaps (L,L) holds
( b2 = ClOpers L iff for f being Function of L,L holds
( f is Element of b2 iff f is closure ) );

theorem Th10: :: WAYBEL10:10
for L being non empty reflexive RelStr
for x being set holds
( x is Element of (ClOpers L) iff x is closure Function of L,L )
proofend;

theorem Th11: :: WAYBEL10:11
for X being set
for L being non empty RelStr
for f, g being Function of X, the carrier of L
for x, y being Element of (L |^ X) st x = f &amp; y = g holds
( x <= y iff f <= g )
proofend;

theorem Th12: :: WAYBEL10:12
for L being complete LATTICE
for c1, c2 being Function of L,L
for x, y being Element of (ClOpers L) st x = c1 &amp; y = c2 holds
( x <= y iff c1 <= c2 )
proofend;

theorem Th13: :: WAYBEL10:13
for L being reflexive RelStr
for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds
S1 is SubRelStr of S2
proofend;

theorem Th14: :: WAYBEL10:14
for L being complete LATTICE
for c1, c2 being closure Function of L,L holds
( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )
proofend;

begin

definition
let L be RelStr ;
func Sub L ->  non empty strict RelStr  means :Def2: :: WAYBEL10:def 2
( ( for x being set holds
( x is Element of it iff x is strict SubRelStr of L ) ) &amp; ( for a, b being Element of it holds
( a <= b iff ex R being RelStr st
( b = R &amp; a is SubRelStr of R ) ) ) );
existence
 ex b1 being non empty strict RelStr st
( ( for x being set holds
( x is Element of b1 iff x is strict SubRelStr of L ) ) &amp; ( for a, b being Element of b1 holds
( a <= b iff ex R being RelStr st
( b = R &amp; a is SubRelStr of R ) ) ) )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict RelStr st ( for x being set holds
( x is Element of b1 iff x is strict SubRelStr of L ) ) &amp; ( for a, b being Element of b1 holds
( a <= b iff ex R being RelStr st
( b = R &amp; a is SubRelStr of R ) ) ) &amp; ( for x being set holds
( x is Element of b2 iff x is strict SubRelStr of L ) ) &amp; ( for a, b being Element of b2 holds
( a <= b iff ex R being RelStr st
( b = R &amp; a is SubRelStr of R ) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def2 defines Sub WAYBEL10:def_2_:_
 for L being RelStr
for b2 being non empty strict RelStr holds
( b2 = Sub L iff ( ( for x being set holds
( x is Element of b2 iff x is strict SubRelStr of L ) ) &amp; ( for a, b being Element of b2 holds
( a <= b iff ex R being RelStr st
( b = R &amp; a is SubRelStr of R ) ) ) ) );

theorem Th15: :: WAYBEL10:15
for L, R being RelStr
for x, y being Element of (Sub L) st y = R holds
( x <= y iff x is SubRelStr of R )
proofend;

registration
let L be RelStr ;
cluster Sub L ->  non empty strict reflexive transitive antisymmetric ;
coherence
 ( Sub L is reflexive &amp; Sub L is antisymmetric &amp; Sub L is transitive )
proofend;
end;

registration
let L be RelStr ;
cluster Sub L ->  non empty strict complete ;
coherence
 Sub L is complete
proofend;
end;

registration
let L be complete LATTICE;
cluster infs-inheriting  ->  non empty for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is infs-inheriting holds
not b1 is empty
proofend;
cluster sups-inheriting  ->  non empty for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is sups-inheriting holds
not b1 is empty
proofend;
end;

definition
let L be RelStr ;
mode System of L is full SubRelStr of L;
end;

notation
let L be non empty RelStr ;
let S be System of L;
synonym  closure S for  infs-inheriting ;
end;

registration
let L be non empty RelStr ;
cluster subrelstr ([#] L) ->  infs-inheriting sups-inheriting ;
coherence
 ( subrelstr ([#] L) is closure &amp; subrelstr ([#] L) is sups-inheriting )
proofend;
end;

definition
let L be non empty RelStr ;
func ClosureSystems L ->  non empty strict full SubRelStr of Sub L means :Def3: :: WAYBEL10:def 3
 for R being strict SubRelStr of L holds
( R is Element of it iff ( R is infs-inheriting &amp; R is full ) );
existence
 ex b1 being non empty strict full SubRelStr of Sub L st
for R being strict SubRelStr of L holds
( R is Element of b1 iff ( R is infs-inheriting &amp; R is full ) )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of Sub L st ( for R being strict SubRelStr of L holds
( R is Element of b1 iff ( R is infs-inheriting &amp; R is full ) ) ) &amp; ( for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is infs-inheriting &amp; R is full ) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def3 defines ClosureSystems WAYBEL10:def_3_:_
 for L being non empty RelStr
for b2 being non empty strict full SubRelStr of Sub L holds
( b2 = ClosureSystems L iff for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is infs-inheriting &amp; R is full ) ) );

theorem Th16: :: WAYBEL10:16
for L being non empty RelStr
for x being set holds
( x is Element of (ClosureSystems L) iff x is strict closure System of L )
proofend;

theorem Th17: :: WAYBEL10:17
for L being non empty RelStr
for R being RelStr
for x, y being Element of (ClosureSystems L) st y = R holds
( x <= y iff x is SubRelStr of R )
proofend;

begin

registration
let L be non empty Poset;
let h be closure Function of L,L;
cluster Image h ->  infs-inheriting ;
coherence
 Image h is closure by WAYBEL_1:53;
end;

definition
let L be non empty Poset;
func ClImageMap L ->  Function of (ClOpers L),((ClosureSystems L) opp) means :Def4: :: WAYBEL10:def 4
 for c being closure Function of L,L holds it . c = Image c;
existence
 ex b1 being Function of (ClOpers L),((ClosureSystems L) opp) st
for c being closure Function of L,L holds b1 . c = Image c
proofend;
correctness
uniqueness
for b1, b2 being Function of (ClOpers L),((ClosureSystems L) opp) st ( for c being closure Function of L,L holds b1 . c = Image c ) &amp; ( for c being closure Function of L,L holds b2 . c = Image c ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def4 defines ClImageMap WAYBEL10:def_4_:_
 for L being non empty Poset
for b2 being Function of (ClOpers L),((ClosureSystems L) opp) holds
( b2 = ClImageMap L iff for c being closure Function of L,L holds b2 . c = Image c );

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
func closure_op S ->  Function of L,L means :Def5: :: WAYBEL10:def 5
 for x being Element of L holds it . x = "/\" (((uparrow x) /\ the carrier of S),L);
existence
 ex b1 being Function of L,L st
for x being Element of L holds b1 . x = "/\" (((uparrow x) /\ the carrier of S),L)
proofend;
uniqueness
 for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) &amp; ( for x being Element of L holds b2 . x = "/\" (((uparrow x) /\ the carrier of S),L) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines closure_op WAYBEL10:def_5_:_
 for L being non empty RelStr
for S being SubRelStr of L
for b3 being Function of L,L holds
( b3 = closure_op S iff for x being Element of L holds b3 . x = "/\" (((uparrow x) /\ the carrier of S),L) );

registration
let L be complete LATTICE;
let S be closure System of L;
cluster closure_op S ->  closure ;
coherence
 closure_op S is closure
proofend;
end;

theorem Th18: :: WAYBEL10:18
for L being complete LATTICE
for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)
proofend;

theorem Th19: :: WAYBEL10:19
for L being complete LATTICE
for c being closure Function of L,L holds closure_op (Image c) = c
proofend;

registration
let L be complete LATTICE;
cluster ClImageMap L -> V7() ;
coherence
 ClImageMap L is one-to-one
proofend;
end;

theorem Th20: :: WAYBEL10:20
for L being complete LATTICE holds (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L)
proofend;

theorem Th21: :: WAYBEL10:21
for L being complete LATTICE
for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S
proofend;

registration
let L be complete LATTICE;
cluster ClImageMap L ->  isomorphic ;
correctness
coherence
ClImageMap L is isomorphic ;
proofend;
end;

theorem :: WAYBEL10:22
for L being complete LATTICE holds ClOpers L,(ClosureSystems L) opp are_isomorphic
proofend;

begin

:: and subalgebras
theorem Th23: :: WAYBEL10:23
for L being RelStr
for S being full SubRelStr of L
for X being Subset of S holds
( ( X is directed Subset of L implies X is directed ) &amp; ( X is filtered Subset of L implies X is filtered ) )
proofend;

:: Corollary 3.14, p. 24
theorem Th24: :: WAYBEL10:24
for L being complete LATTICE
for S being closure System of L holds
( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )
proofend;

theorem :: WAYBEL10:25
for L being complete LATTICE
for h being closure Function of L,L holds
( h is directed-sups-preserving iff Image h is directed-sups-inheriting )
proofend;

registration
let L be complete LATTICE;
let S be closure directed-sups-inheriting System of L;
cluster closure_op S ->  directed-sups-preserving ;
coherence
 closure_op S is directed-sups-preserving by Th24;
end;

registration
let L be complete LATTICE;
let h be directed-sups-preserving closure Function of L,L;
cluster Image h ->  directed-sups-inheriting ;
coherence
 Image h is directed-sups-inheriting
proofend;
end;

definition
let L be non empty reflexive RelStr ;
func DsupClOpers L ->  non empty strict full SubRelStr of ClOpers L means :Def6: :: WAYBEL10:def 6
 for f being closure Function of L,L holds
( f is Element of it iff f is directed-sups-preserving );
existence
 ex b1 being non empty strict full SubRelStr of ClOpers L st
for f being closure Function of L,L holds
( f is Element of b1 iff f is directed-sups-preserving )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of ClOpers L st ( for f being closure Function of L,L holds
( f is Element of b1 iff f is directed-sups-preserving ) ) &amp; ( for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def6 defines DsupClOpers WAYBEL10:def_6_:_
 for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of ClOpers L holds
( b2 = DsupClOpers L iff for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) );

theorem Th26: :: WAYBEL10:26
for L being non empty reflexive RelStr
for x being set holds
( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )
proofend;

definition
let L be non empty RelStr ;
func Subalgebras L ->  non empty strict full SubRelStr of ClosureSystems L means :Def7: :: WAYBEL10:def 7
 for R being strict closure System of L holds
( R is Element of it iff R is directed-sups-inheriting );
existence
 ex b1 being non empty strict full SubRelStr of ClosureSystems L st
for R being strict closure System of L holds
( R is Element of b1 iff R is directed-sups-inheriting )
proofend;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of ClosureSystems L st ( for R being strict closure System of L holds
( R is Element of b1 iff R is directed-sups-inheriting ) ) &amp; ( for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def7 defines Subalgebras WAYBEL10:def_7_:_
 for L being non empty RelStr
for b2 being non empty strict full SubRelStr of ClosureSystems L holds
( b2 = Subalgebras L iff for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) );

theorem Th27: :: WAYBEL10:27
for L being non empty RelStr
for x being set holds
( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )
proofend;

theorem Th28: :: WAYBEL10:28
for L being complete LATTICE holds Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp
proofend;

registration
let L be complete LATTICE;
cluster corestr ((ClImageMap L) | (DsupClOpers L)) ->  isomorphic ;
coherence
 corestr ((ClImageMap L) | (DsupClOpers L)) is isomorphic
proofend;
end;

theorem :: WAYBEL10:29
for L being complete LATTICE holds DsupClOpers L,(Subalgebras L) opp are_isomorphic
proofend;