# Expressing a value related to an infinitary relation through ultrafilters

Let $U$ be a set. I denote $\mathfrak{A}$ the lattice of filters on $U$ ordered reverse to set theoretic inclusion of filters. I denote $\bigvee$ and $\bigwedge$ correspondingly the supremum and infimum on $\mathfrak{A}$.

Let $N$ be a (possibly infinite) index set. Let $f$ be an $N$-ary relation.

I denote $\langle f\rangle_k L = \{ x \mid L\cup\{(k,x)\}\in f \}$ for $k\in N$.

I denote $\langle \upuparrows f\rangle_k \mathcal{L} = \bigwedge_{L\in\prod \mathcal{L}} \uparrow \langle f\rangle_k L$ for every $(N\setminus\{k\})$-indexed family $\mathcal{L}$ of filters on $U$ (here $\uparrow X$ is the principal filter corresponding to $X$).

Conjecture $$\langle \upuparrows f\rangle_k \mathcal{L} = \bigvee_{a\in \prod_{i\in N\setminus\{k\}} \operatorname{atoms} \mathcal{L}_i} \langle \upuparrows f\rangle_k a,$$

where $\operatorname{atoms} \mathcal{X}$ is the set of ultrafilters over $\mathcal{X}$.

I will denote $a\not\asymp b$ iff there is a non-least element which is below both $a$ and $b$.
Take $\mathcal{P} \in F$ from the previous counter-example. We have $$\forall a \in \prod_{i \in \operatorname{dom} F} \operatorname{atoms} \mathcal{P}_i : a \notin \mathcal{P} .$$ Take $k = 1$.
Let $\mathcal{L} = \mathcal{P} |_{(\operatorname{dom} F) \setminus \{ k \}}$. Then $a \notin \mathrel{\upuparrows F}$ and thus $a_k \asymp \langle \upuparrows F \rangle_k a|_{(\operatorname{dom} F) \setminus \{ k \}}$.
Consequently $\mathcal{P}_k \asymp \langle \upuparrows F \rangle_k a|_{(\operatorname{dom} F) \setminus \{ k \}}$ and thus $\mathcal{P}_k \asymp \bigvee^{\mathfrak{F}}_{a \in \prod_{i \in (\operatorname{dom} F) \setminus \{ k \}} \operatorname{atoms} \mathcal{L_{}}_i} \langle \upuparrows F \rangle_k a$ because $\mathcal{P}_k$ is principal.
But $\mathcal{P}_k \not\asymp \langle \upuparrows F \rangle_k \mathcal{L}$. Thus follows $\langle \upuparrows F \rangle_k \mathcal{L} \neq \bigvee^{\mathfrak{F}}_{a \in \prod_{i \in (\operatorname{dom} F) \setminus \{ k \}} \operatorname{atoms} \mathcal{L}_i} \langle \upuparrows F \rangle_k a$.