:: Galois Connections
:: by Czes\law Byli\'nski
::
:: Received September 25, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

definition

let L1, L2 be non empty 1-sorted ;
let f be Function of L1,L2;

:: original: one-to-one
redefine attr f is one-to-one means :: WAYBEL_1:def 1
for x, y being Element of L1 st f . x = f . y holds
x = y;

compatibility
( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds
x = y )

proof end;

end;

:: deftheorem defines one-to-one WAYBEL_1:def 1 :
for L1, L2 being non empty 1-sorted
for f being Function of L1,L2 holds
( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds
x = y );

definition

let L1, L2 be non empty RelStr ;
let f be Function of L1,L2;

redefine attr f is monotone means :: WAYBEL_1:def 2
for x, y being Element of L1 st x <= y holds
f . x <= f . y;

compatibility
( f is monotone iff for x, y being Element of L1 st x <= y holds
f . x <= f . y ) ;

end;

:: deftheorem defines monotone WAYBEL_1:def 2 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is monotone iff for x, y being Element of L1 st x <= y holds
f . x <= f . y );

theorem Th1: :: WAYBEL_1:1

for L being transitive antisymmetric with_infima RelStr
for x, y, z being Element of L st x <= y holds
x "/\" z <= y "/\" z

proof end;

theorem Th2: :: WAYBEL_1:2

for L being transitive antisymmetric with_suprema RelStr
for x, y, z being Element of L st x <= y holds
x "\/" z <= y "\/" z

proof end;

theorem Th3: :: WAYBEL_1:3

for L being non empty antisymmetric lower-bounded RelStr
for x being Element of L holds
( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) )

proof end;

theorem Th4: :: WAYBEL_1:4

for L being non empty antisymmetric upper-bounded RelStr
for x being Element of L holds
( ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) & ( L is with_suprema implies (Top L) "\/" x = Top L ) )

proof end;

definition

let L be non empty RelStr ;

attr L is distributive means :Def3: :: WAYBEL_1:def 3
for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z);

end;

:: deftheorem Def3 defines distributive WAYBEL_1:def 3 :
for L being non empty RelStr holds
( L is distributive iff for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) );

theorem Th5: :: WAYBEL_1:5

for L being LATTICE holds
( L is distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) )

proof end;

registration

let X be set ;

cluster BoolePoset X -> distributive ;

coherence
BoolePoset X is distributive

proof end;

end;

definition

let S be non empty RelStr ;
let X be set ;

