 15.1. SECOND PRODUCT. OBLIQUE PRODUCT

256

Let

g

= (

RLD

(

N

,

N

)

F

)

|

ω

. If

g

is constant, then there exist a constant function

G

up

g

and

F

G

is also constant. Obviously dom

RLD

(

N

×

N

,

N

)

(

F

G

)

w

ω

.

The function

F

G

cannot be constant because otherwise

ω

v

dom

RLD

(

N

×

N

,

N

)

(

F

G

)

v↑

N

×

N

(

{

x

} ×

N

) for some

x

N

what is impossible by proved above. So

g

is not constant.

Suppose that

g

is injective. Then there exists an injection

G

up

g

.

F

u

G

up

g

is an injection which depends only on the first argument. So dom(

F

u

G

)

intersects each vertical line by atmost one element that is dom(

F

u

G

) inter-

sects every vertical line by the whole line or the line without one element. Thus

dom(

F

u

G

)

T

w

ω

and consequently dom(

F

u

G

)

/

ω

what is impossible.

Thus

g

is neither injective nor constant.

15.1. Second product. Oblique product

Definition

1357

.

A ×

RLD

F

B

= (

RLD

)

out

(

A ×

FCD

B

) for every filters

A

and

B

.

I will call it

second product

of filters

A

and

B

.

Remark

1358

.

The letter

F

is the above definition is from the word “funcoid”.

It signifies that it seems to be impossible to define

A ×

RLD

F

B

directly without

referring to funcoidal product.

Definition

1359

.

Oblique products

of filters

A

and

B

are defined as

A

n

B

=

l

RLD

f

f

Rel

(Base(

A

)

,

Base(

B

))

,

B

up

B

:

FCD

f

w A×

FCD

B

;

A

o

B

=

l

RLD

f

f

Rel

(Base(

A

)

,

Base(

B

))

,

A

up

A

:

FCD

f

w↑

A

×

FCD

B

.

Proposition

1360

.

1

.

A

n

B

=

A ×

RLD

F

B

if

A

and

B

are filters and

B

is principal.

2

.

A

o

B

=

A

×

RLD

F

B

if

A

and

B

are filters and

A

is principal.

Proof.

A

o

B

=

d

RLD

n

f

f

Rel

,f

w

A

×

FCD

B

o

=

A

×

RLD

F

B

. The other is analogous.

Proposition

1361

.

A ×

RLD

F

B v A

n

B v A ×

RLD

B

for every filters

A

,

B

.

Proof.

A

n

B v

l

RLD

f

f

Rel

(Base(

A

)

,

Base(

B

))

,

A

up

A

, B

up

B

:

FCD

f

w↑

A

×

FCD

B

v

l

A

×

RLD

B

A

up

A

, B

up

B

=

A ×

RLD

B

.

A

n

B w

l

RLD

f

f

Rel

(Base(

A

)

,

Base(

B

))

,

FCD

f

w A ×

FCD

B

=

l

RLD

f

f

up(

A ×

FCD

B

)

=

(

RLD

)

out

(

A ×

FCD

B

) =

A ×

RLD

F

B

.