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

As an Amazon Associate I earn from qualifying purchases.

Let a be a an anchored relation of the form A and dom A = n.
Let every f
i
(for all i 2 n) be a pointfree funcoid with Src f
i
= A
i
.
The star-composition of a with f is an anchored relation of the form λi 2 dom A: Dst f
i
deﬁned by
the formula [TODO: it should have a distinct notation with the other star-composition of staroids]
L 2 GR StarComp(a; f ) , (λi 2 n: hf
i
¡1
iL
i
) 2 GR a:
Theorem 1. Let Src f
i
be separable join-semilattice and Dst f
i
be a starrish join-semilattice for
every i 2 n for a set n. Let form a =
Q
i2 n
(Src f
i
)
1. If a is a prestaroid then StarComp(a; f ) is a prestaroid.
2. If a is a staroid then StarComp(a; f ) is a staroid.
3. If a is a completary staroid and then StarComp(a; f ) is a completary staroid.
Proof. We have hf
i
¡1
i(X t Y ) = hf
i
¡1
iX t hf
i
¡1
iY .
1. Let L 2
Q
i2(arity f )nfkg
(form f
i
) for some k 2 n and X ; Y 2 form f
k
. Then
X t Y 2 hStarComp(a; f)i
k
L ,
λi 2 dom f : hf
i
¡1
i
X t Y if i = k
L
i
if i =/ k
i
2 GR a ,
λi 2 dom f :
(
hf
i
¡1
iX t hf
i
¡1
iY if i = k
hf
i
¡1
iL
i
if i =/ k
!
i
!
2 GR a ,
hf
i
¡1
iX t hf
i
¡1
iY 2 hai
k
(λi 2 (dom f ) n fkg: hf
i
¡1
iL
i
) ,
hf
i
¡1
iX 2 hai
k
(λi 2 n n fkg: hf
i
¡1
iL
i
) _ hf
i
¡1
iY 2 hai
k
(λi 2 n n fkg: hf
i
¡1
iL
i
) ,
λ i 2 dom f:
(
hf
i
¡1
iX if i = k
hf
i
¡1
iL
i
if i =/ k
!
i
!
2 GR a _
λ i 2 dom f:
(
hf
i
¡1
iY if i = k
hf
i
¡1
iL
i
if i =/ k
!
i
!
2 GR a ,
λ i 2 dom f : hf
i
¡1
i
X if i = k
L
i
if i =/ k
i
2 GR a _
λ i 2 dom f :
hf
i
¡1
i
Y if i = k
L
i
if i =/ k
i
2 GR a ,
X 2 hStarComp(a; f )i
k
L _ Y 2 hStarComp(a; f )i
k
L:
Thus StarComp(a; f ) is a pre-staroid.
2. hf
i
i are monotone functions by the proposition 15.14. Thus hf
i
¡1
iX
i
v hf
i
¡1
iY
i
if X ;
Y 2
Q
i2(arity f)nfkg
(form f
i
) and X v Y . So if a is a staroid and X 2 GR StarComp(a;
f) then (λi 2 dom f : hf
i
¡1
iX
i
) 2 GR a then (λi 2 dom f: hf
i
¡1
iY
i
) 2 GR a that is
Y 2 GR StarComp(a; f ).
3.
L
0
t L
1
2 GR StarComp(a; f ) ,
(λi 2 n: hf
i
¡1
i(L
0
t L
1
)i) 2 GR a ,
(λi 2 n: hf
i
¡1
iL
0
i t hf
i
¡1
iL
1
i) 2 GR a ,
9c 2 f0; 1g: (λi 2 n: hf
i
¡1
iL
c(i)
i) 2 GR a ,
9c 2 f0; 1g: (λi 2 n: L
c(i)
i) 2 GR StarComp(a; f ):
1
Conjecture 2. 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 on powersets.
It's conequence:
Conjecture 3. b /
Anch(A)
StarComp(a; f ) , a /
Anch(A)
StarComp(b; f
y
) for anchored relations a
and b on powersets.
Conjecture 4. b /
pStrd(A)
StarComp(a; f) , a /
pStrd(A)
StarComp(b; f
y
) for pre-staroids a and b
on powersets.
Proposition 5. Anchored relations with objects being posets with above deﬁned star-morphisms
is a category with star morphisms.
Proof. We need to prove:
1. StarComp(StarComp(m; f ); g) = StarComp(m; λi 2 arity m: g
i
f
i
);
2. StarComp(m; λi 2 arity m: id
Obj
m
i
) = m.
(the rest is obvious).
Really, L 2 GR StarComp(StarComp(m; f ); g) , (λi 2 arity m: hg
i
¡1
iL
i
) 2 GR StarComp(m; f ) ,
(λi 2 n: hf
i
¡1
i(λi 2 n: hg
i
¡1
iL
i
)
i
) 2 GR m , (λi 2 arity m: hf
i
¡1
ihg
i
¡1
iL
i
) 2 GR m , (λi 2 arity m:
h(g
i
f
i
)
¡1
iL
i
) 2 GR m , L 2 GR StarComp(m; λi 2 arity m : g
i
f
i
);
L 2 GR StarComp(m; λi 2 arity m: id
Obj
m
i
) , (λi 2 n: hid
Obj
m
i
iL
i
) 2 GR m , (λi 2 arity m:
hid
Obj
m
i
iL
i
) 2 GR m , (λi 2 arity m: L
i
) 2 GR m , L 2 GR m.
Conjecture 6. StarComp(a t b; f ) = StarComp(a; f ) t StarComp(b; f ) for anchored relations a, b
of a form A, where every A
i
is a distributive lattice, and an indexed family f of pointfree funcoids
with Src f
i
= A
i
.