pred ex_min_of X,S means :: WAYBEL_1:def 4
( ex_inf_of X,S & "/\" (X,S) in X );

pred ex_max_of X,S means :: WAYBEL_1:def 5
( ex_sup_of X,S & "\/" (X,S) in X );

end;

:: deftheorem defines ex_min_of WAYBEL_1:def 4 :
for S being non empty RelStr
for X being set holds
( ex_min_of X,S iff ( ex_inf_of X,S & "/\" (X,S) in X ) );

:: deftheorem defines ex_max_of WAYBEL_1:def 5 :
for S being non empty RelStr
for X being set holds
( ex_max_of X,S iff ( ex_sup_of X,S & "\/" (X,S) in X ) );

notation

let S be non empty RelStr ;
let X be set ;
synonym X has_the_min_in S for ex_min_of X,S;
synonym X has_the_max_in S for ex_max_of X,S;

end;

definition

let S be non empty RelStr ;
let s be Element of S;
let X be set ;

pred s is_minimum_of X means :: WAYBEL_1:def 6
( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X );

pred s is_maximum_of X means :: WAYBEL_1:def 7
( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X );

end;

:: deftheorem defines is_minimum_of WAYBEL_1:def 6 :
for S being non empty RelStr
for s being Element of S
for X being set holds
( s is_minimum_of X iff ( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X ) );

:: deftheorem defines is_maximum_of WAYBEL_1:def 7 :
for S being non empty RelStr
for s being Element of S
for X being set holds
( s is_maximum_of X iff ( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X ) );

registration

let L be RelStr ;

cluster id L -> isomorphic ;

coherence
id L is isomorphic

proof end;

end;

definition

let L1, L2 be RelStr ;

pred L1,L2 are_isomorphic means :: WAYBEL_1:def 8
ex f being Function of L1,L2 st f is isomorphic ;

reflexivity
for L1 being RelStr ex f being Function of L1,L1 st f is isomorphic

proof end;

end;

:: deftheorem defines are_isomorphic WAYBEL_1:def 8 :
for L1, L2 being RelStr holds
( L1,L2 are_isomorphic iff ex f being Function of L1,L2 st f is isomorphic );

theorem :: WAYBEL_1:6

for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds
L2,L1 are_isomorphic

proof end;

theorem :: WAYBEL_1:7

for L1, L2, L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds
L1,L3 are_isomorphic

proof end;

definition

let S, T be RelStr ;

mode Connection of S,T -> set means :Def9: :: WAYBEL_1:def 9
ex g being Function of S,T ex d being Function of T,S st it = [g,d];

existence
ex b₁ being set ex g being Function of S,T ex d being Function of T,S st b₁ = [g,d]

proof end;

end;

:: deftheorem Def9 defines Connection WAYBEL_1:def 9 :
for S, T being RelStr
for b₃ being set holds
( b₃ is Connection of S,T iff ex g being Function of S,T ex d being Function of T,S st b₃ = [g,d] );

definition

let S, T be RelStr ;
let g be Function of S,T;
let d be Function of T,S;
:: original: [
redefine func [g,d] -> Connection of S,T;
coherence
[g,d] is Connection of S,T by Def9;

end;

:: Definition 3.1

definition

let S, T be non empty RelStr ;
let gc be Connection of S,T;

attr gc is Galois means :: WAYBEL_1:def 10
ex g being Function of S,T ex d being Function of T,S st
( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) );

end;

:: deftheorem defines Galois WAYBEL_1:def 10 :
for S, T being non empty RelStr
for gc being Connection of S,T holds
( gc is Galois iff ex g being Function of S,T ex d being Function of T,S st
( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) );

theorem Th8: :: WAYBEL_1:8

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )

proof end;

:: Definition 3.1

definition

let S, T be non empty RelStr ;
let g be Function of S,T;

attr g is upper_adjoint means :: WAYBEL_1:def 11
ex d being Function of T,S st [g,d] is Galois ;

end;

:: deftheorem defines upper_adjoint WAYBEL_1:def 11 :
for S, T being non empty RelStr
for g being Function of S,T holds
( g is upper_adjoint iff ex d being Function of T,S st [g,d] is Galois );

:: Definition 3.1

definition

let S, T be non empty RelStr ;
let d be Function of T,S;

attr d is lower_adjoint means :Def12: :: WAYBEL_1:def 12
ex g being Function of S,T st [g,d] is Galois ;

end;

:: deftheorem Def12 defines lower_adjoint WAYBEL_1:def 12 :
for S, T being non empty RelStr
for d being Function of T,S holds
( d is lower_adjoint iff ex g being Function of S,T st [g,d] is Galois );

theorem :: WAYBEL_1:9

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is upper_adjoint & d is lower_adjoint ) ;

:: Theorem 3.2 (1) iff (2)

theorem Th10: :: WAYBEL_1:10

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )

proof end;

:: Theorem 3.2 (1) iff (3)

theorem Th11: :: WAYBEL_1:11

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )

proof end;

:: Theorem 3.3 (first part)

theorem Th12: :: WAYBEL_1:12

for S, T being non empty Poset
for g being Function of S,T st g is upper_adjoint holds
g is infs-preserving

proof end;

registration

let S, T be non empty Poset;

cluster Function-like quasi_total upper_adjoint -> infs-preserving for M3( bool [: the carrier of S, the carrier of T:]);

coherence
for b₁ being Function of S,T st b₁ is upper_adjoint holds
b₁ is infs-preserving by Th12;

end;

:: Theorem 3.3 (second part)

theorem Th13: :: WAYBEL_1:13

for S, T being non empty Poset
for d being Function of T,S st d is lower_adjoint holds
d is sups-preserving

proof end;

registration

let S, T be non empty Poset;

cluster Function-like quasi_total lower_adjoint -> sups-preserving for M3( bool [: the carrier of S, the carrier of T:]);

coherence
for b₁ being Function of S,T st b₁ is lower_adjoint holds
b₁ is sups-preserving by Th13;

