:: Closure Operators and Subalgebras
:: by Grzegorz Bancerek
::
:: Copyright (c) 1997-2019 Association of Mizar Users

scheme :: WAYBEL10:sch 1
SubrelstrEx{ F1() -> non empty RelStr , P1[ object ], 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()
proof end;

scheme :: WAYBEL10:sch 2
RelstrEq{ F1() -> non empty RelStr , F2() -> non empty RelStr , P1[ object ], 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 object holds
( x is Element of F1() iff P1[x] ) and
A2: for x being object 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] )
proof end;

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

scheme :: WAYBEL10:sch 4
SubrelstrEq2{ F1() -> non empty RelStr , F2() -> non empty full SubRelStr of F1(), F3() -> non empty full SubRelStr of F1(), P1[ object ] } :
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] )
proof end;

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

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

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 ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )
proof end;

definition
let L be RelStr ;
let S be full SubRelStr of L;
:: original: ~
redefine func S 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 ;
cluster X --> L -> non-Empty ;
coherence
X --> L is non-Empty
proof end;
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
proof end;
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 & 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;
coherence
proof end;
end;

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

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

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 & b1 is infs-preserving & b1 is closure & b1 is kernel & b1 is V7() )
proof end;
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
proof end;

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 & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
proof end;

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
proof end;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
let R be SubRelStr of S;
cluster f | R -> monotone ;
coherence
f | R is monotone
proof end;
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() & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )
proof end;

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
proof end;
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 )
proof end;

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 )
proof end;
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 ) ) & ( for f being Function of L,L holds
( f is Element of b2 iff f is closure ) ) holds
b1 = b2
;
proof end;
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 () iff x is closure Function of L,L ) by ;

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 & y = g holds
( x <= y iff f <= g )
proof end;

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

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
proof end;

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 )
proof end;

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

registration
let L be RelStr ;
coherence
( Sub L is reflexive & Sub L is antisymmetric & Sub L is transitive )
proof end;
end;

registration
let L be RelStr ;
coherence
Sub L is complete
proof end;
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
proof end;
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
proof end;
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 ;
coherence
( subrelstr ([#] L) is closure & subrelstr ([#] L) is sups-inheriting )
proof end;
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 & 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 & R is full ) )
proof end;
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 & R is full ) ) ) & ( for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is infs-inheriting & R is full ) ) ) holds
b1 = b2
;
proof end;
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 & R is full ) ) );

theorem Th16: :: WAYBEL10:16
for L being non empty RelStr
for x being object holds
( x is Element of () iff x is strict closure System of L )
proof end;

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

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

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

:: deftheorem Def4 defines ClImageMap WAYBEL10:def 4 :
for L being non empty Poset
for b2 being Function of (),() 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 = "/\" ((() /\ the carrier of S),L);
existence
ex b1 being Function of L,L st
for x being Element of L holds b1 . x = "/\" ((() /\ the carrier of S),L)
proof end;
uniqueness
for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = "/\" ((() /\ the carrier of S),L) ) & ( for x being Element of L holds b2 . x = "/\" ((() /\ the carrier of S),L) ) holds
b1 = b2
proof end;
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 = "/\" ((() /\ the carrier of S),L) );

registration
let L be complete LATTICE;
let S be closure System of L;
coherence
proof end;
end;

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

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

registration
let L be complete LATTICE;
cluster ClImageMap L -> V7() ;
coherence
proof end;
end;

theorem Th20: :: WAYBEL10:20
for L being complete LATTICE holds () " is Function of (),()
proof end;

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

registration
let L be complete LATTICE;
correctness
coherence ;
proof end;
end;

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

:: 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 ) & ( X is filtered Subset of L implies X is filtered ) )
proof end;

:: 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 )
proof end;

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 )
proof end;

registration
let L be complete LATTICE;
let S be closure directed-sups-inheriting System of L;
coherence by Th24;
end;

registration
let L be complete LATTICE;
let h be directed-sups-preserving closure Function of L,L;
coherence
proof end;
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 )
proof end;
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 ) ) & ( for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) ) holds
b1 = b2
;
proof end;
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 () iff x is directed-sups-preserving closure Function of L,L )
proof end;

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 )
proof end;
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 ) ) & ( for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) ) holds
b1 = b2
;
proof end;
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 object holds
( x is Element of () iff x is strict closure directed-sups-inheriting System of L )
proof end;

theorem Th28: :: WAYBEL10:28
for L being complete LATTICE holds Image (() | ()) = () opp
proof end;

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

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