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

As an Amazon Associate I earn from qualifying purchases.

This ﬁle is with partial proofs (with rough gibberish) about open problems I have tried to solve

but have failed. If you solve something of this please notify me by email porton@narod.ru.

Conjecture 1. (RLD)

out

(g ◦ f )w (RLD)

out

g ◦ (RLD)

out

f ( v or w) for composable funcoids f and

g.

Proof. (RLD)

out

g ◦ (RLD)

out

f =

d

G2up g

RLD

G ◦

d

F 2up f

RLD

F v G ◦ F for every F 2 up f and G 2 up g.

Thus (RLD)

out

g ◦ (RLD)

out

f v

d

F 2up f ;G2up g

RLD

(G ◦ F ) v ?? [FIXME: Opposite inequalities!]

(RLD)

out

(g ◦ f ) =

d

RLD

up(g ◦ f ) = ?? =

d

F 2up f ;G 2up g

RLD

(G ◦ F ) w

d

G2up (RLD)

out

g;F 2up (RLD)

out

f

RLD

(G ◦ F ) =

d

G2up

d

R L D

up g;F 2up

d

R L D

up f

RLD

(G ◦ F ) =

d

RLD

up g ◦

d

RLD

up f

Proposition 2. A product of nonempty posets is a dcpo if and only iﬀ each multiplier is a dcpo.

Proof. [TODO: More detailed proof] Suppose one multiplier is not a dcpo. Take a chain with ﬁxed

elements (thanks our posets are nonempty) from other multipliers and for this multiplier take the

values which form a chain without the join. This proves that the product is not a dcpo.

Now take that all multipliers are dcpo. Take a chain that is a set for which holds a vb ^ b v a )

a = b.

We have

??

Take an element t of the chain.

For each k we have a

i

0

=

a

i

if i = k

t

i

if i =/ k

and b

i

0

=

b

i

if i = k

t

i

if i =/ k

a

0

?? belongs to the chain?

??We have a

i

v b

i

^ b

i

v a

i

) a

i

= b

i

for all a, b in the chain. Take

Let . Take

??

It is a chain componentwise because the predicate a v b ^ b v a ) a = b holds?? componentwise.

Thus every component has a (calculated componentwise) join.

Conjecture 3. Funcoids f from A to B bijectively corresponds to the sets R of pairs (X ; Y) of

ﬁlters (on A and B correspondingly) that

1. R is nonempty.

2. R is a lower set.

3. R is a dcpo (or what is the same product of two dcpos)

4. We can add axiom: A ×

FCD

B v

F

fX ×

FCD

Y j (X ; Y) 2 R

0

g ) (A; B) 2 R

by the mutually inverse formulas:

(X ; Y) 2 R , X ×

FCD

Y v f (1)

f =

G

fX ×

FCD

Y j (X ; Y) 2 Rg: (2)

Proof. Let R be deﬁned by formula (1). That R is a nonempty lower set is obvious. Let's prove

that R is a dcpo.

Let T be a chain in R and 8(A; B) 2 T : A ×

FCD

B v f.

8(A; B) 2 T : (X / A ) B v hf iX )

taking join we have:

X / A )

F

B2Pr

1

T

B v hf iX

A ×

FCD

F

B2Pr

1

T

B v f

Repeating this, we get

F

A2Pr

0

T

A ×

FCD

F

B2Pr

1

T

B v f . Thus R is a dcpo.

It remains to prove that the formulas are mutually inverse.

Let f

0

be a funcoid, R be induced by f

0

by formula (1), f

1

be induced by R by formula (2).

We will prove that f

1

= f

0

.

Misc 1

f

1

=

F

fX ×

FCD

Y j X ×

FCD

Y v f

0

g what is equal to f

0

because the lattice of funcoids is

atomistic and every atom is a funcoidal product.

Let now R

0

be a set of pairs of ﬁlters conformung to our axioms, f be a funcoid induced by R

by formula (2), R

1

be a set of pairs of ﬁlters induced by f by formula (1). We will prove R

1

= R

0

.

(X ; Y) 2 R

1

, X ×

FCD

Y v

F

fX ×

FCD

Y j (X ; Y) 2 R

0

g ( (X ; Y) 2 R

0

X ×

FCD

Y v

F

fX ×

FCD

Y j (X ; Y) 2 R

0

g ) (X ; Y) 2 R

0

because ??. [FIXME: It seems we need

additional axioms!]

Theorem 4. If a funcoid is weakly metamonovalued, then it is monovalued.

Proof. We have (g u h) ◦ f = (g ◦ f) u (h ◦ f) for every reloids g, h. We need to prove that f is

monovalued.

Prove that exists F 2 up f such that for every g, h we have (g u h) ◦ F = (g ◦ F ) u (h ◦ F ).

it's enough to prove that (g u h) ◦ F w (g ◦ F ) u (h ◦ F )

Really, ??

thus F is monovalued.

f ◦ f

¡1

=

d

fF ◦ F

¡1

j F 2 up f g

Proposition 5. The following statements are equivalent for every endofuncoid µ and a set U:

1. U is connected regarding µ.

2. For every a; b 2 U there exists a totally ordered set P ⊆ U such that min P = a, max P = b,

and for every partion fX; Y g of P into two sets X, Y such that 8x 2 X ; y 2 Y : x < y, we

have X [µ]

∗

Y.

Proof.

(. Let A; B 2 PU are nonempty. We need to prove A [µ]

∗

B. We can assume without loss of

generality that A \ B = ;. Because A and B are nonempty, we can take a 2 A and b 2 B. ??

). The case a =b is trivial. Assume a=/ b. Take A; B 2PU such that a 2A, b 2 B and A[B = U

and A \ B = ;. Then take orders P

A

on A with min P

A

= a and P

B

on B with max P

B

= b.

Then the poset P = P

A

+ P

B

??

1 Directed funcoids

Let [¡1; +1] be the extended real line with the complete funcoid induced by the usual topology

on this set.

Proposition 6. Every ultraﬁlter on [¡1; +1] converges to exactly one point.

Proof. It is a well known fact.

Below is wrong: http://math.stackexchange.com/q/1874451/4876

[FIXME: below is wrong] Use http://math.stackexchange.com/a/1874862/4876

[TODO: ∆

+

! ∆

>

or ∆

≥

]

[TODO: Compare without explicit formulas.]

Lemma 7. For every ultraﬁlter a and its limit point x:

0. h[¡1; +1]ia = ∆(x) if x = a

1. h[¡1; +1]ia = ∆

+

(x) if x > a

2. h[¡1; +1]ia = ∆

¡

(x) if x < a

Proof. 0. Obvious.

1. h[¡1; +1]ia =

d

A2up a

h[¡1; +1]i

∗

A =

d

A2up a; Av]x;+1]

h[¡1; +1]i

∗

A =

d

A2up a; Av]x;+1]

F

y2A

∆(y)

2 Section 1

Because every y > x, we have ∆(y) v ]x; +1] and thus h[¡1; +1]ia v ]x; +1].

It is clear that

F

y2A

∆(y) w ∆

+

(x) and h[¡1; +1]ia v ∆

+

(x). Thus h[¡1; +1]ia = ∆

+

(x).

2. h[¡1; +1]ia =

d

A2up a

h[¡1; +1]i

∗

A =

d