end;

:: Theorem 3.4

theorem Th14: :: WAYBEL_1:14

for S, T being non empty Poset
for g being Function of S,T st S is complete & g is infs-preserving holds
ex d being Function of T,S st
( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )

proof end;

:: Theorem 3.4 (dual)

theorem Th15: :: WAYBEL_1:15

for S, T being non empty Poset
for d being Function of T,S st T is complete & d is sups-preserving holds
ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )

proof end;

:: Corollary 3.5 (i)

theorem :: WAYBEL_1:16

for S, T being non empty Poset
for g being Function of S,T st S is complete holds
( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) )

proof end;

:: Corollary 3.5 (ii)

theorem Th17: :: WAYBEL_1:17

for S, T being non empty Poset
for d being Function of T,S st T is complete holds
( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) )

proof end;

:: Theorem 3.6 (1) iff (2)

theorem Th18: :: WAYBEL_1:18

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( d * g <= id S & id T <= g * d )

proof end;

:: Theorem 3.6 (2) implies (1)

theorem Th19: :: WAYBEL_1:19

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
[g,d] is Galois

proof end;

:: Theorem 3.6 (2) implies (3)

theorem Th20: :: WAYBEL_1:20

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
( d = (d * g) * d & g = (g * d) * g )

proof end;

:: Theorem 3.6 (3) implies (4)

theorem Th21: :: WAYBEL_1:21

for S, T being non empty RelStr
for g being Function of S,T
for d being Function of T,S st g = (g * d) * g holds
g * d is idempotent

proof end;

:: Proposition 3.7 (1) implies (2)

theorem Th22: :: WAYBEL_1:22

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}

proof end;

:: Proposition 3.7 (2) implies (3)

theorem Th23: :: WAYBEL_1:23

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds
g * d = id T

proof end;

:: Proposition 3.7 (4) iff (1)

theorem :: WAYBEL_1:24

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is onto iff d is V13() )

proof end;

:: Proposition 3.7 (1*) implies (2*)

theorem Th25: :: WAYBEL_1:25

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}

proof end;

:: Proposition 3.7 (2*) implies (3*)

theorem Th26: :: WAYBEL_1:26

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds
d * g = id S

proof end;

:: Proposition 3.7 (1*) iff (4*)

theorem :: WAYBEL_1:27

for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is V13() iff d is onto )

proof end;

:: Definition 3.8 (i)

definition

let L be non empty RelStr ;
let p be Function of L,L;

attr p is projection means :Def13: :: WAYBEL_1:def 13
( p is idempotent & p is monotone );

end;

:: deftheorem Def13 defines projection WAYBEL_1:def 13 :
for L being non empty RelStr
for p being Function of L,L holds
( p is projection iff ( p is idempotent & p is monotone ) );

registration

let L be non empty RelStr ;

cluster id L -> projection ;

coherence
id L is projection by YELLOW_2:21;

end;

registration

let L be non empty RelStr ;

cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total projection for M3( bool [: the carrier of L, the carrier of L:]);

existence
ex b₁ being Function of L,L st b₁ is projection

proof end;

end;

:: Definition 3.8 (ii)

definition

let L be non empty RelStr ;
let c be Function of L,L;

attr c is closure means :: WAYBEL_1:def 14
( c is projection & id L <= c );

end;

:: deftheorem defines closure WAYBEL_1:def 14 :
for L being non empty RelStr
for c being Function of L,L holds
( c is closure iff ( c is projection & id L <= c ) );

registration

let L be non empty RelStr ;

cluster Function-like quasi_total closure -> projection for M3( bool [: the carrier of L, the carrier of L:]);

coherence
for b₁ being Function of L,L st b₁ is closure holds
b₁ is projection ;

end;

Lm1: for L1, L2 being non empty RelStr
for f being Function of L1,L2 st L2 is reflexive holds
f <= f

proof end;

registration

let L be non empty reflexive RelStr ;

cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total closure for M3( bool [: the carrier of L, the carrier of L:]);

existence
ex b₁ being Function of L,L st b₁ is closure

proof end;

end;

registration

let L be non empty reflexive RelStr ;

cluster id L -> closure ;

coherence
id L is closure by Lm1;

