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

scheme :: WAYBEL10:sch 1
SubrelstrEx{ F₁() -> non empty RelStr , P₁[ object ], F₂() -> set } :

ex S being non empty strict full SubRelStr of F₁() st
for x being Element of F₁() holds
( x is Element of S iff P₁[x] )

provided

A1: P₁[F₂()] and
A2: F₂() in the carrier of F₁()

proof end;

scheme :: WAYBEL10:sch 2
RelstrEq{ F₁() -> non empty RelStr , F₂() -> non empty RelStr , P₁[ object ], P₂[ set , set ] } :

RelStr(# the carrier of F₁(), the InternalRel of F₁() #) = RelStr(# the carrier of F₂(), the InternalRel of F₂() #)

provided

A1: for x being object holds
( x is Element of F₁() iff P₁[x] ) and
A2: for x being object holds
( x is Element of F₂() iff P₁[x] ) and
A3: for a, b being Element of F₁() holds
( a <= b iff P₂[a,b] ) and
A4: for a, b being Element of F₂() holds
( a <= b iff P₂[a,b] )

proof end;

scheme :: WAYBEL10:sch 3
SubrelstrEq1{ F₁() -> non empty RelStr , F₂() -> non empty full SubRelStr of F₁(), F₃() -> non empty full SubRelStr of F₁(), P₁[ object ] } :

RelStr(# the carrier of F₂(), the InternalRel of F₂() #) = RelStr(# the carrier of F₃(), the InternalRel of F₃() #)

provided

A1: for x being object holds
( x is Element of F₂() iff P₁[x] ) and
A2: for x being object holds
( x is Element of F₃() iff P₁[x] )

proof end;

scheme :: WAYBEL10:sch 4
SubrelstrEq2{ F₁() -> non empty RelStr , F₂() -> non empty full SubRelStr of F₁(), F₃() -> non empty full SubRelStr of F₁(), P₁[ object ] } :

RelStr(# the carrier of F₂(), the InternalRel of F₂() #) = RelStr(# the carrier of F₃(), the InternalRel of F₃() #)

provided

A1: for x being Element of F₁() holds
( x is Element of F₂() iff P₁[x] ) and
A2: for x being Element of F₁() holds
( x is Element of F₃() iff P₁[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 b₁ being Function of S,T st b₁ 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 b₁ being Function of L,L st b₁ is projection holds
( b₁ is monotone & b₁ 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

proof end;

end;

registration

let L be non empty reflexive RelStr ;

cluster id L -> infs-preserving sups-preserving ;

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 (subrelstr S),L & ( for f being Function of (subrelstr S),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 b₁ being Function of L,L st
( b₁ is sups-preserving & b₁ is infs-preserving & b₁ is closure & b₁ is kernel & b₁ 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 b₁ being non empty strict full SubRelStr of MonMaps (L,L) st
for f being Function of L,L holds
( f is Element of b₁ iff f is closure )

proof end;

correctness
uniqueness
for b₁, b₂ being non empty strict full SubRelStr of MonMaps (L,L) st ( for f being Function of L,L holds
( f is Element of b₁ iff f is closure ) ) & ( for f being Function of L,L holds
( f is Element of b₂ iff f is closure ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def1 defines ClOpers WAYBEL10:def 1 :
for L being non empty reflexive RelStr
for b₂ being non empty strict full SubRelStr of MonMaps (L,L) holds
( b₂ = ClOpers L iff for f being Function of L,L holds
( f is Element of b₂ 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 ) by YELLOW_0:58, Def1, Th9;

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 (ClOpers L) 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 b₁ being non empty strict RelStr st
( ( for x being object holds
( x is Element of b₁ iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b₁ holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) )

proof end;

correctness
uniqueness
for b₁, b₂ being non empty strict RelStr st ( for x being object holds
( x is Element of b₁ iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b₁ 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 b₂ iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b₂ holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def2 defines Sub WAYBEL10:def 2 :
for L being RelStr
for b₂ being non empty strict RelStr holds
( b₂ = Sub L iff ( ( for x being object holds
( x is Element of b₂ iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b₂ 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 ;

cluster Sub L -> non empty strict reflexive transitive antisymmetric ;

coherence
( Sub L is reflexive & Sub L is antisymmetric & Sub L is transitive )

proof end;

end;

registration

let L be RelStr ;

cluster Sub L -> non empty strict complete ;

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 b₁ being SubRelStr of L st b₁ is infs-inheriting holds
not b₁ is empty

proof end;

cluster sups-inheriting -> non empty for SubRelStr of L;

coherence
for b₁ being SubRelStr of L st b₁ is sups-inheriting holds
not b₁ 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 ;

cluster subrelstr ([#] L) -> infs-inheriting sups-inheriting ;

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 b₁ being non empty strict full SubRelStr of Sub L st
for R being strict SubRelStr of L holds
( R is Element of b₁ iff ( R is infs-inheriting & R is full ) )

proof end;

correctness
uniqueness
for b₁, b₂ being non empty strict full SubRelStr of Sub L st ( for R being strict SubRelStr of L holds
( R is Element of b₁ iff ( R is infs-inheriting & R is full ) ) ) & ( for R being strict SubRelStr of L holds
( R is Element of b₂ iff ( R is infs-inheriting & R is full ) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def3 defines ClosureSystems WAYBEL10:def 3 :
for L being non empty RelStr
for b₂ being non empty strict full SubRelStr of Sub L holds
( b₂ = ClosureSystems L iff for R being strict SubRelStr of L holds
( R is Element of b₂ 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 (ClosureSystems L) 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 (ClosureSystems L) 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;

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 b₁ being Function of (ClOpers L),((ClosureSystems L) opp) st
for c being closure Function of L,L holds b₁ . c = Image c

proof end;

correctness
uniqueness
for b₁, b₂ being Function of (ClOpers L),((ClosureSystems L) opp) st ( for c being closure Function of L,L holds b₁ . c = Image c ) & ( for c being closure Function of L,L holds b₂ . c = Image c ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def4 defines ClImageMap WAYBEL10:def 4 :
for L being non empty Poset
for b₂ being Function of (ClOpers L),((ClosureSystems L) opp) holds
( b₂ = ClImageMap L iff for c being closure Function of L,L holds b₂ . 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 b₁ being Function of L,L st
for x being Element of L holds b₁ . x = "/\" (((uparrow x) /\ the carrier of S),L)

proof end;

uniqueness
for b₁, b₂ being Function of L,L st ( for x being Element of L holds b₁ . x = "/\" (((uparrow x) /\ the carrier of S),L) ) & ( for x being Element of L holds b₂ . x = "/\" (((uparrow x) /\ the carrier of S),L) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines closure_op WAYBEL10:def 5 :
for L being non empty RelStr
for S being SubRelStr of L
for b₃ being Function of L,L holds
( b₃ = closure_op S iff for x being Element of L holds b₃ . 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

proof end;

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 #)

proof end;

theorem Th19: :: WAYBEL10:19

for L being complete LATTICE
for c being closure Function of L,L holds closure_op (Image c) = c

proof end;

registration

let L be complete LATTICE;

cluster ClImageMap L -> V7() ;

coherence
ClImageMap L is one-to-one

proof end;

end;

theorem Th20: :: WAYBEL10:20

for L being complete LATTICE holds (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L)

proof end;

theorem Th21: :: WAYBEL10:21

for L being complete LATTICE
for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S

proof end;

registration

let L be complete LATTICE;

cluster ClImageMap L -> isomorphic ;

correctness
coherence
ClImageMap L is isomorphic ;

proof end;

end;

theorem :: WAYBEL10:22

for L being complete LATTICE holds ClOpers L,(ClosureSystems 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;

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

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 b₁ being non empty strict full SubRelStr of ClOpers L st
for f being closure Function of L,L holds
( f is Element of b₁ iff f is directed-sups-preserving )

proof end;

correctness
uniqueness
for b₁, b₂ being non empty strict full SubRelStr of ClOpers L st ( for f being closure Function of L,L holds
( f is Element of b₁ iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds
( f is Element of b₂ iff f is directed-sups-preserving ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def6 defines DsupClOpers WAYBEL10:def 6 :
for L being non empty reflexive RelStr
for b₂ being non empty strict full SubRelStr of ClOpers L holds
( b₂ = DsupClOpers L iff for f being closure Function of L,L holds
( f is Element of b₂ 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 )

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 b₁ being non empty strict full SubRelStr of ClosureSystems L st
for R being strict closure System of L holds
( R is Element of b₁ iff R is directed-sups-inheriting )

proof end;

correctness
uniqueness
for b₁, b₂ being non empty strict full SubRelStr of ClosureSystems L st ( for R being strict closure System of L holds
( R is Element of b₁ iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds
( R is Element of b₂ iff R is directed-sups-inheriting ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def7 defines Subalgebras WAYBEL10:def 7 :
for L being non empty RelStr
for b₂ being non empty strict full SubRelStr of ClosureSystems L holds
( b₂ = Subalgebras L iff for R being strict closure System of L holds
( R is Element of b₂ 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 (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )

proof end;

theorem Th28: :: WAYBEL10:28

for L being complete LATTICE holds Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp

proof end;

registration

let L be complete LATTICE;

cluster corestr ((ClImageMap L) | (DsupClOpers L)) -> isomorphic ;

coherence
corestr ((ClImageMap L) | (DsupClOpers L)) is isomorphic

proof end;

end;

theorem :: WAYBEL10:29

for L being complete LATTICE holds DsupClOpers L,(Subalgebras L) opp are_isomorphic

proof end;