A2up a;Av[¡1;x[

h[¡1; +1]i

∗

A =

d

A2up a; Av[¡1;x [

F

y2A

∆(y)

Because every y < x we have ∆(y) v [¡1; x[ and thus h[¡1; +1]ia v [¡1; x[.

It is clear that

F

y2A

∆(y) w ∆

¡

(x) and h[¡1; +1]ia v ∆

¡

(x). Thus h[¡1; +1]ia = ∆

¡

(x).

[TODO: More detailed proof.]

Corollary 8. For every ultraﬁlter a and its limit point x:

h[¡1; +1] u ≥ia = ∆

+

(x) if x ≥ a

h[¡1; +1] u ≥ia = ? if x < a

Proof. Take into account h[¡1; +1] u ≥ia = h[¡1; +1]i a u h≥ia.

Lemma 9. . Then for every ultraﬁlter a and its limit point x:

0. ??

1.

D

[¡1; +1]

E

a = ∆

+

(x) if x ≥ a

2.

D

[¡1; +1]

E

a = ∆

¡

(x) if x < a

Proof. hRia =

d

A2up a

hRi

∗

A =

d

A2up a

F

y2A

∆

+

(y)

1. ??

2. hRia =

d

A2up a;Av[¡1;x[

F

y2A

∆

+

(y) = ??

F

y2A

∆

+

(y) w ∆

¡

(x);

F

y2A;A v[¡1;x[

∆

+

(y) w ∆

¡

(x)

hRia v ∆

¡

(x) is obvious.

Theorem 10. [¡1; +1] u

FCD

>=/ [¡1; +1].

Proof. h[¡1; +1] u ≥ia = ? if x < a but

D

[¡1; +1]

E

a = ∆

¡

(x) if x < a.

Proposition 11. f

~

= Compl(f u >).

Proof. ??

2 Entourages of product of funcoids

Lemma 12. 8H 2 up(g ◦ f)9F 2 up f : H w g ◦ F

Proof. H w g ◦ F , H ◦ f

¡1◦

w g (proposition 1813). But f

¡1◦

w f

¡1

, thus H w g ◦ F (

H ◦ f

¡1

w g. Take G = H ◦ f

¡1

, but H ◦ f

¡1

2/ up g because g ◦ f ◦ f

¡1

w g does not hold by

http://math.stackexchange.com/a/1862976/4876

??

[FIXME: This was proof of another lemma. ]

Instead of funcoids we will assume that f and g are ﬁlters on ¡ (they are isomorphic).

g ◦ f =

d

F¡

up

¡

(g ◦ f) =

d

F¡

((up

¡

g) ◦ (up

¡

f)) =

d

F 2up

¡

f ;G 2up

¡

g

F¡

(G ◦ F ) (lemma 1274).

g ◦ f =

d

F 2up f ;G 2up g

F¡

(G ◦ F ) (follows from above or directly from theorm 781)

fG ◦ F j F 2 up f ; G 2 up gg is?? a generalized ﬁlter base on ¡.

Thus by properties of generalized ﬁlter bases (on ¡) for every H 2 up

¡

(g ◦ f) there exists

F 2 up

¡

f, G 2 up

¡

g such that G ◦ F v H.

??

Attempt to construct it: [Example: f =1, choose F

H

0

= 1 and G

H

0

= H

0

. Then

d

H

0

2up

¡

H

G

H

0

=

d

H

0

2up

¡

H

H

0

= Cor H 2 up f .]

Entourages of product of funcoids 3

Represent H as a meet of elements of ¡ (H =

d

up

¡

H). For each H

0

2up

¡

H choose F

H

0

2up

¡

f,

G

H

0

2 up

¡

g such that H

0

w G

H

0

◦ F

H

0

. Moreover we can choose maximal F

H

0

, G

H

0

such that this

inequatily holds. Then take F =

d

H

0

2up

¡

H

F

H

0

and G =

d

H

0

2up

¡

H

G

H

0

. [FIXME: Does F 2 up f ?]

[TODO: If this does not work, then seems that there is a counter-example, because it is the

stongest.]

[TODO: We MUST take maximal rather than arbitrary F

H

0

, G

H

0

. Otherwise take f = 1, g = id

Ω

.

Then if we take F

H

0

= 1 and replace all possible G

H

0

! G

H

0

n f(a; b)g, then G = ? 2/ up g]

??

H 2 up(g ◦ f ) ) hH i

∗

X w hg ◦ f i

∗

X = hgihf i

∗

X.

For every X take Y

X

2 up hf i

∗

X such that hgiY

X

v hH i

∗

X. If g is complete, we may assume

that Y

X

is a maximal set for which hgiY

X

v hH i

∗

X holds.

Take F =

d

f(X × Y

X

) t (X × >) j X 2 T Src f g. But is F complete or co-complete, or if meet

is taken on Rel, do we have F 2 up f?

??

Let g be principal. Let a be an atomic ﬁlter. Take (??not always possible) Y

a

2 up hf i

∗

a such

that hgiY

a

v hH ia

Let F =

F

a2atoms

(a × Y

a

) - also co-complete

??

Let for each b 2 atoms hf i

∗

a deﬁne Z

b

= ??

??

Let f be complete. Replace it with principal funcoid F , such that hf i

∗

fxg v hF i

∗

x v Y

fxg

.

Prove g ◦ F v H

??

Split F into a join of monovalued functions. This does not work because every function produces

its own g.

??

G ◦ f v H; G ◦ Compl f = Compl(G ◦ f ) v H

??

hG ◦ f i

∗

X = hGihf i

∗

X = hGi

d

hhf i

∗

i

∗

up X v

d

hhG ◦ f i

∗

i

∗

up X v ?? v hg ◦ f i

∗

X v hH iX

??

Find maximal [FIXME: there is no maximal because composition is not distributive over arbi-

trary joins.] funcoids F and G such that G ◦ F v H, then prove they are principal (or (co-)complete)

??

Replace G with G

M

mapping x 7! hGi

∗

fxg, Then ?? consider it as an isomorphism between sets.

(Q ◦ P )

M

x = hQ ◦ P i

∗

fxg = hQihP i

∗

fxg = hQiP

M

x

g ◦ F v H , hgi ◦ F

M

v H

M

??

f = (FCD)(RLD)

in

f, g = (FCD)(RLD)

in

g; H 2 up(g ◦ f )

??

Use Todd Trimble's idea with ξ: H 2 up(g ◦ f ) , (AH

~

C ( A(g ◦ f)

~

C) , (AH

~

C ( 9B :

(Af

~

B ^Bg

~

C)) ,(AH

~

C ( 9B: (B w hf iA ^ C whg iB)) [FIXME: check direction of implication]

f(A; C) j C w hH iAg ⊇ f(A; C) j 9B: (B w hf iA ^ C w hg iB)g.

Suppose A 2 dom f(A; C) j 9B: (B w hf iA ^ C w hgiB)g or C 2 im f(A; C) j 9B: (B w hf iA ^

C w hgiB)g.

Then 9B: (B w hf iA ^ C w hgiB). Take B

A;C

such that B

A;C

w hf iA ^ C w hg iB

A;C

Take B

A

0

=

T

C 2??

B

A;C

.

Then B

A

0

w hf iA ^ C w hgiB

A

0

. [FIXME: it does not hold, only B

A

0

w Cor hf iA]

Take co-complete funcoid hF iA = B

A

0

. It is possible?? because B

X tY

0

=

T

C 2??

B

X tY ;C

= ??

B

A;X tY

w hf i(X t Y ) ^ C w hg iB

X tY ;C

??

Instead of intersecting funcoids, consider join f =

F

X 2??

X × Y

X

or f =

F

X 2??

X × Y

X

. It is

enough to consider ultraﬁlters X .

Theorem 13. 8H 2 up(g ◦ f )9F 2 up f ; G 2 up g: H w G ◦ F for every composable funcoids f and

g. [TODO: Also state it for reloids.]

4 Section 2

Proof. Let H 2 up(g ◦ f ). Then 9F 2 up f: H w g ◦ F that is H 2 up(g ◦ F ). Thus 9G 2 up g such

that H w G ◦ F .

3 Join of transitive reloids

(f t g) ◦ (f t g) w (f ◦ f ) t (g ◦ g) [need other direction]

Join of compositions of all ﬁnite sequences of f and g (in any order). It is equivalent to taking

all alternating S

∗

(f ◦ g ◦ f ◦ ::: ◦ f) starting or ending with f or g.

“Relationships between completeness properties” in https://en.wikipedia.org/wiki/Complete-

ness_%28order_theory%29

or alternatively:

µ = (f t g) t ((f t g) ◦ (f t g)) t ((f t g) ◦ (f t g) ◦ (f t g)) t :::

µ ◦ µ w µ

“No similarly useful description of a subbase for the inﬁmum of a family of quasi-uniformities

is known.” by http://www.sciencedirect.com/science/article/pii/S0166864107000181

—

up

F

n2N; f

n;i

2S

(f

n;n

◦ ::: ◦ f

n;0

)

=

T

n2N;f

n;i

2S;F

n;i

2up f

n;i

(F

n;n

◦ ::: ◦ F

n;0

)

Lemma 14. µ =

F

n2N; f

n;i

2S

(f

n;n

◦ ::: ◦ f

n;0

) is a transitive reloid, for every set S of endoreloids

(on the same set).

Proof. Denote [U

n

: n 2 N] =

F

n2N

(U

n

◦ ::: ◦ U

0

).

Let U

n;X

2 up X for all n 2 N and X 2 S.

S

X 2S

U

n;X

: n 2 N

is ??

We need to prove µ ◦ µ v µ.

F

X 2S

U

n;X

: n 2 N

2 up µ.

Let U

n;X

2 X and U

n

=

S

X 2S

U

n;X

.

Then

F

X 2S

U

2n;X

: n 2 N

◦

F

X 2S

U

2n¡1;X

: n 2 N

⊆

F

X 2S

U

n;X

: n 2 N

because??

U

2n;X

◦ U

2n¡1;X

2

F

X 2S

U

n;X

: n 2 N

?? [TODO: No need for reindexation.]

??

U

n

is the join of all compositions of n-tuples. They form a generalized ﬁlter base. Thus it's

enough to show that every U

n

can be decomposed into smaller n-tuples. But that's obvious. (It

isn't because it is an inﬁnite join!)

Thus is above U

n

0

◦ U

n

00

.

Thus µ is also decomposed, because every its element is minorated as shown above.

??

Take P 2 up µ. Then P 2 up A for every A 2 up(f

n;n

◦ ::: ◦ f

n;0

).

P w F

N ;N

◦ ::: ◦ F

N ;0

for some F

N ;i

2 up f

N ;i

for all N 2 N.

Thus P w

F

n2N; f

i

2S

(F

N ;N

◦ ::: ◦ F

N ;0

) where F

N ;i

2 up f

N ;i

.

Take F

N

0

= F

N ;bN /2 c

◦ ::: ◦ F

N ;0

and F

N

00

= F

N ;N

◦ ::: ◦ F

N ;bN /2 c+1

This way we exhaust all possible values?

(F

n;n

◦ ::: ◦ F

n;n

) ◦ (F

m;m

◦ ::: ◦ F

m;0

) v P . But this is obvious.

Thus easily follows P w

¡

F

n2N; f

i

2S

(F

n;n

◦ ::: ◦ F

n;0

)

◦

¡

F

n2N; f

i

2S

(F

n;n

◦ ::: ◦ F

n;0

)

;

P 2 up(µ ◦ µ).

Alternative formula:

S

hGRi

∗

S t Z(

S

hGRi

∗

S) t Z(Z(

S

hGRi

∗

S)) t :::

[TODO: Both for reloids and for Cauchy spaces ¡

i

as in the attached article in email.]

[TODO: Also for funcoids (using (FCD)).]

3.1 Exponentials in category of graphs

http://arxiv.org/pdf/math/0605275.pdf deﬁnition 2.3 deﬁnes exponential graph

Join of transitive reloids 5

Let G and H are graphs.

The exponential graph MOR(G; H) is deﬁned by the formulas:

Ob MOR(G; H) = (Ob H)

Ob G

;

(f; g) 2 GR MOR(G; H) , 8(v; w) 2 GR G: (f (v); g(w)) 2 GR H

for every f ; g 2 Ob MOR(G; H) = (Ob H)

Ob G

.

Equivalently

(f; g) 2 GR MOR(G; H) , 8(v; w) 2 GR G: g ◦ f(v; w)g ◦ f

¡1

⊆ GR H

(f; g) 2 GR MOR(G; H) , g ◦ (GR G) ◦ f

¡1

⊆ GR H

(f; g) 2 GR MOR(G; H) ,

f ×

(C)

g

GR G ⊆ GR H

Evaluation ": (MOR(G; H) × G) ! H

If (f; g) 2 GR MOR(G; H) and x 2 GR G then "((f; g); x) = (fx; gx) = g ◦ f(x; x )g ◦ f

¡1

3.2 Exponentials in category Fcd

The below gives deﬁnitions for exponential object, (exponential) evaluation, and exponential trans-

pose, but no proof is given that they are really exponential object, (exponential) evaluation, and

exponential transpose. Please write porton@narod.ru if you ﬁnd a proof.

If G, H are endofuncoids, then MOR(G ; H) (exponential object) is an endofuncoid.

MOR(G; H) =

G

ft 2 atoms FCD((Ob H)

Ob G

; (Ob H)

Ob G

) j (im t) ◦ G ◦ (dom t)

¡1

v H g =

G

t 2 atoms FCD((Ob H)

Ob G

; (Ob H)

Ob G

) j

(dom t) ×

(C)

(im t)

G v H

:

Evaluation:

"

¡¡

f ×

(A)

g

×

(A)

x

= hf i(RLD)

in

x ×

FCD

hgi(RLD)

in

x:

"

¡¡

f ×

(A)

g

×

(A)

x

= g ◦ ((RLD)

in

x ×

FCD

(RLD)

in

x) ◦ f

¡1

=

f ×

(C)

g

((RLD)

in

x ×

FCD

(RLD)

in

x)

for atomic f ; g 2 FCD(Ob G; Ob H).

Evaluation ": MOR(A; B) × A ! B

"(F × x) =

G

g ◦ (x ×

FCD

x) ◦ f

¡1

j f ; g 2 atoms

FCD(Ob A;Ob B)

; f × g / F

:

"(F × x) =

F

fg

1

×

FCD

f

1

j f

0

; g

0

; f

1

; g

1

2 atoms

F

; (f

0

×

FCD

f

1

) × (g

0

×

FCD

g

1

) / F g.

Proposition 15. ": MOR(A; B) × A ! B.

Proof. We need to prove " ◦ (MOR(A; B) × A) v B ◦ ". ??

Transpose ∼f: Z ! MOR(A; B) for a morphism f: Z × A ! B

(∼f )x =

G

fb ×

FCD

hf i(x × b) j b 2 atoms

FCD

g:

Proposition 16. ∼f : Z ! MOR(A; B).

Proof. We need to prove ∼f ◦ Z v MOR(A; B) ◦ ∼f whenever f ◦ (Z × A) v B ◦ f . ??

Awoday 6.5 “Equational deﬁnition” gives a simple way to check cartesian closed categories.

It's enough to prove:

1. " ◦ (∼f × 1

A

) = f

2. " ◦ ∼(g × 1

A

) = g

"(∼f × 1

A

)x = "((∼f )x × x) =

F

fg

1

×

FCD

f

1

j f

0

; g

0

; f

1

; g

1

2 atoms

F

; (f

0

×

FCD

f

1

) × (g

0

×

FCD

g

1

) /

(∼f )xg = ??

??

6 Section 3

4 Exponentials in category Rld

If now G, H are endoreloids, then MOR(G; H) is an endoreloid.

Deﬁnition 17. MOR

α

(G;H)=

F

t 2atoms

RLD((Ob H)

Ob G

;(Ob H)

Ob G

)

j (im t)◦ G◦(domt)

¡1

vH

.

Proposition 18. MOR

α

(G; H) =

F

t

0

×

RLD

t

1

j t

0

; t

1

2 atoms

F((Ob H)

Ob G

)

; t

1

◦ G ◦ t

0

¡1

v H

.

Proof. If t

0

; t

1

2 F((Ob H)

Ob G

) and t

1

◦ G ◦ t

0

¡1

v H then there are t 2 atoms(t

0

×

RLD

t

1

). Thus

(im t) ◦ G ◦ (dom t)

¡1

v H and t 2 atoms

RLD((Ob H)

Ob G

;(Ob H )

Ob G

)

.

If t 2 atoms

RLD((Ob H)

Ob G

;(Ob H)

Ob G

)

and (im t) ◦ G ◦ (dom t)

¡1

v H then dom t = t

0

and im t = t

1

for some t

0

; t

1

2 atoms

F((Ob H)

Ob G

)

and thus t

1

◦ G ◦ t

0

¡1

v H.

Deﬁnition 19. MOR

β

(G; H)=

F

ft 2 RLD((Ob H)

Ob G

; (Ob H)

Ob G

) j (im t) ◦ G ◦(dom t)

¡1

vH g.

Conjecture 20. MOR

α

(G; H) = MOR

β

(G; H).

Obvious 21.

1. MOR

α

(G; H) =

F

t 2 atoms

RLD((Ob H)

Ob G

;(Ob H)

Ob G

)

j

(dom t) ×

(C)

(im t)

G v H

;

2. MOR

β

(G; H) =

F

t 2 RLD((Ob H)

Ob G

; (Ob H)

Ob G

) j

(dom t) ×

(C)

(im t)

G v H

.

Conjecture 22.

1. t 2 atoms MOR

a

(G; H) , (im t) ◦ G ◦ (dom t)

¡1

v H;

2. t 2 atoms MOR

β

(G; H) , (im t) ◦ G ◦ (dom t)

¡1

v H.

Evaluation ": (MOR(G; H) × G) ! H that is for x 2 G = RLD(Ob G; Ob G)

it is a function on objects deﬁned by the formula:

[TODO: Infer x and y from x × y.]

"((f ×

RLD

g) × x) = g ◦ (x ×

RLD

x) ◦ f

¡1

=

f ×

(C)

g

(x ×

RLD

x)

for atomic f ; g 2 F((Ob H)

Ob G

).

"(F × x) =

F

fg ◦ (x ×

RLD

x) ◦ f

¡1

j f ; g 2 F((Ob H)

Ob G

); f ×

RLD

g / F g

Let now f : Z × A ! B.

In Set f

~

(a)(b) = f (a; b); f

~

(a) = b 7! f (a; b)

(∼f )a =

F

fb × h(FCD)f i(a × b) j b 2 atoms

F

g [FIXME: Loss of information, see below.]

Awoday 6.5 “Equational deﬁnition” gives a simple way to check cartesian closed categories.

It's enough to prove:

1. " ◦ (∼f × 1

A

) = f

2. " ◦ ∼(g × 1

A

) = g

Really, "(∼f × 1

A

)z = "(∼fz × z) = "(

F

fb × h(FCD)f i(z × b) j b 2 atoms

F

g × z) =

F

fg

0

◦

(z ×

RLD

z) ◦ f

0¡1

j f

0

; g

0

2 F((Ob H)

Ob G

); f

0

×

RLD

g

0

/

F

fb × h(FCD)f i(z × b) j b 2 atoms

F

gg

[FIXME: It cannot be equal to f due loss on information in (FCD).]

5 On decomposisiton of binary relations and reloids

Example 23. ρ

d

G =/

d

hρiG for some st G of reloids (with matching sources and destinations).

Proof. Take ∆ =

d

f"

R

(¡"; ") j " > 0g. Take fαg ×

RLD

p where p v ∆ is a nontrivial ultraﬁlter.

hρ

d

Gi(fαg ×

RLD

p) = (

d

G) ◦ (fαg ×

RLD

p)

h

d

hρiGi(fαg ×

RLD

p) = (because f αg ×

RLD

p is atomic)=

d

fhρgi(fαg ×

RLD

p) j g 2 Gg =

d

fg ◦ (fαg ×

RLD

p) j g 2 Gg.

On decomposisiton of binary relations and reloids 7

6 Rest

Lemma 24. Every non-empty set has a well ordering with greatest element.

Proof. Take an arbitrary well ordering of our set and move the ﬁrst element to the end of the

order.

Theorem 25. L 2 [f])[f]\

Q

i2dom A

atoms L

i

=/ ; for every pre-multifuncoid f of the form whose

elements are atomic posets.

Proof. If arity f = 0 our theorem is trivial, so let arity f =/ 0. Let v is a well-ordering of arity f

with greatest element m (it exists by the lemma).

Let Φ is a function which maps non-least elements of posets into atoms under these elements and

least elements into themselves. (Note that Φ is deﬁned on least elements only for completeness, Φ

is never taken on a least element in the proof below.) [TODO: Fix the “universal set” paradox here.]

Deﬁne a transﬁnite sequence a by transﬁnite induction with the formula

a

c

= Φhf i

c

(aj

X(c)nfcg

[Lj

(arity f )nX(c)

):

Let b

c

= aj

X(c)nfcg

[Lj

(arity f )nX(c)

. Then a

c

= Φhf i

c

b

c

.

Let us prove by transﬁnite induction

a

c

2 atoms L

c

:

a

c

= Φhf i

c

Lj

(arity f )nfcg

vhf i

c

Lj

(arity f )nfcg

. Thus a

c

v L

c

. [TODO: Is it true for pre-multifun-

coids?]

The only thing remained to prove is that hf i

c

b

c

=/ 0

that is hf i

c

(aj

X(c)nfcg

[Lj

(arity f )nX(c)

) =/ 0 that is y / hf i

c

b

c

??

L

c

/ hf i

c

b

c

, b

c

(0) / hf i

0

(b

c

j

(arity f )nf0g

[fc; L

c

g) , a

0

/ hf i

0

(aj

X(c)nf0;cg

[

Lj

(arity f )nX(c)

[fc; L

c

g) , a

0

/ hf i

0

(aj

X(c)nf0;c g

[Lj

((arity f )nX(c))[fcg

) ( a

0

/ hf i

0

(aj

X(c)nf0;cg

[

aj

((arity f )nX(c))[fcg

) , a

0

/ hf i

0

(aj

(X(c)nf0;c g) [((arity f)n X (c))[fcg

) , a

0

/ hf i

0

(aj

(arity f )nf0g

) ,

Φhf i

0

(Lj

(arity f )nf0g

) / hf i

0

(aj

(arity f )nf0g

).

??

a

0

= Φhf i

0

(Lj

(arity f )nf0g

)

??

??Two ways to prove:??

L

c

/ hf i

c

b

c

, b

c

(k) / hf i

k

(b

c

j

(arity f )nfkg

[fc; L

c

g) , a

k

/ hf i

k

(aj

X(c)nfk;c g

[

Lj

(arity f )nX(c)

[fc; L

c

g) , a

k

/ hf i

k

(aj

X(c)nfk;c g

[Lj

((arity f )nX(c))[fcg

) ( a

k

/ hf i

k

(aj

X(c)nfk;c g

[

aj

((arity f )nX(c))[fcg

) , a

k

/ hf i

k

(aj

(X(c)nfk;c g)[((arity f )nX(c))[fcg

) , a

k

/ hf i

k

(aj

(arity f )nfkg

)

??

L

c

/ hf i

c

b

c

, a

k

/ hf i

k

(aj

X(c)nfc;kg

[Lj

(arity f )nX(c)

[f(c; L

c

)g) , a

k

/ hf i

k

(aj

X(c)nfc;k g

[

Lj

((arity f )nX(c))[fcg

) ( a

k

/ hf i

k

(aj

X(c)nfc;k g

[aj

((arity f )nX(c))[fcg

) , a

k

/ hf i

k

(aj

(arity f )nfkg

)

??

y / hf i

c

b

c

, a

k

/ hf i

k

(aj

X(c)nfc;k g

[Lj

(arity f )nX(c)

[f(c; y)g) ( a

k

/ hf i

k

(aj

X(k)nfk g

[

Lj

(arity f )nX(c)

[f(c; y)g)

y / hf i

c

b

c

, L

k

/ hf i

k

(aj

X(c)nfcg

[Lj

(arity f )n(X(c)[fkg)

[f(c; y)g) (

??

a

m

= Φhf i

m

(λi 2 (arity f ) n fmg: a

i

) = Φhf i

m

aj

(arity f )nfmg

; a

m

/ Φhf i

m

aj

(arity f )nfmg

;

a

m

/ hf i

m

aj

(arity f )nfmg

; a 2 [f].

Theorem 26. Let A = A

i2n

is a family of boolean lattices.

A relation δ 2 P

Q

atoms

F(A

i

)

such that for every a 2

Q

atoms

F(A

i

)

8A 2 a: δ \

Y

i2n

atoms "

A

i

A

i

=/ ; ) a 2 δ (3)

can be continued till the function f for a unique staroid f of the form λi 2 n: P(A

i

). The funcoid

f is completary.

8 Section 6

For every X 2

Q

i2n

F(A

i

)

X 2 GR f , δ \

Y

i2n

atoms X

i

=/ ;: (4)

Proof. [FIXME: ??Use of unproved conjecture ?.]

By the theorem 11 (used that it is a boolean lattice) we have X 2 GR f , GR f \

Q

i2n

atoms X

i

=/ ; and thus (4). From this also follows uniqueness.

It is left to prove that there exists a completary staroid f such that f is a continuation of δ.

Consider the relation f deﬁned by the formula X 2 f , δ \

Q

i2n

atoms "

A

i

X

i

=/ ;.

I

0

t I

1

2 f , δ \

Q

i2n

atoms "

A

i

(I

0

i t I

1

i) =/ ; , δ \

Q

i2n

(atoms "

A

i

I

0

i [ atoms "

A

i

I

1

i) =/ ;.

Thus by the lemma I

0

t I

1

2 f , 9c 2 f0; 1g

n

: δ \

Q

i2n

atoms "

A

i

I

c(i)

=/ ; , 9c 2 f0; 1g

n

:

(λi 2 n: I

c(i)

i) 2 f . Trivially if 9i 2 n: X

i

= 0 then X 2/ f . So f is a completary staroid.

Let a 2

Q

atoms

F(A

i

)

.

The reverse of (3) is obvious. So we have a 2 δ , 8A 2 a: δ \

Q

i2n

atoms "

A

i

A

i

=/ ; , 8A 2 a:

A 2 f , 8A 2 a: A 2 f , a ⊆ f , a 2 f. Thus f is a continuation of δ .

hf

0

× f

1

ix =

F

fhf

0

iX ×

FCD

hf

1

iX j X 2 atoms xg

h(f

0

× f

1

)

¡1

iy = hf

0

¡1

idom y u hf

1

¡1

iim y (not only for atomic y):

h(f

0

× f

1

)

¡1

iy =

F

fh(f

0

× f

1

)

¡1

ifpg j p 2 yg =

F

fhf

0

¡1

idom fpg u hf

1

¡1

iim fpg j p 2 yg =

F

fhf

0

¡1

idom fpg j p 2 yg u

F

fhf

1

¡1

iim fpg j p 2 yg = hf

0

¡1

idom y u hf

1

¡1

iim y

It seems that these are not components of a funcoid.

Conjecture 27. Let R is a set of staroids of the form λi 2 n: F(A

i

) where every A

i

is a boolean

lattice. If x 2

Q

i2n

atoms

F(A

i

)

then x 2 GR

d

R , 8f 2 R: x 2 f .

Proof. Let denote x 2 δ , 8f 2 R: x 2 f for every x 2

Q

i2n

atoms

F(A

i

)

. For every a 2

Q

i2n

atoms

F(A

i

)

8X 2 a: δ \

Q

i2n

atoms "

A

i

X

i

=/ ; , 8X 2 a9x 2

Q

i2n

atoms "

A

i

X

i

: x 2 δ , 8X 2 a9x 2

Q

i2n

atoms "

A

i

X

i

8f 2 R: x 2 f ) 8X 2 a; f 2 R9x 2

Q

i2n

atoms "

A

i

X

i

: x 2 f ) 8X 2 a; f 2 R:

X 2 f , 8f 2 R : a ⊆ f , 8f 2 R: a 2 f , a 2 δ.

So by the previous theorem δ can be contimued till p for some staroid p of the form λi 2 n:

P(f

i

).

Let's prove p =

d

R.

x 2 p,x 2δ ) x 2 f for every f 2R and x2

Q

i2n

atoms

F(A

i

)

. Thus p ⊆ f . Consequently

8f 2 R: p ⊆ f .

Suppose that q is a staroid of the form λi 2 n: P(A

i

) such that 8f 2 R: q ⊆ f. Then for every

x 2

Q

i2n

atoms

F(A

i

)

we have x 2 q ) 8f 2 R: x 2 f , x 2 δ , x 2 p. So q ⊆p that is q ⊆ p.

We have proved p =

d

R. It's remained to prove that x 2 p , 8f 2 R: x 2 f for every

x 2

Q

i2n

atoms

F(A

i

)

. Really, x 2 p , x 2 δ , 8f 2 R: x 2 f .

Example 28. There exists a multifuncoid on power sets, which is not a completary multifuncoid.

Proof. Let arity f = N and form f = ( P f0; 1g)

N

.

Characteristic function of a set D is Λ(D) = λi 2 N :

f1g if i 2 D;

f0g if i 2/ D:

GR f = fΛ(D) j D 2 Ωg.

Obviously f is an anchored relation.

Let k 2 N .

(val f)

k

L = fX 2 (form f)

k

j L [ f(k; X)g 2 GR f g = fX 2 (P f0g)

N

j 9D 2 Ω: L [ f(k;

X)g = Λ(D)g = fX 2 (P f0; 1g)

N

j 9D 2 Ω: (L = Λ(D)j

N nfkg

^X = Λ(D)(k))g.

X 2 (val f)

k

L, 9D 2 Ω: (L = Λ(D)j

N nfkg

^X

k

= Λ(D)(k)) , ?? , 9D 2 Ω

N nfkg

; P 2 ff0g; f1gg:

(L = Λ(D) ^ X

k

= P ) , 9D 2 Ω

N nfkg

: L = Λ(D) ^ 9P 2 ff0g; f0; 1gg: X

k

= P , 9D 2 Ω

N nfkg

:

L = Λ(D) ^ X 2 ff0g; f1gg (Note it does not depend on X.)

Let X ; Y 2(P f0; 1g)

N

. Then X t Y 2 (val f )

k

L, 9D 2 Ω

N nfkg

: L = Λ(D) ^ X tY 2f f0g; f1gg

Rest 9

If X 2 ff0gg, Y 2 ff1gg then X t Y 2/ ff0g; f0; 1gg

??

That X

i

= ; ) X 2/ (val f )

k

L is obvious. So f is a pre-multifuncoid.

??

Conjecture 29. If a is a completary multifuncoid and Dst f

i

is a starrish poset for every i 2 n

then StarComp(a; f) is a completary multifuncoid.

Proof. Let 8K 2

Q

form f: (K w L

0

^ K w L

1

) K 2 StarComp(a; f)) that is 8K 2

Q

form f:

¡

K w L

0

^ K w L

1

) 9y 2

Q

i2n

atoms A

i

: (8i 2 n: y

i

[f

i

] K

i

^ y 2 a)

that is

8K 2

Q

form f9y 2

Q

i2n

atoms A

i

: (K w L

0

^ K w L

1

) (8i 2 n: y

i

[f

i

] K

i

^ y 2 a)) that is

8K 2

Q

form f9y 2

Q

i2n

atoms A

i

: ((K w L

0

^ K w L

1

) 8i 2 n: y

i

[f

i

] K

i

) ^ y 2 a) that is??

8K 2

Q

form f9y 2

Q

i2n

atoms A

i

: (9c 2 f0; 1g

n

8i 2 n: y

i

[f

i

] L

c(i)

i ^ y 2 a) that is ??

Conjecture 30.

Q

(D)

F is a pre-multifuncoid if every F

i

is a pre-multifuncoid.

Proof. Let X ; Y 2

form

Q

(D)

F

(i;j)

.

8Z 2

form

Q

(D)

F

(i;j)

:

Z ⊇ X ^ Z ⊇ Y ) Z 2

val

Q

(D)

F

(i;j)

L

, 8Z 2

form

Q

(D)

F

(i;j)

: (Z ⊇ X ^ Z ⊇ Y ) 9K 2 (form F

i

)j

(arity F

i

)nfj g

: Z 2 (val F

j

)K) , 8Z 2

form

Q

(D)

F

(i;j)

: (9K 2 (form F

i

)j

(arity F

i

)nfj g

: (Z ⊇ X ^ Z ⊇ Y ) Z 2 (val F

j

)K)) ,

?? , 8Z 2

form

Q

(D)

F

(i;j)

: (9K 2 (form F

i

)j

(arity F

i

)nfj g

: (X 2 (val F

j

)K _ Y 2 (val F

j

)K)) ,

8Z 2

form

Q

(D)

F

(i;j)

: (9K 2 (form F

i

)j

(arity F

i

)nfj g

: X 2 (val F

j

)K _ 9 K 2 (form F

i

)j

(arity F

i

)nfj g

:

Y 2 (val F

j

)K) ,

Let f is a funcoid.

Then there exists a reloid g such that ??

=============

(RLD)

in

f =

S

a ×

RLD

b j a 2 atoms 1

F(Src f )

; b 2 atoms 1

F(Dst f )

; a ×

FCD

b ⊆ f

(RLD)

in

(g ◦ f) =

S

a ×

RLD

b j a 2 atoms 1

F(Src f )

; b 2 atoms 1

F(Dst f )

; a ×

FCD

b ⊆ g ◦ f

=

S

a ×

RLD

b j a 2 atoms 1

F(Src f )

; b 2 atoms 1

F(Dst f )

; a ×

RLD

b ⊆ (RLD)

in

(g ◦ f )

(RLD)

in

(FCD)((RLD)

in

g ◦ (RLD)

in

f) = (RLD)

in

((FCD)(RLD)

in

g ◦ (FCD)(RLD)

in

f) = (RLD)

in

(g ◦

f)

Lemma 31. 8Y 2 up hf i

∗

X9F 2 up f: hF iX ⊆ Y for every funcoid f.

Proof. ??

(RLD)

in

(g ◦ f ) =

Theorem 32. g ◦ f =

T

"

FCD(Src f ;Dst g)

(G ◦ F ) j F 2 up f ; G 2 up g

Proof. It's enough?? to prove that 8H 2 up(g ◦ f)9F 2 up f ; G 2 up g: H ⊇ G ◦ F .

X [g ◦ f]

∗

Y , hf i

∗

X / hg

¡1

i

∗

Y , 8X

0

2 up hf i

∗

X ; Y

0

2 up hg

¡1

i

∗

Y : X

0

/ Y

0

, 9F 2 up f ;

G 2 up g: hF iX / hGiY , 9F 2 up f ; G 2 up g: X [G ◦ F ] Y (used the lemma).

Let H 2 up(g ◦ f). Then X [H]

∗

Y ) X [g ◦ f ]

∗

Y ) 9F 2 up f ; G 2 up g: X [G ◦ F ] Y for every

X, Y . Thus ??(it does not work because F amd G depend on X and Y ).

Lemma 33. f ◦ r =

T

ff ◦ "

FCD

R j R 2 up rg

Proof. Obviously f ◦ r ⊆

T

ff ◦ "

FCD

R j R 2 up rg.

hf ◦ ri

∗

X ⊇ ??

T

fhf ihRiX j R 2 up rg =

T

fhf ih"

FCD

Ri

∗

X j R 2 up rg =

T

fhf ◦

"

FCD

Ri

∗

X j R 2 up rg ⊇ h

T

ff ◦ "

FCD

R j R 2 up rgi

∗

X

10 Section 6

W = fhRiX j R 2 up rg is?? a generalized ﬁlter base?? (No, it isn't, up r isn't a ﬁlter.)

Let P

0

; P

1

2 W . Then P

0

= hR

0

iX, P

1

= hR

1

iX

Let F 2 up(f ◦ r). Then ?? F 2 up

T

ff ◦ "

FCD

R j R 2 up rg.

So f ◦ r ⊇

T

ff ◦ "

FCD

R j R 2 up rg

X [f ◦ "

FCD

R] Y , ["

FCD

R]X / hf

¡1

iY

??

Let W = fh"

FCD

Ria j R 2 up rg. W is a generalized ﬁlter base??. Really If X ; Y 2 W . Then

X = h"

FCD

X ia and Y = h"

FCD

Y ia for some X 2 up r, Y 2 up r.

\

ff ◦ "

FCD

R j R 2 up rg

a =

\

fhf ◦ "

FCD

Ria j R 2 up rg = (because fh"

FCD

Ria j R 2 up rg is a g.f.b.??)

hf i

\

fh"

FCD

Ria j R 2 up rg =

hf ihria

Counter-example attempt: Let r = id

Ω

FCD

. ??

Corollary 34. g ◦ f =

T

"

FCD(Src f ;Dst g)

(G ◦ F ) j F 2 up f ; G 2 up g

.

Proof. x

"

FCD(Src f ;Dst g)

(G ◦ F )

z , 9y 2 atoms Dst f: (x ["F ] y ^ y ["G] z)

x

T

"

FCD(Src f ;Dst g)

(G ◦ F ) j F 2 up f ; G 2 up g

z , 8F 2 up f ; G 2 up g:

x

"

FCD(Src f ;Dst g)

(G ◦ F )

z , 8F 2 up f ; G 2 up g9y 2 atoms Dst f :

¡

x

"

FCD(Src f ;Dst g)

F

y ^ y

"

FCD(Src f ;Dst g)

G

z

Conjecture 35. Let f be a set, F be the set of f.o. on f, P be the set of principal f.o. on f,

let n be an index set. Consider the ﬁltrator ( F

n

; P

n

). Then if f is a multifuncoid of the form P

n

,

then E

∗

f is a multifuncoid of the form F

n

.

Proof. (val E

∗

f)

i

L = ?? = fX 2 A

i

j 8K 2 up L: K [ f(i; X)g 2 f g = fX 2 A

i

j 8K 2 up L:

X 2 (val f )

i

K g = fX 2 A

i

j 8K 2 up L: K [ f(i; X)g 2 f g = ?? = fX 2 A

i

j L [ f(i; X)g 2 E

∗

f g

X 2 (val E

∗

f)

i

L , ?? , L [ f(i; X)g 2 f

A [ B 2 (val E

∗

f)

i

L = ?? = L [ f(i; A [ B)g 2 f , (futher trivial)

??

(val E

∗

f)

i

L = fX 2 A

i

j L [ f(i; X)g 2 E

∗

f g = fX 2 A

i

j up(L [ f(i; X)g) ⊆ f g = ?? =

fX 2 A

i

j up L × X ⊆ f g = fX 2 A

i

j 8K 2 up L; x 2 up X: K [ f(i; x)g 2 f g , fX 2 A

i

j 8K 2 up L;

x 2 up X: x 2 (val f)

i

K g = fX 2 A

i

j 8K 2 up L: up X ⊆ (val f )

i

K g. [TODO: The same formula as

below only with other variable names.] [TODO: Correct order of coords.]

up(L [ f(i; X)g) ⊆ f , 8K 2 up(L [ f(i; X)g): K 2 f , 8P 2 up L; X

0

2 up X:

P [ f(i; X

0

)g 2 f , 8P 2 up L; X

0

2 up X: X

0

2 (val f)

i

P , 8P 2 up L: up X ⊆ (val f)

i

P

Thus (val E

∗

f)

i

L = fX 2 A

i

j 8P 2 up L: up X ⊆ (val f)

i

P g =

X 2 A

i

j up X ⊆

T

P 2up L

(val f)

i

P

. [TODO: First try to prove for the binary case.]

A [ B 2 (val E

∗

f)

i

L ,

X 2 A

i

j up (A [ B) ⊆

T

P 2up L

(val f )

i

P

,

X 2 A

i

j up A \ up B ⊆

T

P 2up L

(val f)

i

P

(the lemma does not work, try to use a ﬁlter base)

A [ B 2 (val E

∗

f)

i

L , 8P 2 up L: up(A [ B) ⊆ (val f)

i

P , 8P 2 up L: (up A ⊆ (val f )

i

P _

up B ⊆ (val f )

i

P ) ( 8P 2 up L: (up A ⊆ (val f)

i

P _ 8P 2 up L: up B ⊆ (val f)

i

P ) (used the lemma).

[TODO: Reverse implication.]

8P 2 up L: (up A ⊆ (val f )

i

P _ up B ⊆ (val f )

i

P ) ) 8P 2 up L: (up A \ up B ⊆ (val f)

i

P ) ,

8P 2 up L: up(A [ B) ⊆ (val f )

i

P .

Thus?? A [ B 2 (val E

∗

f)

i

L , A 2 (val E

∗

f)

i

L _ B 2 (val E

∗

f)

i

L.

Consider f \

RLD

S

S =

S

hf \

RLD

iS.

1. If f is not required to be complete this formula fails even for set-valued S.

2. Let f is complete. Then it fails for speciﬁcally choosen S.

Rest 11

Theorem 36. If f is a complete reloids and S is a set of complete reloids. Then [TODO: The

same for funcoids?]

f \

RLD

[

S =

[

hf \

RLD

iS:

Theorem 37. Composition with a (co?)complete reloid is an adjoint:

Proof. F ◦ is a lower adjoint. Let ξ is its upper adjoint. Then

F ◦ x ⊆ y , x ⊆ ξ(y)

x ⊆ ξ(F ◦ x) , F ◦ ξ(y)

ξ(b) = max fx 2 RLD j F ◦ x ⊆ bg (a proof circle follows this)

x ⊆ F

¡1

◦ b ) F ◦ x ⊆ F ◦ b

F ◦

S

RLD

R =

T

RLD

fF ◦ K j K 2 up

S

RLD

Rg

S

RLD

hF ◦ iR =

S

RLD

f

T

RLD

fF ◦ G j G 2 up g g j g 2 Rg

Conjecture 38. Compl f \

RLD

Compl g = Compl(f \

RLD

g) for every reloids f and g.

Proof. Compl(f \

RLD

g) =

S

RLD

(f \

RLD

g)j

fαg

RLD

j α 2 f

Compl f \

RLD

Compl g =

S

RLD

f j

fαg

RLD

j α 2 f

\

RLD

S

RLD

gj

fαg

RLD

j α 2 f

(Compl(f \

RLD

g))j

fβ g

RLD

=(f \

RLD

g)j

fβg

RLD

(Compl f \

RLD

Compl g)j

fβg

RLD

=(f \

RLD

g)j

fβg

RLD

.

So enough to prove that Compl f \

RLD

Compl g is complete.

Let A = atoms

ComplRLD

f and B = atoms

ComplRLD

g. Then ??

Obviously Compl f \

RLD

Compl g ⊇ Compl f \

ComplRLD

Compl g

Suppose it exists a 2 atoms

RLD

(Compl f \

RLD

Compl g) such that a 2/

toms

RLD

(Compl f \

ComplRLD

Compl g). Then ??

Conjecture 39. If f and g are reloids, then

g ◦ f =

[

RLD

fG ◦ F j F 2 atoms

RLD

f ; G 2 atoms

RLD

gg:

Proof. g ◦ f = ?? = g ◦

S

RLD

atoms

RLD

f = ?? =

S

RLD

hg ◦ iatoms

RLD

f

S

RLD

fG ◦ F j F 2 atoms

RLD

f ; G 2 atoms

RLD

ggs ⊆

S

RLD

fg ◦ F j F 2 atoms

RLD

f g ⊆ g ◦ f

??

Theorem 40. dom (RLD)

in

f = dom f and im (RLD)

in

f = im f for every funcoid f.

Proof. Let an atomic f.o. a ⊆ dom f . Then exists atomic f.o. b ⊆ im f such that a ×

FCD

b ⊆ f .

Consequently

a ×

RLD

b ⊆ (RLD)

in

f ) 8K 2 up (RLD)

in

f: a ×

RLD

b ⊆ K ) 8K 2 up (RLD)

in

f: a ⊆ dom K ,

a ⊆

T

F

hdomiup (RLD)

in

f , a ⊆ dom (RLD)

in

f.

Let now an atomic f.o. a ⊆ dom (RLD)

in

f. Then 8K 2 up (RLD)

in

f: a ⊆ dom K

What is equivalent to

8K 2

\

fup(a ×

RLD

b) j a; b 2 atoms

F

f; a ×

FCD

b ⊆ f g: a ⊆ dom K

Let K 2 up f . Then K ⊇ a ×

FCD

b for every a; b 2 atoms

F

f where a ×

FCD

b ⊆ f that is exist ??

K 2 up(a ×

RLD

b) for ??

??

from what follows?? [FIXME: b is depended on K] that exist b ⊆ im f such that 8K 2

up (RLD)

in

f: a ×

RLD

b ⊆ K that is 8K 2 up (RLD)

in

f: K 2up(a ×

RLD

b) and thus (RLD)

in

f ⊇a ×

RLD

b

and consequently dom (RLD)

in

f ⊇ dom(a ×

RLD

b) = a.

Thus a ⊆ dom f , a ⊆ dom (RLD)

in

f for each atomic f.o. a from what follows dom (RLD)

in

f =

dom f.

12 Section 6

im (RLD)

in

f = im f is similar.

Theorem 41. A reloid f is monovalued iﬀ 8g 2 RLD: (g ⊆ f ) g = f j

dom g

RLD

).

Proof.

). Let f is monovalued. Then exists F 2 up f such that f = F j

dom f

RLD

. Let g 2 RLD

and g ⊆ f . Then exists G 2 up g such that g = Gj

dom g

RLD

. We have g = g \

RLD

f =

Gj

dom g

RLD

\

RLD

F j

dom f

RLD

=Gj

dom g

RLD

\

RLD

F j

dom g

RLD

=(G \

RLD

F )j

dom g

RLD

⊇f j

dom g

RLD

. But obviously g ⊆

f j

dom g

RLD

. So g = f j

dom g

RLD

.

Conjecture 42. Compl f = f n

∗ FCD

(Ω ×

FCD

f) for every funcoid f.

This conjecture may be proved by considerations similar to these in the section “Fréchet ﬁlter”

in [?].

Example 43. (RLD)

in

is not a lower adjoint (in general).

Proof. Enough to prove one of the following:

Enough to prove non-existence of max ff 2 FCD j (RLD)

in

f ⊆ gg for some reloid g.

??Enough to prove (RLD)

in

S

FCD

S =/

S

FCD

h(RLD)

in

iS for some set S of funcoids.

??

Theorem 44. A ﬁlter A is connected regarding a reloid f iﬀ it is connected regarding the funcoid

(FCD)f.

Proof. A is connected regarding f iﬀ A is connected regarding every element of F 2 up f

(considered as reloids) that is iﬀ S

∗

(F \

RLD

(A ×

RLD

A)) = A ×

RLD

A.

??

Theorem 45. (RLD)

out

(A ×

FCD

B) =/ A ×

RLD

B in general.

Proof. (RLD)

out

(A ×

FCD

B) =

T

RLD

up(A ×

FCD

B)

If the equality holds, 8F 2 up(A ×

FCD

B)9A 2 up A; B 2 up B: A × B ⊆ F .

Let L, B are f.o. and the cardinality of the set H = fY 2 F j B ⊂ Y ⊆ Lg is inﬁnite but not

greater than cardinality of a set A. (We can always assume existence of such set A, extending the

base set f above if necessary.)

For every f.o. Y 2 H choose a set Y

Y

2 up B such that Y

Y

2/ up Y

Let z is a surjection from A to H.

Consider the binary relation F =

S

ffαg × Y

zα

j α 2 Ag.

We have F ⊇ A ×

FCD

B that is F 2 up(A ×

FCD

B).

But if B 2 up B then ?? A × B * F because Fα = Y

zα

2/ up zα that is 8Y ⊃ B: Y

zα

2/ up Y

[Not needed] Consider funcoid f =

S

FCD

ffαg ×

FCD

zα j α 2 Ag.

??

Theorem 46.

T

Z(DA)

fX \

F

A j X 2 T g = A \

F

T

T.

Proof. That A \

F

T

T is a lower bound of fX \

F

A j X 2 T g is obvious.

We need to prove that it is the greatest lower bound, that is that for every lower bound

B 2 Z( D A) of fX \

F

A j X 2 T g we have A \

F

T

T ⊇ B.

Let B = B \

F

A is a lower bound of fX \

F

A j X 2 T g that is 8X 2 T : B \

F

A ⊆ X \

F

A. Left

to prove that A \

F

T

T ⊇ B \

F

A.

(X [ B) \

F

A = (X \

F

A) [

F

(B \

F

A) = X \

F

A

B [

F

(A \

F

T

T ) = (B [

F

A) \

F

(B [

T

T )

Rest 13

T

Z(DA)

fX \

F

A j X 2 T g =

T

Z(DA)

f(X [ B) \

F

A j X 2 T g ⊇ B \

F

A.

Suppose that A \

F

T

T + B \

F

A. Then exists K 2 up(A \

F

T

T ) such that K 2/ up(B \

F

A).

That is 9L 2 up A: K = L \

T

T and @L 2 up A: K = L \ B.

For every X 2 T we have up(B \

F

A) ⊇ up(X \

F

A) that is 8Y 2 up( X \

F

A): Y 2 up(B \

F

A);

8P 2 up A: P \ X 2 up(B \

F

A); 8P 2 up A9Q 2 up A: P \ X = B \ Q.

Thus 9Q 2 up A: L \ X = B \ Q

(B \

F

X) \

F

A = (B \

F

A) \

F

X = B \

F

A.

8X 2 T : (B \

F

X) \

F

A ⊆ X \

F

A

??

(B \

F

A) \

F

X = (B \

F

A) \

F

(X \

F

A) = B \

F

A

??

Theorem 47.

S

Z(DA)

fX \

F

A j X 2 T g = A \

F

S

T.

Proof. ??

Lemma 48. If staroid 0 =/ f v a

Strd

n

for an ultraﬁlter a and an index set n, then n × fag 2 GR f.

[TODO: Can be generalized for arbitrary staroidal products?]

Proof. If K

i

w a

i

for some i 2 n then K 2/ GR a

Strd

n

and thus K 2/ GR f .

Suppose that for every K such that K

i

w a

i

for every i 2 n we have K 2/ GR f . Then GR f = ;

what is impossible.

Thus there exists K such that K

i

w a

i

for every i 2 n and K 2 GR f.

By the previous lemma, λi 2 n: K

i

u a 2 GR f that is n × fag 2 GR f .

Theorem 49. id

a[n]

Strd

is an atomic ?? if a is an atomic ﬁlter.

Proof. Suppose 0 =/ f v id

a[n]

Strd

. Then f v a

Strd

n

and thus by the lemma n × fag 2 GR f.

We need to prove that f w id

a[n]

Strd

that is L 2 GR f ( L 2 id

a[n]

Strd

that is L 2 GR f (

d

i2n

Z

L

i

2 @ a.

Really,

d

i2n

Z

L

i

2 @ a ) 8i 2 n: L

i

2 @ a ) 8i 2 n: L

i

w a ) L 2 GR f .

7 Misc

Lemma 50. x ×

FCD

y ⊆ F ^ x ×

FCD

y ⊆ G ) x ×

FCD

y ⊆ F \ G for any atomic ﬁlters x and y and

binary relations F and G.

Proof. x ×

FCD

y ⊆ F , hF ix ⊇ y , 8X 2 up x: hF iX ⊇ y , 8X 2 up x: X / hF

¡1

iy.

Consider an inﬁnite lineraly ordered set.

Let a is a nontrivial atomic ﬁlter. Choose atomic reloid f in (a × a) \ (>).

f ◦ f

¡1

⊆ ((a × a) \ (>)) ◦ ((a × a) \ (<)) ⊆ a × a

y > x; z < y

??f ◦ f

¡1

⊆ 1

Dst f

A space is compact if and only if every collection of closed sets satisfying the ﬁnite intersection

property has nonempty intersection itself. (See here).

Theorem 51. If S 2 P F

2

then

\

F

fA × B j (A; B) 2 S g =

\

F

dom S ×

\

F

im S:

14 Section 7

Proof. Let P 2 dom S, Q 2 im S. Then there exist P

0

and Q

0

such that (P; Q

0

) 2 S, (P

0

;

Q) 2 S. P × Q

0

\ P

0

× Q = (P \ P

0

) × (Q \ Q

0

) (used the previous theorem).

T

F

fA × B j (A;

B) 2 S g ⊆ P × Q

0

\ P

0

× Q = (P \ P

0

) × (Q \ Q

0

) ⊆ P × Q. This implies that

\

F

fA × B j (A; B) 2 S g =

\

F

fA × B j A 2 dom S ; B 2 im S g

=

\

F

fA × B j A 2 hupidom S ; B 2 hupiim S g:

On the other side

T

F

dom S ×

T

F

im S =

T

F

fA × B j A 2 up

T

F

dom S ; B 2 up

T

F

im S g

??

If A 2 hupidom S then A 2 up

T

F

dom S. If A 2 up

T

F

dom S then

8S 2 P F: (F \

S

F

S =/ ; ) 9K 2 S: F \ K =/ ;)

8S 2 P F: (hf iA \

S

F

S =/ ; ) 9K 2 S: hf iA \ K =/ ;)

8S 2 P F: (A [f]

S

F

S ) 9K 2 S: A [f ] K)

8S 2 P F: hf i

S

F

S =

S

F

hhf iiS;

8S 2 PP f: hf i

S

S =

S

F

hhf iiS

Proposition 52. Equivalence of morphisms is an equivalence relation.

Proof.

Reﬂexity. Follows from the identity.

Symmetry. Obvious.

Transitivity. Let f ∼ g and g ∼ h. Then there exist a morphism p such that Src p v Src f ,

Src p v Src g, Dst p v Dst f , Dst p v Dst g and ι

Src f ;Dst f

p = f and ι

Src g;Dst g

p = g and ??

??

f = ι

Src f ;Dst f

p = (Dst p ,! Dst f ) ◦ p ◦ (Src p ,! Src f)

y

g = ι

Src g;Dst g

p = (Dst p ,! Dst g) ◦ p ◦ (Src p ,! Src g)

y

g = ι

Src g;Dst g

q = (Dst q ,! Dst g) ◦ q ◦ (Src q ,! Src g)

y

h = ι

Src h;Dst h

q = (Dst q ,! Dst h) ◦ q ◦ (Src q ,! Src h)

y

??

We have like:

(X ,! A) ◦ p = (Y ,! A) ◦ q and need z v p; q such that

(Dst z ,! A) ◦ z = (X ,! A) ◦ p = (Y ,! A) ◦ q:

Take z = p u q. Repeating this, we get:

g = ι

Src g;Dst g

p = (Dst z ,! Dst g) ◦ z ◦ (Src z ,! Src g)

y

g = ι

Src g;Dst g

q = (Dst z ,! Dst g) ◦ z ◦ (Src z ,! Src g)

y

??

Axiom: X ,! A is metamonovalued (requires order on the set of all objects).

Conjecture 53. (RLD)

in

f =

d

RLD

up

¡(Src f ; Dst f)

f for every funcoid f.

Proof. Let K 2 (RLD)

in

f.

d

RLD

up

¡(Src f ;Dst f)

f =

d

RLD

up

¡(Src f;Dst f )

F

atoms f v

d

RLD

up

¡(Src f ; Dst f)

F

FCD

fX

A

×

Y

B

j A 2 F(Src f); B 2 F(Dst f ); A ×

FCD

B v f g =

d

RLD

up

¡(Src f ; Dst f)

S

fX

A

× Y

B

j A 2 F(Src f);

B 2 F(Dst f); A ×

FCD

B v f g

Pattern theorem 8.19.

Conjecture 54. (FCD)f =

d

FCD

(¡(A; B) \ GR f ) for every reloid f 2 RLD(A; B).

Proof. x ×

FCD

y 2 atoms (FCD)f , x ×

RLD

y / f , ??

Misc 15

x ×

FCD

y 2 atoms

d

FCD

(¡(A; B) \ GR f) , 8K 2 ¡(A; B) \ GR f: x ×

FCD

y 2 atoms K (

8K 2 GR f : x ×

FCD

y 2 atoms K , x ×

RLD

y / f.

??

It's enough to prove up

¡(A;B)

(FCD) f = ¡(A; B) \ GR f .

Really, up

¡(A;B)

(FCD) f = up

¡(A;B)

d

FCD

GR f

K 2 up

¡(A;B)

d

FCD

GR f ) K w

d

FCD

GR f [TODO: To continue this implication we MUST

use that K 2 ¡ (otherwise take thick identity as a counterexample)]

??

Theorem 55. b /

Anch(A)

StarComp(a; f) , 8A 2 GR a; B 2 GR b; i 2 n: A

i

[f

i

] B

i

for anchored

relations a and b, provided that Src f

i

are atomic posets.

Proof.

b /

Anch(A)

StarComp(a; f ) ,

9x 2 Anch(A) n f?g: (x v b ^ x v StarComp(a; f )) ,

9x 2 Anch(A) n f?g: (x v b ^ 8B 2 GR x: B 2 GR StarComp(a; f )) ,

9x 2 Anch(A) n f?g: (x v b ^ 8B 2 GR x: (λi 2 n: hf

i

¡1

iB

i

) 2 GR a) , remove?

9x 2 Anch(A) n f?g: (8B 2 GR x: B 2 GR b ^ 8B 2 GR x: (λi 2 n: hf

i

¡1

iB

i

) 2 GR a) ,

9x 2 Anch(A) n f?g 8B 2 GR x: (B 2 GR b ^ (λi 2 n: hf

i

¡1

iB

i

) 2 GR a) ,

??

8A 2 GR a; B 2 GR b; i 2 n: A

i

/ hf

i

¡1

iB

i

,

8A 2 GR a; B 2 GR b; i 2 n: A

i

[f

i

] B

i

: ,

??

9x 2 Anch(A) n f?g: (8A 2 GR x: (A 2 GR a ^ (λi 2 n: hf

i

iA

i

) 2 GR b))

9x 2 Anch(A) n f?g: (x v a ^ 8A 2 GR x: (λi 2 n: hf

i

iA

i

) 2 GR b)

9x 2 Anch(A) n f?g: (x v a ^ 8A 2 GR x: A 2 GR StarComp(b; f

y

))

9x 2 Anch(A) n f?g: (x v a ^ x v StarComp(b; f

y

)) ,

a /

Anch(A)

StarComp(b; f

y

)

16 Section 7