end;

:: Definition 3.8 (iii)

definition

let L be non empty RelStr ;
let k be Function of L,L;

attr k is kernel means :: WAYBEL_1:def 15
( k is projection & k <= id L );

end;

:: deftheorem defines kernel WAYBEL_1:def 15 :
for L being non empty RelStr
for k being Function of L,L holds
( k is kernel iff ( k is projection & k <= id L ) );

registration

let L be non empty RelStr ;

cluster Function-like quasi_total kernel -> projection for M3( bool [: the carrier of L, the carrier of L:]);

coherence
for b₁ being Function of L,L st b₁ is kernel holds
b₁ is projection ;

end;

registration

let L be non empty reflexive RelStr ;

cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total kernel for M3( bool [: the carrier of L, the carrier of L:]);

existence
ex b₁ being Function of L,L st b₁ is kernel

proof end;

end;

registration

let L be non empty reflexive RelStr ;

cluster id L -> kernel ;

coherence
id L is kernel by Lm1;

end;

Lm2: for L being non empty 1-sorted
for p being Function of L,L st p is idempotent holds
for x being set st x in rng p holds
p . x = x

proof end;

theorem Th28: :: WAYBEL_1:28

for L being non empty Poset
for c being Function of L,L
for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)

proof end;

theorem Th29: :: WAYBEL_1:29

for L being non empty Poset
for k being Function of L,L
for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)

proof end;

definition

let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;

func corestr g -> Function of L1,(Image g) equals :: WAYBEL_1:def 16
the carrier of (Image g) |` g;

coherence
the carrier of (Image g) |` g is Function of L1,(Image g)

proof end;

end;

