Algebraic General Topology. Vol 1: Paperback / E-book || Axiomatic Theory of Formulas: Paperback / E-book

As an Amazon Associate I earn from qualifying purchases.

Pointf ree Funcoids
by Victor Porton
Web: http://www.mathematics21.org
October 13, 2012
Abstract
It is a part of my Algebraic General Topology research.
I generalize the point-set notion of funcoids to pointfree topology notion of pointfree
funcoids.
In my yet unpublished research pointfree funcoids are used to dene products of funcoids.
Keywords: algebraic general topology, funcoids, reloids
A.M.S. subject classication: 54J05, 54A05, 54D99, 54E05, 54E15, 54E17, 54E99
Table of contents
1 Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
2 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
3 Pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
3.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
3.2 Composition of pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
3.3 Pointfree funcoid as continuation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
3.4 The preorder of pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
3.5 More on composition of pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
3.6 Domain and range of a pointfree funcoid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
3.7 Category of pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
3.8 Specifying funcoids by functions or relations on atomic filter objects . . . . . . . . . . . 9
3.9 Direc t product of elements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.10 Atomic pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.11 Complete pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.12 Completion and co-completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.13 Monovalued and injective pointfree funcoids . . . . . . . . . . . . . . . . . . . . . . . . . 1 8
3.14 Elements closed regarding a pointfree funcoid . . . . . . . . . . . . . . . . . . . . . . . . 19
3.15 Connectedness regarding a pointfree funcoid . . . . . . . . . . . . . . . . . . . . . . . . . 20
Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1 Preface
This article generalizes the notions of funcoids introduce d in [2], I call this gen eralization pointfree
funcoids.
In my yet unpublished research pointfree funco ids are used to define products of funcoids .
2 Notat ion
First we use the notation introduced in [3] and [2].
. This document has been written using the GNU T
E
X
MACS
text editor (see www.texmacs.org).
1
In addition to atoms
A
x, the set of atoms under an element x of a poset A we will write just
atoms
A
for all atoms of a poset A.
3 Pointfree funcoids
3.1 Definition
Definition 1. Pointfree funcoid is a quadruple (A; B; α; β) w here A and B are posets, α B
A
and β A
B
such that
x A, y B: (y
B
αx x
A
βy).
Definition 2. The source Src (A; B; α; β) = A and destin ation Dst (A; B; α; β) = B for every
pointfree funcoid (A; B; α; β).
Definition 3. I will denote FCD(A; B) the set of pointfree funcoids from A to B (that is with
source A and de stination B), for every posets A and B.
Proposition 4. If A and B have least elements, then FCD(A; B) has least element.
Proof. It is (A; B; A × {0
B
}; B × {0
A
}).
Definition 5. h(A; B; α; β)i =
def
α for a pointfree funcoid (A; B; α ; β).
Definition 6. (A; B; α; β)
1
= (B; A; β; α) for a pointfree funcoid (A; B; α; β).
Proposition 7. If f is a pointfree funcoid then f
1
is also a pointfree funcoid.
Proof. Follows from symmetry in the definitio n of pointfree funcoid.
Obvious 8 . (f
1
)
1
= f for a pointfree funcoid f.
Definition 9. The relation [f]P(Src f × Ds t f ) is defined by the formula (for every pointfree
funcoid f and x Src f, y Dst f)
x [f ] y =
def
y
Dst f
hf ix.
Obvious 10. x [f ] y y
Dst f
hf ix x
Src f
hf
1
iy for every pointfree funcoid f an d x Src f ,
y Dst f.
Obvious 1 1. [f
1
]=[f ]
1
for a pointfree funcoid f .
Theorem 12. Let A and B are posets. Then:
1. If A is separable, for given value o f hf i exists no more than one f FCD(A; B);
2. If A and B are separable, for given value of [f ] exists no more than one f FCD(A; B).
Proof. Let f , g FCD(A; B).
1. Let hf i = hg i. Then for every x A, y B we have x
A
hf
1
iy y
B
hf ix y
B
hgix
x
A
hg
1
iy and thus by separability of A we have hf
1
iy = hg
1
iy th at is hf
1
i = hg
1
i
and so f = g.
2. Let [f ]=[g]. Then for every x A, y B we have y
B
hf ix x [f ] y x [g ] y y
B
hgix
and t hus by separability of B we have hf ix = hgix that is hf i = hgi. Similarly we have
hf
1
i = hg
1
i. Thus f = g.
Proposition 13. If Dst f is separable, then hf i0
Src f
= 0
Dst f
for e very p ointfree funcoid f.
2 Section 3
Proof. y
hf i0
Src f
0
Src f
hf
1
iy 0 y
0
Dst f
. Thus by separability, hf i0
Src f
= 0
Dst f
.
Proposition 14. If Dst f is a separable meet semilattice with le ast element then hf i is a monotone
function (for a pointfree funcoid f).
Proof. a b x Dst f : (a
hf
1
ix b
hf
1
ix) x A: (x
hf ia x
hf ib) hf ia hf ib
(used the theorem 19 in [3]).
Theorem 15. Let f is a pointfree funcoid from a distributive lattice Src f with least element to
a separ able distributive lattice Dst f with least element. Then hf i(i
Src f
j) = hf ii
Dst f
hf ij for
every i, j Src f .
[TODO: In the book this theorem is strenghtened for starrish semilattices instead
of distributive lattices.]
Proof.
hf i(i
Src f
j) =
{y A | y
Dst f
hf i(i
Src f
j)
0
Dst f
} =
{y A | (i
Src f
j)
Src f
hf
1
iy
0
Src f
} =
{y A | (i
Src f
hf
1
iy)
Src f
(j
Src f
hf
1
iy)
0
Src f
} =
{y A | i
Src f
hf
1
iy
0
Src f
j
Src f
hf
1
iy
0
Src f
} =
{y A | y
Dst f
hf ii
0
Dst f
y
Dst f
hf ij
0
Dst f
} =
{y A | (y
Dst f
hf ii)
Dst f
(y
Dst f
hf ij)
0
Dst f
} =
{y A | y
Dst f
(hf ii
Dst f
hf ij)
0
Dst f
} =
(hf ii
Dst f
hf ij).
Thus hf i(i
Src f
j) = hf ii
Src f
hf ij by separability.
Proposition 16. Let f is a pointfree funcoid. Then:
[TODO: This theorem is also strenghtened
in the book.]
1. k [f] i j k [f ] i k [f ] k for every i, j Dst f, k Src f if Dst f is a distributive lattice
with least element.
2. i j [f ] k i [f] k j [f ] k for every i, j Src f, k Dst f if Src f is a distributive lattice
with least element.
Proof. 1. k [f ] i
Dst f
j (i j)
Dst f
hf ik
0
Dst f
(i
Dst f
hf ik) (j
Dst f
hf ik)
0
Dst f
i
Dst f
hf ik
0
Dst f
j
Dst f
hf ik
0
Dst f
k [f ] i k [f ] j.
2. Similar.
3.2 Composition of pointfree funcoids
Definition 17. Composition of pointfree funcoids is defined by the formula
(B; C; α
2
; β
2
) (A; B; α
1
; β
1
) = (A; C; α
2
α
1
; β
1
β
2
).
Definition 18. I will call funcoids f and g compo sable when Dst f = Src g.
Proposition 19. If f , g are pointfree funcoids and Dst f = Src g then g f is pointfree funcoid.
Proof. Let f = (A; B; α
1
; β
1
), g = (B; C; α
2
; β
2
). For every x, y A we have
y
C
(α
2
α
1
)x y
C
α
2
α
1
x α
1
x
B
β
2
y x
A
β
1
β
2
y x
A
(β
1
β
2
)y.
So (A; C; α
2
α
1
; β
1
β
2
) is a pointfree funcoid.
Obvious 2 0. hg f i = hg i hf i for every composable pointfree funcoids f and g.
Pointfree funcoids 3
Theorem 21. (g f)
1
= f
1
g
1
for every composable pointfree funcoids f and g.
Proof.
h(g f )
1
i = hf
1
i hg
1
i = hf
1
g
1
i;
h((g f )
1
)
1
i = hg f i = h(f
1
g
1
)
1
i.
Proposition 22. (h g) f = h (g f) for every composable pointfree funcoids f, g, h.
Proof.
h(h g) f i = hh gi hf i = hhi hgi hf i = hhi hg f i = hh (g f)i.
h((h g) f )
1
i = hf
1
(h g)
1
i = hf
1
g
1
h
1
i = h(g f )
1
h
1
i = h(h (g f ))
1
i.
3.3 Pointfree funcoid as continuation
Proposition 23. Let f is a pointfree funcoid. Then for every x Src f, y Dst f we have
1. If (Src f ; Z) is a filtrator with separable core then x [f] y X up
(Src f;Z)
x: X [f ] y.
2. If (Dst f ; Z) is a filtrator with separable c ore then x [f ] y Y up
(Dst f ;Z)
x: x [f] Y .
Proof. We will prove on ly the second because the rst is similar.
x [f ] y y
Dst f
hf ix Y up y: Y
Dst f
hf ix Y up y: x [f] Y .
Corollary 24. Let f is a pointfree funcoid and (Src f; Z
0
), (Dst f; Z
1
) are filtrators with separable
core. Then
x [f] y X up
(Src f ;Z
0
)
x, Y up
(Dst f ;Z
1
)
y: X [f ] Y .
Proof. Apply the proposition twice.
Theorem 25. Let f be a pointfree funcoid. Let (Src f ; Z
0
) is a finitely meet-closed filtrator with
separable core and (Dst f ; Z
1
) is a primary filtrator over a distribut ive lattice.
hf ix =
\
Dst f
hhf iiup
(Src f;Z)
x.
Proof. By the previous proposition for every y Dst f :
y
Dst f
hf ix x [f ] y X up
(Src f;Z
0
)
x: X [f ] y X up
(Src f;Z
0
)
x: y
Dst f
hf iX.
Let’s denote W =
y
Dst f
hf iX | X up
(Src f;Z
0
)
x
. We will prove that W is a generalized filter
base over Z
1
. To prove this enough to show that V =
hf iX | X up
(Src f ;Z
0
)
x
is a generalized
filter base.
Let P, Q V . Then P = hf iA, Q = hf iB where A, B up
(Src f;Z
0
)
x; A
Z
0
B up
(Src f ;Z
0
)
x
(used the fact that it is a finitely meet-closed and the theorem 29 in [3]) and R P
Dst f
Q for
R = hf i(A
Z
0
B) V . So V is a generalized filter base and thus W is a generalized filter base.
0
Dst f
W
T
Dst f
W
0
Dst f
by the properties o f generalized filter bases. That is
X up
(Src f ;Z
0
)
x: y
Dst f
hf iX
0
Dst f
y
Dst f
\
Dst f
hhf iiup
(Src f ;Z
0
)
x
0
Dst f
.
Comparing with the above, y
Dst f
hf ix
0
Dst f
y
Dst f
T
Dst f
hhf iiup
(Src f;Z
0
)
x
0
Dst f
. So
hf ix =
T
Dst f
hhf iiup
(Src f ;Z
0
)
x because Dst f is separable.
Theorem 26. Let (A; Z
0
) and (B; Z
1
) are primary ltrators over boolean lattices.
1. A function α B
Z
0
conforming to the formulas (for every I , J Z
0
)
α0
Z
0
= 0
B
, α(I
Z
0
J) = αI
B
αJ
4 Section 3
can be continued to the function hf i for a unique f FCD(A; B);
hf iX =
\
B
hαiup
(A;Z
0
)
X (1)
for every X A.
2. A relation δ P(Z
0
× Z
1
) conforming to the formulas (for every I , J , K Z
0
and I
, J
,
K
Z
1
)
¬(0
Z
0
δ I), I
Z
0
J δ K
I δ K
J δ K
,
¬(I
δ 0
Z
1
), K δ I
Z
1
J
K δ I
K δ J
(2)
can be continued to the relation [f ] for a unique f FCD(A; B);
X [f ] Y X up
(A;Z
0
)
X , Y up
(B;Z
1
)
Y: X δ Y (3)
for every X A, Y B.
Proof. E xistence of no more than one such pointfree funcoids and formulas (1) and (3) follow
from two previous theorems.
2. {Y Z
1
| X δ Y } is obviously a free star for every X Z
0
. By properties of filters on bo olean
lattices, there exist a unique filter object αX such that (αX) = {Y Z
1
| X δ Y } for every X Z
0
.
Thus α B
Z
0
. Similarly it can be de fined β A
Z
1
by the formula (βX) = {X Z
0
| X δ Y }. Le t’s
continue the functions α and β to α
B
A
and β
A
B
by the formulas
α
X =
\
B
hαiup
(A;Z
0
)
X and β
X =
\
A
hβ iup
(B;Z
1
)
X
and δ to δ
P(A × B) by the formula
X δ
Y X up
(A;Z
0
)
X , Y up
(B;Z
1
)
Y: X δ Y .
Y
B
α
X
0
B
Y
B
T
B
hαiup
(A;Z
0
)
X
0
B
T
B
hY
B
ihαiup
(A;Z
0
)
X
0
B
. Let’s prove that
W = hY
B
ihαiup
(A;Z
0
)
X
is a generalized filter base: To prove it is enou gh to show that hαiup
(A;Z
0
)
X is a generalized filter
base.
If A, B hαiup
(A;Z
0
)
X then exis t X
1
, X
2
up
(A;Z
0
)
X such that A = αX
1
and B = αX
2
.
Then α(X
1
Z
0
X
2
)hαiupX . So hαiupX is a g eneralized filter base and thus W is a generalized
filter base.
By properties of generalized filter bases,
T
B
hY
B
ihαiup
(A;Z
0
)
X
0
B
is equivalent to
X up
(A;Z
0
)
X : Y
B
αX
0
B
,
what is equivalent to X up
(A;Z
0
)
X , Y up
(B;Z
1
)
Y: Y
B
αX
0
B
X up
(A;Z
0
)
X ,
Y up
(B;Z
1
)
Y: Y (α X) X up
(A;Z
0
)
X , Y up
(B;Z
1
)
Y: X δ Y . C ombining the
equivalencies we get Y
B
α
X
0 X δ
Y . Analogously X
A
β
Y
0
A
X δ
Y . So
Y
B
α
X
0
B
X
A
β
Y
0
A
, that is (A; B; α
; β
) is a pointfree funcoid. From the formula
Y
B
α
X
X δ
Y follows tha t [(A; B; α
; β
)] is a continuation of δ.
1. Let de fine the relation δ P (Z
0
× Z
1
) by the formula X δ Y Y
B
αX
0
B
.
That ¬(0
Z
0
δ I
) and ¬(I δ 0
Z
1
) is obvious. We have K δ I
Z
1
J
(I
Z
1
J
)
B
αK
0
B
(I
B
J
)
B
αK
0
B
(I
B
αK)
B
(J
B
αK)
0
B
I
B
αK
0
B
J
B
αK
0
B
K δ I
K δ J
and I
Z
0
J δ K
K
B
α(I
Z
0
J)
0
B
K
B
(α I
B
αJ)
0
B
(K
B
αI)
B
(K
B
αJ)
0
B
K
B
αI
0
B
K
B
αJ
0
B
I δ K
J δ K
.
That is the formulas (2) are true.
Accordingly the above δ can be continued to th e relation [f ] for some f FCD(A; B).
X Z
0
, Y Z
1
:(Y
B
hf iX
0 X [f] Y Y
B
αX
0
B
), consequently X Z
0
:αX =hf iX
because our filtrato r is with separable core. So hf i is a continuation of α.
Proposition 27. Let (Src f; Z
0
) is a primary ltrator over a bounded distributive lattic e element
and (Dst f; Z
1
) is a primary filtrator over a distributive lattice. If S is a genera lize d filter ba se on
Src f then hf i
T
Src f
S =
T
Dst f
hhf iiS for every pointfree funcoid f.
Pointfree funcoids 5
Proof. (Src f ; Z
0
) is a finitely meet-closed filtrator by theorem 29 in [3] and with separable core
by theorem 37 and corollary 10 in [3]; thus we can apply theorem 25.
hf i
T
Src f
S hf iX for every X S a nd thus hf i
T
Src f
S
T
Dst f
hhf iiS.
Taking into account properties of generalized filter bases:
hf i
\
Src f
S =
\
Dst f
hhf iiup
\
S =
\
Dst f
{hhf iiX | ∃P S: X up P } =
\
Dst f
{hf iX | ∃P S: X up P }
\
Dst f
{hf iP | P S } =
\
Dst f
hhf iiS.
3.4 The preorder of pointfree funcoids
The preorder of pointfree funcoids is defined by the formula f g [f][g] for every po intfree
funcoids f and g.
Remark 28. It is enough to define preorder of pointfree funcoids on every set FCD(A; B) where
A and B are posets. We d o not need to compare pointfree funcoids with different sources or
destinations.
Theorem 29. If A and B are sep arable posets then FCD(A; B) is a poset.
Proof. From the theorem 12.
Theorem 3 0. Let (A; Z
0
) and (B; Z
1
) are primary filtrators over boolean lattices. Then for
R P FCD(A; B) and X Z
0
, Y Z
1
we have:
1. X
S
FCD(A;B)
R
Y f R: X [f] Y ;
2.
S
FCD(A;B)
R
X =
S
B
{hf iX | f R}.
Proof.
2. αX =
def
S
B
{hf iX | f R} (by corollary 8 in [3] all joins on B exist). We have α0
A
= 0
B
;
α(I
Z
0
J) =
[
B
{hf i(I
Z
0
J) | f R}
=
[
B
{hf i(I
A
J) | f R}
=
[
B
{hf iI
B
hf i J | f R}
=
[
B
{hf iI | f R}
B
[
B
{hf iJ | f R}
= αI
B
αJ
(used the theorem 15). By the theorem 26 the function α can be continued to hhi for a h FCD(A;
B). Obviously
f R: h f. (4)
And h is the least element of FCD(A; B) for which holds the condition (4). So h =
S
FCD(A;B)
R.
1. X [
S
FCD
R] Y Y
B
h
S
FCD
RiX
0
B
Y
B
S
B
{hf iX | f R}
0
B
f R:
Y
B
hf iX
0
B
f R: X [f ] Y (used the theorem 40 in [3]).
Corollary 31. If (A; Z
0
) and (B; Z
1
) are primary filtrators over boolean lattices then FCD(A; B)
is a complete latt ic e.
6 Section 3
Proof. A and B are separable accordingly obvious 20 in [3].
Then apply [1] taking in account the theorem 12.
Theorem 32. Let A and B are starrish join-semilattices. Then:
1.
f
FCD(A;B)
g
x = hf ix
B
hgix for every x A;
2.
f
FCD(A;B)
g
=[f ][g].
Proof.
1. Let α X =
def
hf ix
B
hgix; β Y =
def
hf
1
iy
A
hg
1
iy for every x A, y B. Then
y
B
αx y
B
hf ix y
B
hgix
x
A
hf
1
iy x
A
hg
1
iy
x
A
hf
1
iy
A
hg
1
iy
x
A
βy.
So h = (A; B; α ; β) is a pointfree funcoid. Obviously h f and h g. If p f and p g for some
p FCD(A; B) then hpi x hf ix
B
hgix = hhix that is p h. So f
FCD(A;B)
g = h.
2. x
f
FCD(A;B)
g
y y
B
f
FCD(A;B)
g
x y
B
hf ix
B
hgix y
B
hf ix y
B
hgix
x [f ] y x [g] y for every x A, y B.
Theorem 33. Let f is a pointfree f uncoid from a separable poset A to a separable poset B. If
hf i is an injection, then hf i is an order embedding A B.
Proof. Suppose x y but hf ix + hf iy.
Then by separability of B there exist z
hf iy such that z hf ix.
Thus hf
1
iz x and hf
1
iz
y what is impossible for x y.
Corollary 34. Let f is a pointfree funcoid from a separable poset A to a se parable poset B. If
hf i is a bij ection A B, then hf i is an order isomorphism A B.
3.5 More on composition of pointfree funcoids
Proposition 35. [g f ]=[g]◦hf i = hg
1
i
1
[f ] for every composable pointfree funcoids f and g.
Proof. x [g f] y y
Dst g
hg f ix y
Dst g
hgihf ix hf ix [g] y x([g]◦hf i)y for every
x A, y B. Thus [g f]=[g]◦hf i. [g f]=[(f
1
g
1
)
1
]=[f
1
g
1
]
1
=([f
1
]◦hg
1
i)
1
=
hg
1
i
1
[f].
Theorem 36. Let f and g are pointfree funcoids and A = Dst f = Src g is an a tomic poset. Then
for every X Src f and Z Dst g
X [g f ] Z y a toms
A
: (X [f] y y [g] Z).
Proof.
y atoms
A
: (X [f ] y y [g] Z) y atoms
A
: (Z
Dst g
hgiy y
A
hf iX )
y atoms
A
: (Z
Dst g
hgiy y hf iX )
Z
Dst g
hgihf iX
X [g f] Z.
Reversely, if X [g f ] Z then hf iX [g] Z, consequently exists y atoms
A
hf iX such that y [g] Z;
we have X [f] y.
Theorem 37. Let A, B, C are posets and B is atomic. Then:
1. f (g
FCD(A;B)
h) = f g
FCD(A;C)
f h for g, h FCD(A; B) and f FCD(B; C).
Pointfree funcoids 7
2. (g
FCD(B;C)
h) f = g f
FCD(A;C)
h f for f FCD(A; B) and g, h FCD(B; C).
Proof. I will prove only the first equality because the other is analogous.
For every X A, Y C
X
f (g
FCD(A;B)
h)
Z y atoms
B
: (X
g
FCD(A;B)
h
y y [f ] Z)
y atoms
B
: ((X [g] y X [h] y) y [f] Z)
y atoms
B
: ((X [g] y y [f] Z) (X [h] y y [f] Z))
y atoms
B
: (X [g] y y [f ] Z) y atoms
B
: (X [h] y y [f] Z)
X [f g] Z X [f h] Z
X
f g
FCD(A;C)
f h
Z.
3.6 Domain and range of a pointfree funcoid
Definition 38. Let A is a poset. The identity pointfree funcoid I
FCD(A)
= (A; A; (=)|
A
; (=)|
A
).
It is trivial that identity funcoid is really a pointfree funcoid.
Let now A is a meet-semilattice.
Definition 39. Let a A. The restricted identity pointfree funcoid I
a
FCD(A)
= (A; A; a
A
; a
A
).
Proposition 40. The restricted pointfree funcoid is a pointfree funcoid.
Proof. We need to prove that (a
A
x)
A
y (a
A
y)
A
x what is obvious.
Obvious 4 1.
I
A
FCD(A)
1
= I
A
FCD(A)
.
Obvious 4 2. x
h
I
A
FCD(A)
i
y a
A
x
A
y for every x, y A.
Definition 43. I will define restricting of a pointfree funcoid f to an element a Src f by the
formula f |
a
=
def
f I
a
FCD(Src f )
.
Definition 44. Let f is a pointfree funcoid whose source has greatest element 1.
Image of f will be defined by the formula im f = hf i1.
Definition 45. Domain of a pointfree funcoid f is defined by the formula dom f = imf
1
(when
f has a poset with greatest element as its destination).
Proposition 46. hf ix = hf i(x
Src f
dom f ) for every pointfree f uncoid f whose destination is a
separable poset with greatest element and source is a meet-semilattice and x Src f .
Proof. For every y Dst f we have y
Dst f
hf i(x
Src f
dom f )
0
Dst f
x
Src f
dom f
Src f
hf
1
iy
0
Src f
x
Src f
imf
1
Src f
hf
1
iy
0
Src f
x
Src f
hf
1
iy
0
Src f
y
Dst f
hf ix. Thus hf ix = hf i(x
Src f
dom f) by separability of Dst f.
Proposition 47. x
Src f
dom f (hf ix is not least) for every pointfree funcoid f whose
destination is a poset with greatest element and x Src f.
Proof. x
Src f
dom f x
Src f
hf
1
i1 1
Dst f
Dst f
hf ix (hf ix is not least).
Corollary 48. dom f =
S
Src f
{a atoms
Src f
| hf ia
0
Dst f
} for every pointfree funcoid f whose
destination is a bounded poset and source is an atomistic meet- semilattice.
Proof. For every a atoms
Src f
we have a
Src f
dom f a
Src f
im f
1
a
Src f
hf
1
i1
Dst f
1
Dst f
hf ia hf ia
0
Dst f
. So
8 Section 3
dom f =
S
Src f
{a atoms
Src f
| a
Src f
dom f } =
S
Src f
{a atoms
Src f
| hf ia
0
Dst f
}.
Proposition 49. dom f |
a
FCD(Src f )
=a
Src f
dom f for every pointfree funcoid f and a Src f where
Src f is a meet-semilattice and Dst f has greatest element.
Proof. dom f |
a
FCD(Src f )
=im
I
a
FCD(Src f )
f
1
=
D
I
a
FCD(Src f )
E
hf
1
i1
Dst f
= a
Src f
hf
1
i1
Dst f
=
a
Src f
dom f .
Proposition 50. For every composable pointfree funcoids f and g where the posets Src f and
Dst f = Src g have greatest elements:
1. If im f dom g then im(g f) = im g.
2. If im f dom g then dom(g f) = dom g.
Proof.
1. im(g f) = hg f i1
Src f
= hg ihf i1
Src f
= hgiim f = hgi(im f
Dst f
dom g) = hgidom g =
hgi1
Src g
= im g.
2. dom(g f) = im(f
1
g
1
) what by the proved is equ al to im f
1
that is dom f.
3.7 Category of pointfree funcoids
I will define the categor y pfFCD of pointfree funcoids:
The class of objects are small po sets.
The set of morphisms from A to B is FCD(A; B).
The composition is the composition of pointfree funcoids.
Id entity morphism for an object A is (A; A; (=)|
A
; (=)|
A
).
To prove that it is really a category is trivial.
The category of funcoid triples is defined as follows:
Objects are pairs (A; A) where A is a small poset and A A.
The morphisms from an object (A; A) to an object (B; B) are tuples (f ; A; B; A; B) where
f FCD(A; B) and dom f A im f B.
The composition is defined by the formula (g; B; C) (f ; A; B) = (g f ; A; C).
Id entity morphism for an object (A; A) is I
A
FCD(A)
.
To prove that it is really a category is trivial.
3.8 Specifying funcoids by functions or relations on atomic filter objects
Theorem 51. Let A is an atomic poset and (B; Z
1
) is a primary fil trator over a boolean lattice.
Then for every f FCD(A; B) and X A we have
hf iX =
[
B
hhf iiatoms
A
X .
Proof. For every Y Z
1
we have
Y
B
hf iX X
A
hf
1
iY
x atoms
A
X : x
A
hf
1
iY
x atoms
A
X : Y
B
hf ix.
Thus hf iX =
S
h i hhf iiatoms
A
X =
S
B
hhf iiatoms
A
X (used the theorem 46 in [3]).
Consequently hf iX =
S
B
hhf iiatoms
A
X by the c orollary 15 in [3].
Pointfree funcoids 9
Proposition 52. Let f is a pointfree funcoid. Then for every X Src f and Y Dst f
1. X [f ] Y x atoms
Src f
X : x [f ] Y if Src f is an atomic poset.
2. X [f ] Y y atoms
Dst f
Y: X [f ] y if Dst f is an atomic pose t.
Proof. I will prove only the second as the first is similar.
If X [f] Y, then Y
Dst f
hf iX , consequently exists y atoms
Dst f
Y such that y
Dst f
hf iX ,
X [f ] y. The reverse is obvious.
Corollary 53. If f is a pointfree funcoid with both source and destination being atomic posets,
then for every X Src f and Y Dst f
X [f ] Y x atoms
Src f
X , y atoms
Dst f
Y: x [f ] y.
Proof. Apply the theorem twice.
Corollary 54. If A is a separable atomic poset and B is an atomistic poset then f is determined
by the values of hf iX for X atoms
A
.
Proof. y
Dst f
hf ix x
Src f
hf
1
iy X atoms x: X
Src f
hf
1
iy X atoms x:
y
Dst f
hf iX.
Thus by atomisticity hf i is determined by hf iX f or X atoms x.
By separability of A we infer that f ca n be restored from hf i.
Theorem 55. Let (A; Z
0
) and (B; Z
1
) are primary ltrators over boolean lattices.
1. A function α B
atoms
A
such that (for every a atoms
A
)
αa
\
B
[
B
hαi atoms
A
up
(A;Z
0
)
a (5)
can be continued to the function hf i for a unique f FCD(A; B);
hf iX =
[
B
hαiatoms
A
X (6)
for every X A.
2. A relation δ P (atoms
A
× atoms
B
) such that (for every a atoms
A
, b atoms
B
)
X up
(A;Z
0
)
a, Y up
(B;Z
1
)
b x atoms
A
X , y atoms
B
Y : x δ y a δ b (7)
can be continued to the relation [f ] for a unique f FCD(A; B);
X [f ] Y x atoms
A
X , y atoms
B
Y: x δ y (8)
for every X A, Y B.
Proof. E xistence of no more than one such funcoids and formulas (6) and (8) follow from the
theorem 51 and corollary 53 and the fact that our ltrators are with separable core.
1. Consider the function α
B
Z
0
defined by the formula (for every X Z
0
)
α
X =
[
B
hαiatoms
A
X.
Obviously α
0
Z
0
= 0
B
. For every I , J Z
0
α
(I J) =
[
B
hα
iatoms
B
(I J)
=
[
B
hα
i(atoms
B
I atoms
B
J)
=
[
B
(hα
iatoms
B
I hα
iatoms
B
J)
=
[
B
hα
i atoms
B
I
B
[
B
hα
iatoms
B
J.
= α
I
B
α
J.
10 Section 3
Let continue α
till a funcoid f (by the theorem 26): hf iX =
T
B
hα
iup
(A;Z
0
)
X .
Let’s prove t he reverse of (5):
\
B
[
B
hαi atoms
A
up
(A;Z
0
)
a =
\
B
[
B
hαi
hatoms
A
iup
(A;Z
0
)
a
\
B
[
B
hαi
{{a}}
=
\
B

[
B
hαi
{a}
=
\
B
[
B
hαi{a}
=
\
B
[
B
{αa}
=
\
B
{αa} = αa.
Finally,
αa =
\
B
[
B
hαi atoms
A
up a =
\
B
hα
iup
(A;Z
0
)
a = hf ia,
so hf i is a continuation of α.
2. Consider the relation δ
P(Z
0
× Z
1
) defined by the formula (for every X Z
0
, Y Z
1
)
X δ
Y x atoms
A
X , y atoms
B
Y : x δ y.
Obviously ¬(X δ
0
Z
1
) and ¬(0
Z
0
δ
Y ).
(I J) δ
Y x atoms
A
(I J ), y atoms
B
Y : x δ y
x atoms
A
I atoms
A
J , y atoms
B
Y : x δ y
x atoms
A
I , y atoms
B
Y : x δ y x atoms
A
J , y atoms
B
Y : x δ y
I δ
Y J δ
Y ;
similarly X δ
(I J) X δ
I X δ
J. Let’s continue δ
till a funcoid f (by the theorem 26):
X [f ] Y X up
(A;Z
0
)
X , Y up
(B;Z
1
)
Y: X δ
Y
The reverse of (7) implication is trivial, so
X up
(A;Z
0
)
a, Y up
(B;Z
1
)
b x atoms
A
X , y atoms
B
Y : x δ y a δ b.
X up
(A;Z
0
)
a, Y up
(B;Z
1
)
b x atoms
A
X , y atoms
B
Y : x δ y X up
(A;Z
0
)
a, Y up
(B;Z
1
)
b:
X δ
Y a [f ] b.
So a δ b a [f ] b, that is [f] is a continuation of δ.
One of uses of the previous theorem is the proof of the following theorem:
Theorem 56. Let (A; Z
0
) and (B;Z
1
) are primary filtrators over boolean lattices. If R P FCD(A;
B) and x atoms
A
, y atoms
B
, then
1.
T
FCD(A;B)
R
x =
T
B
{hf ix | f R};
2. x
T
FCD(A;B)
R
y f R: x [f ] y.
Proof.
2. Let de note x δ y f R: x [f ] y.
X up
(A;Z
0
)
a, Y up
(B;Z
1
)
b x atoms
A
X , y atoms
B
Y : x δ y
f R, X up
(A;Z
0
)
a, Y up
(B;Z
1
)
b x atoms
A
X , y atoms
B
Y : x [f ] y
f R, X up
(A;Z
0
)
a, Y up
(B;Z
1
)
b: X [f ] Y
f R: a [f ] b
a δ b.
So, by the theorem 55, δ can be continued till [p] for some p FCD(A; B).
For every q FCD(A; B) such that f R: q f we have x [q] y f R: x [f] y x δ y x [p] y,
so q p. Consequently p =
T
FCD(A;B)
R.
Pointfree funcoids 11
From this x
T
FCD(A;B)
R
y f R: x [f ] y.
1. From the former y atoms
B
T
FCD(A;B)
R
x y
B
T
FCD(A;B)
R
x
0
B
f R :
y
B
hf ix
0
B
y
T
hatoms
B
i{hf ix | f R} y atoms
B
T
B
{hf ix | f R} for every
y atoms
B
.
B is atomically separable by the corollary 17 in [3]. Thus
\
FCD(A;B)
R
x =
\
B
{hf ix | f R}.
Theorem 57. Let A, B, C are posets of filter objects over some boolean lattices, f FCD(A; B),
g FCD(B; C), h FCD(A; C). Then
g f
h g
h f
1
.
Proof.
g f
h
a atoms 1
A
, c atoms 1
C
: a [(g f ) h] c
a atoms 1
A
, c atoms 1
C
: (a [g f ] c a [h] c)
a atoms 1
A
, b atoms 1
B
, c atoms 1
C
: (a [f] b b [g] c a [h] c)
b atoms 1
B
, c atoms 1
C
: (b [g] c b [h f
1
] c)
b atoms 1
B
, c atoms 1
C
: b [g (h f
1
)] c
g
h f
1
.
3.9 Direct product of elements
Definition 58. Let A and B are posets with least ele ments and A A, B B. Funcoidal product
of A, B A is such a pointfree funcoid A ×
FCD
B FCD(A; B) that
X [A ×
FCD
B] Y X
A
A Y
B
B.
Proposition 59. A ×
FCD
B is really a pointfree funcoid and for every X A
hA ×
FCD
BiX =
(
B if X
A
A;
0
B
if X
A
A.
Proof. Obvious.
Proposition 60. Let A and B are bounde d posets, f FCD(A; B), A A, B B. Then
f A ×
FCD
B dom f A im f B.
Proof. If f A ×
FCD
B then do m f dom(A ×
FCD
B) A, im f im(A ×
FCD
B) B. If
dom f A im f B then
∀X A, Y B: (X [f] Y X
A
A Y
B
B);
consequently f A ×
FCD
B.
Theorem 61. Let A, B are sets of filters over boolean lattices. For every f FCD(A; B) and
A A, B B
f
FCD(A;B)
(A ×
FCD
B) = I
B
FCD(B)
f I
A
FCD(A)
.
Proof. From above FCD(A; B) is a (complete) lattice.
12 Section 3
h =
def
I
B
FCD(B)
f I
A
FCD(A)
. For every X A
hhiX =
D
I
B
FCD(B)
E
hf i
D
I
A
FCD(A)
E
X = B
B
hf i(A
A
X ).
From this, as easy to show, h f and h A ×
FCD
B. If g f g A ×
FCD
B for a g FCD(A; B)
then dom g A, im g B,
hgiX = B
B
hgi(A
A
X ) B
B
hf i(A
A
X ) =
D
I
B
FCD(B)
E
hf i
D
I
A
FCD(A)
E
X = hhiX ,
g h. So h = f
FCD(A;B)
(A ×
FCD
B).
Corollary 62. Let A, B are sets of lters over boolean lattices. For every f FCD(A; B) and
A A we have f |
A
=f (A ×
FCD
1
B
).
Proof. f (A ×
FCD
1
B
) = I
1
B
FCD(B)
f I
A
FCD(A)
= f I
A
FCD(A)
= f |
A
.
Corollary 63. Let A, B are sets of lters over boolean lattices. For every f FCD(A; B) and
A A, B B we have
f
FCD(A;B)
(A ×
FCD
B)
0
FCD(A;B)
A [f ] B.
Proof. f
FCD(A;B)
(A ×
FCD
B)
0
FCD(A;B)
f
FCD(A;B)
(A ×
FCD(A;B)
B)
1
A
0
B
D
I
B
FCD(B)
f I
A
FCD(A)
E
1
A
0
B
D
I
B
FCD(B)
E
hf i
D
I
A
FCD(A)
E
1
A
0
B
B
B
hf i(A
A
1
A
)
0
B
B
B
hf iA
0
B
A [f] B.
Theorem 6 4. Let A, B are sets of filters over boolean lattices. Then the poset FCD(A; B) is
separable.
Proof. Let f , g FCD(A;B) and f
g. By the theorem 12 [f]
[g]. That is there exist x, y A such
that x[f ] y <x [g] y that is f
FCD(A;B)
(x ×
FCD
y)
0
FCD(A;B)
< g
FCD(A;B)
(x ×
FCD
y)
0
FCD(A;B)
.
Thus FCD(A; B) is separable.
Theorem 65. Let (A; Z
0
) and (B; Z
1
) are primary filtrators over b oolean lattices. If S P (A × B)
then
\
FCD(A;B)
{A ×
FCD
B | (A; B) S } =
\
A
dom S ×
FCD
\
B
im S.
Proof. If x atoms
A
then by the theorem 56
\
FCD(A;B)
{A ×
FCD
B | (A; B) S }
x =
\
B
{hA ×
FCD
Bix | (A; B) S }.
If x
A
T
A
dom S
0
A
then
(A; B) S: (x
A
A
0
A
A ×
FCD(A;B)
B
x = B);
{hA ×
FCD
Bix | (A; B) S } = im S;
if x
A
T
A
dom S = 0
A
then
(A; B) S: (x
A
A = 0
A
hA ×
FCD
Bix = 0
B
);
{hA ×
FCD
Bix | (A; B) S } 0
B
.
So
\
FCD(A;B)
{A ×
FCD
B | (A; B) S }
x =
(
T
B
im S if x
A
T
A
dom S
0
A
;
0
B
if x
A
T
A
dom S = 0
A
.
From this by corollary 53 (taking in account 47 in [3]) follows the statement of the theorem.
Corollary 66. Let (A; Z
0
) and (B; Z
1
) are primary filtrato rs over boolean lattices.
Pointfree funcoids 13
For every A
0
, A
1
A and B
0
, B
1
B
(A
0
×
FCD
B
0
)
FCD(A;B)
(A
1
×
FCD
B
1
) = (A
0
FCD(A;B)
A
1
) ×
FCD
(B
0
FCD(A;B)
B
1
).
Proof. (A
0
×
FCD
B
0
)
FCD(A;B)
(A
1
×
FCD
B
1
) =
T
FCD(A;B)
{A
0
×
FCD
B
0
, A
1
×
FCD
B
1
} what is by the
last theorem equal to (A
0
FCD(A;B)
A
1
) ×
FCD
(B
0
FCD(A;B)
B
1
).
Theorem 67. Let (A; Z
0
) and (B; Z
1
) are primary filtrato rs over boolean lattices. If A A then
A ×
FCD
is a complete homomorphism of the lattice A to a the lattice FCD(A; B), if also A
0
A
then it is an order embedding.
Proof. Let S PA, X Z
0
, x atoms
A
.
[
FCD(A;B)
hA ×
FCD
iS
X =
[
B
{hA ×
FCD
BiX | B S }
=
(
S
B
S if X
A
A
0
A
;
0
B
if X
A
A = 0
A
=
A ×
FCD
[
B
S
X.
Thus
S
FCD(A;B)
hA ×
FCD
iS = A ×
FCD
S
B
S by the theorem 25 (taking in account obvious 20 in [3]).
\
FCD(A;B)
hA ×
FCD
iS
x =
\
B
{hA ×
FCD
Bix | B S }
=
(
T
B
S if x
A
A
0
A
;
0
B
if x
A
A = 0
A
=
A ×
FCD
\
B
S
x.
Thus
T
FCD(A;B)
hA ×
FCD
iS = A ×
FCD
T
B
S by the theorem 56.
If A
0
A
then obviously the function A ×
FCD
is injective.
Proposition 68. Let A is a meet-semilattice and B is a poset with least element. If a is an atom
of A, f FCD(A; B) then f |
a
=a ×
FCD
hf ia.
Proof. Let X A.
X
A
a
0
A
hf |
a
iX = hf ia, X
A
a = 0
A
hf |
a
iX = 0
B
.
3.10 Atomic pointfree funcoids
Theorem 69. Let A, B are se ts of filters over boolean lattices. A f FCD(A; B) is a n atom of
the poset FCD(A; B) iff there exist a atoms
A
and b atoms
B
such that f = a ×
FCD
b.
Proof. A and B are atomic by the theorem 47 in [3].
. Let f is an a tom of the pose t FCD(A; B). Let’s get ele ments a atoms
A
dom f and
b atoms
B
hf ia. Then for every X A
X
A
a ha ×
FCD
biX = 0
B
hf iX , X
A
a ha ×
FCD
biX = b hf iX .
So a ×
FCD
b f; because f is atomic we have f = a ×
FCD
b.
. Let a atoms
A
, b atoms
B
, f FCD(A; B). If b
B
hf ia then ¬(a [f ] b),
f
FCD(A;B)
(a ×
FCD
b) = 0
FCD(A;B)
(because A and B are bounded meet-semilattices); if b
hf ia then ∀X A:(X
A
a hf iX b), f a ×
FCD
b. Consequently f
FCD(A;B)
(a ×
FCD
b) =
0
FCD(A;B)
f a ×
FCD
b; that is a ×
FCD
b is an atomic filter object.
Theorem 70. Let A, B are sets of lters over boolean lattices. Then FCD(A; B) is atomic.
14 Section 3