:: deftheorem defines corestr WAYBEL_1:def 16 :
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g = the carrier of (Image g) |` g;

theorem Th30: :: WAYBEL_1:30

for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g = g

proof end;

Lm3: for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g is onto

proof end;

registration

let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;

cluster corestr g -> onto ;

coherence
corestr g is onto by Lm3;

end;

theorem Th31: :: WAYBEL_1:31

for L1, L2 being non empty RelStr
for g being Function of L1,L2 st g is monotone holds
corestr g is monotone

proof end;

definition

let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;

func inclusion g -> Function of (Image g),L2 equals :: WAYBEL_1:def 17
id (Image g);

coherence
id (Image g) is Function of (Image g),L2

proof end;

end;

:: deftheorem defines inclusion WAYBEL_1:def 17 :
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g = id (Image g);

Lm4: for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g is monotone
by YELLOW_0:59;

registration

let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;

cluster inclusion g -> V13() monotone ;

coherence
( inclusion g is one-to-one & inclusion g is monotone ) by Lm4;

end;

theorem Th32: :: WAYBEL_1:32

for L being non empty RelStr
for f being Function of L,L holds (inclusion f) * (corestr f) = f

proof end;

::Theorem 3.10 (1) implies (2)

theorem Th33: :: WAYBEL_1:33

for L being non empty Poset
for f being Function of L,L st f is idempotent holds
(corestr f) * (inclusion f) = id (Image f)

proof end;

::Theorem 3.10 (1) implies (3)

theorem :: WAYBEL_1:34

for L being non empty Poset
for f being Function of L,L st f is projection holds
ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )

proof end;

::Theorem 3.10 (3) implies (1)

theorem :: WAYBEL_1:35

for L being non empty Poset
for f being Function of L,L st ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & i is monotone & f = i * q & id T = q * i ) holds
f is projection

proof end;

::Theorem 3.10 (1_1) implies (2_1)

theorem Th36: :: WAYBEL_1:36

for L being non empty Poset
for f being Function of L,L st f is closure holds
[(inclusion f),(corestr f)] is Galois

proof end;

::Theorem 3.10 (2_1) implies (3_1)

theorem :: WAYBEL_1:37

for L being non empty Poset
for f being Function of L,L st f is closure holds
ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d )

proof end;

::Theorem 3.10 (3_1) implies (1_1)

theorem Th38: :: WAYBEL_1:38

for L being non empty Poset
for f being Function of L,L st f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) holds
f is closure

proof end;

::Theorem 3.10 (1_2) implies (2_2)

theorem Th39: :: WAYBEL_1:39

for L being non empty Poset
for f being Function of L,L st f is kernel holds
[(corestr f),(inclusion f)] is Galois

proof end;

::Theorem 3.10 (2_2) implies (3_2)

theorem :: WAYBEL_1:40

for L being non empty Poset
for f being Function of L,L st f is kernel holds
ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )

proof end;

::Theorem 3.10 (3_2) implies (1_2)

theorem :: WAYBEL_1:41

for L being non empty Poset
for f being Function of L,L st f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) holds
f is kernel

proof end;

:: Lemma 3.11 (i) (part I)

theorem Th42: :: WAYBEL_1:42

for L being non empty Poset
for p being Function of L,L st p is projection holds
rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }

proof end;

theorem Th43: :: WAYBEL_1:43

for L being non empty Poset
for p being Function of L,L st p is projection holds
( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L )

proof end;

:: Lemma 3.11 (i) (part II)

theorem Th44: :: WAYBEL_1:44

for L being non empty Poset
for p being Function of L,L st p is projection holds
( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p )

proof end;

theorem Th45: :: WAYBEL_1:45

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc)

proof end;

theorem :: WAYBEL_1:46

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
p | Lk is Function of (subrelstr Lk),(subrelstr Lk)

proof end;

:: Lemma 3.11 (i) (part IIIa)

theorem Th47: :: WAYBEL_1:47

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure

proof end;

:: Lemma 3.11 (i) (part IIIb)

theorem :: WAYBEL_1:48

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel

proof end;

:: Lemma 3.11 (ii) (part I)

theorem Th49: :: WAYBEL_1:49

for L being non empty Poset
for p being Function of L,L st p is monotone holds
for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting

proof end;

:: Lemma 3.11 (ii) (part II)

theorem Th50: :: WAYBEL_1:50

for L being non empty Poset
for p being Function of L,L st p is monotone holds
for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
subrelstr Lk is infs-inheriting

proof end;

:: Lemma 3.11 (iii) (part I)

theorem :: WAYBEL_1:51

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) )

proof end;

:: Lemma 3.11 (iii) (part II)

theorem :: WAYBEL_1:52

for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) )

proof end;

:: Proposition 3.12 (i)

theorem Th53: :: WAYBEL_1:53

for L being non empty Poset
for p being Function of L,L holds
( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) )

proof end;

:: Proposition 3.12 (ii)

theorem :: WAYBEL_1:54

for L being non empty complete Poset
for p being Function of L,L st p is projection holds
Image p is complete

proof end;

:: Proposition 3.12 (iii)

theorem :: WAYBEL_1:55

for L being non empty Poset
for c being Function of L,L st c is closure holds
( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) )

proof end;

:: Proposition 3.12 (iv)

theorem :: WAYBEL_1:56

for L being non empty Poset
for k being Function of L,L st k is kernel holds
( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) )

proof end;

:: Proposition 3.15 (i)

theorem Th57: :: WAYBEL_1:57

for L being non empty complete Poset holds
( [(IdsMap L),(SupMap L)] is Galois & SupMap L is sups-preserving )

proof end;

:: Proposition 3.15 (ii)

theorem :: WAYBEL_1:58

for L being non empty complete Poset holds
( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic )

proof end;

definition

let S be non empty RelStr ;
let x be Element of S;

func x "/\" -> Function of S,S means :Def18: :: WAYBEL_1:def 18
for s being Element of S holds it . s = x "/\" s;

existence
ex b₁ being Function of S,S st
for s being Element of S holds b₁ . s = x "/\" s

proof end;

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

proof end;

end;

:: deftheorem Def18 defines "/\" WAYBEL_1:def 18 :
for S being non empty RelStr
for x being Element of S
for b₃ being Function of S,S holds
( b₃ = x "/\" iff for s being Element of S holds b₃ . s = x "/\" s );

theorem Th59: :: WAYBEL_1:59

for S being non empty RelStr
for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)

proof end;

theorem Th60: :: WAYBEL_1:60

for S being Semilattice
for x being Element of S holds x "/\" is monotone

proof end;

registration

let S be Semilattice;
let x be Element of S;

cluster x "/\" -> monotone ;

coherence
x "/\" is monotone by Th60;

end;

theorem Th61: :: WAYBEL_1:61

for S being non empty RelStr
for x being Element of S
for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }

proof end;

:: Lemma 3.16 (1) iff (2)

theorem Th62: :: WAYBEL_1:62

for S being Semilattice holds
( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S )

proof end;

:: Lemma 3.16 (1) implies (3)

theorem Th63: :: WAYBEL_1:63

for S being Semilattice st ( for x being Element of S holds x "/\" is lower_adjoint ) holds
for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)

proof end;

:: Lemma 3.16 (1) iff (3)

theorem :: WAYBEL_1:64

for S being non empty complete Poset holds
( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for X being Subset of S
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )

proof end;

:: Lemma 3.16 (3) implies (D)

theorem Th65: :: WAYBEL_1:65

for S being LATTICE st ( for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) holds
S is distributive

proof end;

definition

let H be non empty RelStr ;

attr H is Heyting means :: WAYBEL_1:def 19
( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) );

end;

:: deftheorem defines Heyting WAYBEL_1:def 19 :
for H being non empty RelStr holds
( H is Heyting iff ( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) ) );

registration

cluster non empty Heyting -> non empty reflexive transitive antisymmetric with_suprema with_infima for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is Heyting holds
( b₁ is with_infima & b₁ is with_suprema & b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric ) ;

end;

definition

let H be non empty RelStr ;
let a be Element of H;
assume A1: H is Heyting ;

func a => -> Function of H,H means :Def20: :: WAYBEL_1:def 20
[it,(a "/\")] is Galois ;

existence
ex b₁ being Function of H,H st [b₁,(a "/\")] is Galois by A1, Def12;
uniqueness
for b₁, b₂ being Function of H,H st [b₁,(a "/\")] is Galois & [b₂,(a "/\")] is Galois holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines => WAYBEL_1:def 20 :
for H being non empty RelStr
for a being Element of H st H is Heyting holds
for b₃ being Function of H,H holds
( b₃ = a => iff [b₃,(a "/\")] is Galois );

theorem Th66: :: WAYBEL_1:66

for H being non empty RelStr st H is Heyting holds
H is distributive

proof end;

registration

cluster non empty Heyting -> non empty distributive for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is Heyting holds
b₁ is distributive by Th66;

end;

definition

let H be non empty RelStr ;
let a, y be Element of H;

func a => y -> Element of H equals :: WAYBEL_1:def 21
(a =>) . y;

correctness
coherence
(a =>) . y is Element of H;
;

end;

:: deftheorem defines => WAYBEL_1:def 21 :
for H being non empty RelStr
for a, y being Element of H holds a => y = (a =>) . y;

theorem Th67: :: WAYBEL_1:67

for H being non empty RelStr st H is Heyting holds
for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y )

proof end;

theorem Th68: :: WAYBEL_1:68

for H being non empty RelStr st H is Heyting holds
H is upper-bounded

proof end;

registration

cluster non empty Heyting -> non empty upper-bounded for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is Heyting holds
b₁ is upper-bounded by Th68;

end;

theorem Th69: :: WAYBEL_1:69

for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds
( Top H = a => b iff a <= b )

proof end;

theorem :: WAYBEL_1:70

for H being non empty RelStr st H is Heyting holds
for a being Element of H holds Top H = a => a

proof end;

theorem :: WAYBEL_1:71

for H being non empty RelStr st H is Heyting holds
for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b

proof end;

theorem Th72: :: WAYBEL_1:72

for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds b <= a => b

proof end;

theorem :: WAYBEL_1:73

for H being non empty RelStr st H is Heyting holds
for a being Element of H holds Top H = a => (Top H)

proof end;

theorem :: WAYBEL_1:74

for H being non empty RelStr st H is Heyting holds
for b being Element of H holds b = (Top H) => b

proof end;

Lm5: for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) <= b

proof end;

theorem Th75: :: WAYBEL_1:75

for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H st a <= b holds
b => c <= a => c

proof end;

theorem :: WAYBEL_1:76

for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H st b <= c holds
a => b <= a => c

proof end;

theorem Th77: :: WAYBEL_1:77

for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) = a "/\" b

proof end;

theorem Th78: :: WAYBEL_1:78

for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c)

proof end;

definition

let H be non empty RelStr ;
let a be Element of H;

func 'not' a -> Element of H equals :: WAYBEL_1:def 22
a => (Bottom H);

correctness
coherence
a => (Bottom H) is Element of H;
;

end;

:: deftheorem defines 'not' WAYBEL_1:def 22 :
for H being non empty RelStr
for a being Element of H holds 'not' a = a => (Bottom H);

theorem :: WAYBEL_1:79

for H being non empty RelStr st H is Heyting & H is lower-bounded holds
for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }

proof end;

theorem Th80: :: WAYBEL_1:80

for H being non empty RelStr st H is Heyting & H is lower-bounded holds
( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H )

proof end;

:: Exercise 3.18 (i)

theorem :: WAYBEL_1:81

for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds
( 'not' a >= b iff 'not' b >= a )

proof end;

:: Exercise 3.18 (ii)

theorem Th82: :: WAYBEL_1:82

for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds
( 'not' a >= b iff a "/\" b = Bottom H )

proof end;

theorem :: WAYBEL_1:83

for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H st a <= b holds
'not' b <= 'not' a

proof end;

theorem :: WAYBEL_1:84

for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds 'not' (a "\/" b) = ('not' a) "/\" ('not' b) by Th78;

theorem :: WAYBEL_1:85

for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)

proof end;

definition

let L be non empty RelStr ;
let x, y be Element of L;

pred y is_a_complement_of x means :: WAYBEL_1:def 23
( x "\/" y = Top L & x "/\" y = Bottom L );

end;

:: deftheorem defines is_a_complement_of WAYBEL_1:def 23 :
for L being non empty RelStr
for x, y being Element of L holds
( y is_a_complement_of x iff ( x "\/" y = Top L & x "/\" y = Bottom L ) );

definition

let L be non empty RelStr ;

attr L is complemented means :: WAYBEL_1:def 24
for x being Element of L ex y being Element of L st y is_a_complement_of x;

end;

:: deftheorem defines complemented WAYBEL_1:def 24 :
for L being non empty RelStr holds
( L is complemented iff for x being Element of L ex y being Element of L st y is_a_complement_of x );

registration

let X be set ;

cluster BoolePoset X -> complemented ;

coherence
BoolePoset X is complemented

proof end;

end;

Lm6: for L being bounded LATTICE st L is distributive & L is complemented holds
for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )

proof end;

Lm7: for L being bounded LATTICE st ( for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) holds
( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )

proof end;

:: Exercise 3.19

theorem Th86: :: WAYBEL_1:86

for L being bounded LATTICE st L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) holds
for x being Element of L holds 'not' x is_a_complement_of x

proof end;

:: Exercise 3.19 (1) iff (2)

theorem Th87: :: WAYBEL_1:87

for L being bounded LATTICE holds
( L is distributive & L is complemented iff ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) )

proof end;

:: Definition 3.20

definition

let B be non empty RelStr ;

attr B is Boolean means :: WAYBEL_1:def 25
( B is LATTICE & B is bounded & B is distributive & B is complemented );

end;

:: deftheorem defines Boolean WAYBEL_1:def 25 :
for B being non empty RelStr holds
( B is Boolean iff ( B is LATTICE & B is bounded & B is distributive & B is complemented ) );

registration

cluster non empty Boolean -> non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is Boolean holds
( b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric & b₁ is with_infima & b₁ is with_suprema & b₁ is bounded & b₁ is distributive & b₁ is complemented ) ;

end;

registration

cluster non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented -> non empty Boolean for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric & b₁ is with_infima & b₁ is with_suprema & b₁ is bounded & b₁ is distributive & b₁ is complemented holds
b₁ is Boolean ;

end;

registration

cluster non empty Boolean -> non empty Heyting for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is Boolean holds
b₁ is Heyting by Th87;

end;

registration

cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Boolean for RelStr ;

existence
ex b₁ being LATTICE st
( b₁ is strict & b₁ is Boolean & not b₁ is empty )

proof end;

end;

registration

cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Heyting for RelStr ;

existence
ex b₁ being LATTICE st
( b₁ is strict & b₁ is Heyting & not b₁ is empty )

proof end;

end;